Ausdrücke einer Subtyp -Beziehung zwischen Aufzählungsarten in Z3

Question

Was ist der beste Weg, um eine Subtyp -Beziehung zwischen Aufzählungstypen in Z3 auszudrücken?

Insbesondere möchte ich so etwas wie Folgendes machen:

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

und erstellen Sie dann einen neuen Subtyp:

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

Daher ist eine Behauptung, dass es 4 verschiedene Konstanten vom Typ Tier gibt, aber eine Behauptung, dass es 4 verschiedene Konstanten vom Typ Säugetier gibt, ist nicht.

Answer 1

Z3 hat keine direkte Unterstützung für Subtypen (Subsort) Beziehungen. Ich kann zwei Möglichkeiten sehen, sie in Z3 zu modellieren.

Zum Beispiel können Sie eine Aufzählungsart haben Animal Das enthält alle Tiere. Dann definieren Sie Prädikate wie: is-mammal, is-reptile, etc.

Hier ist das Skript, das diesen Ansatz verwendet:

(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

Eine andere Lösung verwendet Datentypen zum Definieren von Aufzählungsarten und Gewerkschaftsarten. Das heißt, wir deklarieren für jede Tierklasse einen Datenatyp: MammalType, ReptileType, usw. Jeder von ihnen ist ein Aufzählungstyp. Dann deklarieren wir eine union Datentyp: AnimalType. Dieser Datentyp enthält einen Konstruktor für jede Tierklasse: Mammal, Reptile, usw. Z3 erzeugt automatisch ein Prädikat is-[constructor-name] (Erkenntnis) für jeden Konstruktor: is-Mammal, is-Reptile, usw. Wir nennen Accessors als "Animal2Class": Animal2Mammal, Animal2Reptile, usw. finden Sie weitere Informationen zu DataTypen unter http://rise4fun.com/z3/tutorial/guide. Hier ist das Skript mit dieser Codierung:

(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