无法验证:!m_var2expr.empty() 在 z3 python 上

这是引发异常的代码。


import z3

solver = z3.Solver()

v1, v2, v3, v4 = [z3.Bool("v{}".format(i)) for i in range(1,5)]

z3_prop1 = z3.And(z3.Or(z3.Or(z3.Not(z3.And(v1,v2)), z3.And(False, v3)),

       z3.And(z3.And(False, v2), z3.Or(z3.Not(False), v1))),

    z3.And(z3.And(z3.And(v3, v2), z3.And(v4, v1)),

        z3.Or(z3.Or(v2, v3), z3.And(v4, False))))

print(z3_prop1)

solver.reset()

solver.add(z3_prop1)

print("CHECK", solver.check()) # z3_prop1 is OK

z3_prop2 = z3.Not(z3_prop1)

solver.reset()

print(z3_prop2)

solver.add(z3_prop2)

print("CHECK", solver.check()) # z3_prop2 throws Error

这是代码的输出。


And(Or(Or(Not(And(v1, v2)), And(False, v3)),

   And(And(False, v2), Or(Not(False), v1))),

And(And(And(v3, v2), And(v4, v1)),

    Or(Or(v2, v3), And(v4, False))))

CHECK unsat

Not(And(Or(Or(Not(And(v1, v2)), And(False, v3)),

       And(And(False, v2), Or(Not(False), v1))),

    And(And(And(v3, v2), And(v4, v1)),

        Or(Or(v2, v3), And(v4, False)))))

Failed to verify: !m_var2expr.empty()

libc++abi.dylib: terminating with uncaught foreign exception

[1]    10607 abort      python -m src.z3_solver

异常的原因是什么?

我的环境如下。

  • macOS 10.13.2

  • Z3 版本 4.8.0 - 64 位(由 brew 安装)

  • Python 3.6.7(由 pyenv 安装)

  • 点Z3 0.2.0

  • pip z3-solver 4.8.0.0


catspeake
浏览 173回答 1
1回答

一只萌萌小番薯

对我来说运行得很好:$ python a.pyAnd(Or(Or(Not(And(v1, v2)), And(False, v3)),       And(And(False, v2), Or(Not(False), v1))),    And(And(And(v3, v2), And(v4, v1)),        Or(Or(v2, v3), And(v4, False))))('CHECK', unsat)Not(And(Or(Or(Not(And(v1, v2)), And(False, v3)),           And(And(False, v2), Or(Not(False), v1))),        And(And(And(v3, v2), And(v4, v1)),            Or(Or(v2, v3), And(v4, False)))))('CHECK', sat)我也在 Mac 上,我有:$ z3 --versionZ3 version 4.8.3 - 64 bit我怀疑您的安装以某种方式被破坏了。从头开始重新安装可能会解决问题。
打开App,查看更多内容
随时随地看视频慕课网APP

相关分类

Python