public final class DefaultTacletSetTranslation extends java.lang.Object implements TacletSetTranslation, TranslationListener
Constructor and Description |
---|
DefaultTacletSetTranslation(Services services,
SMTSettings settings) |
Modifier and Type | Method and Description |
---|---|
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.
|
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
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.
Copyright © 2003-2019 The KeY-Project.