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

Class BindVariablesInstruction.VariableSVBinder

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.BindVariablesInstruction.VariableSVBinder

All Implemented Interfaces:

BindVariablesInstruction.VariableBinderSubinstruction, MatchInstruction

Enclosing class:

BindVariablesInstruction

private static class BindVariablesInstruction.VariableSVBinder
extends MatchSchemaVariableInstruction<VariableSV>
implements BindVariablesInstruction.VariableBinderSubinstruction

Field Summary

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

op

Constructor Summary

Constructors

Constructor and Description
VariableSVBinder(VariableSV templateVar)

Method Summary

Modifier and Type	Method and Description
MatchConditions	match(LogicVariable instantiationCandidate, MatchConditions matchCond, Services services)
MatchConditions	match(Term instantiationCandidate, MatchConditions matchCond, 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 matchConditions, 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

VariableSVBinder

public VariableSVBinder(VariableSV templateVar)

Method Detail

match

public MatchConditions match(LogicVariable instantiationCandidate,
                             MatchConditions matchCond,
                             Services services)

Specified by:

match in interface BindVariablesInstruction.VariableBinderSubinstruction

match

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

Specified by:

match in interface MatchInstruction

match

public MatchConditions match(Term instantiationCandidate,
                             MatchConditions matchCond,
                             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<VariableSV>

Parameters:

instantiationCandidate - the Term to be matched

matchCond - 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