0

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

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

sexpr()我使用接口中的方法将断言转换为 smt-lib 格式z3 Solver，即使状态为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 接口获取此模型的任何建议？

model()z3 在调用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

谢谢

4

2 回答 2

0

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

于 2020-09-02T08:04:03.187 回答
0

如果求解器返回，您就不能依赖模型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 在这里做的是正确的事情，并告诉你没有可行的模型可用。）

于 2020-09-02T14:39:41.650 回答