mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 07:53:15 +00:00
Code Activity

initial warppers for seq-map/seq-fold

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-09 14:52:49 -07:00
parent f9176fb4b7
commit fc6c4c98e2
5 changed files with 67 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/api/api_util.h
View file

@ -160,6 +160,23 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) { \
MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE); \
}
#define MK_FOURARY_BODY(NAME, FID, OP, EXTRA_CODE) \
Z3_TRY; \
RESET_ERROR_CODE(); \
EXTRA_CODE; \
expr * args[4] = { to_expr(n1), to_expr(n2), to_expr(n3), to_expr(n4) }; \
ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 4, args); \
mk_c(c)->save_ast_trail(a); \
check_sorts(c, a); \
RETURN_Z3(of_ast(a)); \
Z3_CATCH_RETURN(0);
#define MK_FOURARY(NAME, FID, OP, EXTRA_CODE) \
Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_ast n3, Z3_ast n4) { \
LOG_ ## NAME(c, n1, n2, n3, n4); \
MK_FOURARY_BODY(NAME, FID, OP, EXTRA_CODE); \
}
#define MK_NARY(NAME, FID, OP, EXTRA_CODE) \
Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \
Z3_TRY; \