3

在 z3 中是否可以声明一个将另一个函数作为参数的函数？例如，这个

(declare-fun foo ( ((Int) Bool) ) Int)

似乎不太奏效。谢谢。

4

2 回答 2

8

正如 Leonardo 所提到的，SMT-Lib不允许使用高阶函数。这不仅仅是句法限制：使用高阶函数进行推理（通常）超出了 SMT 求解器可以处理的范围。（尽管在某些特殊情况下可以使用未解释的函数。）

如果您确实需要使用高阶函数进行推理，那么交互式定理证明器是首选的主要武器： Isabelle、HOL、Coq就是其中的一些例子。

但是，有时您不希望高阶函数对它们进行推理，而只是为了简化编程任务。SMT-Lib 输入语言不适用于最终用户在实际情况中通常需要的高级编程。如果这是您的用例，那么我建议您不要直接使用 SMT-Lib，而是使用可以让您访问 Z3（或其他 SMT 求解器）的编程语言。有多种选择，具体取决于最适合您的用例的宿主语言：

  • 如果你是 Python 用户，那么 Z3 4.0 附带的Z3Py就是你要走的路，
  • 如果您是 Scala 用户，请查看Scala^Z3。
  • 如果 Haskell 是您的首选语言，请查看SBV。

每个绑定都有自己的功能集，Z3Py 可能是最通用的，因为它直接受到 Z3 人员的支持。（它还提供了对其他选择仍然无法访问的 Z3 内部的访问，至少目前是这样。）

于 2012-05-13T20:06:21.120 回答
6

不，这是不可能的。但是，您可以定义一个将数组作为参数的函数。

(declare-fun foo ((Array Int Bool)) Int)

您可以使用此技巧来模拟高阶函数，例如您的问题中的函数。

这是一个例子：http ://rise4fun.com/Z3/qsED

Z3 指南包含有关 Z3 和 SMT 的更多信息。

于 2012-05-12T23:02:59.937 回答