mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
Implement parallel python example
This commit is contained in:
parent
ad973d5c6d
commit
7d51353b8b
33
examples/python/parallel.py
Normal file
33
examples/python/parallel.py
Normal file
|
@ -0,0 +1,33 @@
|
||||||
|
from z3 import *
|
||||||
|
from multiprocessing.pool import ThreadPool
|
||||||
|
from copy import deepcopy
|
||||||
|
|
||||||
|
pool = ThreadPool(8)
|
||||||
|
x = Int('x')
|
||||||
|
|
||||||
|
assert x.ctx == main_ctx()
|
||||||
|
|
||||||
|
|
||||||
|
def calculate(x, n, ctx):
|
||||||
|
""" Do a simple computation with a context"""
|
||||||
|
assert x.ctx == ctx
|
||||||
|
assert x.ctx != main_ctx()
|
||||||
|
|
||||||
|
condition = And(x < 2, x > n, ctx)
|
||||||
|
solver = Solver(ctx=ctx)
|
||||||
|
solver.add(condition)
|
||||||
|
solver.check()
|
||||||
|
|
||||||
|
|
||||||
|
for i in range(100):
|
||||||
|
# Create new context for the computation
|
||||||
|
# Note that we need to do this sequentially, as parallel access to the current context or its objects
|
||||||
|
# will result in a segfault
|
||||||
|
i_context = Context()
|
||||||
|
x_i = deepcopy(x).translate(i_context)
|
||||||
|
|
||||||
|
# Kick off parallel computation
|
||||||
|
pool.apply_async(calculate, [x_i, i, i_context])
|
||||||
|
|
||||||
|
pool.close()
|
||||||
|
pool.join()
|
Loading…
Reference in a new issue