|
==Example==
An example of uninterpreted functions in SMT-LIB, an input standard for [[SMT|SMT Solvers]]:
An [[array data structure|array]] can be specified by the following equational [[axiom]]:<ref group=note>Here, ''select''(''a'',''i'') informally designates the value of the ''i''th element of ''a'', written e.g. in [[C (programming language)|C]] as <code lang="C">a[i]</code>, while ''store''(''a'',''i'',''v'') informally designates the array resulting from writing the value ''v'' to the ''i''th element of ''a'', written in C as <code lang="C">a[i]=v</code>.
The axiom then informally means that the value obtained by the statements <code lang="C">a[i]=v;return a[j];</code> equals <code lang="C">v</code> if <code lang="C">i</code>=<code lang="C">j</code>, and <code lang="C">a[j]</code>, else.</ref>
<code>
: ''select''(''store''(''a'',''i'',''v''),''j'') = (if ''i'' = ''j'' then ''v'' else ''select''(''a'',''j''))
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
This axiom can be used to deduce<ref group=note>This deduction corresponds to the computation of the value obtained by <code lang="C">a[1]=-1;a[2]=-2;return a[1];</code></ref>
</code>
This is satisfiable: <code>f</code> is an uninterpreted function. All that is known about <code>f</code> is its signature, so it is possible that <code>f(10) = 1</code>.
: ''select''(''store''(''store''(''a'',1,−1),2,−2),1)
:: = ''select''(''store''(''a'',1,−1),1)
:: = −1
<code>
Note that this reasoning did ''not'' use any 'definition' or [[interpretation (logic)|interpretation]] for the functions ''select'' and ''store''. All that is known is the axiom.
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))
</code>
This is unsatisfiable: although <code>f</code> has no interpretation, it is impossible that it returns different values for the same input.
==Discussion==
| 