public class MatchSortDependingFunctionInstruction extends Instruction<SortDependingFunction>
Modifier and Type | Field and Description |
---|---|
private GenericSort |
genericSortOfOp |
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) |
private MatchConditions |
matchSorts(Sort dependingSortToMatch,
MatchConditions matchConditions,
Services services)
matches the depending sort of this instructions sort depending function against the given sort.
|
matchAndBindVariables, matchElementaryUpdate, matchFormulaSV, matchModalOperatorSV, matchOp, matchProgram, matchProgramSV, matchSortDependingFunction, matchTermLabelSV, matchTermSV, matchUpdateSV, matchVariableSV, unbindVariables
private final GenericSort genericSortOfOp
protected MatchSortDependingFunctionInstruction(SortDependingFunction op)
private MatchConditions matchSorts(Sort dependingSortToMatch, MatchConditions matchConditions, Services services)
null
is returned.dependingSortToMatch
- the depending Sort
of the concrete function to be matchedmatchConditions
- the MatchConditions
accumulated so farnull
if failed the resulting match conditions
otherwise the resulting MatchConditions
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)