Expresando una relación de subtipo entre los tipos de enumeración en Z3

Question

¿Cuál es la mejor manera de expresar una relación de subtipo entre los tipos de enumeración en Z3?

Específicamente, quiero hacer algo como lo siguiente:

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

y luego crea un nuevo subtipo:

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

de modo que se satia una afirmación de que hay 4 constantes distintas de animales tipo, pero una afirmación de que hay 4 constantes distintas de tipo mamífero es unsat.

Answer 1

Z3 no tiene soporte directo para las relaciones de subtipo (subsort). Puedo ver dos formas de modelarlos en Z3.

Por ejemplo, puede tener un tipo de enumeración Animal que contiene todos los animales. Entonces, defines predicados como: is-mammal, is-reptile, etc.

Aquí está el script que utiliza este enfoque:

(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

Otra solución utiliza los tipos de datos para definir tipos de enumeración y tipos de sindicatos. Es decir, declaramos un tipo de datos para cada clase de animales: MammalType, ReptileType, etc. Cada uno de ellos es un tipo de enumeración. Entonces, declaramos un union tipo de datos: AnimalType. Este tipo de datos contiene un constructor para cada clase de animales: Mammal, Reptile, etc. Z3 crea automáticamente un predicado is-[constructor-name] (Reconocer) para cada constructor: is-Mammal, is-Reptile, etc. Nombramos accesorios como "Animal2Class": Animal2Mammal, Animal2Reptile, etc., puede encontrar más información sobre los tipos de datos en http://rise4fun.com/z3/tutorial/guide. Aquí está el script usando esta codificación:

(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