public class MatchSortDependingFunctionInstruction extends Instruction<SortDependingFunction>
op
Modifier | Constructor and Description |
---|---|
protected |
MatchSortDependingFunctionInstruction(SortDependingFunction op) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
match(Term instantiationCandidate,
MatchConditions matchConditions,
Services services)
Tries to match the top level operator of the given term with this instruction's sort depending function symbol.
|
MatchConditions |
match(TermNavigator termPosition,
MatchConditions mc,
Services services) |
matchAndBindVariables, matchElementaryUpdate, matchFormulaSV, matchModalOperatorSV, matchOp, matchProgram, matchProgramSV, matchSortDependingFunction, matchTermLabelSV, matchTermSV, matchUpdateSV, matchVariableSV, unbindVariables
protected MatchSortDependingFunctionInstruction(SortDependingFunction op)
public final MatchConditions match(Term instantiationCandidate, MatchConditions matchConditions, Services services)
null
if no match is possible because the top level operator is
not a sort depending function or the resulting constraints on the sorts are unsatisfiable.match
in class Instruction<SortDependingFunction>
instantiationCandidate
- the Term
to be matchedmatchConditions
- the MatchConditions
specifying the constraints to be consideredservices
- the Services
null
if no matches have been found or the new MatchConditions
with the pair (sv, instantiationCandidate)
addedpublic MatchConditions match(TermNavigator termPosition, MatchConditions mc, Services services)
Copyright © 2003-2019 The KeY-Project.