Package org.sosy_lab.java_smt.delegate.debugging

Class DebuggingQuantifiedFormulaManager

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

Constructor Summary

Constructors

Constructor	Description
DebuggingQuantifiedFormulaManager(QuantifiedFormulaManager pDelegate, org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)

Method Summary

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

Constructor Detail

DebuggingQuantifiedFormulaManager

public DebuggingQuantifiedFormulaManager(QuantifiedFormulaManager pDelegate,
                                         org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)

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