Package org.sosy_lab.java_smt.utils
Class UfElimination.Result
- 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()
-
-
-
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.
-
-