From 7d51353b8b097a22b0278cb50006c6b4ff5e0fe1 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Sat, 19 May 2018 11:13:53 +0200 Subject: [PATCH 1/2] Implement parallel python example --- examples/python/parallel.py | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 examples/python/parallel.py diff --git a/examples/python/parallel.py b/examples/python/parallel.py new file mode 100644 index 000000000..7903f58c9 --- /dev/null +++ b/examples/python/parallel.py @@ -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() From e32dfad81e7fc14816c034d1a527975d0cc97138 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Sat, 19 May 2018 11:16:20 +0200 Subject: [PATCH 2/2] Add comments --- examples/python/parallel.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/examples/python/parallel.py b/examples/python/parallel.py index 7903f58c9..42ff50927 100644 --- a/examples/python/parallel.py +++ b/examples/python/parallel.py @@ -13,7 +13,10 @@ def calculate(x, n, ctx): assert x.ctx == ctx assert x.ctx != main_ctx() + # Parallel creation of z3 object condition = And(x < 2, x > n, ctx) + + # Parallel solving solver = Solver(ctx=ctx) solver.add(condition) solver.check()