查询:当Z3返回未知状态时，我们可以使用z3 Python获得部分模型吗？
我很确定这与python有关。是否有一种方法可以从z3获得部分模型，即使状态为unknown
我试图从z3中获取一个模型，即使状态返回unknown结果。它在为exception引发model not available时失败。有什么建议可以做吗？
我使用sexpr()方法从z3 Solver接口将断言转换为smt格式，即使状态为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谢谢
回答 2
Stack Overflow用户
发布于 2020-09-02 14:39:41
如果求解器返回unknown，则不能依赖该模型。也就是说，您得到的模型无论如何都不是“部分的”：它可能满足或可能不满足某些约束，但否则，您就没有什么办法了。它充其量是求解者内部状态的表示。但总的来说，它不一定是任何事物的代表。
此外，当我使用SMTLib运行您的z3脚本时，我得到：
unknown
(error "line 21 column 10: model is not available")大约一周前，我从他们的集线器主人那里建立了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在这里做了正确的事情，告诉你没有可行的模型。)
Stack Overflow用户
发布于 2020-09-02 08:04:03
除了上面提到的那个之外，我还没有找到其他的选择。
https://stackoverflow.com/questions/63701223
复制相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号