如何在 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()

要重现错误，请记住您可以使用以下代码安装 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

Answer 1

每个 z3 表达式都是在给定的上下文中创建的，只有属于同一上下文的表达式才能一起操作。如果不这样做，您将收到“上下文不匹配”错误，这实际上是一个您无法从中恢复的错误，它会导致崩溃。

z3 的多线程使用确实是可能的，但是如果需要它们协作，您必须小心操作上下文并将它们相互“翻译”。由于大多数 z3 API 函数只使用全局上下文，这使情况变得更加复杂，因此作为程序员很容易犯错。但是，它们中的大多数还允许您传递上下文以供使用；这就是你需要在这里做的。

有关此问题的更详细讨论，请参阅 Multi-threaded Z3?。长话短说，您需要明确地跟踪和操作上下文；如果您在不同的线程中，请确保永远不要 mix-and-match 它们。

如何在 python 中使用线程模块使用 z3-solver？

How to use z3-solver using threading module in python?

python

python-3.x

multithreading

z3

smt