de.uni_freiburg.informatik.ultimate.logic

Class FormulaUnLet

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.NonRecursive

de.uni_freiburg.informatik.ultimate.logic.TermTransformer

de.uni_freiburg.informatik.ultimate.logic.FormulaUnLet

public class FormulaUnLet
extends TermTransformer

This class removes all let terms from the formula. The result

Author:

Jochen Hoenicke

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	FormulaUnLet.UnletType

Nested classes/interfaces inherited from class de.uni_freiburg.informatik.ultimate.logic.TermTransformer

TermTransformer.BuildAnnotation, TermTransformer.BuildApplicationTerm, TermTransformer.BuildLetTerm, TermTransformer.BuildQuantifier, TermTransformer.StartLetTerm

Nested classes/interfaces inherited from class de.uni_freiburg.informatik.ultimate.logic.NonRecursive

NonRecursive.TermWalker, NonRecursive.Walker

Constructor Summary

Constructors

Constructor and Description
FormulaUnLet() Create a FormulaUnLet with the standard SMT-LIB semantics for let.
FormulaUnLet(FormulaUnLet.UnletType type) Create a FormulaUnLet.

Method Summary

Modifier and Type	Method and Description
void	addSubstitutions(java.util.Map<TermVariable,Term> termSubst) Add user defined substitutions.
void	convert(Term term) The function that does the transformation.
void	postConvertLet(LetTerm oldLet, Term[] newValues, Term newBody)
void	postConvertQuantifier(QuantifiedFormula old, Term newBody) Build the converted formula for a quantified formula.
void	preConvertLet(LetTerm oldLet, Term[] newValues)
Term	unlet(Term term) Unlet a term, i.e., remove all LetTerm and replace the term variables accordingly.

Methods inherited from class de.uni_freiburg.informatik.ultimate.logic.TermTransformer

beginScope, convertApplicationTerm, endScope, getConverted, getConverted, postConvertAnnotation, pushTerm, pushTerms, reset, setResult, transform

Methods inherited from class de.uni_freiburg.informatik.ultimate.logic.NonRecursive

enqueueWalker, run, run, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

FormulaUnLet

public FormulaUnLet()

Create a FormulaUnLet with the standard SMT-LIB semantics for let.

FormulaUnLet

public FormulaUnLet(FormulaUnLet.UnletType type)

Create a FormulaUnLet.

Parameters:

type - The type of the unletter.

Method Detail

addSubstitutions

public void addSubstitutions(java.util.Map<TermVariable,Term> termSubst)

Add user defined substitutions. This allows to map variables to terms, without adding a surrounding let term first. Note that these substitutions are then used for all formulas unletted by this class.

Parameters:

termSubst - The substitution, which maps term variables to the term with which they should be substituted.

unlet

public Term unlet(Term term)

Unlet a term, i.e., remove all LetTerm and replace the term variables accordingly.

Parameters:

term - the term to unlet

Returns:

the resulting let-free term.

convert

public void convert(Term term)

Description copied from class: TermTransformer

The function that does the transformation. Override this function if you build your own term transformer. It does not return the result but instead it puts it on the converted stack using setResult(). Instead it can also enqueue some Builders that will in the end put the result on the converted stack. You can always call super.convert() if you do not need to convert the term. It will still convert the sub-terms. If you do not want to convert the sub terms, call setResult(term) instead.

Overrides:

convert in class TermTransformer

Parameters:

term - The term to convert.

preConvertLet

public void preConvertLet(LetTerm oldLet,
                          Term[] newValues)

Overrides:

preConvertLet in class TermTransformer

postConvertLet

public void postConvertLet(LetTerm oldLet,
                           Term[] newValues,
                           Term newBody)

Overrides:

postConvertLet in class TermTransformer

postConvertQuantifier

public void postConvertQuantifier(QuantifiedFormula old,
                                  Term newBody)

Build the converted formula for a quantified formula. This also ends the scope of the quantifier. It stores the converted quantifier using TermTransformer.setResult(Term).

Overrides:

postConvertQuantifier in class TermTransformer

Parameters:

old - the quantifier to convert.

newBody - the converted sub formula.