Z3の列挙タイプ間のサブタイプの関係を表す

Question

Z3の列挙タイプ間のサブタイプの関係を表現する最良の方法は何ですか？

具体的には、次のようなことをしたい：

(declare-datatypes () ((Animal Eagle Snake Scorpion)))

そして、新しいサブタイプを作成します：

(declare-datatypes () ((Mammal Cat Rat Bat)))

そのため、タイプの動物の4つの異なる定数があるという主張は座っていますが、哺乳類の4つの異なる定数があるという主張は不定です。

Answer 1

Z3は、サブタイプ（サブソート）関係を直接サポートしていません。 Z3でそれらをモデル化する2つの方法を見ることができます。

たとえば、列挙ソートを使用できます Animal それにはすべての動物が含まれています。次に、次のような述語を定義します。 is-mammal, is-reptile, 、など

このアプローチを使用するスクリプトは次のとおりです。

(set-option :produce-models true)
(declare-datatypes () ((Animal Eagle Snake Scorpion Cat Rat Man)))

(define-fun is-mammal ((x Animal)) Bool
        (or (= x Cat) (= x Rat) (= x Man)))

(declare-const a1 Animal)
(declare-const a2 Animal)
(declare-const a3 Animal)
(declare-const a4 Animal)


(assert (distinct a1 a2 a3 a4))
(check-sat)
; sat
(get-model)

; now, we constraint a1, a2, a3 and a4 to be mammals.
(assert (is-mammal a1))
(assert (is-mammal a2))
(assert (is-mammal a3))
(assert (is-mammal a4))
(check-sat)
; unsat

別のソリューションでは、列挙のソートとユニオンソートを定義するためにデータ型を使用します。つまり、各動物クラスに1つのデータ型を宣言します。 MammalType, ReptileType, 、など。それぞれが列挙タイプです。次に、Anを宣言します union データ・タイプ： AnimalType。このデータ型には、各動物クラスのコンストラクターが含まれています。 Mammal, Reptile, 、など。Z3は自動的に述語を作成します is-[constructor-name] （認識者）各コンストラクターの： is-Mammal, is-Reptile, 、など。アクセターを「Animal2class」と名付けます。 Animal2Mammal, Animal2Reptile, 、など。データ型の詳細情報をの詳細 http://rise4fun.com/z3/tutorial/guide。このエンコードを使用したスクリプトは次のとおりです。

(set-option :produce-models true)

(declare-datatypes () ((AveType Eagle Sparrow)))
(declare-datatypes () ((ReptileType Snake)))
(declare-datatypes () ((ArachnidType Scorpion Spider)))
(declare-datatypes () ((MammalType Cat Rat Man)))

(declare-datatypes () ((AnimalType 
                        (Ave (Animal2Ave AveType))
                        (Reptile (Animal2Reptile ReptileType))
                        (Arachnid (Animal2Arachnid ArachnidType))
                        (Mammal (Animal2Mammal MammalType)))))

(declare-const a1 AnimalType)
(declare-const a2 AnimalType)
(declare-const a3 AnimalType)
(declare-const a4 AnimalType)

(assert (distinct a1 a2 a3 a4))
(check-sat)
; sat
(get-model)

; now, we constraint a1, a2, a3 and a4 to be mammals.
(assert (is-Mammal a1))
(assert (is-Mammal a2))
(assert (is-Mammal a3))
(assert (is-Mammal a4))
(check-sat)
; unsat