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

Class MatchSchemaVariableInstruction<SV extends SchemaVariable>

java.lang.Object

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

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

All Implemented Interfaces:

MatchInstruction

Direct Known Subclasses:

BindVariablesInstruction.VariableSVBinder, MatchFormulaSVInstruction, MatchModalOperatorSVInstruction, MatchProgramSVInstruction, MatchTermSVInstruction, MatchUpdateSVInstruction, MatchVariableSVInstruction

public abstract class MatchSchemaVariableInstruction<SV extends SchemaVariable>
extends Instruction<SV>

Field Summary

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

op

Constructor Summary

Constructors

Constructor and Description
MatchSchemaVariableInstruction(SV op)

Method Summary

Modifier and Type	Method and Description
protected MatchConditions	addInstantiation(Term term, MatchConditions matchCond, Services services) Tries to add the pair (this,term) to the match conditions.
MatchConditions	match(ProgramElement instantiationCandidate, MatchConditions mc, Services services) tries to match the schema variable of this instruction with the specified ProgramElement instantiationCandidate w.r.t. the given constraints by MatchConditions

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

match, 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

Methods inherited from interface de.uka.ilkd.key.rule.match.vm.instructions.MatchInstruction

match

Constructor Detail

MatchSchemaVariableInstruction

public MatchSchemaVariableInstruction(SV op)

Method Detail

addInstantiation

protected final MatchConditions addInstantiation(Term term,
                                                 MatchConditions matchCond,
                                                 Services services)

Tries to add the pair (this,term) to the match conditions. If successful the resulting conditions are returned, otherwise null. Failure is possible e.g. if this schemavariable has been already matched to a term t2 which is not unifiable with the given term.

match

public MatchConditions match(ProgramElement instantiationCandidate,
                             MatchConditions mc,
                             Services services)

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

Parameters:

instantiationCandidate - the ProgramElement to be matched

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