de.uka.ilkd.key.rule.match.vm.instructions

Class MatchModalOperatorSVInstruction

java.lang.Object

de.uka.ilkd.key.rule.match.vm.instructions.Instruction<SV>

de.uka.ilkd.key.rule.match.vm.instructions.MatchSchemaVariableInstruction<ModalOperatorSV>

de.uka.ilkd.key.rule.match.vm.instructions.MatchModalOperatorSVInstruction

All Implemented Interfaces:

MatchInstruction

public class MatchModalOperatorSVInstruction
extends MatchSchemaVariableInstruction<ModalOperatorSV>

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.match.vm.instructions.Instruction

op

Constructor Summary

Constructors

Constructor and Description
MatchModalOperatorSVInstruction(ModalOperatorSV op)

Method Summary

Modifier and Type	Method and Description
MatchConditions	match(Term subst, MatchConditions mc, Services services) tries to match the schema variable of this instruction with the specified Term instantiationCandidate w.r.t. the given constraints by MatchConditions
MatchConditions	match(TermNavigator termPosition, MatchConditions mc, Services services)

Methods inherited from class de.uka.ilkd.key.rule.match.vm.instructions.MatchSchemaVariableInstruction

addInstantiation, match

Methods inherited from class de.uka.ilkd.key.rule.match.vm.instructions.Instruction

matchAndBindVariables, matchElementaryUpdate, matchFormulaSV, matchModalOperatorSV, matchOp, matchProgram, matchProgramSV, matchSortDependingFunction, matchTermLabelSV, matchTermSV, matchUpdateSV, matchVariableSV, unbindVariables

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

MatchModalOperatorSVInstruction

public MatchModalOperatorSVInstruction(ModalOperatorSV op)

Method Detail

match

public MatchConditions match(Term subst,
                             MatchConditions mc,
                             Services services)

Description copied from class: Instruction

tries to match the schema variable of this instruction with the specified Term instantiationCandidate w.r.t. the given constraints by MatchConditions

Specified by:

match in class Instruction<ModalOperatorSV>

Parameters:

subst - the Term to be matched

mc - the MatchConditions with additional constraints (e.g. previous matches of this schemavariable)

services - the Services

Returns:

null if no matches have been found or the new MatchConditions with the pair (sv, instantiationCandidate) added

match

public MatchConditions match(TermNavigator termPosition,
                             MatchConditions mc,
                             Services services)