public final class DefaultTacletSetTranslation extends java.lang.Object implements TacletSetTranslation, TranslationListener
Modifier and Type | Field and Description |
---|---|
private ImmutableList<java.lang.String> |
instantiationFailures
If a instantiation failure occurs the returned information is stored
in a String.
|
private ImmutableList<TacletFormula> |
notTranslated
Taclets can not be translated because checking the taclet failed.
|
private Services |
services |
private SMTSettings |
settings |
private boolean |
translate
if
translate is true the method
getTranslation() will first translate the given taclets
before it returns translation . |
private ImmutableList<TacletFormula> |
translation
Translation of the taclets stored in
taclets . |
private ImmutableSet<Sort> |
usedFormulaSorts |
private java.util.HashSet<SchemaVariable> |
usedFormulaSV |
private java.util.HashSet<QuantifiableVariable> |
usedQuantifiedVariable
Shema variables of the type Variable that have been used while
translating the set of taclets.
|
private java.util.HashSet<Sort> |
usedSorts
Sorts that have been used while translating the set of taclets.
|
Constructor and Description |
---|
DefaultTacletSetTranslation(Services services,
SMTSettings settings) |
Modifier and Type | Method and Description |
---|---|
private java.lang.String |
convertTerm(Term term) |
void |
eventFormulaSV(SchemaVariable formula)
Called when the translator finds a schema variable of type formula.
|
boolean |
eventInstantiationFailure(GenericSort dest,
Sort sort,
Taclet t,
Term term)
Called when the translator can not instantiate a generic sort
with a particular sort in the given term.
|
void |
eventQuantifiedVariable(QuantifiableVariable var)
Called when the translator finds a term that has a quantified variable.
|
void |
eventSort(Sort sort)
Called when the translator finds a term that have a sort.
|
ImmutableList<TacletFormula> |
getNotTranslated()
Returns all taclet that have not been translated.
|
ImmutableList<TacletFormula> |
getTranslation(ImmutableSet<Sort> sorts)
Builds the translation of the taclets given by calling the method
setTacletSet() . |
void |
storeToFile(java.lang.String dest)
Stores the translation to a file by using the key-format for problem
files.
|
java.lang.String |
toString() |
void |
update()
Updates the translation, i.d. the given list of taclets is being
translated again.
|
private boolean translate
translate
is true
the method
getTranslation()
will first translate the given taclets
before it returns translation
.private ImmutableList<TacletFormula> translation
taclets
.private ImmutableList<TacletFormula> notTranslated
private ImmutableList<java.lang.String> instantiationFailures
private ImmutableSet<Sort> usedFormulaSorts
private java.util.HashSet<Sort> usedSorts
private java.util.HashSet<QuantifiableVariable> usedQuantifiedVariable
private Services services
private java.util.HashSet<SchemaVariable> usedFormulaSV
private final SMTSettings settings
public DefaultTacletSetTranslation(Services services, SMTSettings settings)
public ImmutableList<TacletFormula> getTranslation(ImmutableSet<Sort> sorts)
TacletSetTranslation
setTacletSet()
.getTranslation
in interface TacletSetTranslation
sorts
- this sorts are used for the instantiation of generic types.public ImmutableList<TacletFormula> getNotTranslated()
TacletSetTranslation
TacletFormula.getStatus()
.getNotTranslated
in interface TacletSetTranslation
public void update()
TacletSetTranslation
update
in interface TacletSetTranslation
public void storeToFile(java.lang.String dest)
dest
- the path of the file.public java.lang.String toString()
toString
in class java.lang.Object
private java.lang.String convertTerm(Term term)
public void eventSort(Sort sort)
TranslationListener
eventSort
in interface TranslationListener
sort
- the sort that has been found.public void eventQuantifiedVariable(QuantifiableVariable var)
TranslationListener
eventQuantifiedVariable
in interface TranslationListener
var
- the quantified variable that has been found.public void eventFormulaSV(SchemaVariable formula)
TranslationListener
eventFormulaSV
in interface TranslationListener
public boolean eventInstantiationFailure(GenericSort dest, Sort sort, Taclet t, Term term)
TranslationListener
eventInstantiationFailure
in interface TranslationListener
dest
- the generic sort to instantiatesort
- the instantiation sort.t
- the taclet thats belongs to the termterm
- the term to be instantiatedtrue
if you want to terminate the translation
of the taclet, otherwise false.