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

Class MatchVariableSVInstruction

java.lang.Object

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

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

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

All Implemented Interfaces:

MatchInstruction

public class MatchVariableSVInstruction
extends MatchSchemaVariableInstruction<VariableSV>

Field Summary

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

op

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	MatchVariableSVInstruction(VariableSV 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

MatchVariableSVInstruction

protected MatchVariableSVInstruction(VariableSV op)

Method Detail

match

public 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

Specified by:

match in class Instruction<VariableSV>

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)