Python Z3 API 查询：当求解器返回未知状态时，我们能否使用 z3 python API 获取部分模型

Question

我很确定它与 python API 有关。即使状态为unknown，有没有办法从z3取回部分模型？

即使状态返回 unknown 结果，我也试图从 z3 中获取模型。为model not available 提升exception 失败。有什么建议可以做什么？

我使用z3 Solver 接口中的sexpr() 方法将断言转换为smt-lib 格式，即使状态为unknown，它也会返回部分模型。我在下面附上了示例。

# -*- coding: utf-8 -*-
​
from z3 import *
​
x, y, z = Reals('x y z')
m, n, l = Reals('m n l')
u, v = Ints('u v')
​
S = SolverFor("NRA")
​
S.add(x >= 0)
S.add(y >= 30, z <= 50)
S.add(m >= 5, n >= 5)
S.add(m * x + n * y + l > 300)
​
S.add(ForAll([u, v], Implies(m * u + n * v + l > 300, u + v + z <= 50)))
​
print(S.check())
print(S.sexpr())

SMMT-LIB 格式

(set-option :print-success true) 
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(set-option :produce-proofs true) ; enable proof generation
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun l () Real)
(assert (>= x 0.0))
(assert (>= y 30.0))
(assert (<= z 50.0))
(assert (>= m 5.0))
(assert (>= n 5.0))
(assert (not (<= (+ (* m x) (* n y) l) 300.0)))
(assert (forall ((u Int) (v Int))
  (let ((a!1 (<= (+ (* m (to_real u)) (* n (to_real v)) l) 300.0)))
    (or (<= (+ (to_real u) (to_real v) z) 50.0) a!1))))
(check-sat)
(get-model)

我正在从命令行（终端）运行这个文件

$ z3 example.py

输出：

success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
unknown
(model 
  (define-fun z () Real
    20.0)
  (define-fun y () Real
    30.0)
  (define-fun l () Real
    145.0)
  (define-fun x () Real
    0.0)
  (define-fun n () Real
    5.0)
  (define-fun m () Real
    5.0)
)

关于如何直接通过python接口获取这个模型有什么建议吗？

z3 在model() 调用unknown 状态后引发的异常。

unknown
Traceback (most recent call last):

  File "C:\Python38\Lib\site-packages\z3\z3.py", line 6696, in model
    return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)

  File "C:\Python38\Lib\site-packages\z3\z3core.py", line 3759, in Z3_solver_get_model
    _elems.Check(a0)

  File "C:\Python38\Lib\site-packages\z3\z3core.py", line 1385, in Check
    raise self.Exception(self.get_error_message(ctx, err))

Z3Exception: b'there is no current model'


During handling of the above exception, another exception occurred:

Traceback (most recent call last):

  File "C:\Users\lahir\Documents\GitHub\codersguild\Research\tangram-solve\z3_tryouts.py", line 19, in <module>
    print(S.model())

  File "C:\Python38\Lib\site-packages\z3\z3.py", line 6698, in model
    raise Z3Exception("model is not available")

Z3Exception: model is not available

谢谢

Answer 1

除了我上面提到的那个之外，我还没有找到替代品。

Answer 2

如果求解器返回 unknown，则您不能依赖该模型。也就是说，您获得的模型无论如何都不是“部分”的：它可能满足也可能不满足某些约束，但除此之外，您无能为力。它充其量是求解器内部状态的表示。但总的来说，它不能保证代表任何东西。

另外，当我使用 z3 运行您的 SMTLib 脚本时，我得到：

unknown
(error "line 21 column 10: model is not available")

大约一周前，我已经从他们的 github master 构建了 z3。我猜你有一个旧版本，我强烈建议你升级。

作为参考，当您得到未知作为答案时，唯一有效的做法是询问求解器为什么结果未知。这通常使用如下代码完成：

r = S.check()
if r == sat:
    print(S.model())
elif r == unknown:
    print("Unknown, reason: %s" % S.reason_unknown())
else:
    print("Solver said: %s" % r)

对于你的 Python 程序，我得到：

smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)

这实际上是您目前掌握的唯一信息：如果求解器状态为 unknown，则模型值的任何“提取”都是错误的。

（一个相关的问题也是关于在调用 z3 的优化求解器期间“中断”计算。如果中断求解器，您得到的“模型”不会到目前为止是“最好的”无论如何，它可能满足也可能不满足现有的约束。长话短说，除非求解器报告sat，否则不要指望你得到的模型：z3 在这里做正确的事情，并告诉你没有可行的模型可用。 )