參數化排序

Question

如何訪問參數化排序的值？

舉例來說，如果我有以下聲明：

(declare-sort Pair 2) 
(declare-const x (Pair Int Int)) 

如何訪問的第一個元素的一對x代表？

Answer 1

您可以使用兩個選擇器first和second創建參數記錄以訪問其字段。

這裏是an example：

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 
(declare-const p1 (Pair Bool Int)) 
(declare-const p2 (Pair Int Int)) 
(assert (first p1)) 
(assert (> (first p2) 2)) 
(assert (= (second p1) (second p2))) 
(check-sat) 
(get-model) 

也有在Z3 SMT指南algebraic datatypes了全面的介紹。