diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 404d9d9ac..81a716b12 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -38,6 +38,8 @@ Revision History: #include"scoped_timer.h" #include"pp_params.hpp" +extern bool is_numeral_sort(Z3_context c, Z3_sort ty); + extern "C" { Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i) { @@ -313,8 +315,6 @@ extern "C" { Z3_CATCH_RETURN(""); } - extern bool is_numeral_sort(Z3_context c, Z3_sort ty); - Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a) { Z3_TRY; LOG_Z3_get_ast_kind(c, a); diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index aaaabb7b2..48c2df4a9 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -43,7 +43,7 @@ extern "C" { } } - void Z3_API Z3_global_param_reset_all() { + void Z3_API Z3_global_param_reset_all(void) { memory::initialize(UINT_MAX); LOG_Z3_global_param_reset_all(); gparams::reset(); @@ -71,7 +71,7 @@ extern "C" { } } - Z3_config Z3_API Z3_mk_config() { + Z3_config Z3_API Z3_mk_config(void) { memory::initialize(UINT_MAX); LOG_Z3_mk_config(); Z3_config r = reinterpret_cast(alloc(context_params)); diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index 84c262a96..4a1ae27e5 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -44,7 +44,7 @@ extern "C" { _Z3_append_log(static_cast(str)); } - void Z3_API Z3_close_log() { + void Z3_API Z3_close_log(void) { if (g_z3_log != 0) { dealloc(g_z3_log); g_z3_log_enabled = false; diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 2660d9a01..d4a6587bc 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -24,27 +24,27 @@ Revision History: #include"bv_decl_plugin.h" #include"algebraic_numbers.h" +bool is_numeral_sort(Z3_context c, Z3_sort ty) { + sort * _ty = to_sort(ty); + family_id fid = _ty->get_family_id(); + if (fid != mk_c(c)->get_arith_fid() && + fid != mk_c(c)->get_bv_fid() && + fid != mk_c(c)->get_datalog_fid()) { + return false; + } + return true; +} + +bool check_numeral_sort(Z3_context c, Z3_sort ty) { + bool is_num = is_numeral_sort(c, ty); + if (!is_num) { + SET_ERROR_CODE(Z3_INVALID_ARG); + } + return is_num; +} + extern "C" { - bool is_numeral_sort(Z3_context c, Z3_sort ty) { - sort * _ty = to_sort(ty); - family_id fid = _ty->get_family_id(); - if (fid != mk_c(c)->get_arith_fid() && - fid != mk_c(c)->get_bv_fid() && - fid != mk_c(c)->get_datalog_fid()) { - return false; - } - return true; - } - - bool check_numeral_sort(Z3_context c, Z3_sort ty) { - bool is_num = is_numeral_sort(c, ty); - if (!is_num) { - SET_ERROR_CODE(Z3_INVALID_ARG); - } - return is_num; - } - Z3_ast Z3_API Z3_mk_numeral(Z3_context c, const char* n, Z3_sort ty) { Z3_TRY; LOG_Z3_mk_numeral(c, n, ty); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 410945235..ea3b05e40 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1274,7 +1274,7 @@ extern "C" { def_API('Z3_global_param_reset_all', VOID, ()) */ - void Z3_API Z3_global_param_reset_all(); + void Z3_API Z3_global_param_reset_all(void); /** \brief Get a global (or module) parameter. @@ -1335,7 +1335,7 @@ extern "C" { def_API('Z3_mk_config', CONFIG, ()) */ - Z3_config Z3_API Z3_mk_config(); + Z3_config Z3_API Z3_mk_config(void); /** \brief Delete the given configuration object. @@ -4765,7 +4765,7 @@ END_MLAPI_EXCLUDE extra_API('Z3_close_log', VOID, ()) */ - void Z3_API Z3_close_log(); + void Z3_API Z3_close_log(void); /** \brief Enable/disable printing warning messages to the console.