de.uni_freiburg.informatik.ultimate.logic

Class FormulaLet

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.NonRecursive

de.uni_freiburg.informatik.ultimate.logic.FormulaLet

public class FormulaLet
extends NonRecursive

Compute the common-subexpression-elimination (cse) form of a term. A term is in cse form if all nodes with an out-degree of at least 1 and an in-degree of at least 2 are eliminated, i.e., factored out into a let.

Author:

hoenicke

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static interface	FormulaLet.LetFilter

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

NonRecursive.TermWalker, NonRecursive.Walker

Constructor Summary

Constructors

Constructor and Description
FormulaLet()
FormulaLet(FormulaLet.LetFilter filter)

Method Summary

Modifier and Type	Method and Description
Term[]	getTerms(Term[] oldArgs)
Term	let(Term input) Compute the cse form of a term.

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

enqueueWalker, reset, run, run, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

FormulaLet

public FormulaLet()

FormulaLet

public FormulaLet(FormulaLet.LetFilter filter)

Method Detail

let

public Term let(Term input)

Compute the cse form of a term. Note that all lets will be removed from the input before computing the cse form.

Parameters:

input - The input term.

Returns:

A term in cse form that represents the same DAG than the input.

getTerms

public Term[] getTerms(Term[] oldArgs)