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

Class MatchElementaryUpdateInstruction

java.lang.Object

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

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

All Implemented Interfaces:

MatchInstruction

public class MatchElementaryUpdateInstruction
extends Instruction<ElementaryUpdate>

Field Summary

Fields

Modifier and Type	Field and Description
private MatchOperatorInstruction	leftHandSide

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

op

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	MatchElementaryUpdateInstruction(ElementaryUpdate op)

Method Summary

Modifier and Type	Method and Description
MatchConditions	match(Term instantiationCandidate, MatchConditions matchCond, 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

Field Detail

leftHandSide

private final MatchOperatorInstruction leftHandSide

Constructor Detail

MatchElementaryUpdateInstruction

protected MatchElementaryUpdateInstruction(ElementaryUpdate op)

Method Detail

match

public MatchConditions match(Term instantiationCandidate,
                             MatchConditions matchCond,
                             Services services)

Description copied from class: Instruction

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<ElementaryUpdate>

Parameters:

instantiationCandidate - the Term to be matched

matchCond - 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(TermNavigator termPosition,
                             MatchConditions matchConditions,
                             Services services)