Uninterpreted function: Difference between revisions

Revision as of 07:21, 27 April 2021

Revision as of 07:38, 27 April 2021

Line 6:

==Example==

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

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

(declare-fun f (Int) Int)

(assert (= (f 10) 1))

</syntaxhighlight>

Thethe 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 (logic)|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)

Line 18:

</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.

==Discussion==