de.uni_freiburg.informatik.ultimate.logic

Class TermTransformer

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.NonRecursive

de.uni_freiburg.informatik.ultimate.logic.TermTransformer

Direct Known Subclasses:

FormulaUnLet, IRAConstantFormatter

public class TermTransformer
extends NonRecursive

This is the base class for transforming formulas. It does nothing by itself but you can use it to create arbitrary transformations on formulas. The transform method applies the transformation in a non-recursive manner. Subclasses should override the function convert. It takes as argument the term to convert and should set its result with setResult. If it needs to build a more complex term with transformed arguments, it can enqueue the subclasses BuildLetTerm, BuildApplicationTerm, BuildAnnotatedTerm with enqueueWalker. The arguments should be added to the work queue by pushTerm/pushTerms. Of course, you can also add your own Build class that takes the converted arguments from the conversion stack using getConverted().

Author:

Jochen Hoenicke

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	TermTransformer.BuildAnnotation Collect the sub term and annotations of an annotated formula from the converted stack.
protected static class	TermTransformer.BuildApplicationTerm Collect the arguments of an application term from the converted stack and finish the conversion of appTerm.
protected static class	TermTransformer.BuildLetTerm Collect the sub term and the values of a let term from the converted stack and finish the conversion of let term.
protected static class	TermTransformer.BuildQuantifier Collect the sub term of a quantified formula and build the converted formula.
protected static class	TermTransformer.StartLetTerm Walker that is called after the variable values are transformed and before the let body starts.

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

NonRecursive.TermWalker, NonRecursive.Walker

Constructor Summary

Constructors

Constructor and Description
TermTransformer()

Method Summary

Modifier and Type	Method and Description
protected void	beginScope()
protected void	convert(Term term) The function that does the transformation.
void	convertApplicationTerm(ApplicationTerm appTerm, Term[] newArgs)
protected void	endScope()
protected Term	getConverted() Get a single converted term from the converted stack.
protected Term[]	getConverted(Term[] oldArgs) Get the converted terms from the converted stack.
void	postConvertAnnotation(AnnotatedTerm old, Annotation[] newAnnots, Term newBody)
void	postConvertLet(LetTerm oldLet, Term[] newValues, Term newBody)
void	postConvertQuantifier(QuantifiedFormula old, Term newBody)
void	preConvertLet(LetTerm oldLet, Term[] newValues)
protected void	pushTerm(Term term) Push a term on the todo stack as CONVERT work item.
protected void	pushTerms(Term[] terms) Push all terms in the array on the todo stack as CONVERT work item.
void	reset() Manually reset this walker.
protected void	setResult(Term term) Set the conversion result to term.
Term	transform(Term term) Transform a term.

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

TermTransformer

public TermTransformer()

Method Detail

pushTerms

protected final void pushTerms(Term[] terms)

Push all terms in the array on the todo stack as CONVERT work item.

Parameters:

terms - the array of terms.

pushTerm

protected final void pushTerm(Term term)

Push a term on the todo stack as CONVERT work item.

Parameters:

term - the term to convert.

setResult

protected final void setResult(Term term)

Set the conversion result to term.

Parameters:

term - the converted term.

beginScope

protected void beginScope()

endScope

protected void endScope()

convert

protected void convert(Term term)

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.

Parameters:

term - The term to convert.

convertApplicationTerm

public void convertApplicationTerm(ApplicationTerm appTerm,
                                   Term[] newArgs)

preConvertLet

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

postConvertLet

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

postConvertQuantifier

public void postConvertQuantifier(QuantifiedFormula old,
                                  Term newBody)

postConvertAnnotation

public void postConvertAnnotation(AnnotatedTerm old,
                                  Annotation[] newAnnots,
                                  Term newBody)

transform

public final Term transform(Term term)

Transform a term.

Parameters:

term - the term to transform.

Returns:

the resulting transformed term.

getConverted

protected final Term getConverted()

Get a single converted term from the converted stack. This is the dual of pushTerm() that is called after the term were removed from the todo stack and pushed to the converted stack.

Returns:

the new converted term.

getConverted

protected final Term[] getConverted(Term[] oldArgs)

Get the converted terms from the converted stack. This is the dual of pushTerms() that is called after the term were removed from the todo stack and pushed to the converted stack. It takes the old terms as argument and checks for changes.

Parameters:

oldArgs - the original arguments.

Returns:

the new converted arguments. It will return the same array oldArgs if there were no changes.

reset

public void reset()

Description copied from class: NonRecursive

Manually reset this walker. This function can be used to clear the todo stack when an exception is raised by a walker. This exception will terminate the non-recursive walk but will leave some walker in the todo stack.

Overrides:

reset in class NonRecursive