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

Question

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

具体的には、私は次のような何かをしたい：その後、

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

と新しいサブタイプの作成：タイプの動物の4つの異なる定数があるという主張があるように

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

をSATですが、Mammal型の4つの異なる定数が存在するという主張はUNSATです。

Answer 1

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

、あなたはすべての動物が含まれているソートAnimal列挙を持つことができます。すると、次のような述語定義：別の解決策を列挙ソートや労働組合の種類を定義するためのデータ型を使用しています

(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 

：ここなど、is-reptile、is-mammalを

は、このアプローチを使用するスクリプトです。など MammalType、ReptileType、それらの各列挙型がある：ある は、我々は1つの各動物のクラスのデータ型を宣言します。次に、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