Package org.sosy_lab.java_smt.utils

Class UfElimination

java.lang.Object

org.sosy_lab.java_smt.utils.UfElimination

public class UfElimination
extends Object

UfElimination replaces UFs by fresh variables and adds constraints to enforce the functional consistency.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	UfElimination.Result

Method Summary

Modifier and Type	Method	Description
BooleanFormula	eliminateUfs(BooleanFormula f)	Applies the Ackermann transformation to the given Formula.
UfElimination.Result	eliminateUfs(BooleanFormula pF, UfElimination.Result pOtherResult)	Applies the Ackermann transformation to the given Formula with respect to the UfElimination.Result of another formula.

Methods inherited from class java.lang.Object

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

Method Detail

eliminateUfs

public BooleanFormula eliminateUfs(BooleanFormula f)

Applies the Ackermann transformation to the given Formula. Quantified formulas are not supported.

Parameters:

f - the Formula to remove all Ufs from

Returns:

the new Formula and the substitution done during transformation

eliminateUfs

public UfElimination.Result eliminateUfs(BooleanFormula pF,
                                         UfElimination.Result pOtherResult)

Applies the Ackermann transformation to the given Formula with respect to the UfElimination.Result of another formula. Quantified formulas are not supported.

Parameters:

pF - the Formula to remove all Ufs from

pOtherResult - result of eliminating Ufs in another BooleanFormula

Returns:

the UfElimination.Result of the Ackermannization