Uninterpreted function: Difference between revisions

Revision as of 07:08, 27 April 2021

Revision as of 07:16, 27 April 2021

Line 7:

==Example==

As an example of uninterpreted functions for SMT-LIB, we give this input to an [[Satisfiability modulo theories|SMT solver]]:

<syntaxhighlight lang="text" line="1">

(declare-fun f (Int) Int)

(assertdeclare-fun (=f (f 10Int) 1)Int)

(assert (= (f 10) 1))

</syntaxhighlight>

The SMT solver would return "This input is satisfiable". That happens because <code>f</code> is an uninterpreted function (i.e., all that is known about <code>f</code> is its signature), so it is possible that <code>f(10) = 1</code>. But by applying the input below:

<syntaxhighlight lang="text" line="1">

(declare-fun f (Int) Int)

(assert (= (f 10) 421))

(assert (= (f 10) 42))

</syntaxhighlight>

The SMT solver would return "This input is unsatisfiable". That happens because although <code>f</code> has no interpretation, but it is impossible that it returns different values for the same input.

(declare-fun f (Int) Int)

(assert (= (f 10) 1))

(assert (= (f 10) 42))

The SMT solver would return "This input is unsatisfiable". That happens because although <code>f</code> has no interpretation, but it is impossible that it returns different values for the same input.

==Discussion==