Esprimere una relazione sottotipo tra i tipi di enumerazione in Z3

Question

Qual è il modo migliore per esprimere una relazione sottotipo tra i tipi di enumerazione in Z3?

In particolare, voglio fare qualcosa come il seguente:

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

e poi crea un nuovo sottotipo:

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

In modo che un'affermazione che esistono 4 costanti distinte di animale di tipo sono sat, ma un'affermazione che esistono 4 costanti distinte di mammifero di tipo non èt.

Answer 1

Z3 non ha supporto diretto per le relazioni sottotipo (subsort). Posso vedere due modi per modellarli in Z3.

Ad esempio, puoi avere un tipo di enumerazione Animal che contiene tutti gli animali. Quindi, si definiscono predicati come: is-mammal, is-reptile, eccetera.

Ecco lo script che utilizza questo approccio:

(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

Un'altra soluzione utilizza i dati dei dati per definire tipi di enumerazione e tipi sindacali. Cioè, dichiariamo un tipo di dati per ogni classe animale: MammalType, ReptileType, ecc. Ognuno di essi è un tipo di enumerazione. Quindi, dichiariamo un union tipo di dati: AnimalType. Questo tipo di dati contiene un costruttore per ogni classe animale: Mammal, Reptile, ecc. Z3 crea automaticamente un predicato is-[constructor-name] (riconoscimento) per ogni costruttore: is-Mammal, is-Reptile, ecc. Nomina gli accessori come "Animal2Class": Animal2Mammal, Animal2Reptile, ecc. Puoi trovare ulteriori informazioni sui dati di dati su http://risise4fun.com/z3/tutorial/guide. Ecco lo script usando questa codifica:

(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