diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 24d7f80dd..95cf94e6e 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -225,13 +225,15 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fresh_func_decl(c, prefix, domain_size, domain, range); RESET_ERROR_CODE(); + CHECK_IS_SORT(range, nullptr); + CHECK_SORTS(domain_size, domain, nullptr); if (prefix == nullptr) { prefix = ""; } func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix, domain_size, - reinterpret_cast(domain), + to_sorts(domain), to_sort(range), false); mk_c(c)->save_ast_trail(d); @@ -243,9 +245,11 @@ extern "C" { Z3_TRY; LOG_Z3_mk_fresh_const(c, prefix, ty); RESET_ERROR_CODE(); + CHECK_IS_SORT(ty, nullptr); if (prefix == nullptr) { prefix = ""; } + app* a = mk_c(c)->m().mk_fresh_const(prefix, to_sort(ty), false); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_ast(a)); @@ -654,6 +658,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_sort_name(c, t); RESET_ERROR_CODE(); + CHECK_IS_SORT(t, of_symbol(symbol::null)); CHECK_VALID_AST(t, of_symbol(symbol::null)); return of_symbol(to_sort(t)->get_name()); Z3_CATCH_RETURN(of_symbol(symbol::null)); diff --git a/src/api/api_context.h b/src/api/api_context.h index c17c0089b..a5e3d844d 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -286,10 +286,13 @@ namespace api { inline api::context * mk_c(Z3_context c) { return reinterpret_cast(c); } #define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); } #define SET_ERROR_CODE(ERR, MSG) { mk_c(c)->set_error_code(ERR, MSG); } -#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == 0) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } } -#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } } +#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == nullptr) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } } +#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } } inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); } -#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } } +#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == nullptr || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } } +#define CHECK_IS_SORT(_p_, _ret_) { if (_p_ == nullptr || !is_sort(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } } +#define CHECK_SORTS(_n_, _ps_, _ret_) { for (unsigned i = 0; i < _n_; ++i) if (!is_sort(_ps_[i])) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } } + inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); } -#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } } +#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } } inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); } diff --git a/src/api/api_util.h b/src/api/api_util.h index e02ac6fee..ee38c4f27 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -67,6 +67,7 @@ inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast(a); } inline Z3_sort of_sort(sort* s) { return reinterpret_cast(s); } +inline bool is_sort(Z3_sort a) { return is_sort(to_sort(a)); } inline sort * const * to_sorts(Z3_sort const* a) { return reinterpret_cast(a); } inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast(s); }