Package org.sosy_lab.java_smt.api

Interface UFManager

All Known Implementing Classes:

AbstractUFManager, DebuggingUFManager

public interface UFManager

Manager for dealing with uninterpreted functions (UFs).

Method Summary

Modifier and Type	Method	Description
<T extends Formula> T	callUF(FunctionDeclaration<T> funcType, List<? extends Formula> args)	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 name, FormulaType<T> returnType, List<FormulaType<?>> args)	Declare an uninterpreted function.
<T extends Formula> FunctionDeclaration<T>	declareUF(String name, FormulaType<T> returnType, FormulaType<?>... args)	Declare an uninterpreted function.

Method Detail

declareUF

<T extends Formula> FunctionDeclaration<T> declareUF(String name,
                                                     FormulaType<T> returnType,
                                                     List<FormulaType<?>> args)

Declare an uninterpreted function.

declareUF

<T extends Formula> FunctionDeclaration<T> declareUF(String name,
                                                     FormulaType<T> returnType,
                                                     FormulaType<?>... args)

Declare an uninterpreted function.

callUF

<T extends Formula> T callUF(FunctionDeclaration<T> funcType,
                             List<? extends Formula> args)

Create an uninterpreted function call.

Simply delegates to FormulaManager.makeApplication(FunctionDeclaration, List)

Parameters:

funcType - Declaration of the function to call.

args - Arguments of the function.

Returns:

Instantiated function call.

callUF

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

See Also:

callUF(FunctionDeclaration, List)

declareAndCallUF

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

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.

declareAndCallUF

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

See Also:

declareAndCallUF(String, FormulaType, List)