1from z3 import * 2from multiprocessing.pool import ThreadPool 3from copy import deepcopy 4 5pool = ThreadPool(8) 6x = Int('x') 7 8assert x.ctx == main_ctx() 9 10 11def calculate(x, n, ctx): 12 """ Do a simple computation with a context""" 13 assert x.ctx == ctx 14 assert x.ctx != main_ctx() 15 16 # Parallel creation of z3 object 17 condition = And(x < 2, x > n, ctx) 18 19 # Parallel solving 20 solver = Solver(ctx=ctx) 21 solver.add(condition) 22 solver.check() 23 24 25for i in range(100): 26 # Create new context for the computation 27 # Note that we need to do this sequentially, as parallel access to the current context or its objects 28 # will result in a segfault 29 i_context = Context() 30 x_i = deepcopy(x).translate(i_context) 31 32 # Kick off parallel computation 33 pool.apply_async(calculate, [x_i, i, i_context]) 34 35pool.close() 36pool.join() 37