From 2bcc8140319ab632028dd5517e9e52bd3f7477dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Jan 2022 02:47:39 -0800 Subject: [PATCH] add macro to track closures declared in z3_api This is to ease integration with external API wrappers that rely on accessing information about type names that are used. #5762 --- src/api/z3_api.h | 17 ++++++++--------- src/api/z3_macros.h | 4 ++++ 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 16b22a991..d7a21ce20 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1423,19 +1423,18 @@ typedef enum /** \brief Z3 custom error handler (See #Z3_set_error_handler). */ -typedef void Z3_error_handler(Z3_context c, Z3_error_code e); - +Z3_DECLARE_CLOSURE(Z3_error_handler, void, (Z3_context c, Z3_error_code e)); /** \brief callback functions for user propagator. */ -typedef void Z3_push_eh(void* ctx); -typedef void Z3_pop_eh(void* ctx, unsigned num_scopes); -typedef void* Z3_fresh_eh(void* ctx, Z3_context new_context); -typedef void Z3_fixed_eh(void* ctx, Z3_solver_callback cb, unsigned id, Z3_ast value); -typedef void Z3_eq_eh(void* ctx, Z3_solver_callback cb, unsigned x, unsigned y); -typedef void Z3_final_eh(void* ctx, Z3_solver_callback cb); -typedef void Z3_created_eh(void* ctx, Z3_solver_callback cb, Z3_ast e, unsigned id); +Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx)); +Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, unsigned num_scopes)); +Z3_DECLARE_CLOSURE(Z3_fresh_eh, void*, (void* ctx, Z3_context new_context)); +Z3_DECLARE_CLOSURE(Z3_fixed_eh, void, (void* ctx, Z3_solver_callback cb, unsigned id, Z3_ast value)); +Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, unsigned x, unsigned y)); +Z3_DECLARE_CLOSURE(Z3_final_eh, void, (void* ctx, Z3_solver_callback cb)); +Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast e, unsigned id)); /** diff --git a/src/api/z3_macros.h b/src/api/z3_macros.h index d42eb508a..08756cf15 100644 --- a/src/api/z3_macros.h +++ b/src/api/z3_macros.h @@ -16,3 +16,7 @@ Copyright (c) 2015 Microsoft Corporation #ifndef DEFINE_TYPE #define DEFINE_TYPE(T) typedef struct _ ## T *T #endif + +#ifndef Z3_DECLARE_CLOSURE +#define Z3_DECLARE_CLOSURE(_NAME_,_RETURN_,_ARGS_) typedef _RETURN_ _NAME_ _ARGS_ +#endif