z3中的函数声明

Question

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

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

似乎不工作。谢谢。

Answer 1

正如莱昂纳多所说，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内部机制的权限，至少暂时不能访问其他选项）。

Answer 2

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

（声明乐趣富（（阵列整数BOOL））智力）

您可以使用这种伎俩来模拟像在你的问题的高阶功能。

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

的Z3 guide包含有关Z3和SMT的详细信息。