From 7eaa5562d8a94452e5eaff2a25c5386e77cec723 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Jan 2013 12:51:03 -0800 Subject: [PATCH 1/3] Fix http://z3.codeplex.com/workitem/19 Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/cmd_context/check_logic.cpp | 3 +++ 2 files changed, 5 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index a2257c610..3145d3b62 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -55,6 +55,8 @@ Version 4.3.2 - Fixed bug reported at http://stackoverflow.com/questions/14307692/unknown-when-using-defs +- Relax check_logic procedure. Now, it accepts coercions (to_real) automatically introduced by Z3. (Thanks to Paul Jackson). This is a fix for http://z3.codeplex.com/workitem/19. + Version 4.3.1 ============= diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 820ef59a4..dfee148b5 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -228,6 +228,9 @@ struct check_logic::imp { bool is_int(expr * t) { if (m_a_util.is_uminus(t)) t = to_app(t)->get_arg(0); + // Take care of coercions automatically added by Z3 + if (m_a_util.is_to_real(t)) + t = to_app(t)->get_arg(0); return m_a_util.is_numeral(t); } From 711abc75fbf7d0aaa0516f598663e0e0f176329b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Jan 2013 13:22:28 -0800 Subject: [PATCH 2/3] Fix issue reported at http://z3.codeplex.com/workitem/14 Signed-off-by: Leonardo de Moura --- src/api/api_ast.cpp | 4 ++-- src/api/api_config_params.cpp | 4 ++-- src/api/api_log.cpp | 2 +- src/api/api_numeral.cpp | 38 +++++++++++++++++------------------ src/api/z3_api.h | 6 +++--- 5 files changed, 27 insertions(+), 27 deletions(-) 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. From 6dd4cb832be160128c3143ddcc06224ae47fda70 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Jan 2013 16:42:34 -0800 Subject: [PATCH 3/3] Fix problem reported by Alex Horn Signed-off-by: Leonardo de Moura --- src/api/c++/z3++.h | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 7875e6ef3..5c1e6ca0c 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1644,11 +1644,6 @@ namespace z3 { }; -template class z3::ast_vector_tpl; -template class z3::ast_vector_tpl; -template class z3::ast_vector_tpl; -template class z3::ast_vector_tpl; - /*@}*/ /*@}*/