update to take effect of def_API for callback functions

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · May 16, 2022 · f6b2874 · f6b2874
1 parent ca2497e
commit f6b2874
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 22 deletions.
diff --git a/scripts/update_api.py b/scripts/update_api.py
@@ -1881,28 +1881,22 @@ def _to_pystr(s):
 _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)
 
-_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]
+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_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
@@ -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: