匿名函数

Question

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

Answer 1

Z3既不支持λ表达式(请参阅主要Z3开发人员之一Nikolaj Bjorner的this answer )，也不是SMTLib2标准的一部分。支持λ表达式的求解器将其作为SMTLib2标准的自定义扩展来支持。

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