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

【问题标题】：In the Scala^Z3 DSL, how is an uninterpreted function declared?在 Scala^Z3 DSL 中，如何声明未解释的函数？
【发布时间】：2012-06-13 05:32:35
【问题描述】：

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

【问题讨论】：

标签： scala dsl z3

【解决方案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

【讨论】：

你能详细说明一下语法吗？我一直在搜索 scala 文档以了解其工作原理，并尝试了数百种组合，但我无法想出从您建议的构造中获取 BoolOperand 的方法。我知道该怎么做的部分是new Eq(function, new IntConstant(3))。除此之外的任何东西都是 scala 和/或 Z3 的一个黑暗而神秘的区域......感谢您的帮助。
你看过ValHandler的定义吗？它定义了一个类型需要的“支持类”，以便在 DSL 中与find、findAll 等一起使用。这是“类型类”概念的一个示例。
是的，我尝试为我的新函数类型制作一个 ValHandler，但我无法正确计算出语法。当我将新的 BoolOperand 传递给 Z3Context 时，它会中止调用方法而不抛出任何异常......！尽管我没有查看字节码，但我不确定这在 JVM 中是如何实现的。无论如何，如果没有完整的示例，我根本无法完成这项工作。你知道我在哪里可以找到吗？