Exprimant une relation de sous-typage entre types de dénombrement dans Z3

Question

Quelle est la meilleure façon d'exprimer une relation de sous-type entre les types d'énumération en Z3?

Plus précisément, je veux faire quelque chose comme ce qui suit:

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

et puis créez un nouveau sous-type:

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

de sorte qu'une affirmation selon laquelle il y a 4 constantes distinctes d'un animal est de type SAT, mais une affirmation selon laquelle il y a 4 constantes distinctes de type mammifère est UNSAT.

Answer 1

Z3 n'a pas de soutien direct pour les relations de sous-type (de subsort). Je vois deux façons de les modéliser dans Z3.

Par exemple, vous pouvez avoir une sorte énumération Animal qui contient tous les animaux. Ensuite, vous définissez prédicats tels que:. is-mammal, de is-reptile, etc

Voici le script qui utilise cette approche:

(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

Une autre solution utilise des types de données pour définir sortes d'énumération et les tris syndicaux. Autrement dit, nous déclarons un type de données pour chaque classe d'animaux: MammalType, ReptileType, etc. Chacun d'eux est un type d'énumération. Ensuite, nous déclarons un union type de données: AnimalType. Ce type de données contient un constructeur pour chaque classe d'animaux: Mammal, Reptile, etc. Z3 crée automatiquement un is-[constructor-name] sous-jacente (de reconnaissance) pour chaque constructeur: is-Mammal, is-Reptile, etc. Nous nommons accesseurs comme "Animal2Class": Animal2Mammal, Animal2Reptile, etc. Vous pouvez trouver plus d'informations sur les types de données à http: / /rise4fun.com/z3/tutorial/guide . Voici le script en utilisant cet encodage:

(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