如何在Z3的SMT-LIB中定义枚举类型

Question

我之前使用Z3的API来定义这样的枚举类型

let T = ctx.MkEnumSort("T", [| "a"; "b"; "c"|])

它将类型 T 的元素枚举为“a”、“b”和“c”（仅此而已）。然而，我现在尝试做类似的事情，但通过 SMT-LIB 而不是 API，我遇到了 Z3 抱怨量词的问题。我正在使用的程序（Boogie）生成以下 smt

...
(declare-sort T@T 0)
(declare-fun a() T@T)
(declare-fun b() T@T)
(declare-fun c() T@T)
(assert (forall ((x T@T) ) 
    (! (or
          (= x a)
          (= x b)
          (= x c)
       )
       :qid |gen.28:15|
       :skolemid |1|
     )))
...

断言是类型闭包公理，断言该类型没有其他成员。但是当我将这个（连同其他东西）发送到 Z3 时，经过一番思考后，返回了

WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5
unknown
(:reason-unknown (incomplete quantifiers))

注意： 1. 我已打开MBQI。 2. Boogie 有一个名为“z3types”的选项，但它似乎没有任何区别

MkEnumSort API 调用的 SMT-LIB 等效项是什么？

谢谢

附注我尝试将 RELEVANCY 设置为 1 和 2，但仍然收到有关相关性的警告（CASE_SPLIT 设置为 3）

Answer 1

使用

 (declare-datatypes () ((T@T (a) (b) (c)))

有一个包含更多详细信息的教程：https://microsoft.github.io/z3guide/docs/theories/Datatypes#scalars-enumeration-types

Answer 2

将此用于 SMTLib v2：

(declare-datatypes ((T@T 0)) (((a) (b) (c))))

其中

T@T

是类型的名称，

a, b, c

是其可能的值。