|
| |
|
| de.uka.ilkd.key.proof.decproc.translation.TranslationVisitor
 de.uka.ilkd.key.proof.decproc.translation.TermTranslationVisitor
| TermTranslationVisitor | | public class TermTranslationVisitor extends TranslationVisitor (Code) | | This class implements a visitor used to translate Terms in KeY into Formulae
in SMT-LIB.
This implementation is intended for KeY Terms of Sort Formula. To
translate a given Term, its execPostOrder method should be called with an
instance of this class as argument. The translation result can then be fetched using the
getTranslationResult method of this class.
Prior to translating a Term with this class, its translatability should be checked by
using the PreTranslationVisitor subclass.
This class also provides a factory method that can be used to get an instance of this class.
It implements the singleton pattern and allows reusing the same visitor object for multiple
successive translations
author:
akuwertz
version:
1.5, 12/10/2006 (Introduced new superclass 'TranslationVisitor') |
| TermTranslationVisitor | | public TermTranslationVisitor(Services services, boolean useQuantifier)(Code) | | Sole constructor.
Creates a new TermTranslationVisitor and initialises it with all known translation
rules.
If useQuantifier is set to true, KeY Terms containing
quantifier operators will be translated; otherwise, they are declared untranslatable
Parameters:
services - the common Services of the KeY prover
Parameters:
useQuantifier - boolean that determines if quantifiers will be translated or not |
| clearTypePreds | | public void clearTypePreds()(Code) | | Empties the type predicate storages.
All type predicates that have been created during Term translation processes since
either the creation of this instance or the last call to this method will be deleted
|
| createTypePredUif | | protected void createTypePredUif(Sort type, String funcName, int argCount)(Code) | | |
| getCreatedTypePreds | | public Vector getCreatedTypePreds()(Code) | | Returns a Vector containing all type predicates created during all Term
translation process since either to creation of this instance or the last call to the
clearTypePreds method
the Vector of created type predicates
throws:
IllegalStateException - if this method is called during an unfinished translationprocess or before any translation was initiated
See Also: TermTranslationVisitor.clearTypePreds()
See Also: |
| getCurrentTerm | | protected Term getCurrentTerm()(Code) | | Returns the currently translated Term
the currently translated Term |
| getHierarchyPreds | | public Vector getHierarchyPreds()(Code) | | Returns a Vector containing all hierarchy predicates needed for the current
translation.
The current translation thereby means all Term translation processes since either
the creation of this instance or the last call to the clearTypePreds method
the Vector of created hierarchy predicates
throws:
IllegalStateException - if this method is called during an unfinished translationprocess or before any translation was initiated
See Also: TermTranslationVisitor.clearTypePreds()
See Also: |
| getInstance | | public static synchronized TranslationVisitor getInstance()(Code) | | A factory method returning a TermTranslationVisitor instance.
This method uses the Singleton pattern. It is intended to enable the reuse of an already created
visitor object after a complete translation. Use this method to get an instance of
TermTranslationVisitor if there is no need for concurrency
A translation process is considered complete after its result has been fetched by the
getTranslationResult method of this class
To specify whether the returned instance should translate quantifiers or not, the
setTranslateQuantifiers method must be called prior to calling this method.
To specify the Services the returned instance should use, the setServices
method must be called prior to calling this method
a TermTranslationVisitor instance
throws:
NullPointerException - if no Services have been set with setServices
throws:
IllegalStateException - if the cached TermTranslationVisitor instance is notconsidered reusable at this point of time
See Also: TranslationVisitor.getInstance
See Also: TermTranslationVisitor.setTranslateQuantifers(boolean)
See Also: TermTranslationVisitor.setServices(Services)
See Also: |
| getResult | | protected Object getResult()(Code) | | Returns the translation of a (logic) Term of Sort Formula,
which was built by successive calls of the visit method through the
execPostOrder method on this Term.
Also resets this TermTranslationVisitor for further reuse, so that this method
can only be called once per Term translation
the translation of the Term on which the execPostOrder method was called with this TermTranslationvisitor as argument |
| getServices | | protected Services getServices()(Code) | | Returns the KeY Services used for translation
the KeY Services used for translation |
| getTranslatedArguments | | protected Object[] getTranslatedArguments(int count)(Code) | | Returns an Object array containing the translation of the last count
translated Terms.
Thereby the latest translation has the highest index. All returned translations are removed
from their internal storage
Parameters:
count - the number of translations that should be returned an Object array containing the last count stored translations
throws:
IndexOutOfBoundsException - if count is higher than the count of currently stored
See Also: TermTranslationVisitor.visit(Term) |
| isReusable | | protected boolean isReusable()(Code) | | Returns true if this TermTranslationVisitor is ready for the next translation
process.
This holds under the following conditions:
- This instance was in reusable state and no translation has yet been initiated
- The reset was called in an arbitrary state
- The current translation has finish and the getTranslationResult method was
called on this instance
true if this TranslationVisitor is ready to be reused; otherwise false |
| reset | | public void reset()(Code) | | Resets this TermTranslationVisitor for reuse.
After execution of this method the state of this TermTranslationVisistor is
equals to that of a newly created TermTranslationVisitor
|
| setServices | | public static void setServices(Services services)(Code) | | Sets the Services that should be used by a TermTranslationVisitor
instance retrieved by the getInstance method
Parameters:
services - Services to be used
See Also: TermTranslationVisitor.getInstance() |
| setTranslateQuantifers | | public static void setTranslateQuantifers(boolean useQuantifiers)(Code) | | Determines whether a TermTranslationVisitor instance retrieved by the
getInstance method translated quantifiers or not
Parameters:
useQuantifiers - specifies if quantifiers should be translated or not
See Also: TermTranslationVisitor.getInstance() |
| translateLvManually | | protected TermVariable translateLvManually(LogicVariable lv)(Code) | | Translates a given LogicVariable into its SMT-LIB representation.
This method uses the same class to translate the given LogicVariable as the
visit method but can be applied to a single LogicVariable instead of
a whole Term.
Parameters:
lv - the LogicVariable to be translated manually the SMT-LIB representation of the translated LogicVariable |
|
|
|