我正在解決一個 SAT 問題，首先，我創建一個約束串列。這些約束彼此不相關，因此我可以將它們并行化。我正在使用下面的代碼來執行此操作（但是，此代碼在此處進行了簡化，因此可以更好地理解問題。）：
from z3 import *
from threading import Thread
def test():
And(Bool('x'), Bool('y'))
for i in range(20):
Thread(target=test).start()
要重現錯誤，請記住您可以使用以下代碼安裝z3模塊：
pip install z3-solver
這是我面臨的錯誤：
Exception in thread Exception in thread Exception in thread Thread-8:
Traceback (most recent call last):
File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
Thread-25:
Traceback (most recent call last):
File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
Thread-18:
Traceback (most recent call last):
File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
Exception in thread self.run()
File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 910, in run
self.run() self._target(*self._args, **self._kwargs)Thread-20self.run()
File "/var/folders/0b/4x6686_n1n19cgncddmh0zym0000gn/T/ipykernel_40113/248907556.py", line 5, in test
:
Traceback (most recent call last):
File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 910, in run
File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 910, in run
Exception in thread Thread-23 :
self._target(*self._args, **self._kwargs)
File "/var/folders/0b/4x6686_n1n19cgncddmh0zym0000gn/T/ipykernel_40113/248907556.py", line 5, in test
self._target(*self._args, **self._kwargs)
File "/var/folders/0b/4x6686_n1n19cgncddmh0zym0000gn/T/ipykernel_40113/248907556.py", line 5, in test
Traceback (most recent call last):
File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 1856, in And
File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 1856, in And
File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 1856, in And
self.run()ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 499, in _ctx_from_ast_arg_list
ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 499, in _ctx_from_ast_arg_list
_z3_assert(ctx == a.ctx, "Context mismatch")
File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 107, in _z3_assert
raise Z3Exception(msg)
z3.z3types.Z3Exception: Context mismatch
顯示此錯誤后，python 崩潰并停止作業。例如，如果您使用 Jupiter，則必須重新啟動內核才能繼續作業。
python version : 3.9.7 (default, Sep 16 2021, 08:50:36) \n[Clang 10.0.0 ]
OS: MacOS monterey version: 12.2.1
z3 version: 4.8.17.0
uj5u.com熱心網友回復：
每個 z3 運算式都是在給定的背景關系中創建的，如果它們屬于同一背景關系，您只能一起操作運算式。如果你不這樣做，你會得到“背景關系不匹配”錯誤，這本質上是一個你無法恢復的錯誤，這會導致崩潰。
z3 的多執行緒使用確實是可能的，但是如果您需要它們合作，您必須小心地操作背景關系并將它們“翻譯”到彼此。由于大多數 z3 API 函式僅使用全域背景關系這一事實，這使情況變得更加復雜，因此作為程式員很容易出錯。但是，它們中的大多數還允許您傳遞背景關系來使用；這就是你需要在這里做的。
看到多執行緒 Z3？有關此問題的更詳細討論。長話短說，您需要明確地跟蹤和操作背景關系；如果您在不同的執行緒中，請確保永遠不要混合搭配它們。
轉載請註明出處，本文鏈接：https://www.uj5u.com/gongcheng/486660.html
標籤：Python python-3.x 多线程 z3 smt