In the Scala^Z3 DSL, how is an uninterpreted function declared?
I have a small Scala program that transforms a Scala^Z3 DSL expression into latex for easy reading. But I don't see how to declare an uninterpreted function using the DSL. There are many ways to hack the behavior of a function using other constructs, and it's easy to print a hacked function so it looks like a normal function in latex. But I would rather just declare an uninterpreted function, if that is possible somehow.
One way to solve with uninterpreted functions is to use Scala function types in the Val[_] type constructor. For instance:
import z3.scala._ import z3.scala.dsl._ choose( (x : Val[Int], f : Val[Int=>Int]) => x < f(x) ) > res0: (Int, Int=>Int) = (0,<function1>)
The function is then modeled by an actual Scala function:
val f = res0._2 f(0) > 1