這是引發(fā)異常的代碼。import z3solver = 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 OKz3_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 unsatNot(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異常的原因是什么？我的環(huán)境如下。macOS 10.13.2Z3 版本 4.8.0 - 64 位（由 brew 安裝）Python 3.6.7（由 pyenv 安裝）點(diǎn)Z3 0.2.0pip z3-solver 4.8.0.0
1 回答
一只萌萌小番薯
TA貢獻(xiàn)1795條經(jīng)驗(yàn) 獲得超7個(gè)贊
對我來說運(yùn)行得很好：
$ python a.py
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)))))
('CHECK', sat)
我也在 Mac 上，我有：
$ z3 --version
Z3 version 4.8.3 - 64 bit
我懷疑您的安裝以某種方式被破壞了。從頭開始重新安裝可能會(huì)解決問題。
添加回答
舉報(bào)
0/150
提交
取消