如何在 SMT-LIB for Z3 中定义枚举类型答案

【问题标题】：How to define enumerated types in SMT-LIB for Z3如何在 SMT-LIB for Z3 中定义枚举类型
【发布时间】：2014-11-09 15:23:13
【问题描述】：

我之前使用 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）

【问题讨论】：

标签： z3 smt

【解决方案1】：

使用

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

有更详细的教程：http://rise4fun.com/z3/tutorialcontent/guide#h27

【讨论】：