1

如何访问参数化排序的值?

例如,如果我有以下声明:

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

如何访问x代表的对中的第一个元素?

4

1 回答 1

1

您可以使用两个选择器创建参数记录firstsecond访问其字段。

这是一个例子

(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指南中也有关于代数数据类型的全面介绍。

于 2012-10-16T21:55:56.840 回答