Uninterpreted Functions
An uninterpreted function is a function where the mapping between input and output is not known. The task of the SMT solver is then to determine a mapping such that some SMT expression holds true.
Satisfiability.jl represents uninterpreted functions as callable structs. This enables the simple syntax:
using Satisfiability
@uninterpreted(myfunc, Int, Int)
# we can call myfunc on an Int constant or variable
@satvariable(a, Int)
myfunc(a)
myfunc(-2) # returns
# we cannot call myfunc on the wrong type
# myfunc(true) yields an error
# myfunc(1.5) yields an error
As a small example, we can ask whether there exists a function f(x)
such that f(f(x)) == x
, f(x) == y
and x != y
.
Note that when using Yices, you must set the logic. Here we set it to "QF_UFLIA" - "Quantifier free uninterpreted functions, linear integer arithmetic". (This is OK even though we're only using Boolean variables. We have to include uninterpreted functions or Yices will hang.)
@satvariable(x, Bool)
@satvariable(y, Bool)
@uninterpreted(f, Bool, Bool)
status = sat!(distinct(x,y), f(x) == y, f(f(x)) == x, solver=Yices(), logic="QF_UFLIA")
println("status = $status")
It turns out there is. Since the satisfying assignment for an uninterpreted function is itself a function, Satisfiability.jl represents this by setting the value of f
to this function. Now calling f(value)
will return the value of this satisfying assignment.
println(x.value == y.value) # false
println(f(x.value) == y.value) # true
println(f(f(x.value)) == x.value) # true