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

Class ElementMatcher.AbstractSVMatcher<S extends AbstractSV>

java.lang.Object

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

de.uka.ilkd.key.rule.match.legacy.ElementMatcher.AbstractSVMatcher<S>

Direct Known Subclasses:

ElementMatcher.FormulaSVMatcher, ElementMatcher.ModalOperatorSVMatcher, ElementMatcher.ProgramSVMatcher, ElementMatcher.SkolemTermSVMatcher, ElementMatcher.TermLabelSVMatcher, ElementMatcher.TermSVMatcher, ElementMatcher.UpdateSVMatcher, ElementMatcher.VariableSVMatcher

Enclosing class:

ElementMatcher<T extends Operator>

private abstract static class ElementMatcher.AbstractSVMatcher<S extends AbstractSV>
extends ElementMatcher<S>

Constructor Summary

Constructors

Modifier	Constructor and Description
private	AbstractSVMatcher()

Method Summary

Modifier and Type	Method and Description
protected MatchConditions	addInstantiation(AbstractSV op, ProgramElement pe, MatchConditions matchCond, Services services) tries to add the pair (op,pe) to the match conditions.
protected MatchConditions	addInstantiation(AbstractSV op, Term term, MatchConditions matchCond, Services services) Tries to add the pair (op,term) to the match conditions.

Methods inherited from class de.uka.ilkd.key.rule.match.legacy.ElementMatcher

getElementMatcherFor, match

Methods inherited from class java.lang.Object

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

Constructor Detail

AbstractSVMatcher

private AbstractSVMatcher()

Method Detail

addInstantiation

protected MatchConditions addInstantiation(AbstractSV op,
                                           ProgramElement pe,
                                           MatchConditions matchCond,
                                           Services services)

tries to add the pair (op,pe) to the match conditions. If possible the resulting match conditions are returned, otherwise null. Such an addition can fail, e.g. if already a pair (op,x) exists where x<>pe

addInstantiation

protected final MatchConditions addInstantiation(AbstractSV op,
                                                 Term term,
                                                 MatchConditions matchCond,
                                                 Services services)

Tries to add the pair (op,term) to the match conditions. If successful the resulting conditions are returned, otherwise null. Failure is possible e.g. if this schemavariable has been already matched to a term t2 which is not unifiable with the given term.