在 Z3 中表达枚举类型之间的子类型关系的最佳方式是什么？
具体来说，我想做如下的事情：
(declare-datatypes () ((Animal Eagle Snake Scorpion)))
然后创建一个新的子类型：
(declare-datatypes () ((Mammal Cat Rat Bat)))
因此，有 4 个不同类型的 Animal 常量的断言是 SAT，但有 4 个不同类型的 Mammal 常量的断言是 UNSAT。
【问题讨论】：
Z3 不直接支持子类型（子排序）关系。 我可以看到在 Z3 中建模它们的两种方法。
例如，您可以有一个枚举排序Animal，其中包含所有动物。然后，您定义谓词，例如：is-mammal、is-reptile 等。
下面是使用这种方法的脚本：
(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
另一种解决方案使用数据类型来定义枚举排序和联合排序。
也就是说，我们为每个动物类声明一个数据类型：MammalType、ReptileType 等。
它们中的每一个都是枚举类型。然后，我们声明一个union 数据类型：AnimalType。
此数据类型包含每个动物类的构造函数：Mammal、Reptile 等。
Z3 自动为每个构造函数创建谓词is-[constructor-name]（识别器）：is-Mammal、is-Reptile 等。
我们将访问器命名为“Animal2Class”：Animal2Mammal、Animal2Reptile 等。您可以在 http://rise4fun.com/z3/tutorial/guide 找到有关数据类型的更多信息。
这是使用这种编码的脚本：
(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
【讨论】：