mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

allow callbacks to be nested

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-02-13 20:30:17 +07:00
parent 53f89a81c1
commit f1d97c7a3a
1 changed files with 14 additions and 7 deletions

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

@ -11570,47 +11570,54 @@ def user_prop_fresh(ctx, _new_ctx):
def user_prop_fixed(ctx, cb, id, value):
prop = _prop_closures.get(ctx)
prop.cb = cb
old_cb = prop.cb
prop.cb = cb
id = _to_expr_ref(to_Ast(id), prop.ctx())
value = _to_expr_ref(to_Ast(value), prop.ctx())
prop.fixed(id, value)
prop.cb = None
prop.cb = old_cb
def user_prop_created(ctx, cb, id):
prop = _prop_closures.get(ctx)
old_cb = prop.cb
prop.cb = cb
id = _to_expr_ref(to_Ast(id), prop.ctx())
prop.created(id)
prop.cb = None
prop.cb = old_cb
def user_prop_final(ctx, cb):
prop = _prop_closures.get(ctx)
old_cb = prop.cb
prop.cb = cb
prop.final()
prop.cb = None
prop.cb = old_cb
def user_prop_eq(ctx, cb, x, y):
prop = _prop_closures.get(ctx)
old_cb = prop.cb
prop.cb = cb
x = _to_expr_ref(to_Ast(x), prop.ctx())
y = _to_expr_ref(to_Ast(y), prop.ctx())
prop.eq(x, y)
prop.cb = None
prop.cb = old_cb
def user_prop_diseq(ctx, cb, x, y):
prop = _prop_closures.get(ctx)
old_cb = prop.cb
prop.cb = cb
x = _to_expr_ref(to_Ast(x), prop.ctx())
y = _to_expr_ref(to_Ast(y), prop.ctx())
prop.diseq(x, y)
prop.cb = None
prop.cb = old_cb
def user_prop_decide(ctx, cb, t, idx, phase):
prop = _prop_closures.get(ctx)
old_cb = prop.cb
prop.cb = cb
t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
prop.decide(t, idx, phase)
prop.cb = None
prop.cb = old_cb
_user_prop_push = Z3_push_eh(user_prop_push)