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

Class Instruction<OP extends Operator>

java.lang.Object

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

All Implemented Interfaces:

MatchInstruction

Direct Known Subclasses:

MatchElementaryUpdateInstruction, MatchOpIdentityInstruction, MatchSchemaVariableInstruction, MatchSortDependingFunctionInstruction

public abstract class Instruction<OP extends Operator>
extends java.lang.Object
implements MatchInstruction

enum encoding the instructions of the matching vm

Field Summary

Fields

Modifier and Type	Field and Description
protected OP	op

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	Instruction(OP op)

Method Summary

Modifier and Type	Method and Description
abstract 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
static MatchInstruction	matchAndBindVariables(ImmutableArray<QuantifiableVariable> boundVars)
static MatchInstruction	matchElementaryUpdate(ElementaryUpdate elementaryUpdate)
static MatchSchemaVariableInstruction<? extends SchemaVariable>	matchFormulaSV(FormulaSV sv)
static MatchSchemaVariableInstruction<? extends SchemaVariable>	matchModalOperatorSV(ModalOperatorSV sv)
static Instruction<Operator>	matchOp(Operator op)
static MatchInstruction	matchProgram(JavaProgramElement prg)
static MatchSchemaVariableInstruction<? extends SchemaVariable>	matchProgramSV(ProgramSV sv)
static Instruction<SortDependingFunction>	matchSortDependingFunction(SortDependingFunction op)
static MatchInstruction	matchTermLabelSV(ImmutableArray<TermLabel> labels)
static MatchSchemaVariableInstruction<? extends SchemaVariable>	matchTermSV(TermSV sv)
static MatchSchemaVariableInstruction<? extends SchemaVariable>	matchUpdateSV(UpdateSV sv)
static MatchSchemaVariableInstruction<? extends SchemaVariable>	matchVariableSV(VariableSV sv)
static MatchInstruction	unbindVariables(ImmutableArray<QuantifiableVariable> boundVars)

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

Field Detail

op

protected final OP extends Operator op

Constructor Detail

Instruction

protected Instruction(OP op)

Method Detail

matchOp

public static Instruction<Operator> matchOp(Operator op)

matchSortDependingFunction

public static Instruction<SortDependingFunction> matchSortDependingFunction(SortDependingFunction op)

matchModalOperatorSV

public static MatchSchemaVariableInstruction<? extends SchemaVariable> matchModalOperatorSV(ModalOperatorSV sv)

matchFormulaSV

public static MatchSchemaVariableInstruction<? extends SchemaVariable> matchFormulaSV(FormulaSV sv)

matchTermSV

public static MatchSchemaVariableInstruction<? extends SchemaVariable> matchTermSV(TermSV sv)

matchVariableSV

public static MatchSchemaVariableInstruction<? extends SchemaVariable> matchVariableSV(VariableSV sv)

matchProgramSV

public static MatchSchemaVariableInstruction<? extends SchemaVariable> matchProgramSV(ProgramSV sv)

matchUpdateSV

public static MatchSchemaVariableInstruction<? extends SchemaVariable> matchUpdateSV(UpdateSV sv)

matchTermLabelSV

public static MatchInstruction matchTermLabelSV(ImmutableArray<TermLabel> labels)

matchProgram

public static MatchInstruction matchProgram(JavaProgramElement prg)

matchAndBindVariables

public static MatchInstruction matchAndBindVariables(ImmutableArray<QuantifiableVariable> boundVars)

unbindVariables

public static MatchInstruction unbindVariables(ImmutableArray<QuantifiableVariable> boundVars)

matchElementaryUpdate

public static MatchInstruction matchElementaryUpdate(ElementaryUpdate elementaryUpdate)

match

public abstract 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

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