python API for z3 的结果不一致

Question

我正在使用 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。然后我在 Z3 的 ocaml 中找到了 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中使用它？

Answer 1

生成的基准测试（通过调用 s.to_smt2()) 没有捕捉到 python 程序实际在做什么。这是不幸和令人困惑的，但从内部约束的翻译方式来看。（它只是不知道你正在尝试做一个 unsat-core。）

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

(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

python API for z3 的结果不一致

inconsistent result in python API for z3

python

ocaml

z3