z3 - 匿名函数

Question

我发现 Yices 中对匿名函数（lambda 表达式）的支持非常有帮助。我现在正在尝试使用 Z3 来实现一个工具，但我无法确定是否支持此功能。我正在使用 -smt2 标志调用该工具。谢谢你的帮助。

Answer 1

AFAIK，Z3 既不支持 lambda 表达式（请参阅主要 Z3 开发人员之一 Nikolaj Bjorner 的回答），它们也不是 SMTLib2 标准的一部分。支持 lambda 表达式的求解器（例如 Yices 或 veriT）支持将它们作为 SMTLib2 标准的自定义扩展。

根据您的需求（您可能想通过在问题中添加示例来说明），您可以尝试 Z3 宏 ( define-fun) 或 Z3Py 之类的前端，与手动编写 SMTLib 代码相比，它大大简化了 Z3 的使用。