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

Class BindVariablesInstruction.LogicVariableBinder

java.lang.Object

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

All Implemented Interfaces:

BindVariablesInstruction.VariableBinderSubinstruction

Enclosing class:

BindVariablesInstruction

private static class BindVariablesInstruction.LogicVariableBinder
extends java.lang.Object
implements BindVariablesInstruction.VariableBinderSubinstruction

Field Summary

Fields

Modifier and Type	Field and Description
private LogicVariable	templateVar

Constructor Summary

Constructors

Constructor and Description
LogicVariableBinder(LogicVariable templateVar)

Method Summary

Modifier and Type	Method and Description
MatchConditions	match(LogicVariable instantiationCandidate, MatchConditions matchCond, Services services) a match between two logic variables is possible if they have been assigned they are same or have been assigned to the same abstract name and the sorts are equal.

Methods inherited from class java.lang.Object

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

Field Detail

templateVar

private final LogicVariable templateVar

Constructor Detail

LogicVariableBinder

public LogicVariableBinder(LogicVariable templateVar)

Method Detail

match

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

a match between two logic variables is possible if they have been assigned they are same or have been assigned to the same abstract name and the sorts are equal.

Specified by:

match in interface BindVariablesInstruction.VariableBinderSubinstruction