我不明白如何在 Z3/Z3py 中使用背景關系。以下示例回傳context mismatch，但如果我將 更改And為 an==或它可以作業，并且如果我從I getImplies的宣告中洗掉背景關系。為什么？我知道在這個簡單的示例中我不需要背景關系，但我需要并行化一個使用 Z3py 的更復雜的腳本。xz3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value
from z3 import *
ctx=Context()
solver=Solver(ctx=ctx)
x=Bool('x',ctx=ctx)
solver.add(And(x,x))
print(solver.check())
Traceback (most recent call last):
File "minimal_test.py", line 6, in <module>
solver.add(And(x,x))
File "[...].local/lib/python3.7/site-packages/z3/z3.py", line 1727, in And
_z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch")
File "[...].local/lib/python3.7/site-packages/z3/z3.py", line 96, in _z3_assert
raise Z3Exception(msg)
z3.z3types.Z3Exception: context mismatch
uj5u.com熱心網友回復：
正如您在問題中給出的那樣，該程式對我來說運行得很好，產生sat. 所以，我不確定你為什么會看到你所看到的，除非你有一個非常舊的 z3 版本，它有一個錯誤或其他東西。（Github master 是 4.11.2；我用的是 4.9.2；你有什么版本？）
如果從 的宣告中洗掉背景關系x，您將得到“z3.z3types.Z3Exception：值無法轉換為 Z3 布林值”，因為它x是在全域背景關系中創建的，但求解器是在特定背景關系中創建的。通常，如果您有多個背景關系，則只需使用該背景關系宣告所有變數。（默認情況下，它們都將使用全域背景關系；當您沒有顯式宣告時，它可以正常作業。）像 // 這樣的函式只需And使用其引數的背景關系來確定在哪個背景關系中創建運算式。OrImplies
因此，您在問題中給出的程式是使用背景關系的正確方法。我不清楚為什么它對你不利；也許你有很多版本的這個程式，不知何故混淆了哪個是哪個？
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/504222.html
下一篇：在多執行緒環境中訪問映射