z3 中的函数声明 [英] function declaration in z3

问题描述

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

In z3 is it possible to declare a function that takes another function as an argument? For instance, this

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

似乎不太好用.谢谢.

推荐答案

正如 Leonardo 所提到的，SMT-Lib 不允许允许高阶函数.这不仅仅是句法限制:高阶函数的推理(通常)超出了 SMT 求解器的处理能力.(尽管在某些特殊情况下可以使用未解释的函数.)

As Leonardo mentioned, SMT-Lib does not allow higher-order functions. This is not merely a syntactic restriction: Reasoning with higher-order functions is (generally) beyond what SMT solvers can deal with. (Although uninterpreted functions can be used in some special cases.)

如果您确实需要对高阶函数进行推理，那么交互式定理证明器是首选的主要武器:伊莎贝尔、HOL、Coq 就是其中的一些例子.

If you do need to reason with higher-order functions, then interactive theorem provers are the main weapon of choice: Isabelle, HOL, Coq being some of the examples.

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

However, sometimes you want the higher-order functions not to reason about them, but rather merely to simplify programming tasks. SMT-Lib input language is not suitable for high-level programming that end-users typically need in practical situations. If that is your use case, then I'd recommend not using SMT-Lib directly, but rather working with a programming language that gives you access to Z3 (or other SMT solvers). There are several choices, depending on what host language is most suitable for your use case:

• 如果您是 Python 用户，那么 Z3 4.0 附带的 Z3Py 是您的最佳选择，立>
• 如果您是 Scala 用户，请查看 Scala^Z3.
• 如果 Haskell 是您的首选语言，请查看 SBV.

• If you are a Python user, Z3Py that just shipped with Z3 4.0 is the way to go,
• If you are a Scala user, then look into Scala^Z3.
• If Haskell is your preferred language, then take a look at SBV.

每个绑定都有自己的功能集，Z3Py 可能是最通用的，因为 Z3 人员直接支持它.(它还提供对 Z3 内部结构的访问，而其他选择仍然无法访问这些内部结构，至少目前是这样.)

Each binding has its own feature set, Z3Py probably being the most versatile since it's directly supported by the Z3 folks. (It also provides access to Z3 internals that remain inaccessible for the other choices, at least for the time being.)

这篇关于z3 中的函数声明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！