2

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

具体的には、次のようなことをしたいと思います。

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

次に、新しいサブタイプを作成します。

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

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

4

1 に答える 1

3

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。それぞれが列挙型です。次に、unionデータ型を宣言しますAnimalType。このデータ型には、各動物クラスのコンストラクターが含まれます： Mammal、など。Z3は、各コンストラクターReptileの述語is-[constructor-name]（認識機能）を自動的に作成します： is-Mammal、、is-Reptileなど。アクセサーの名前は「Animal2Class」：、などです。データ型の詳細については、次を参照してくださいAnimal2Mammal。http://rise4fun.com/z3/tutorial/guide。このエンコーディングを使用するスクリプトは次のとおりです。Animal2Reptile

(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
于 2011-12-04T21:08:34.900 に答える