| Interface | Description |
|---|---|
| BindVariablesInstruction.VariableBinderSubinstruction | |
| MatchInstruction |
Interface that has to be implemented by instructions for the matching virtual machine
|
| MatchOperatorInstruction |
| Class | Description |
|---|---|
| BindVariablesInstruction |
This instructions matches the variable below a binder (e.g. a quantifier).
|
| BindVariablesInstruction.LogicVariableBinder | |
| BindVariablesInstruction.VariableSVBinder | |
| Instruction<OP extends Operator> |
enum encoding the instructions of the matching vm
|
| MatchElementaryUpdateInstruction | |
| MatchFormulaSVInstruction | |
| MatchModalOperatorSVInstruction | |
| MatchOpIdentityInstruction<T extends Operator> |
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
|
| MatchProgramInstruction | |
| MatchProgramSVInstruction | |
| MatchSchemaVariableInstruction<SV extends SchemaVariable> | |
| MatchSortDependingFunctionInstruction | |
| MatchTermLabelInstruction |
This match instruction implements the matching logic for term labels.
|
| MatchTermSVInstruction | |
| MatchUpdateSVInstruction | |
| MatchVariableSVInstruction | |
| UnbindVariablesInstruction |