如何使用Python中的螺纹模块使用Z3-Solver？

Question

我正在解决一个SAT问题，首先，我创建了约束列表。这些约束与彼此无关，因此我可以并行处理。我正在使用下面的代码进行此操作（但是，此代码在此处进行了简化，因此可以更好地理解问题。）：

from z3 import *
from threading import Thread

def test():
    And(Bool('x'), Bool('y'))

for i in range(20):
    Thread(target=test).start()

要重现 error ，请记住，您可以安装 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崩溃并停止工作。例如，如果您使用木星，则必须重新启动内核才能继续工作。

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

Answer 1

每个Z3表达式都是在给定上下文中创建的，只有在属于同一上下文的情况下，您只能将它们一起操纵。如果不这样做，您将获得“上下文不匹配”错误，这本质上是您无法从中恢复的错误，这导致了崩溃。

Z3的多线程用途确实是可能的，但是如果您需要合作，您必须仔细操纵上下文并将它们“转换”到彼此。大多数Z3 API函数仅使用全局上下文，这使这更加复杂，因此很容易将其作为程序员弄错。但是，其中大多数还允许您通过上下文使用；这就是您需要在这里做的。

有关此问题，请参见多线程Z3？有关此问题的更详细讨论。长话短说，您需要明确跟踪和操纵环境；如果您在不同的线程中，请确保永远不要混合并匹配它们。