de.uka.ilkd.key.rule.match.legacy

Class ElementMatcher.LogicVariableMatcher

java.lang.Object

de.uka.ilkd.key.rule.match.legacy.ElementMatcher<LogicVariable>

de.uka.ilkd.key.rule.match.legacy.ElementMatcher.LogicVariableMatcher

Enclosing class:

ElementMatcher<T extends Operator>

private static class ElementMatcher.LogicVariableMatcher
extends ElementMatcher<LogicVariable>

Constructor Summary

Constructors

Modifier	Constructor and Description
private	LogicVariableMatcher()

Method Summary

Modifier and Type	Method and Description
MatchConditions	match(LogicVariable op, SVSubstitute subst, MatchConditions mc, 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 de.uka.ilkd.key.rule.match.legacy.ElementMatcher

getElementMatcherFor

Methods inherited from class java.lang.Object

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

Constructor Detail

LogicVariableMatcher

private LogicVariableMatcher()

Method Detail

match

public MatchConditions match(LogicVariable op,
                             SVSubstitute subst,
                             MatchConditions mc,
                             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 class ElementMatcher<LogicVariable>