| java.lang.Object
 de.uka.ilkd.key.proof.decproc.SmtAufliaTranslation
| SmtAufliaTranslation | | public class SmtAufliaTranslation (Code) | | This class is responsible for converting a Sequent into the language of the SMT logic
(QF_)AUFLIA.
To translate a given Sequent, a new instance of this class must be created with that
Sequent and common Services as arguments. The translation is done during the
creation process, so the translation result can be fetched by calling the getBenchmark
on the newly created SmtAufliaTranslation instance.
author:
akuwertz
version:
1.5, 11/15/2006 (Added support for type predicates)
See Also: de.uka.ilkd.key.proof.decproc.smtlib.Benchmark |
| Constructor Summary | |
| public | SmtAufliaTranslation(Sequent sequent, Services services, boolean useQuantifiers)
A constructor which starts the translation a given Sequent to SMT AUFLIA syntax. |
| SmtAufliaTranslation | | public SmtAufliaTranslation(Sequent sequent, Services services, boolean useQuantifiers)(Code) | | A constructor which starts the translation a given Sequent to SMT AUFLIA syntax.
The result can be fetched with the getBenchmark method
Parameters:
sequent - the Sequent which shall be translated
Parameters:
services - the common Services of the KeY prover
Parameters:
useQuantifiers - determines whether quantifiers should be translated or not
See Also: SmtAufliaTranslation.getBenchmark() |
| getBenchmark | | public Benchmark getBenchmark()(Code) | | Returns the resulting translation of the Sequent this class was created with, as a
Benchmark
the Benchmark representing the result of the translation process |
| legaliseIdentifier | | final public static String legaliseIdentifier(String identifier)(Code) | | Converts an arbitrary identifier (as String) into a legal SMT-LIB identifier
An identifier thereby is legal according to the SMT-LIB specifications, if it contains
letters, digits and '_', '.' or ''' only.
The following replacements are done by this method:
- Letters and digits remain untouched
- The characters '_', '.' and ''' also remain untouched
- The characters '<' and '>' are replaced by '.'
- All unmentioned characters are replaced by '_'
Further on, all sequences of "_" are replaced by a single "_" character in the end
Parameters:
identifier - the identifier to be converted a legal identifier according to SMT-LIB specifications, built upon the given identifier |
|
|