支持列表理论

Question

我很好奇Z3是否有内置列表排序？从C API看起来好像是这样，但我有兴趣输入SMTLIB/SMTLIB-2格式而不是使用C API，所以我想知道Z3是否提供了这种支持。谢谢。

Answer 1

是的，Z3有一个内置的列表排序。引用自Z3 guide, section Recursive datatypes：

列表递归数据类型在Z3中内置。空列表为零， ，构造函数插入用于构建新列表。头部和尾部的访问器按照惯例定义。

以下是该部分的示例：http://rise4fun.com/Z3/qXj9。