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

Question

I am solving an SAT problem in which first, I create a list of constraints. These constraints are not related to each other so I can parallelise them. I am using the code below to do so (however, this code is simplified here, so the problem is better understood.):

from z3 import *
from threading import Thread

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

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

to reproduce the error, keep in mind you can install the z3 module using the following code:

pip install z3-solver

And this is the error I'm facing:

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

After showing this error, python crashes and stops working. For example, if you use Jupiter, you have to restart the kernel to continue working.

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

alias · Accepted Answer · 2022-06-02T03:04:09.713

Each z3 expression is created in a given context, and you can only manipulate expressions together if they belong to the same context. If you don't, you'll get the "Context Mismatch" error, which is essentially an error you cannot recover from, which leads to the crash.

Multithreaded uses of z3 is indeed possible, but you have to carefully manipulate contexts and "translate" them to each other if you need them to cooperate. This is further complicated by the fact most z3 API functions simply use the global context, and thus it is easy to get this wrong as a programmer. However, most of them also allow you to pass the context to use; which is what you need to do here.

See Multi-threaded Z3? for a more detailed discussion of this issue. Long story short, you need to keep track of and manipulate contexts explicitly; making sure to never mix-and-match them if you are in different threads.

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

1 Answers1