Package org.sosy_lab.java_smt.basicimpl

Class AbstractEnumerationFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

java.lang.Object

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

All Implemented Interfaces:

EnumerationFormulaManager

public abstract class AbstractEnumerationFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
implements EnumerationFormulaManager

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
protected class	AbstractEnumerationFormulaManager.EnumType	The class 'EnumType' is just a plain internal value-holding class.

Field Summary

Fields

Modifier and Type	Field	Description
protected Map<String,AbstractEnumerationFormulaManager.EnumType>	enumerations
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	formulaCreator

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method	Description
FormulaType.EnumerationFormulaType	declareEnumeration(String pName, Set<String> pElementNames)	Declare an enumeration.
protected abstract AbstractEnumerationFormulaManager.EnumType	declareEnumeration0(FormulaType.EnumerationFormulaType pType)
protected FormulaType.EnumerationFormulaType	declareEnumerationImpl(String pName, Set<String> pElementNames)
BooleanFormula	equivalence(EnumerationFormula pF1, EnumerationFormula pF2)	Make a BooleanFormula that represents the equality of two EnumerationFormula of identical enumeration type.
protected abstract TFormulaInfo	equivalenceImpl(TFormulaInfo pF1, TFormulaInfo pF2)
protected TFormulaInfo	extractInfo(Formula pBits)
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	getFormulaCreator()
EnumerationFormula	makeConstant(String pName, FormulaType.EnumerationFormulaType pType)	Creates a constant of given enumeration type with exactly the given name.
protected TFormulaInfo	makeConstantImpl(String pName, FormulaType.EnumerationFormulaType pType)
EnumerationFormula	makeVariable(String pVar, FormulaType.EnumerationFormulaType pType)	Creates a variable of given enumeration type with exactly the given name.
protected TFormulaInfo	makeVariableImpl(String pVar, FormulaType.EnumerationFormulaType pType)
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.EnumerationFormulaManager

declareEnumeration

Field Detail

enumerations

protected final Map<String,AbstractEnumerationFormulaManager.EnumType> enumerations

formulaCreator

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

Constructor Detail

AbstractEnumerationFormulaManager

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

Method Detail

declareEnumeration

public FormulaType.EnumerationFormulaType declareEnumeration(String pName,
                                                             Set<String> pElementNames)

Description copied from interface: EnumerationFormulaManager

Declare an enumeration.

Specified by:

declareEnumeration in interface EnumerationFormulaManager

Parameters:

pName - the unique name to identify the new enumeration type.

pElementNames - names for all individual elements of this enumeration type.

declareEnumerationImpl

protected FormulaType.EnumerationFormulaType declareEnumerationImpl(String pName,
                                                                    Set<String> pElementNames)

declareEnumeration0

protected abstract AbstractEnumerationFormulaManager.EnumType declareEnumeration0(FormulaType.EnumerationFormulaType pType)

makeConstant

public EnumerationFormula makeConstant(String pName,
                                       FormulaType.EnumerationFormulaType pType)

Description copied from interface: EnumerationFormulaManager

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.

Specified by:

makeConstant in interface EnumerationFormulaManager

makeConstantImpl

protected TFormulaInfo makeConstantImpl(String pName,
                                        FormulaType.EnumerationFormulaType pType)

makeVariable

public EnumerationFormula makeVariable(String pVar,
                                       FormulaType.EnumerationFormulaType pType)

Description copied from interface: EnumerationFormulaManager

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.

Specified by:

makeVariable in interface EnumerationFormulaManager

makeVariableImpl

protected TFormulaInfo makeVariableImpl(String pVar,
                                        FormulaType.EnumerationFormulaType pType)

equivalence

public BooleanFormula equivalence(EnumerationFormula pF1,
                                  EnumerationFormula pF2)

Description copied from interface: EnumerationFormulaManager

Make a BooleanFormula that represents the equality of two EnumerationFormula of identical enumeration type.

Specified by:

equivalence in interface EnumerationFormulaManager

equivalenceImpl

protected abstract TFormulaInfo equivalenceImpl(TFormulaInfo pF1,
                                                TFormulaInfo pF2)

getFormulaCreator

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

extractInfo

protected final TFormulaInfo extractInfo(Formula pBits)

toSolverType

protected final TType toSolverType(FormulaType<?> formulaType)