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

Class MatchProgramSVInstruction

java.lang.Object

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

de.uka.ilkd.key.rule.match.vm.instructions.MatchSchemaVariableInstruction<ProgramSV>

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

All Implemented Interfaces:

MatchInstruction, MatchOperatorInstruction

public class MatchProgramSVInstruction
extends MatchSchemaVariableInstruction<ProgramSV>
implements MatchOperatorInstruction

Field Summary

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

op

Constructor Summary

Constructors

Constructor and Description
MatchProgramSVInstruction(ProgramSV sv)

Method Summary

Modifier and Type	Method and Description
protected MatchConditions	addInstantiation(ProgramElement pe, MatchConditions matchCond, Services services) tries to add the pair (this,pe) to the match conditions.
MatchConditions	match(Operator instantiationCandidate, MatchConditions matchConditions, Services services)
MatchConditions	match(ProgramElement instantiationCandidate, MatchConditions matchCond, Services services) tries to match the schema variable of this instruction with the specified ProgramElement instantiationCandidate w.r.t. the given constraints by MatchConditions
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 mc, Services services)

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

addInstantiation

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

MatchProgramSVInstruction

public MatchProgramSVInstruction(ProgramSV sv)

Method Detail

addInstantiation

protected MatchConditions addInstantiation(ProgramElement pe,
                                           MatchConditions matchCond,
                                           Services services)

tries to add the pair (this,pe) to the match conditions. If possible the resulting match conditions are returned, otherwise null. Such an addition can fail, e.g. if already a pair (this,x) exists where x<>pe

match

public MatchConditions match(Operator instantiationCandidate,
                             MatchConditions matchConditions,
                             Services services)

Specified by:

match in interface MatchOperatorInstruction

match

public 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

Specified by:

match in class Instruction<ProgramSV>

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(ProgramElement instantiationCandidate,
                             MatchConditions matchCond,
                             Services services)

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

Overrides:

match in class MatchSchemaVariableInstruction<ProgramSV>

Parameters:

instantiationCandidate - the ProgramElement to be matched

matchCond - the MatchConditions with additional constraints (e.g. previous matches of this instructions SchemaVariable)

services - the Services

Returns:

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

match

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

Specified by:

match in interface MatchInstruction