Uninterpreted function: Difference between revisions

Revision as of 20:26, 7 December 2019

Revision as of 07:06, 27 April 2021

Line 6:

==Example==

AnAs an example of uninterpreted functions infor SMT-LIB, anwe inputgive standardthis forinput to [[Satisfiability modulo theories|SMT Solvers]]:

(declare-fun f (Int) Int)

(assert (= (f 10) 1))

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

(declare-fun f (Int) Int)

Line 15:

(assert (= (f 10) 42))

The SMT Solver would return "This 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==

The [[decision problem]] for free theories is particularly important, asbecause many theories can be reduced toby it.{{citation needed|date=December 2019}}

Free theories can be solved by searching for [[common subexpression]]s to form the [[congruence closure]].{{clarify|reason=Indicate about solving which problem in free theories the sentence is supposed to speak. E.g. to solve the satisfiability problem of conjunctions of equations, the Martelli-Montanari syntactic unification algorithm suffices, neither common subexpressions nor congruence closures are needed. Maybe, satisfiability of arbitrary boolean combinations of equations is meant?|date=May 2014}} Solvers include [[satisfiability modulo theories]] solvers.