首页 文章

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

提问于
浏览
1

我以前使用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)

1 回答

相关问题