Python Z3 API查询：当求解程序返回未知状态时，我们可以使用z3 python API获得部分模型吗？

编程问答 2022-08-12

问题描述

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

即使状态返回unkNown结果，我仍试图从z3中获取模型。无法为exception筹集model not available。有什么建议可以做什么？

我从sexpr()接口使用z3 Solver方法将断言转换为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

谢谢

解决方法

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

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

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

大约一周前，我已经从他们的github管理员那里构建了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在这里做正确的事，并告诉您没有可行的模型可用。）

pythonsmtz3z3-fixedpointz3py