Content deleted Content added
→Example: the previous example was not about uninterpreted functions. This edit replaces it. Tag: references removed |
m →Example: formatting, and corrected the link to the smt page. |
||
Line 6:
==Example==
An example of uninterpreted functions in SMT-LIB, an input standard for [[
(declare-fun f (Int) Int)▼
(assert (= (f 10) 1))▼
▲(declare-fun f (Int) Int)
▲(assert (= (f 10) 1))
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>.
(declare-fun f (Int) Int)
(
(assert (= (f 10) 42))▼
▲(assert (= (f 10) 42))
This is unsatisfiable: although <code>f</code> has no interpretation, it is impossible that it returns different values for the same input.
| |||