Z3中的SMT-LIB 2.0断言的标签

Question

您能告诉我如何在Z3 SMT-LIB 2.0基准中命名断言吗？我更喜欢使用SMT-LIB的标准语法，但是由于Z3似乎不了解它，我只是在寻找使用Z3的一种。需求是获得带有标签的Unsat内核。

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

(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 and y <= x），unsat core {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文档中的另一种方法。

请问你能帮帮我吗？

Answer 1

如果我更改您的第一个命令

(set-option enable-cores)

至

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

然后我运行您的脚本：

z3 -smt2 script.smt2

我作为输出

unsat
(hyp4 hyp5)

我相信您的期望。请注意，我正在使用Z3 3.2（对于Linux，但这应该没有任何区别）。