Package org.sosy_lab.java_smt.basicimpl

Class AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

java.lang.Object

org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

All Implemented Interfaces:

QuantifiedFormulaManager

public abstract class AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
implements QuantifiedFormulaManager

Nested Class Summary

Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager

QuantifiedFormulaManager.Quantifier

Field Summary

Fields

Modifier and Type	Field	Description
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	formulaCreator

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractQuantifiedFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)

Method Summary

Modifier and Type	Method	Description
BooleanFormula	eliminateQuantifiers(BooleanFormula pF)	Eliminate the quantifiers for a given formula.
protected abstract TFormulaInfo	eliminateQuantifiers(TFormulaInfo pExtractInfo)
protected TFormulaInfo	extractInfo(Formula pBits)
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	getFormulaCreator()
BooleanFormula	mkQuantifier(QuantifiedFormulaManager.Quantifier q, List<? extends Formula> pVariables, BooleanFormula pBody)
abstract TFormulaInfo	mkQuantifier(QuantifiedFormulaManager.Quantifier q, List<TFormulaInfo> vars, TFormulaInfo body)
protected TType	toSolverType(FormulaType<?> formulaType)

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

Field Detail

formulaCreator

protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator

Constructor Detail

AbstractQuantifiedFormulaManager

protected AbstractQuantifiedFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)

Method Detail

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

eliminateQuantifiers

protected abstract TFormulaInfo eliminateQuantifiers(TFormulaInfo pExtractInfo)
                                              throws SolverException,
                                                     InterruptedException

Throws:

SolverException

InterruptedException

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

mkQuantifier

public abstract TFormulaInfo mkQuantifier(QuantifiedFormulaManager.Quantifier q,
                                          List<TFormulaInfo> vars,
                                          TFormulaInfo body)

getFormulaCreator

protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> getFormulaCreator()

extractInfo

protected final TFormulaInfo extractInfo(Formula pBits)

toSolverType

protected final TType toSolverType(FormulaType<?> formulaType)