Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

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
 =============
 

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);

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<Z3_config>(alloc(context_params));

src/api/api_log.cpp

@@ -44,7 +44,7 @@ extern "C" {
         _Z3_append_log(static_cast<char const *>(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;

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);

src/api/c++/z3++.h

@@ -1644,11 +1644,6 @@ namespace z3 {
 
 };
 
-template class z3::ast_vector_tpl<z3::ast>;
-template class z3::ast_vector_tpl<z3::expr>;
-template class z3::ast_vector_tpl<z3::sort>;
-template class z3::ast_vector_tpl<z3::func_decl>;
-
 /*@}*/
 /*@}*/
 

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.

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);
     }