de.uka.ilkd.key.taclettranslation.assumptions

Class DefaultTacletSetTranslation

java.lang.Object

de.uka.ilkd.key.taclettranslation.assumptions.DefaultTacletSetTranslation

All Implemented Interfaces:

TacletSetTranslation, TranslationListener

public final class DefaultTacletSetTranslation
extends java.lang.Object
implements TacletSetTranslation, TranslationListener

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
DefaultTacletSetTranslation(Services services, SMTSettings settings)

Method Summary

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

translate

private boolean translate

if translate is true the method getTranslation() will first translate the given taclets before it returns translation.

translation

private ImmutableList<TacletFormula> translation

Translation of the taclets stored in taclets.

notTranslated

private ImmutableList<TacletFormula> notTranslated

Taclets can not be translated because checking the taclet failed.

instantiationFailures

private ImmutableList<java.lang.String> instantiationFailures

If a instantiation failure occurs the returned information is stored in a String.

usedFormulaSorts

private ImmutableSet<Sort> usedFormulaSorts

usedSorts

private java.util.HashSet<Sort> usedSorts

Sorts that have been used while translating the set of taclets.

usedQuantifiedVariable

private java.util.HashSet<QuantifiableVariable> usedQuantifiedVariable

Shema variables of the type Variable that have been used while translating the set of taclets.

services

private Services services

usedFormulaSV

private java.util.HashSet<SchemaVariable> usedFormulaSV

settings

private final SMTSettings settings

Constructor Detail

DefaultTacletSetTranslation

public DefaultTacletSetTranslation(Services services,
                                   SMTSettings settings)

Method Detail

getTranslation

public ImmutableList<TacletFormula> getTranslation(ImmutableSet<Sort> sorts)

Description copied from interface: TacletSetTranslation

Builds the translation of the taclets given by calling the method setTacletSet().

Specified by:

getTranslation in interface TacletSetTranslation

Parameters:

sorts - this sorts are used for the instantiation of generic types.

Returns:

returns the resulting formulae of the taclets. Each formula of the resulting set is associated with one taclet.

getNotTranslated

public ImmutableList<TacletFormula> getNotTranslated()

Description copied from interface: TacletSetTranslation

Returns all taclet that have not been translated. The reason can be got by TacletFormula.getStatus().

Specified by:

getNotTranslated in interface TacletSetTranslation

Returns:

a list of taclets.

update

public void update()

Description copied from interface: TacletSetTranslation

Updates the translation, i.d. the given list of taclets is being translated again.

Specified by:

update in interface TacletSetTranslation

storeToFile

public void storeToFile(java.lang.String dest)

Stores the translation to a file by using the key-format for problem files.

Parameters:

dest - the path of the file.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

convertTerm

private java.lang.String convertTerm(Term term)

eventSort

public void eventSort(Sort sort)

Description copied from interface: TranslationListener

Called when the translator finds a term that have a sort. You can use this event to collect all sorts that are used.

Specified by:

eventSort in interface TranslationListener

Parameters:

sort - the sort that has been found.

eventQuantifiedVariable

public void eventQuantifiedVariable(QuantifiableVariable var)

Description copied from interface: TranslationListener

Called when the translator finds a term that has a quantified variable. You can use this event to collect all quantified variables that are used.

Specified by:

eventQuantifiedVariable in interface TranslationListener

Parameters:

var - the quantified variable that has been found.

eventFormulaSV

public void eventFormulaSV(SchemaVariable formula)

Description copied from interface: TranslationListener

Called when the translator finds a schema variable of type formula. You can use this event to collect all schema variables of type formula that are used.

Specified by:

eventFormulaSV in interface TranslationListener

eventInstantiationFailure

public boolean eventInstantiationFailure(GenericSort dest,
                                         Sort sort,
                                         Taclet t,
                                         Term term)

Description copied from interface: TranslationListener

Called when the translator can not instantiate a generic sort with a particular sort in the given term. The result type determines whether the translation is aborted: The idea is, to make the translation robust against invalid instantiation.

Specified by:

eventInstantiationFailure in interface TranslationListener

Parameters:

dest - the generic sort to instantiate

sort - the instantiation sort.

t - the taclet thats belongs to the term

term - the term to be instantiated

Returns:

return true if you want to terminate the translation of the taclet, otherwise false.