Package org.sosy_lab.java_smt.basicimpl

Class AbstractArrayFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

java.lang.Object

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

All Implemented Interfaces:

ArrayFormulaManager

public abstract class AbstractArrayFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
implements ArrayFormulaManager

Field Summary

Fields

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

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractArrayFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pFormulaCreator)

Method Summary

Modifier and Type	Method	Description
<TI extends Formula,TE extends Formula> BooleanFormula	equivalence(ArrayFormula<TI,TE> pArray1, ArrayFormula<TI,TE> pArray2)	Make a BooleanFormula that represents the equality of two ArrayFormula.
protected abstract TFormulaInfo	equivalence(TFormulaInfo pArray1, TFormulaInfo pArray2)
<TE extends Formula> FormulaType<TE>	getElementType(ArrayFormula<?,TE> pArray)
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	getFormulaCreator()
<TI extends Formula> FormulaType<TI>	getIndexType(ArrayFormula<TI,?> pArray)
protected abstract <TI extends Formula,TE extends Formula> TFormulaInfo	internalMakeArray(String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType)
protected abstract <TI extends Formula,TE extends Formula> TFormulaInfo	internalMakeArray(FormulaType<TI> pIndexType, FormulaType<TE> pElementType, TFormulaInfo elseElem)
<TI extends Formula,TE extends Formula,FTI extends FormulaType<TI>,FTE extends FormulaType<TE>> ArrayFormula<TI,TE>	makeArray(FTI pIndexType, FTE pElementType, TE elseElem)	Create a new array constant with values initialized to elseElem.
<TI extends Formula,TE extends Formula,FTI extends FormulaType<TI>,FTE extends FormulaType<TE>> ArrayFormula<TI,TE>	makeArray(String pName, FTI pIndexType, FTE pElementType)	Declare a new array with exactly the given name.
<TI extends Formula,TE extends Formula> TE	select(ArrayFormula<TI,TE> pArray, TI pIndex)	Read a value that is stored in the array at the specified position.
protected abstract TFormulaInfo	select(TFormulaInfo pArray, TFormulaInfo pIndex)
<TI extends Formula,TE extends Formula> ArrayFormula<TI,TE>	store(ArrayFormula<TI,TE> pArray, TI pIndex, TE pValue)	Store a value into a cell of the specified array.
protected abstract TFormulaInfo	store(TFormulaInfo pArray, TFormulaInfo pIndex, TFormulaInfo pValue)
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.ArrayFormulaManager

makeArray, makeArray

Field Detail

formulaCreator

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

Constructor Detail

AbstractArrayFormulaManager

protected AbstractArrayFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pFormulaCreator)

Method Detail

select

public <TI extends Formula,TE extends Formula> TE select(ArrayFormula<TI,TE> pArray,
                                                               TI pIndex)

Description copied from interface: ArrayFormulaManager

Read a value that is stored in the array at the specified position.

Specified by:

select in interface ArrayFormulaManager

Parameters:

pArray - The array from which to read

pIndex - The position from which to read

Returns:

A formula that represents the result of the "read"

select

protected abstract TFormulaInfo select(TFormulaInfo pArray,
                                       TFormulaInfo pIndex)

store

public <TI extends Formula,TE extends Formula> ArrayFormula<TI,TE> store(ArrayFormula<TI,TE> pArray,
                                                                                     TI pIndex,
                                                                                     TE pValue)

Description copied from interface: ArrayFormulaManager

Store a value into a cell of the specified array.

Specified by:

store in interface ArrayFormulaManager

Parameters:

pArray - The array to which to write

pIndex - The position to which to write

pValue - The value that should be written

Returns:

A formula that represents the "write"

store

protected abstract TFormulaInfo store(TFormulaInfo pArray,
                                      TFormulaInfo pIndex,
                                      TFormulaInfo pValue)

makeArray

public <TI extends Formula,TE extends Formula,FTI extends FormulaType<TI>,FTE extends FormulaType<TE>> ArrayFormula<TI,TE> makeArray(String pName,
                                                                                                                                                             FTI pIndexType,
                                                                                                                                                             FTE pElementType)

Description copied from interface: ArrayFormulaManager

Declare a new array with exactly the given name.

Please make sure that the given name is valid in SMT-LIB2. Take a look at FormulaManager.isValidName(java.lang.String) for further information.

This method does not quote or unquote the given name, but uses the plain name "AS IS". Formula.toString() can return a different String than the given one.

Specified by:

makeArray in interface ArrayFormulaManager

pIndexType - The type of the array index

pElementType - The type of the array elements

makeArray

public <TI extends Formula,TE extends Formula,FTI extends FormulaType<TI>,FTE extends FormulaType<TE>> ArrayFormula<TI,TE> makeArray(FTI pIndexType,
                                                                                                                                                             FTE pElementType,
                                                                                                                                                             TE elseElem)

Description copied from interface: ArrayFormulaManager

Create a new array constant with values initialized to elseElem.

Specified by:

makeArray in interface ArrayFormulaManager

elseElem - The default value of all entries in the array.

internalMakeArray

protected abstract <TI extends Formula,TE extends Formula> TFormulaInfo internalMakeArray(String pName,
                                                                                                FormulaType<TI> pIndexType,
                                                                                                FormulaType<TE> pElementType)

internalMakeArray

protected abstract <TI extends Formula,TE extends Formula> TFormulaInfo internalMakeArray(FormulaType<TI> pIndexType,
                                                                                                FormulaType<TE> pElementType,
                                                                                                TFormulaInfo elseElem)

getIndexType

public <TI extends Formula> FormulaType<TI> getIndexType(ArrayFormula<TI,?> pArray)

Specified by:

getIndexType in interface ArrayFormulaManager

getElementType

public <TE extends Formula> FormulaType<TE> getElementType(ArrayFormula<?,TE> pArray)

Specified by:

getElementType in interface ArrayFormulaManager

equivalence

public <TI extends Formula,TE extends Formula> BooleanFormula equivalence(ArrayFormula<TI,TE> pArray1,
                                                                                ArrayFormula<TI,TE> pArray2)

Description copied from interface: ArrayFormulaManager

Make a BooleanFormula that represents the equality of two ArrayFormula.

Specified by:

equivalence in interface ArrayFormulaManager

equivalence

protected abstract TFormulaInfo equivalence(TFormulaInfo pArray1,
                                            TFormulaInfo pArray2)

getFormulaCreator

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

toSolverType

protected final TType toSolverType(FormulaType<?> formulaType)