时间戳

首页 > 解决方案 > z3的python API中的结果不一致

python - 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。assert_and_track然后我在 ocaml 中为 Z3找到了一个 API ，在 python 中找到了一个解决方案（在 Z3 Python 中的 Unsatisfiable Cores），然后我有以下简单示例：

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中使用？

标签： pythonocamlz3

解决方案

生成的基准（通过调用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

推荐阅读