参数化排序

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了全面的介绍。