mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fixing issues with user propagator from python

Browse source 
"fresh" remains broken (not working yet).
This commit is contained in:
Nikolaj Bjorner 2021-11-07 17:04:11 -08:00
parent f2fcbc7cb7
commit 3a9656bc59
1 changed files with 24 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
src/api/python/z3/z3.py
View file

@ -11102,33 +11102,34 @@ class PropClosures:
self.bases = {} self.bases = {}
self.lock = None self.lock = None
def set_threaded(): def set_threaded(self):
if self.lock is None: if self.lock is None:
import threading import threading
self.lock = threading.thread.Lock() self.lock = threading.Lock()
def get(self, ctx): def get(self, ctx):
if self.lock: if self.lock:
self.lock.acquire() with self.lock:
r = self.bases[ctx] r = self.bases[ctx]
if self.lock: else:
self.lock.release() r = self.bases[ctx]
return r return r
def set(self, ctx, r): def set(self, ctx, r):
if self.lock: if self.lock:
self.lock.acquire() with self.lock:
self.bases[ctx] = r self.bases[ctx] = r
if self.lock: else:
self.lock.release() self.bases[ctx] = r
def insert(self, r): def insert(self, r):
if self.lock: if self.lock:
self.lock.acquire() with self.lock:
id = len(self.bases) + 3 id = len(self.bases) + 3
self.bases[id] = r self.bases[id] = r
if self.lock: else:
self.lock.release() id = len(self.bases) + 3
self.bases[id] = r
return id return id
@ -11151,8 +11152,9 @@ def user_prop_pop(ctx, num_scopes):
def user_prop_fresh(id, ctx): def user_prop_fresh(id, ctx):
_prop_closures.set_threaded() _prop_closures.set_threaded()
new_prop = UsePropagateBase(None, ctx) prop = _prop_closures.get(id)
_prop_closures.set(new_prop.id, new_prop.fresh()) new_prop = prop.fresh()
_prop_closures.set(new_prop.id, new_prop)
return ctypes.c_void_p(new_prop.id) return ctypes.c_void_p(new_prop.id)
@ -11214,11 +11216,12 @@ class UserPropagateBase:
self.eq = None self.eq = None
self.diseq = None self.diseq = None
if ctx: if ctx:
# TBD fresh is broken: ctx is not of the right type when we reach here.
self._ctx = Context() self._ctx = Context()
Z3_del_context(self._ctx.ctx) #Z3_del_context(self._ctx.ctx)
self._ctx.ctx = ctx #self._ctx.ctx = ctx
self._ctx.eh = Z3_set_error_handler(ctx, z3_error_handler) #self._ctx.eh = Z3_set_error_handler(ctx, z3_error_handler)
Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT) #Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
if s: if s:
Z3_solver_propagate_init(self.ctx_ref(), Z3_solver_propagate_init(self.ctx_ref(),
s.solver, s.solver,