public class TacletMatchProgram
extends java.lang.Object
createProgram(Term)
and provide as argument the pattern
for which you want to get a matcher.
The program is executed by invoking match(Term, MatchConditions, Services)
.Modifier and Type | Field and Description |
---|---|
static TacletMatchProgram |
EMPTY_PROGRAM
the skip program (matches anything)
|
Modifier and Type | Method and Description |
---|---|
static TacletMatchProgram |
createProgram(Term pattern)
creates a matcher for the given pattern
|
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
getMatchInstructionForSV(SchemaVariable op)
returns the instruction for the specified variable
|
MatchConditions |
match(Term p_toMatch,
MatchConditions p_matchCond,
Services services)
executes the program and tries to match the provided term; additional restrictions are provided via match conditions.
|
public static final TacletMatchProgram EMPTY_PROGRAM
public static TacletMatchProgram createProgram(Term pattern)
pattern
- the Term
specifying the patternpublic static MatchSchemaVariableInstruction<? extends SchemaVariable> getMatchInstructionForSV(SchemaVariable op)
sv
- the SchemaVariable
for which to get the instructionpublic MatchConditions match(Term p_toMatch, MatchConditions p_matchCond, Services services)
null
if no match is possible or MatchConditions
which extends the given conditions
by additional constraints (e.g., instantiations of schemavariables) such that they describe the found matchp_toMatch
- the Term
to matchp_matchCond
- the initial MatchConditions
which have to be satisfied in addition to those generated by this matchservices
- the Services
null
if no match was found or the match resultCopyright © 2003-2019 The KeY-Project.