z3 - パラメータ化された並べ替え

Question

パラメータ化された並べ替えの値にアクセスするにはどうすればよいですか?

たとえば、次の宣言があるとします。

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

xを表すペアの最初の要素にアクセスするにはどうすればよいですか?

Answer 1

2 つのセレクターfirstを持ちsecond、そのフィールドにアクセスするためのパラメトリック レコードを作成できます。

例を次に示します。

(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 ガイドには、代数データ型に関する包括的な紹介もあります。