Expresando una relación de subtipo entre los tipos de enumeración en Z3
Pregunta
¿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.
Solución
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