Expressing a subtype relation between enumeration types in Z3

Question

What's the best way to express a subtype relation between enumeration types in Z3?

Specifically, I want to do something like the following:

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

and then create a new subtype:

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

so that an assertion that there are 4 distinct constants of type Animal is SAT, but an assertion that there are 4 distinct constants of type Mammal is UNSAT.

Answer 1

Z3 has no direct support for subtype (subsort) relationships. I can see two ways to model them in Z3.

For example, you can have an enumeration sort Animal that contains all animals. Then, you define predicates such as: is-mammal, is-reptile, etc.

Here is the script that uses this approach:

(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

Another solution uses datatypes for defining enumeration sorts and union sorts. That is, we declare one datatype for each animal class: MammalType, ReptileType, etc. Each of them is an enumeration type. Then, we declare an union datatype: AnimalType. This datatype contains a constructor for each animal class: Mammal, Reptile, etc. Z3 automatically creates a predicate is-[constructor-name] (recognizer) for each constructor: is-Mammal, is-Reptile, etc. We name accessors as "Animal2Class": Animal2Mammal, Animal2Reptile, etc. You can find more information about datatypes at http://rise4fun.com/z3/tutorial/guide. Here is the script using this encoding:

(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