TacletMatcher (KeY API Documentation)

All Known Implementing Classes:

LegacyTacletMatcher, VMTacletMatcher
```
public interface TacletMatcher
```

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`MatchConditions`	`checkConditions(MatchConditions p_matchconditions, Services services)` checks the provided matches against the variable conditions of this taclet It returns the resulting match conditions or `null` if the found matches do not satisfy the variable conditions.
`MatchConditions`	`checkVariableConditions(SchemaVariable var, SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services)` checks if the conditions for a correct instantiation are satisfied
`MatchConditions`	`matchFind(Term term, MatchConditions matchCond, Services services)` matches the given term against the taclet's find term if the taclet has no find term or the match is unsuccessful `null is returned`
`IfMatchResult`	`matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch, Term p_template, MatchConditions p_matchCond, Services p_services)` Match the given template (which is probably a formula of the if sequence) against a list of constraint formulas (probably the formulas of the antecedent or the succedent), starting with the given instantiations and constraint p_matchCond.
`MatchConditions`	`matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch, MatchConditions p_matchCond, Services p_services)` Match the whole if sequent using the given list of instantiations of all if sequent formulas, starting with the instantiations given by p_matchCond.
`MatchConditions`	`matchSV(SchemaVariable sv, ProgramElement term, MatchConditions matchCond, Services services)` checks whether the given `SchemaVariable` `sv` matches the `ProgramElement` `pe` w.r.t.
`MatchConditions`	`matchSV(SchemaVariable sv, Term term, MatchConditions matchCond, Services services)` checks whether the given `SchemaVariable` `sv` matches the `Term` `term` w.r.t.

- Method Detail
  - matchIf
```
IfMatchResult matchIf(ImmutableList<IfFormulaInstantiation> p_toMatch,
                      Term p_template,
                      MatchConditions p_matchCond,
                      Services p_services)
```
    Match the given template (which is probably a formula of the if sequence) against a list of constraint formulas (probably the formulas of the antecedent or the succedent), starting with the given instantiations and constraint p_matchCond.
    
    Parameters:
    
    p_toMatch - list of constraint formulas to match p_template to
    
    p_template - template formula as in "match"
    
    p_matchCond - already performed instantiations
    
    p_services - the Services object encapsulating information about the java datastructures like (static)types etc.
    
    Returns:
    
    Two lists (in an IfMatchResult object), containing the the elements of p_toMatch that could successfully be matched against p_template, and the corresponding MatchConditions.
  - matchIf
```
MatchConditions matchIf(java.lang.Iterable<IfFormulaInstantiation> p_toMatch,
                        MatchConditions p_matchCond,
                        Services p_services)
```
    Match the whole if sequent using the given list of instantiations of all if sequent formulas, starting with the instantiations given by p_matchCond. PRECONDITION: p_toMatch.size () == ifSequent ().size ()
    
    Returns:
    
    resulting MatchConditions or null if the given list p_toMatch does not match
  - checkConditions
```
MatchConditions checkConditions(MatchConditions p_matchconditions,
                                Services services)
```
    checks the provided matches against the variable conditions of this taclet It returns the resulting match conditions or null if the found matches do not satisfy the variable conditions. If the given matchconditions are null then null is returned
    
    Parameters:
    
    p_matchconditions - the matches to be checked
    
    services - the Services
    
    Returns:
    
    the resulting match conditions or null if given matches do not satisfy the taclet's variable conditions
  - checkVariableConditions
```
MatchConditions checkVariableConditions(SchemaVariable var,
                                        SVSubstitute instantiationCandidate,
                                        MatchConditions matchCond,
                                        Services services)
```
    checks if the conditions for a correct instantiation are satisfied
    
    Parameters:
    
    var - the SchemaVariable to be instantiated
    
    instantiationCandidate - the SVSubstitute, which is a candidate for a possible instantiation of var
    
    matchCond - the MatchConditions which have to be respected for the new match
    
    services - the Services object encapsulating information about the Java type model
    
    Returns:
    
    the match conditions resulting from matching var with instantiationCandidate or null if a match was not possible
  - matchFind
```
MatchConditions matchFind(Term term,
                          MatchConditions matchCond,
                          Services services)
```
    matches the given term against the taclet's find term if the taclet has no find term or the match is unsuccessful null is returned
    Parameters: term - the Term to be matched against the find expression of the taclet matchCond - the MatchConditions with side conditions to be satisfied, eg. partial instantiations of schema variables; before calling this method the constraint contained in the match conditions must be ensured to be satisfiable, i.e. matchCond.getConstraint ().isSatisfiable () must return true services - the Services Returns: the found schema variable mapping or null if the matching failed
  matchSV MatchConditions matchSV(SchemaVariable sv, Term term, MatchConditions matchCond, Services services) checks whether the given SchemaVariable sv matches the Term term w.r.t. the constraints (e.g., previous matches of sv) specified in the MatchConditions matchCond Parameters: sv - the SchemaVariable term - the Term as a candidate for instantition of sv matchCond - the MatchConditions with additional constraints that need to be considered services - the Services Returns: null if the match is not possible or the new MatchConditions with the instantiation sv <- term added matchSV MatchConditions matchSV(SchemaVariable sv, ProgramElement term, MatchConditions matchCond, Services services) checks whether the given SchemaVariable sv matches the ProgramElement pe w.r.t. the constraints (e.g., previous matches of sv) specified in the MatchConditions matchCond Parameters: sv - the SchemaVariable pe - the ProgramElement as a candidate for instantition of sv matchCond - the MatchConditions with additional constraints that need to be considered services - the Services Returns: null if the match is not possible or the new MatchConditions with the instantiation sv <- term added

Interface TacletMatcher

Method Summary

Method Detail

matchIf

matchIf

checkConditions

checkVariableConditions

matchFind

matchSV

matchSV