scala - 在 Scala^Z3 DSL 中，如何声明未解释的函数？

Question

我有一个小型 Scala 程序，可以将 Scala^Z3 DSL 表达式转换为 Latex 以便于阅读。但我看不到如何使用 DSL 声明未解释的函数。有很多方法可以使用其他构造来破解函数的行为，并且很容易打印被破解的函数，因此它看起来就像乳胶中的普通函数。但我宁愿只声明一个未解释的函数，如果以某种方式可能的话。

Answer 1

解决未解释函数的一种方法是在Val[_]类型构造函数中使用 Scala 函数类型。例如：

import z3.scala._
import z3.scala.dsl._

choose(
  (x : Val[Int], f : Val[Int=>Int]) => x < f(x)
)

> res0: (Int, Int=>Int) = (0,<function1>)

然后该函数由实际的 Scala 函数建模：

val f = res0._2
f(0)

> 1