DebuggingQuantifiedFormulaManager (JavaSMT Solver Library)

java.lang.Object
- org.sosy_lab.java_smt.delegate.debugging.DebuggingQuantifiedFormulaManager

All Implemented Interfaces:: QuantifiedFormulaManager

public class DebuggingQuantifiedFormulaManager
extends Object
implements QuantifiedFormulaManager

Nested Class Summary
- Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager
  QuantifiedFormulaManager.Quantifier

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`BooleanFormula`	`eliminateQuantifiers(BooleanFormula pF)`	Eliminate the quantifiers for a given formula.
`BooleanFormula`	`mkQuantifier(QuantifiedFormulaManager.Quantifier q, List<? extends Formula> pVariables, BooleanFormula pBody)`

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

Methods inherited from interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager
exists, exists, forall, forall

- Method Detail
  - mkQuantifier
```
public BooleanFormula mkQuantifier(QuantifiedFormulaManager.Quantifier q,
                                   List<? extends Formula> pVariables,
                                   BooleanFormula pBody)
```
    Specified by:
    
    mkQuantifier in interface QuantifiedFormulaManager
    
    Parameters:
    
    q - Quantifier type
    
    pVariables - The variables that will get bound (variables) by the quantification.
    
    pBody - The BooleanFormula} within that the binding will be performed.
    
    Returns:
    
    A quantified formula
  - eliminateQuantifiers
```
public BooleanFormula eliminateQuantifiers(BooleanFormula pF)
                                    throws InterruptedException,
                                           SolverException
```
    Description copied from interface: QuantifiedFormulaManager
    
    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.
    
    Specified by:
    
    eliminateQuantifiers in interface QuantifiedFormulaManager
    
    Parameters:
    
    pF - Formula with quantifiers.
    
    Returns:
    
    New formula without quantifiers.
    
    Throws:
    
    InterruptedException
    
    SolverException