arrays - Z3 是否支持对对象数组进行编码？

Question

我想知道 Z3 是否支持对任意复杂对象的数组进行编码，例如列表或其他东西。谢谢。

Answer 1

Z3 支持递归数据类型。我们可以使用它们来定义列表、树等。请参阅Z3 教程中的数据类型部分。我们还可以使用任意索引和值类型定义数组。所以，我们可以有数组数组、列表数组等。这是一个例子。也可在此处在线获取。

(declare-const l (List Int))
(declare-const a (Array Int (List Int)))

(assert (= (select a 0) l))
(assert (not (= l nil)))
(check-sat)