Package org.sosy_lab.java_smt.api
Interface QuantifiedFormulaManager
-
- All Known Implementing Classes:
AbstractQuantifiedFormulaManager
,DebuggingQuantifiedFormulaManager
public interface QuantifiedFormulaManager
This interface contains methods for working with any theory with quantifiers.ATTENTION: Not every theory has a quantifier elimination property!
-
-
Nested Class Summary
Nested Classes Modifier and Type Interface Description static class
QuantifiedFormulaManager.Quantifier
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description BooleanFormula
eliminateQuantifiers(BooleanFormula pF)
Eliminate the quantifiers for a given formula.default BooleanFormula
exists(List<? extends Formula> pVariables, BooleanFormula pBody)
default BooleanFormula
exists(Formula quantifiedArg, BooleanFormula pBody)
Syntax sugar, seeexists(List, BooleanFormula)
.default BooleanFormula
forall(List<? extends Formula> pVariables, BooleanFormula pBody)
default BooleanFormula
forall(Formula quantifiedArg, BooleanFormula pBody)
Syntax sugar, seeforall(List, BooleanFormula)
.BooleanFormula
mkQuantifier(QuantifiedFormulaManager.Quantifier q, List<? extends Formula> pVariables, BooleanFormula pBody)
-
-
-
Method Detail
-
exists
default BooleanFormula exists(List<? extends Formula> pVariables, BooleanFormula pBody)
- Parameters:
pVariables
- The variables that will get bound (variables) by the quantification.pBody
- TheBooleanFormula
} within that the binding will be performed.- Returns:
- An existentially quantified formula.
- Throws:
IllegalArgumentException
- If the listpVariables
is empty.
-
forall
default BooleanFormula forall(List<? extends Formula> pVariables, BooleanFormula pBody)
- Parameters:
pVariables
- The variables that will get bound (variables) by the quantification.pBody
- TheBooleanFormula
} within that the binding will be performed.- Returns:
- A universally quantified formula.
- Throws:
IllegalArgumentException
- If the listpVariables
is empty.
-
forall
default BooleanFormula forall(Formula quantifiedArg, BooleanFormula pBody)
Syntax sugar, seeforall(List, BooleanFormula)
.
-
exists
default BooleanFormula exists(Formula quantifiedArg, BooleanFormula pBody)
Syntax sugar, seeexists(List, BooleanFormula)
.
-
mkQuantifier
BooleanFormula mkQuantifier(QuantifiedFormulaManager.Quantifier q, List<? extends Formula> pVariables, BooleanFormula pBody)
- Parameters:
q
- Quantifier typepVariables
- The variables that will get bound (variables) by the quantification.pBody
- TheBooleanFormula
} within that the binding will be performed.- Returns:
- A quantified formula
- Throws:
IllegalArgumentException
- If the listpVariables
is empty.
-
eliminateQuantifiers
BooleanFormula eliminateQuantifiers(BooleanFormula pF) throws InterruptedException, SolverException
Eliminate the quantifiers for a given formula. If this is not possible, it will return the input formula. Note that CVC4 only supports this for LIA and LRA.- Parameters:
pF
- Formula with quantifiers.- Returns:
- New formula without quantifiers.
- Throws:
InterruptedException
SolverException
-
-