Make the C-layer of Z3's OCaml bindings compatible with C89 (for older Visual Studio builds)

scripts/mk_unix_dist.py

@@ -58,7 +58,7 @@ def display_help():
 
 # Parse configuration option for mk_make script
 def parse_options():
-    global FORCE_MK, JAVA_ENABLED, GIT_HASH
+    global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED
     path = BUILD_DIR
     options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 
                                                                    'help',

scripts/mk_win_dist.py

@@ -63,7 +63,7 @@ def display_help():
 
 # Parse configuration option for mk_make script
 def parse_options():
-    global FORCE_MK, JAVA_ENABLED, GIT_HASH
+    global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED
     path = BUILD_DIR
     options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 
                                                                    'help',

scripts/update_api.py

@@ -1324,36 +1324,80 @@ def mk_z3native_stubs_c(ml_dir): # C interface
         if len(ap) > 0:
             ml_wrapper.write('  unsigned _i;\n')
 
-        # declare locals, preprocess arrays, strings, in/out arguments
-        have_context = False
+        # determine if the function has a context as parameter.
+        have_context = (len(params) > 0) and (param_type(params[0]) == CONTEXT)
+
+        if have_context and name not in Unwrapped:
+            ml_wrapper.write('  Z3_error_code ec;\n')
+
+        if result != VOID:
+            ts = type2str(result)
+            if ml_has_plus_type(ts):
+                pts = ml_plus_type(ts)
+                ml_wrapper.write('  %s z3rv_m;\n' % ts)
+                ml_wrapper.write('  %s z3rv;\n' % pts)
+            else:
+                ml_wrapper.write('  %s z3rv;\n' % ts)
+
+        # declare all required local variables
+        # To comply with C89, we need to first declare the variables and initialize them
+        # only afterwards.
         i = 0
         for param in params:
             if param_type(param) == CONTEXT and i == 0:
-                ml_wrapper.write('  Z3_context_plus ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
-                ml_wrapper.write('  Z3_context _a0 = ctx_p->ctx;\n')
-                have_context = True
+                ml_wrapper.write('  Z3_context_plus ctx_p;\n')
+                ml_wrapper.write('  Z3_context _a0;\n')
             else:
                 k = param_kind(param)
                 if k == OUT_ARRAY:
-                    ml_wrapper.write('  %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
-                        type2str(param_type(param)),
+                    ml_wrapper.write('  %s * _a%s;\n' % (type2str(param_type(param)), i))
+                elif k == OUT_MANAGED_ARRAY:
+                    ml_wrapper.write('  %s * _a%s;\n' % (type2str(param_type(param)), i))
+                elif k == IN_ARRAY or k == INOUT_ARRAY:
+                    t = param_type(param)
+                    ts = type2str(t)
+                    ml_wrapper.write('  %s * _a%s;\n' % (ts, i))
+                elif k == IN:
+                    t = param_type(param)
+                    ml_wrapper.write('  %s _a%s;\n' % (type2str(t), i))
+                elif k == OUT or k == INOUT:
+                    t = param_type(param)
+                    ml_wrapper.write('  %s _a%s;\n' % (type2str(t), i))
+                    ts = type2str(t)
+                    if ml_has_plus_type(ts):
+                        pts = ml_plus_type(ts)
+                        ml_wrapper.write('  %s _a%dp;\n' % (pts, i))
+            i = i + 1
+
+
+        # End of variable declarations in outermost block:
+        # To comply with C89, no variable declarations may occur in the outermost block
+        # from that point onwards (breaks builds with at least VC 2012 and prior)
+        ml_wrapper.write('\n')
+
+        # Declare locals, preprocess arrays, strings, in/out arguments
+        i = 0
+        for param in params:
+            if param_type(param) == CONTEXT and i == 0:
+                ml_wrapper.write('  ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
+                ml_wrapper.write('  _a0 = ctx_p->ctx;\n')
+            else:
+                k = param_kind(param)
+                if k == OUT_ARRAY:
+                    ml_wrapper.write('  _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
                         i,
                         type2str(param_type(param)),
                         type2str(param_type(param)),
                         param_array_capacity_pos(param)))
                 elif k == OUT_MANAGED_ARRAY:
-                    ml_wrapper.write('  %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
+                    ml_wrapper.write('  _a%s = 0;\n' % i)
                 elif k == IN_ARRAY or k == INOUT_ARRAY:
                     t = param_type(param)
                     ts = type2str(t)
-                    ml_wrapper.write('  %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param)))
+                    ml_wrapper.write('  _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (i, ts, ts, param_array_capacity_pos(param)))
                 elif k == IN:
                     t = param_type(param)
-                    ml_wrapper.write('  %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i))))
-                elif k == OUT:
-                    ml_wrapper.write('  %s _a%s;\n' % (type2str(param_type(param)), i))
-                elif k == INOUT:
-                    ml_wrapper.write('  %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i))
+                    ml_wrapper.write('  _a%s = %s;\n' % (i, ml_unwrap(t, type2str(t), 'a' + str(i))))
             i = i + 1
 
         i = 0
@@ -1375,9 +1419,9 @@ def mk_z3native_stubs_c(ml_dir): # C interface
         if result != VOID:
             ts = type2str(result)
             if ml_has_plus_type(ts):
-                ml_wrapper.write('%s z3rv_m = ' % ts)
+                ml_wrapper.write('z3rv_m = ')
             else:
-                ml_wrapper.write('%s z3rv = ' % ts)
+                ml_wrapper.write('z3rv = ')
 
         # invoke procedure
         ml_wrapper.write('%s(' % name)
@@ -1397,8 +1441,8 @@ def mk_z3native_stubs_c(ml_dir): # C interface
         ml_wrapper.write(');\n')
 
         if have_context and name not in Unwrapped:
-            ml_wrapper.write('  int ec = Z3_get_error_code(ctx_p->ctx);\n')
-            ml_wrapper.write('  if (ec != 0) {\n')
+            ml_wrapper.write('  ec = Z3_get_error_code(ctx_p->ctx);\n')
+            ml_wrapper.write('  if (ec != Z3_OK) {\n')
             ml_wrapper.write('    const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n')
             ml_wrapper.write('    caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), msg);\n')
             ml_wrapper.write('  }\n')
@@ -1408,9 +1452,9 @@ def mk_z3native_stubs_c(ml_dir): # C interface
             if ml_has_plus_type(ts):
                 pts = ml_plus_type(ts)
                 if name in NULLWrapped:
-                    ml_wrapper.write('  %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts))
+                    ml_wrapper.write('  z3rv = %s_mk(z3rv_m);\n' % pts)
                 else:
-                    ml_wrapper.write('  %s z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, pts, ml_minus_type(ts)))
+                    ml_wrapper.write('  z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, ml_minus_type(ts)))
 
         # convert output params
         if len(op) > 0:
@@ -1450,7 +1494,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface
                 elif is_out_param(p):
                     if ml_has_plus_type(ts):
                         pts = ml_plus_type(ts)
-                        ml_wrapper.write('  %s _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (pts, i, pts, ml_minus_type(ts), i))
+                        ml_wrapper.write('  _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (i, pts, ml_minus_type(ts), i))
                         ml_wrapper.write('  %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%dp' % i))
                     else:
                         ml_wrapper.write('  %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%d' % i))

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -74,6 +74,10 @@ class ackermannize_bv_tactic : public tactic {
         m_lemma_limit = p.div0_ackermann_limit();
     }
 
+    virtual void collect_param_descrs(param_descrs & r) {
+        ackermannize_bv_tactic_params::collect_param_descrs(r);
+    }
+
     virtual void collect_statistics(statistics & st) const {
         st.update("ackr-constraints", m_st.m_ackrs_sz);
     }

src/ackermannization/lackr.cpp

@@ -134,7 +134,6 @@ void lackr::eager_enc() {
     const fun2terms_map::iterator e = m_fun2terms.end();
     for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
         checkpoint();
-        func_decl* const fd = i->m_key;
         app_set * const  ts = i->get_value();
         const app_set::iterator r = ts->end();
         for (app_set::iterator j = ts->begin(); j != r; ++j) {
@@ -143,8 +142,8 @@ void lackr::eager_enc() {
             for (;  k != r; ++k) {
                 app * const t1 = *j;
                 app * const t2 = *k;
-                SASSERT(t1->get_decl() == fd);
-                SASSERT(t2->get_decl() == fd);
+                SASSERT(t1->get_decl() == i->m_key);
+                SASSERT(t2->get_decl() == i->m_key);
                 if (t1 == t2) continue;
                 ackr(t1,t2);
             }

src/api/api_ast.cpp

@@ -1066,15 +1066,14 @@ extern "C" {
             case OP_BV2INT:    return Z3_OP_BV2INT;
             case OP_CARRY:     return Z3_OP_CARRY;
             case OP_XOR3:      return Z3_OP_XOR3;
-            case OP_BSMUL_NO_OVFL:
-            case OP_BUMUL_NO_OVFL:
-            case OP_BSMUL_NO_UDFL:
-            case OP_BSDIV_I:
-            case OP_BUDIV_I:
-            case OP_BSREM_I:
-            case OP_BUREM_I:
-            case OP_BSMOD_I:
-                return Z3_OP_UNINTERPRETED;
+            case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
+            case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
+            case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
+            case OP_BSDIV_I: return Z3_OP_BSDIV_I;
+            case OP_BUDIV_I: return Z3_OP_BUDIV_I;
+            case OP_BSREM_I: return Z3_OP_BSREM_I;
+            case OP_BUREM_I: return Z3_OP_BUREM_I;
+            case OP_BSMOD_I: return Z3_OP_BSMOD_I;
             default:
                 UNREACHABLE();
                 return Z3_OP_UNINTERPRETED;
@@ -1184,10 +1183,10 @@ extern "C" {
             case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV;
             case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL;
             case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
+            case OP_FPA_INTERNAL_MIN_I: return Z3_OP_FPA_MIN_I;
+            case OP_FPA_INTERNAL_MAX_I: return Z3_OP_FPA_MAX_I;
+            case OP_FPA_INTERNAL_BV2RM:
             case OP_FPA_INTERNAL_BVWRAP:
-            case OP_FPA_INTERNAL_BVUNWRAP:
-            case OP_FPA_INTERNAL_MIN_I:
-            case OP_FPA_INTERNAL_MAX_I:
             case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
             case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
             case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:

src/api/api_model.cpp

@@ -50,14 +50,13 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
+    Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
         Z3_TRY;
         LOG_Z3_model_get_const_interp(c, m, a);
         RESET_ERROR_CODE();
         CHECK_NON_NULL(m, 0);
         expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a));
         if (!r) {
-            SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
         mk_c(c)->save_ast_trail(r);

src/api/api_quant.cpp

@@ -72,7 +72,7 @@ extern "C" {
         expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns);
         pattern_validator v(mk_c(c)->m());
         for (unsigned i = 0; i < num_patterns; i++) {
-            if (!v(num_decls, ps[i])) {
+            if (!v(num_decls, ps[i], 0, 0)) {
                 SET_ERROR_CODE(Z3_INVALID_PATTERN);
                 return 0;
             }

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

@@ -1582,6 +1582,9 @@ namespace z3 {
 	    return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
 	}
 
+        // returns interpretation of constant declaration c.
+        // If c is not assigned any value in the model it returns 
+        // an expression with a null ast reference.
         expr get_const_interp(func_decl c) const {
             check_context(*this, c);
             Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);

src/api/ml/z3native_stubs.c.pre

@@ -227,6 +227,7 @@ void Z3_ast_finalize(value v) {
 int Z3_ast_compare(value v1, value v2) {
   Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
   Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2);
+  unsigned id1, id2;
 
   /* if the two ASTs belong to different contexts, we take
      their contexts' addresses to order them (arbitrarily, but fixed) */
@@ -242,8 +243,8 @@ int Z3_ast_compare(value v1, value v2) {
     return +1;
 
   /* Comparison according to AST ids. */
-  unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
-  unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
+  id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
+  id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
   if (id1 == id2)
     return 0;
   else if (id1 < id2)
@@ -255,7 +256,7 @@ int Z3_ast_compare(value v1, value v2) {
 int Z3_ast_compare_ext(value v1, value v2) {
   Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
   unsigned id1;
-  int id2 = Val_int(v2);
+  unsigned id2 = (unsigned)Val_int(v2);
   if (a1->p == NULL && id2 == 0)
     return 0;
   if (a1->p == NULL)

src/api/python/z3.py

@@ -3468,7 +3468,7 @@ def is_bv_value(a):
     """
     return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
 
-def BV2Int(a):
+def BV2Int(a, is_signed=False):
     """Return the Z3 expression BV2Int(a).
 
     >>> b = BitVec('b', 3)
@@ -3477,14 +3477,18 @@ def BV2Int(a):
     >>> x = Int('x')
     >>> x > BV2Int(b)
     x > BV2Int(b)
+    >>> x > BV2Int(b, is_signed=False)
+    x > BV2Int(b)
+    >>> x > BV2Int(b, is_signed=True)
+    x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
     >>> solve(x > BV2Int(b), b == 1, x < 3)
     [b = 1, x = 2]
     """
     if __debug__:
         _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
     ctx = a.ctx
     ## investigate problem with bv2int
-    return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
+    return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
 
 def BitVecSort(sz, ctx=None):
     """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
@@ -5516,7 +5520,10 @@ def get_interp(self, decl):
             decl = decl.decl()
         try:
             if decl.arity() == 0:
-                r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
+                _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast)
+                if _r.value is None:
+                    return None
+                r = _to_expr_ref(_r, self.ctx)
                 if is_as_array(r):
                     return self.get_interp(get_as_array_func(r))
                 else:

src/api/z3_api.h

@@ -1060,6 +1060,15 @@ typedef enum {
     Z3_OP_CARRY,
     Z3_OP_XOR3,
 
+    Z3_OP_BSMUL_NO_OVFL,
+    Z3_OP_BUMUL_NO_OVFL,
+    Z3_OP_BSMUL_NO_UDFL,
+    Z3_OP_BSDIV_I,
+    Z3_OP_BUDIV_I,
+    Z3_OP_BSREM_I,
+    Z3_OP_BUREM_I,
+    Z3_OP_BSMOD_I,
+
     // Proofs
     Z3_OP_PR_UNDEF = 0x500,
     Z3_OP_PR_TRUE,
@@ -1205,6 +1214,9 @@ typedef enum {
 
     Z3_OP_FPA_TO_IEEE_BV,
 
+    Z3_OP_FPA_MIN_I,
+    Z3_OP_FPA_MAX_I,
+
     Z3_OP_UNINTERPRETED
 } Z3_decl_kind;
 

src/ast/ast.cpp

@@ -1495,6 +1495,7 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
             if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
       if (!m_family_manager.has_family(fid)) {
           family_id new_fid = mk_family_id(fid_name);
+          (void)new_fid;
           TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
       }
       TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);

src/ast/datatype_decl_plugin.cpp

@@ -462,7 +462,7 @@ func_decl * datatype_decl_plugin::mk_update_field(
     }
     range = domain[0];
     func_decl_info info(m_family_id, k, num_parameters, parameters);
-    return m.mk_func_decl(symbol("update_field"), arity, domain, range, info);
+    return m.mk_func_decl(symbol("update-field"), arity, domain, range, info);
 }
 
 func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 

src/ast/datatype_decl_plugin.h

@@ -109,7 +109,7 @@ class datatype_decl_plugin : public decl_plugin {
          parameters[o]            - (int) m - number of constructors
          parameters[o+1]          - (int) k_1 - offset for constructor definition
          ...
-         parameters[o+m]          - (int) k_m - offset ofr constructor definition
+         parameters[o+m]          - (int) k_m - offset for constructor definition
 
          for each offset k_i at parameters[o+s] for some s in 0..m-1
          parameters[k_i]          - (symbol) name of the constructor