Uninterpreted Functions

[juliusbrehme]

Hello everyone,

I have a question how to declare and call uninterpreted functions.

I found the function uninterpreted_function(const std::string& name, const Variables& vars) to declare an uninterpreted functions. Is it possible to set the return type? For example if I want to do the following:

(declare-sort A)
(declare-const x A)
(declare-const y A)
(declare-fun f (A) A)
(assert (= (f (f x)) x))
(assert (= (f x) y))
(assert (not (= x y)))
(check-sat)
(get-model)

I declare the function f with A. After that I can call the function with the parameter. Does the function allow that too?

If I want to do the following:

(declare-sort Int)
(declare-fun f (Int) Int)

is it possible to do so. The function mentioned above let's me define the function only with variables, can I set Constants as well?

Thanks in advance.

[soonhokong]

First of all, dReal does not support the theory of uninterpreted functions (UF). uninterpreted_function in its symbolic language is provided for symbolic manipulation (e.g. you can replace an uninterpreted function with a concrete term).

[juliusbrehme]

Thanks for all the answers to my questions. That has already helped me a lot.

But regarding the UF's, in SMT (with UF theory), the solver is responsible for finding the 'concrete term' for an UF. This is not the task of the user. In most cases, the solver chooses a partial model that contains only/exactly those return-values that are required for the given input-values. After finding such a partial model, you can of course convert it into a 'concrete term' and substitute the UF with it.