支持列表理論

Question

我很好奇Z3是否有內置列表排序？從C API看起來好像是這樣，但我有興趣輸入SMTLIB/SMTLIB-2格式而不是使用C API，所以我想知道Z3是否提供了這種支持。謝謝。

Answer 1

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

列表遞歸數據類型在Z3中內置。空列表爲零， ，構造函數插入用於構建新列表。頭部和尾部的訪問器按照慣例定義。

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