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

Modifier and Type	Method	Description
protected TFormulaInfo	extractInfo(Formula pBits)
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	getFormulaCreator()
<AF extends Formula,VF extends Formula,AT extends FormulaType<AF>,VT extends FormulaType<VF>> BooleanFormula	makeEmptyHeap(AT pAdressType, VT pValueType)	Creates a formula representing an empty heap.
protected abstract TFormulaInfo	makeEmptyHeap(TType e1, TType e2)
BooleanFormula	makeMagicWand(BooleanFormula f1, BooleanFormula f2)	Creates a formula representing the "magic wand" (-*) operator in separation logic.
protected abstract TFormulaInfo	makeMagicWand(TFormulaInfo e1, TFormulaInfo e2)
<AF extends Formula,AT extends FormulaType<AF>> AF	makeNilElement(AT pAdressType)	Creates a formula representing the "nil" element for a given address type.
protected abstract TFormulaInfo	makeNilElement(TType type)
BooleanFormula	makePointsTo(Formula ptr, Formula to)	Creates a formula representing a "points-to" relation in the heap.
protected abstract TFormulaInfo	makePointsTo(TFormulaInfo ptr, TFormulaInfo to)
BooleanFormula	makeStar(BooleanFormula f1, BooleanFormula f2)	Creates a formula representing the "separating conjunction" (*) of two Boolean formulas.
protected abstract TFormulaInfo	makeStar(TFormulaInfo e1, TFormulaInfo e2)
protected TType	toSolverType(FormulaType<?> formulaType)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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)

Description copied from interface: SLFormulaManager

Creates a formula representing the "separating conjunction" (*) of two Boolean formulas. In separation logic, the separating conjunction asserts that the two formulas describe disjoint parts of the heap. It is similar to the logical AND operator, but with the additional constraint that the memory regions described by the two formulas do not overlap.

Specified by:

makeStar in interface SLFormulaManager

Returns:

a Boolean formula representing the separating conjunction of f1 and f2.

makeStar

protected abstract TFormulaInfo makeStar(TFormulaInfo e1,
                                         TFormulaInfo e2)

makePointsTo

public BooleanFormula makePointsTo(Formula ptr,
                                   Formula to)

Description copied from interface: SLFormulaManager

Creates a formula representing a "points-to" relation in the heap. The "points-to" relation asserts that a pointer points to a specific value in memory.

Specified by:

makePointsTo in interface SLFormulaManager

Parameters:

ptr - the pointer formula.

to - the value formula.

Returns:

a Boolean formula representing the "points-to" relation.

makePointsTo

protected abstract TFormulaInfo makePointsTo(TFormulaInfo ptr,
                                             TFormulaInfo to)

makeMagicWand

public BooleanFormula makeMagicWand(BooleanFormula f1,
                                    BooleanFormula f2)

Description copied from interface: SLFormulaManager

Creates a formula representing the "magic wand" (-*) operator in separation logic. The "magic wand" operator asserts that if the first formula holds, then the second formula can be added to the heap without conflict. It is a form of implication (=>) that takes into account the disjointness of memory regions.

Specified by:

makeMagicWand in interface SLFormulaManager

Returns:

a Boolean formula representing the "magic wand" of f1 and f2.

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)

Description copied from interface: SLFormulaManager

Creates a formula representing an empty heap. The empty heap formula asserts that no memory is allocated for the given address and value types.

Specified by:

makeEmptyHeap in interface SLFormulaManager

Type Parameters:

AF - the type of the address formula.

VF - the type of the value formula.

AT - the type of the address formula type.

VT - the type of the value formula type.

Parameters:

pAdressType - the type of the address formula.

pValueType - the type of the value formula.

Returns:

a Boolean formula representing an empty heap.

makeEmptyHeap

protected abstract TFormulaInfo makeEmptyHeap(TType e1,
                                              TType e2)

makeNilElement

public <AF extends Formula,AT extends FormulaType<AF>> AF makeNilElement(AT pAdressType)

Description copied from interface: SLFormulaManager

Creates a formula representing the "nil" element for a given address type. The "nil" element is used to represent a null pointer or an unallocated memory address.

Specified by:

makeNilElement in interface SLFormulaManager

Type Parameters:

AF - the type of the address formula.

AT - the type of the address formula type.

Parameters:

pAdressType - the type of the address formula.

Returns:

a formula representing the "nil" element for the given address type.

makeNilElement

protected abstract TFormulaInfo makeNilElement(TType type)

getFormulaCreator

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

extractInfo

protected final TFormulaInfo extractInfo(Formula pBits)

toSolverType

protected final TType toSolverType(FormulaType<?> formulaType)