z3 - smtlib 是否支持一流的功能？

Question

假设为 haskellmap函数建模，它接受一个“映射器”函数，该函数应用于列表的所有元素。如何map在 smtlib 中声明？

标签： z3smt

Answer 1

不; SMTLib 本质上是一阶理论；根本不支持高阶函数。

然而，Z3 允许通过(_ map f)扩展名映射函数到数组上。请参阅https://rise4fun.com/Z3/tutorial/guide，搜索“数组上的映射函数”。这不会为您提供任意的高阶函数，但可以用来模拟那些在 SMTLib 数组上运行的函数。

如果您确实打算推理高阶函数，那么 SMTLib 对您来说可能是错误的逻辑。使用更传统的定理证明器（如 HOL/Isabelle）或 Agda/Coq 中的现代化身会更合适。您还可以查看精益，它在功能和自动化方面取得了很好的折衷。