Package org.sosy_lab.java_smt.api
Interface EnumerationFormulaManager
-
- All Known Implementing Classes:
AbstractEnumerationFormulaManager
,DebuggingEnumerationFormulaManager
,StatisticsEnumerationFormulaManager
,SynchronizedEnumerationFormulaManager
public interface EnumerationFormulaManager
This interface represents the theory of enumeration, i.e., datatype of limited domain sort (as defined in the SMTLIB2 standard).
-
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description default FormulaType.EnumerationFormulaType
declareEnumeration(String pName, String... pElementNames)
FormulaType.EnumerationFormulaType
declareEnumeration(String pName, Set<String> ppElementNames)
Declare an enumeration.BooleanFormula
equivalence(EnumerationFormula pEnumeration1, EnumerationFormula pEnumeration2)
Make aBooleanFormula
that represents the equality of twoEnumerationFormula
of identical enumeration type.EnumerationFormula
makeConstant(String pName, FormulaType.EnumerationFormulaType pType)
Creates a constant of given enumeration type with exactly the given name.EnumerationFormula
makeVariable(String pVar, FormulaType.EnumerationFormulaType pType)
Creates a variable of given enumeration type with exactly the given name.
-
-
-
Method Detail
-
declareEnumeration
FormulaType.EnumerationFormulaType declareEnumeration(String pName, Set<String> ppElementNames)
Declare an enumeration.- Parameters:
pName
- the unique name to identify the new enumeration type.ppElementNames
- names for all individual elements of this enumeration type.
-
declareEnumeration
default FormulaType.EnumerationFormulaType declareEnumeration(String pName, String... pElementNames)
- See Also:
declareEnumeration(String, Set)
-
makeConstant
EnumerationFormula makeConstant(String pName, FormulaType.EnumerationFormulaType pType)
Creates a constant of given enumeration type with exactly the given name. This constant (symbol) needs to be an element from the given enumeration type.
-
makeVariable
EnumerationFormula makeVariable(String pVar, FormulaType.EnumerationFormulaType pType)
Creates a variable of given enumeration type with exactly the given name.This variable (symbol) represents a "String" for which the SMT solver needs to find a model.
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.
-
equivalence
BooleanFormula equivalence(EnumerationFormula pEnumeration1, EnumerationFormula pEnumeration2)
Make aBooleanFormula
that represents the equality of twoEnumerationFormula
of identical enumeration type.
-
-