public class DefaultTacletTranslator
extends java.lang.Object
DEFAULT_TACLET_TRANSLATOR
Constructor and Description |
---|
DefaultTacletTranslator() |
Modifier and Type | Method and Description |
---|---|
protected Term |
getFindFromTaclet(FindTaclet findTaclet)
Retrieve the "find" Term from a FindTaclet.
|
protected Term |
translate(Sequent s,
TermServices services)
Translates a sequent to a term by using the following translations rules:
T ==> D is translated to: And(T)->Or(D).
And(s): conjunction between all formulae in set s. |
Term |
translate(Taclet taclet,
TermServices services)
Translates a RewriteTaclet to a formula.
|
public Term translate(Taclet taclet, TermServices services) throws IllegalTacletException
taclet
- taclet to be translated.services
- TODOIllegalTacletException
protected Term getFindFromTaclet(FindTaclet findTaclet)
FindTaclet.find()
.
Overriding classes may choose to garnish the result with additional
information.findTaclet
- a non-null taclet instanceprotected Term translate(Sequent s, TermServices services)
s
- The sequent to be translated.services
- TODOnull
if
both antecedent and succendent are empty.Copyright © 2003-2019 The KeY-Project.