Package org.sosy_lab.java_smt.api

Interface ArrayFormulaManager

All Known Implementing Classes:

AbstractArrayFormulaManager, DebuggingArrayFormulaManager

public interface ArrayFormulaManager

This interface represents the theory of (arbitrarily nested) arrays. (as defined in the SMTLIB2 standard)

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.
<TE extends Formula> FormulaType<TE>	getElementType(ArrayFormula<?,TE> pArray)
<TI extends Formula> FormulaType<TI>	getIndexType(ArrayFormula<TI,?> pArray)
<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.
default <TI extends Formula,TE extends Formula> ArrayFormula<TI,TE>	makeArray(String pName, FormulaType.ArrayFormulaType<TI,TE> type)	Declare a new array with exactly the given name.
default <TI extends Formula,TE extends Formula> ArrayFormula<TI,TE>	makeArray(FormulaType.ArrayFormulaType<TI,TE> type, TE elseElem)	Create a new array constant with values initialized to elseElem.
<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.
<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.

Method Detail

select

<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.

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"

store

<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.

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"

makeArray

<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.

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.

Parameters:

pIndexType - The type of the array index

pElementType - The type of the array elements

makeArray

default <TI extends Formula,TE extends Formula> ArrayFormula<TI,TE> makeArray(String pName,
                                                                                          FormulaType.ArrayFormulaType<TI,TE> type)

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.

Parameters:

type - The type of the array, consisting of index type and element type

makeArray

<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.

Parameters:

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

makeArray

default <TI extends Formula,TE extends Formula> ArrayFormula<TI,TE> makeArray(FormulaType.ArrayFormulaType<TI,TE> type,
                                                                                          TE elseElem)

Create a new array constant with values initialized to elseElem.

Parameters:

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

equivalence

<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.

getIndexType

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

getElementType

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