这是引发异常的代码。
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
一只萌萌小番薯
相关分类