1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 api_util.h
7
8 Abstract:
9 Goodies used to build the Z3 external API.
10
11 Author:
12
13 Leonardo de Moura (leonardo) 2012-02-29.
14
15 Revision History:
16
17 --*/
18 #pragma once
19
20 #include "util/params.h"
21 #include "util/lbool.h"
22 #include "ast/ast.h"
23
24 #define Z3_TRY try {
25 #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }
26 #define Z3_CATCH Z3_CATCH_CORE(return;)
27 #define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;)
28 #define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; }
29
30 #define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
31
32 namespace api {
33 class context;
34
35 // Generic wrapper for ref-count objects exposed by the API
36 class object {
37 unsigned m_ref_count;
38 unsigned m_id;
39 context& m_context;
40 public:
41 object(context& c);
~object()42 virtual ~object() {}
ref_count()43 unsigned ref_count() const { return m_ref_count; }
id()44 unsigned id() const { return m_id; }
45 void inc_ref();
46 void dec_ref();
47 };
48 };
49
to_ast(Z3_ast a)50 inline ast * to_ast(Z3_ast a) { return reinterpret_cast<ast *>(a); }
of_ast(ast * a)51 inline Z3_ast of_ast(ast* a) { return reinterpret_cast<Z3_ast>(a); }
52
to_expr(Z3_ast a)53 inline expr * to_expr(Z3_ast a) { return reinterpret_cast<expr*>(a); }
of_expr(expr * e)54 inline Z3_ast of_expr(expr* e) { return reinterpret_cast<Z3_ast>(e); }
55
to_exprs(unsigned n,Z3_ast const * a)56 inline expr * const * to_exprs(unsigned n, Z3_ast const* a) { return reinterpret_cast<expr* const*>(a); }
of_exprs(expr * const * e)57 inline Z3_ast * const * of_exprs(expr* const* e) { return reinterpret_cast<Z3_ast* const*>(e); }
58
to_app(Z3_app a)59 inline app * to_app(Z3_app a) { return reinterpret_cast<app*>(a); }
to_app(Z3_ast a)60 inline app * to_app(Z3_ast a) { return reinterpret_cast<app*>(a); }
of_app(app * a)61 inline Z3_app of_app(app* a) { return reinterpret_cast<Z3_app>(a); }
62
to_apps(Z3_ast const * a)63 inline app * const* to_apps(Z3_ast const* a) { return reinterpret_cast<app * const*>(a); }
64
to_asts(Z3_ast const * a)65 inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast<ast* const*>(a); }
66
to_sort(Z3_sort a)67 inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); }
of_sort(sort * s)68 inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); }
69
to_sorts(Z3_sort const * a)70 inline sort * const * to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); }
of_sorts(sort * const * s)71 inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }
72
to_func_decl(Z3_func_decl a)73 inline func_decl * to_func_decl(Z3_func_decl a) { return reinterpret_cast<func_decl*>(a); }
of_func_decl(func_decl * f)74 inline Z3_func_decl of_func_decl(func_decl* f) { return reinterpret_cast<Z3_func_decl>(f); }
75
to_func_decls(Z3_func_decl const * f)76 inline func_decl * const * to_func_decls(Z3_func_decl const* f) { return reinterpret_cast<func_decl*const*>(f); }
77
to_symbol(Z3_symbol s)78 inline symbol to_symbol(Z3_symbol s) { return symbol::c_api_ext2symbol(s); }
of_symbol(symbol s)79 inline Z3_symbol of_symbol(symbol s) { return static_cast<Z3_symbol>(s.c_api_symbol2ext()); }
80
of_pattern(ast * a)81 inline Z3_pattern of_pattern(ast* a) { return reinterpret_cast<Z3_pattern>(a); }
to_pattern(Z3_pattern p)82 inline app* to_pattern(Z3_pattern p) { return reinterpret_cast<app*>(p); }
83
of_lbool(lbool b)84 inline Z3_lbool of_lbool(lbool b) { return static_cast<Z3_lbool>(b); }
to_lbool(Z3_lbool b)85 inline lbool to_lbool(Z3_lbool b) { return static_cast<lbool>(b); }
86
87 struct Z3_params_ref : public api::object {
88 params_ref m_params;
Z3_params_refZ3_params_ref89 Z3_params_ref(api::context& c): api::object(c) {}
~Z3_params_refZ3_params_ref90 ~Z3_params_ref() override {}
91 };
92
to_params(Z3_params p)93 inline Z3_params_ref * to_params(Z3_params p) { return reinterpret_cast<Z3_params_ref *>(p); }
of_params(Z3_params_ref * p)94 inline Z3_params of_params(Z3_params_ref * p) { return reinterpret_cast<Z3_params>(p); }
to_param_ref(Z3_params p)95 inline params_ref& to_param_ref(Z3_params p) { return p == nullptr ? const_cast<params_ref&>(params_ref::get_empty()) : to_params(p)->m_params; }
96
97 struct Z3_param_descrs_ref : public api::object {
98 param_descrs m_descrs;
Z3_param_descrs_refZ3_param_descrs_ref99 Z3_param_descrs_ref(api::context& c): api::object(c) {}
~Z3_param_descrs_refZ3_param_descrs_ref100 ~Z3_param_descrs_ref() override {}
101 };
102
to_param_descrs(Z3_param_descrs p)103 inline Z3_param_descrs_ref * to_param_descrs(Z3_param_descrs p) { return reinterpret_cast<Z3_param_descrs_ref *>(p); }
of_param_descrs(Z3_param_descrs_ref * p)104 inline Z3_param_descrs of_param_descrs(Z3_param_descrs_ref * p) { return reinterpret_cast<Z3_param_descrs>(p); }
to_param_descrs_ptr(Z3_param_descrs p)105 inline param_descrs * to_param_descrs_ptr(Z3_param_descrs p) { return p == nullptr ? nullptr : &(to_param_descrs(p)->m_descrs); }
106
107
108 #define SKIP ((void) 0)
109
110 #define MK_UNARY_BODY(NAME, FID, OP, EXTRA_CODE) \
111 Z3_TRY; \
112 RESET_ERROR_CODE(); \
113 EXTRA_CODE; \
114 expr * _n = to_expr(n); \
115 ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 1, &_n); \
116 mk_c(c)->save_ast_trail(a); \
117 check_sorts(c, a); \
118 RETURN_Z3(of_ast(a)); \
119 Z3_CATCH_RETURN(0);
120
121 #define MK_UNARY(NAME, FID, OP, EXTRA_CODE) \
122 Z3_ast Z3_API NAME(Z3_context c, Z3_ast n) { \
123 LOG_ ## NAME(c, n); \
124 MK_UNARY_BODY(NAME, FID, OP, EXTRA_CODE); \
125 }
126
127 #define MK_BINARY_BODY(NAME, FID, OP, EXTRA_CODE) \
128 Z3_TRY; \
129 RESET_ERROR_CODE(); \
130 EXTRA_CODE; \
131 expr * args[2] = { to_expr(n1), to_expr(n2) }; \
132 ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 2, args); \
133 mk_c(c)->save_ast_trail(a); \
134 check_sorts(c, a); \
135 RETURN_Z3(of_ast(a)); \
136 Z3_CATCH_RETURN(0);
137
138 #define MK_BINARY(NAME, FID, OP, EXTRA_CODE) \
139 Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) { \
140 LOG_ ## NAME(c, n1, n2); \
141 MK_BINARY_BODY(NAME, FID, OP, EXTRA_CODE); \
142 }
143
144 #define MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE) \
145 Z3_TRY; \
146 RESET_ERROR_CODE(); \
147 EXTRA_CODE; \
148 expr * args[3] = { to_expr(n1), to_expr(n2), to_expr(n3) }; \
149 ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 3, args); \
150 mk_c(c)->save_ast_trail(a); \
151 check_sorts(c, a); \
152 RETURN_Z3(of_ast(a)); \
153 Z3_CATCH_RETURN(0);
154
155 #define MK_TERNARY(NAME, FID, OP, EXTRA_CODE) \
156 Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_ast n3) { \
157 LOG_ ## NAME(c, n1, n2, n3); \
158 MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE); \
159 }
160
161 #define MK_NARY(NAME, FID, OP, EXTRA_CODE) \
162 Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \
163 Z3_TRY; \
164 LOG_ ## NAME(c, num_args, args); \
165 RESET_ERROR_CODE(); \
166 EXTRA_CODE; \
167 ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, num_args, to_exprs(num_args, args)); \
168 mk_c(c)->save_ast_trail(a); \
169 check_sorts(c, a); \
170 RETURN_Z3(of_ast(a)); \
171 Z3_CATCH_RETURN(0); \
172 }
173
174