我以前使用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 回答
使用
有一个更详细的教程:http://rise4fun.com/z3/tutorialcontent/guide#h27