From 7d51353b8b097a22b0278cb50006c6b4ff5e0fe1 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sat, 19 May 2018 11:13:53 +0200
Subject: [PATCH] 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()