From f6b2874d7ce951a0771c504f6ea7c4894342dfb2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 May 2022 10:30:54 -0700 Subject: [PATCH] update to take effect of def_API for callback functions Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 24 +++++++++--------------- src/api/python/z3/z3.py | 14 +++++++------- 2 files changed, 16 insertions(+), 22 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 0553843cb..6fb4fee53 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1881,28 +1881,22 @@ _error_handler_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint) _lib.Z3_set_error_handler.restype = None _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type] -push_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p) -pop_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint) -fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) +Z3_push_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p) +Z3_pop_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint) +Z3_fresh_eh = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) -fixed_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) -final_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p) -eq_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) +Z3_fixed_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) +Z3_final_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p) +Z3_eq_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) + +Z3_created_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) +Z3_decide_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) _lib.Z3_solver_propagate_init.restype = None -_lib.Z3_solver_propagate_init.argtypes = [ContextObj, SolverObj, ctypes.c_void_p, push_eh_type, pop_eh_type, fresh_eh_type] - _lib.Z3_solver_propagate_final.restype = None -_lib.Z3_solver_propagate_final.argtypes = [ContextObj, SolverObj, final_eh_type] - _lib.Z3_solver_propagate_fixed.restype = None -_lib.Z3_solver_propagate_fixed.argtypes = [ContextObj, SolverObj, fixed_eh_type] - _lib.Z3_solver_propagate_eq.restype = None -_lib.Z3_solver_propagate_eq.argtypes = [ContextObj, SolverObj, eq_eh_type] - _lib.Z3_solver_propagate_diseq.restype = None -_lib.Z3_solver_propagate_diseq.argtypes = [ContextObj, SolverObj, eq_eh_type] on_model_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p) _lib.Z3_optimize_register_model_eh.restype = None diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 69959d181..c45a3d86e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11330,13 +11330,13 @@ def user_prop_diseq(ctx, cb, x, y): prop.cb = None -_user_prop_push = push_eh_type(user_prop_push) -_user_prop_pop = pop_eh_type(user_prop_pop) -_user_prop_fresh = fresh_eh_type(user_prop_fresh) -_user_prop_fixed = fixed_eh_type(user_prop_fixed) -_user_prop_final = final_eh_type(user_prop_final) -_user_prop_eq = eq_eh_type(user_prop_eq) -_user_prop_diseq = eq_eh_type(user_prop_diseq) +_user_prop_push = Z3_push_eh(user_prop_push) +_user_prop_pop = Z3_pop_eh(user_prop_pop) +_user_prop_fresh = Z3_fresh_eh(user_prop_fresh) +_user_prop_fixed = Z3_fixed_eh(user_prop_fixed) +_user_prop_final = Z3_final_eh(user_prop_final) +_user_prop_eq = Z3_eq_eh(user_prop_eq) +_user_prop_diseq = Z3_eq_eh(user_prop_diseq) class UserPropagateBase: