mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

ensure that objects in callback are of sort Ast.

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-03-19 15:34:06 -07:00
parent 3439d2407b
commit bbb27775ed
1 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -11252,35 +11252,38 @@ def user_prop_fresh(id, ctx):
_prop_closures.set(new_prop.id, new_prop)
return ctypes.c_void_p(new_prop.id)
def to_Ast(ptr,):
ast = Ast(ptr)
super(ctypes.c_void_p, ast).__init__(ptr)
return ast
def user_prop_fixed(ctx, cb, id, value):
prop = _prop_closures.get(ctx)
prop.cb = cb
prop.fixed(_to_expr_ref(ctypes.c_void_p(id), prop.ctx()), _to_expr_ref(ctypes.c_void_p(value), prop.ctx()))
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
def user_prop_final(ctx, cb):
prop = _prop_closures.get(ctx)
prop.cb = cb
prop.final()
prop.cb = None
def user_prop_eq(ctx, cb, x, y):
prop = _prop_closures.get(ctx)
prop.cb = cb
x = _to_expr_ref(ctypes.c_void_p(x), prop.ctx())
y = _to_expr_ref(ctypes.c_void_p(y), prop.ctx())
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
def user_prop_diseq(ctx, cb, x, y):
prop = _prop_closures.get(ctx)
prop.cb = cb
x = _to_expr_ref(ctypes.c_void_p(x), prop.ctx())
y = _to_expr_ref(ctypes.c_void_p(y), prop.ctx())
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