问题描述
您能告诉我如何在z3 SMT-LIB 2.0基准测试中命名断言吗?我更喜欢使用SMT-LIB的标准语法，但是由于z3似乎不了解它，我只是在寻找一种使用z3的工具.需要获得带有标签的非饱和核.
Could you tell me how to name assertions in a z3 SMT-LIB 2.0 benchmark? I would prefer to use the standard syntax of SMT-LIB, but as z3 seems not to understand it, I'm just looking for one working with z3. The need is to get unsat cores with labels.
这是我测试过的基准测试的一个示例:
Here is an example of benchmark I tested:
(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
I am expecting the unsat core {hyp4, hyp5} because of the contradiction (x < y and y <= x), but z3 returns:
(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文档中找不到另一种方式.
I understand that z3 does not understand this way of naming, but I could not find another way in z3 documentation.
你能帮我吗?
推荐答案
如果我将第一个命令更改为
If I change your first command from
(set-option enable-cores)
到
(set-option :produce-unsat-cores true)
然后我运行您的脚本:
z3 -smt2 script.smt2
我得到了输出
unsat
(hyp4 hyp5)
这是我相信您所期望的.请注意，我使用的是Z3 3.2(适用于Linux，但这应该没有任何区别).
which is I believe what you were expecting. Note that I'm using Z3 3.2 (for Linux, but that shouldn't make any difference).
这篇关于z3中SMT-LIB 2.0断言上的标签的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！