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

Class MatchOpIdentityInstruction<T extends Operator>

java.lang.Object

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

de.uka.ilkd.key.rule.match.vm.instructions.MatchOpIdentityInstruction<T>

Type Parameters:

T - the type of the operator used as template

All Implemented Interfaces:

MatchInstruction, MatchOperatorInstruction

public class MatchOpIdentityInstruction<T extends Operator>
extends Instruction<T>
implements MatchOperatorInstruction

The match instruction reports a success if the top level operator of the term to be matched is the same(identical) operator like the one for which this instruction has been instantiated

Field Summary

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

op

Constructor Summary

Constructors

Constructor and Description
MatchOpIdentityInstruction(T op)

Method Summary

Modifier and Type	Method and Description
MatchConditions	match(Operator instantiationCandidate, MatchConditions matchConditions, Services services)
MatchConditions	match(Term instantiationCandidate, MatchConditions matchConditions, Services services) tries to match the schema variable of this instruction with the specified Term instantiationCandidate w.r.t. the given constraints by MatchConditions
MatchConditions	match(TermNavigator termPosition, MatchConditions matchConditions, Services services)

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

Constructor Detail

MatchOpIdentityInstruction

public MatchOpIdentityInstruction(T op)

Method Detail

match

public final MatchConditions match(Term instantiationCandidate,
                                   MatchConditions matchConditions,
                                   Services services)

tries to match the schema variable of this instruction with the specified Term instantiationCandidate w.r.t. the given constraints by MatchConditions

Specified by:

match in class Instruction<T extends Operator>

Parameters:

instantiationCandidate - the Term to be matched

matchConditions - the MatchConditions with additional constraints (e.g. previous matches of this schemavariable)

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(Operator instantiationCandidate,
                             MatchConditions matchConditions,
                             Services services)

Specified by:

match in interface MatchOperatorInstruction

match

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

Specified by:

match in interface MatchInstruction