UfElimination.Result (JavaSMT Solver Library)

java.lang.Object
- org.sosy_lab.java_smt.utils.UfElimination.Result

Enclosing class:: UfElimination

public static class UfElimination.Result
extends Object

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`static UfElimination.Result`	`empty(FormulaManager pFormulaManager)`
`BooleanFormula`	`getConstraints()`
`BooleanFormula`	`getFormula()`
`Map<Formula,Formula>`	`getSubstitution()`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

empty

public static UfElimination.Result empty(FormulaManager pFormulaManager)

getFormula
```
public BooleanFormula getFormula()
```
Returns:

the new Formula without UFs

getConstraints
```
public BooleanFormula getConstraints()
```
Returns:

the constraints enforcing the functional consistency.

getSubstitution
```
public Map<Formula,Formula> getSubstitution()
```
Returns:

the substitution used to replace UFs