Z3是否支持編碼對象數組？

Question

我想知道Z3是否支持對任意複雜對象的數組進行編碼，例如列表或其他東西。 謝謝。

Answer 1

Z3支持遞歸的數據類型。我們可以使用它們來定義列表，樹等。請參見Z3 tutorial中的數據類型一節。我們也可以使用任意索引和值類型來定義數組。所以，我們可以有陣列數組，列表數組等等。 這裏是一個例子。也可在線獲得here。

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

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