z3的python API不一致的结果

如何解决z3的python API不一致的结果

我正在使用 Z3 的 ocaml 以便在获得 unsat 核心时命名每个约束，例如

(set-option :produce-unsat-cores true)
(declare-fun x () Int)
(assert (!(> x 0) :named p1))
(assert (!(not (= x 1)) :named p2))
(assert (!(< x 0) :named p3))
(check-sat)
(get-unsat-core)

结果是unsat。然后我在ocaml中为Z3找到了一个API assert_and_track，在python中找到了一个解决方案（Unsatisfiable Cores in Z3 Python），然后我有以下简单的例子：

from z3 import *

x = Int('x')
s = Solver()
s.set(unsat_core=True)
s.assert_and_track(x > 0,'p1')
s.assert_and_track(x != 1,'p2')
s.assert_and_track(x < 0,'p3')
print(s.check())
print(s.to_smt2())
c = s.unsat_core()
for i in range(0,len(c)):
    print(c[i])

这个例子的结果是

unsat
; benchmark generated from python API
(set-info :status unknown)
(declare-fun x () Int)
(declare-fun p1 () Bool)
(declare-fun p2 () Bool)
(declare-fun p3 () Bool)
(assert
 (let (($x7 (> x 0)))
 (=> p1 $x7)))
(assert
 (let (($x33 (and (distinct x 1) true)))
 (=> p2 $x33)))
(assert
 (let (($x40 (< x 0)))
 (=> p3 $x40)))
(check-sat)

p1
p3

然后我把生成的SMT2格式复制到z3，发现结果是sat。为什么python生成的z3 smt2格式代码与python不一致，如何在ocaml中使用？

解决方法

生成的基准（通过调用 s.to_smt2()) 并没有捕捉到 python 程序实际在做什么。这是令人遗憾和令人困惑的，但遵循内部约束的转换方式。（它只是不知道你正在尝试做一个不饱和的核心。）

好消息是修复并不难。您需要获取生成的基准，并在顶部添加以下行：

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

然后，您需要将 (check-sat) 替换为：

(check-sat-assuming (p1 p2 p3))
(get-unsat-core)

所以，最终的程序看起来像：

; benchmark generated from python API
(set-info :status unknown)
(set-option :produce-unsat-cores true)
(declare-fun x () Int)
(declare-fun p1 () Bool)
(declare-fun p2 () Bool)
(declare-fun p3 () Bool)
(assert
 (let (($x7 (> x 0)))
 (=> p1 $x7)))
(assert
 (let (($x33 (and (distinct x 1) true)))
 (=> p2 $x33)))
(assert
 (let (($x40 (< x 0)))
 (=> p3 $x40)))
(check-sat-assuming (p1 p2 p3))
(get-unsat-core)

如果你运行这个最终程序，你会看到它会打印：

unsat
(p1 p3)

正如预期的那样。

关于如何从 O'Caml 执行此操作：您需要使用 get_unsat_core 函数，请参阅此处：https://github.com/Z3Prover/z3/blob/master/src/api/ml/z3.ml#L1843