Package org.sosy_lab.java_smt.basicimpl

Class AbstractUFManager<TFormulaInfo,TFunctionDecl,TType,TEnv>

java.lang.Object

org.sosy_lab.java_smt.basicimpl.AbstractUFManager<TFormulaInfo,TFunctionDecl,TType,TEnv>

Type Parameters:

TFormulaInfo - The solver specific type.

TFunctionDecl - The solver specific type of declarations of any function application

TType - The solver specific type of formula-types.

All Implemented Interfaces:

UFManager

public abstract class AbstractUFManager<TFormulaInfo,TFunctionDecl,TType,TEnv>
extends Object
implements UFManager

This class simplifies the implementation of the FunctionFormulaManager by converting the types to the solver specific type.

Field Summary

Fields

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

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractUFManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFunctionDecl> pCreator)

Method Summary

Modifier and Type	Method	Description
<T extends Formula> T	callUF(FunctionDeclaration<T> pFunc, List<? extends Formula> pArgs)	Create an uninterpreted function call.
<T extends Formula> T	callUF(FunctionDeclaration<T> funcType, Formula... args)
<T extends Formula> T	declareAndCallUF(String name, FormulaType<T> pReturnType, List<Formula> pArgs)	Declares and calls an uninterpreted function with exactly the given name.
<T extends Formula> T	declareAndCallUF(String name, FormulaType<T> pReturnType, Formula... pArgs)
<T extends Formula> FunctionDeclaration<T>	declareUF(String pName, FormulaType<T> pReturnType, List<FormulaType<?>> pArgTypes)	Declare an uninterpreted function.
<T extends Formula> FunctionDeclaration<T>	declareUF(String pName, FormulaType<T> pReturnType, FormulaType<?>... pArgs)	Declare an uninterpreted function.
protected TFormulaInfo	extractInfo(Formula pBits)
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	getFormulaCreator()
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

AbstractUFManager

protected AbstractUFManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFunctionDecl> pCreator)

Method Detail

declareUF

public final <T extends Formula> FunctionDeclaration<T> declareUF(String pName,
                                                                  FormulaType<T> pReturnType,
                                                                  List<FormulaType<?>> pArgTypes)

Description copied from interface: UFManager

Declare an uninterpreted function.

Specified by:

declareUF in interface UFManager

declareUF

public <T extends Formula> FunctionDeclaration<T> declareUF(String pName,
                                                            FormulaType<T> pReturnType,
                                                            FormulaType<?>... pArgs)

Description copied from interface: UFManager

Declare an uninterpreted function.

Specified by:

declareUF in interface UFManager

callUF

public <T extends Formula> T callUF(FunctionDeclaration<T> funcType,
                                    Formula... args)

Specified by:

callUF in interface UFManager

See Also:

UFManager.callUF(FunctionDeclaration, List)

callUF

public final <T extends Formula> T callUF(FunctionDeclaration<T> pFunc,
                                          List<? extends Formula> pArgs)

Description copied from interface: UFManager

Create an uninterpreted function call.

Simply delegates to FormulaManager.makeApplication(FunctionDeclaration, List)

Specified by:

callUF in interface UFManager

Parameters:

pFunc - Declaration of the function to call.

pArgs - Arguments of the function.

Returns:

Instantiated function call.

declareAndCallUF

public <T extends Formula> T declareAndCallUF(String name,
                                              FormulaType<T> pReturnType,
                                              List<Formula> pArgs)

Description copied from interface: UFManager

Declares and calls an uninterpreted function 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:

declareAndCallUF in interface UFManager

declareAndCallUF

public <T extends Formula> T declareAndCallUF(String name,
                                              FormulaType<T> pReturnType,
                                              Formula... pArgs)

Specified by:

declareAndCallUF in interface UFManager

See Also:

UFManager.declareAndCallUF(String, FormulaType, List)

getFormulaCreator

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

extractInfo

protected final TFormulaInfo extractInfo(Formula pBits)

toSolverType

protected final TType toSolverType(FormulaType<?> formulaType)