Package org.sosy_lab.java_smt.basicimpl
Class AbstractSLFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
- java.lang.Object
-
- org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
-
- All Implemented Interfaces:
SLFormulaManager
public abstract class AbstractSLFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> extends Object implements SLFormulaManager
-
-
Field Summary
Fields Modifier and Type Field Description protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>
formulaCreator
-
Constructor Summary
Constructors Modifier Constructor Description protected
AbstractSLFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)
-
Method Summary
-
-
-
Field Detail
-
formulaCreator
protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator
-
-
Constructor Detail
-
AbstractSLFormulaManager
protected AbstractSLFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)
-
-
Method Detail
-
makeStar
public BooleanFormula makeStar(BooleanFormula f1, BooleanFormula f2)
- Specified by:
makeStar
in interfaceSLFormulaManager
-
makeStar
protected abstract TFormulaInfo makeStar(TFormulaInfo e1, TFormulaInfo e2)
-
makePointsTo
public BooleanFormula makePointsTo(Formula ptr, Formula to)
- Specified by:
makePointsTo
in interfaceSLFormulaManager
-
makePointsTo
protected abstract TFormulaInfo makePointsTo(TFormulaInfo ptr, TFormulaInfo to)
-
makeMagicWand
public BooleanFormula makeMagicWand(BooleanFormula f1, BooleanFormula f2)
- Specified by:
makeMagicWand
in interfaceSLFormulaManager
-
makeMagicWand
protected abstract TFormulaInfo makeMagicWand(TFormulaInfo e1, TFormulaInfo e2)
-
makeEmptyHeap
public <AF extends Formula,VF extends Formula,AT extends FormulaType<AF>,VT extends FormulaType<VF>> BooleanFormula makeEmptyHeap(AT pAdressType, VT pValueType)
- Specified by:
makeEmptyHeap
in interfaceSLFormulaManager
-
makeEmptyHeap
protected abstract TFormulaInfo makeEmptyHeap(TType e1, TType e2)
-
makeNilElement
public <AF extends Formula,AT extends FormulaType<AF>> AF makeNilElement(AT pAdressType)
- Specified by:
makeNilElement
in interfaceSLFormulaManager
-
makeNilElement
protected abstract TFormulaInfo makeNilElement(TType type)
-
getFormulaCreator
protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> getFormulaCreator()
-
toSolverType
protected final TType toSolverType(FormulaType<?> formulaType)
-
-