2

你能告诉我如何在 z3 SMT-LIB 2.0 基准测试中命名断言吗？我更喜欢使用 SMT-LIB 的标准语法，但由于 z3 似乎不理解它，我只是在寻找一个使用 z3 的语法。需要获得带有标签的未饱和核心。

这是我测试的基准测试示例：

(set-option enable-cores)
(set-logic AUFLIA)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (! (<= 0 x) :named hyp1))
(assert (! (<= 0 y) :named hyp2))
(assert (! (<= 0 z) :named hyp3))
(assert (! (< x y) :named hyp4))
(assert (! (and (<= 0 y) (<= y x)) :named hyp5))
(assert (! (not (= x z)) :named goal))
(check-sat)
(get-unsat-core)

由于矛盾（x < y 和 y <= x），我期待 unsat 核心 {hyp4, hyp5}，但 z3 返回：

(error "ERROR: line 10 column 31: could not locate id  hyp1.")
(error "ERROR: line 11 column 31: could not locate id  hyp2.")
(error "ERROR: line 12 column 31: could not locate id  hyp3.")
(error "ERROR: line 13 column 30: could not locate id  hyp4.")
(error "ERROR: line 16 column 36: could not locate id  hyp5.")
(error "ERROR: line 18 column 35: could not locate id  goal.")
sat
()

我知道 z3 不理解这种命名方式，但我在 z3 文档中找不到另一种方式。

请问你能帮帮我吗？

4

1 回答 1

4

如果我将您的第一个命令从

(set-option enable-cores)

到

(set-option :produce-unsat-cores true)

然后我运行你的脚本：

z3 -smt2 script.smt2

我得到作为输出

unsat
(hyp4 hyp5)

这就是我相信你所期待的。请注意，我使用的是 Z3 3.2（对于 Linux，但这应该没有任何区别）。

于 2011-10-18T10:22:46.600 回答