z3 - 支持列表理论

Question

我很好奇Z3是否有内置列表排序？从 C API 看来确实如此，但我有兴趣以 SMTLIB / SMTLIB-2 格式输入而不是使用 C API，所以我想知道 Z3 是否提供任何此类支持。谢谢。

Answer 1

是的，Z3 有一个内置的列表排序。引用Z3 指南，递归数据类型部分：

List 递归数据类型是 Z3 内置的。空列表为 nil，构造函数 insert 用于构建新列表。访问器的头部和尾部像往常一样定义。

这是该部分的一个示范性示例：http ://rise4fun.com/Z3/qXj9 。