public class Matcher
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
java.util.List<VariableAssignments> |
matchPattern(java.lang.String pattern,
Sequent currentSeq,
VariableAssignments assignments)
Matches a sequent against a sequent pattern (a schematic sequent) returns a list of Nodes containing matching
results from where the information about instantiated schema variables can be extracted.
|
void |
parseDecls(java.lang.String s,
Services services)
Parse the declaration string for the current pattern and add the variables to the namespace
|
public Matcher(ProofApi api)
api
- reference to proof api in order to get access to the key environmentpublic java.util.List<VariableAssignments> matchPattern(java.lang.String pattern, Sequent currentSeq, VariableAssignments assignments)
pattern
- a string representation of the pattern sequent against which the current sequent should be matchedcurrentSeq
- current concrete sequentassignments
- variables appearing in the pattern as schemavariables with their corresponding type in KeYpublic void parseDecls(java.lang.String s, Services services)
s
- declaration part of a tacletCopyright © 2003-2019 The KeY-Project.