Package org.sosy_lab.java_smt.api
Interface SLFormulaManager
-
- All Known Implementing Classes:
AbstractSLFormulaManager
,DebuggingSLFormulaManager
public interface SLFormulaManager
TheSLFormulaManager
can build formulae for separation logic.Info: A
ProverEnvironment
only supports the assertion of well-typed SL-formulae, i.e. all formulae for one heap need to use matching types (sorts) for the AdressFormulae and ValueFormulae. The user has to take care of this, otherwise theProverEnvironment
complains at runtime!
-
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method Description <AF extends Formula,VF extends Formula,AT extends FormulaType<AF>,VT extends FormulaType<VF>>
BooleanFormulamakeEmptyHeap(AT pAdressType, VT pValueType)
BooleanFormula
makeMagicWand(BooleanFormula f1, BooleanFormula f2)
<AF extends Formula,AT extends FormulaType<AF>>
AFmakeNilElement(AT pAdressType)
<AF extends Formula,VF extends Formula>
BooleanFormulamakePointsTo(AF ptr, VF to)
BooleanFormula
makeStar(BooleanFormula f1, BooleanFormula f2)
-
-
-
Method Detail
-
makeStar
BooleanFormula makeStar(BooleanFormula f1, BooleanFormula f2)
-
makePointsTo
<AF extends Formula,VF extends Formula> BooleanFormula makePointsTo(AF ptr, VF to)
-
makeMagicWand
BooleanFormula makeMagicWand(BooleanFormula f1, BooleanFormula f2)
-
makeEmptyHeap
<AF extends Formula,VF extends Formula,AT extends FormulaType<AF>,VT extends FormulaType<VF>> BooleanFormula makeEmptyHeap(AT pAdressType, VT pValueType)
-
makeNilElement
<AF extends Formula,AT extends FormulaType<AF>> AF makeNilElement(AT pAdressType)
-
-