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

Class MatchSortDependingFunctionInstruction

java.lang.Object

de.uka.ilkd.key.rule.match.vm.instructions.Instruction<SortDependingFunction>

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

All Implemented Interfaces:

MatchInstruction

public class MatchSortDependingFunctionInstruction
extends Instruction<SortDependingFunction>

Field Summary

Fields

Modifier and Type	Field and Description
private GenericSort	genericSortOfOp

Fields inherited from class de.uka.ilkd.key.rule.match.vm.instructions.Instruction

op

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	MatchSortDependingFunctionInstruction(SortDependingFunction op)

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.rule.match.vm.instructions.Instruction

matchAndBindVariables, matchElementaryUpdate, matchFormulaSV, matchModalOperatorSV, matchOp, matchProgram, matchProgramSV, matchSortDependingFunction, matchTermLabelSV, matchTermSV, matchUpdateSV, matchVariableSV, unbindVariables

Methods inherited from class java.lang.Object

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

Field Detail

genericSortOfOp

private final GenericSort genericSortOfOp

Constructor Detail

MatchSortDependingFunctionInstruction

protected MatchSortDependingFunctionInstruction(SortDependingFunction op)

Method Detail

matchSorts

private MatchConditions matchSorts(Sort dependingSortToMatch,
                                   MatchConditions matchConditions,
                                   Services services)

matches the depending sort of this instructions sort depending function against the given sort. If a match is possible the resulting match conditions are returned otherwise null is returned.

Parameters:

dependingSortToMatch - the depending Sort of the concrete function to be matched

matchConditions - the MatchConditions accumulated so far

Returns:

null if failed the resulting match conditions otherwise the resulting MatchConditions

match

public final 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. It returns the resulting match conditions or 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.

Specified by:

match in class Instruction<SortDependingFunction>

Parameters:

instantiationCandidate - the Term to be matched

matchConditions - the MatchConditions specifying the constraints to be considered

services - the Services

Returns:

null if no matches have been found or the new MatchConditions with the pair (sv, instantiationCandidate) added

match

public MatchConditions match(TermNavigator termPosition,
                             MatchConditions mc,
                             Services services)