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

src/ast/bv_decl_plugin.cpp

@@ -766,7 +766,7 @@ bool bv_recognizers::is_zero(expr const * n) const {
     return decl->get_parameter(0).get_rational().is_zero();
 }
 
-bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) {
+bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) const {
     if (!is_extract(e)) return false;
     low = get_extract_low(e);
     high = get_extract_high(e);
@@ -774,7 +774,7 @@ bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, ex
     return true;
 }
 
-bool bv_recognizers::is_bv2int(expr const* e, expr*& r) {
+bool bv_recognizers::is_bv2int(expr const* e, expr*& r) const {
     if (!is_bv2int(e)) return false;
     r = to_app(e)->get_arg(0);
     return true;

src/ast/bv_decl_plugin.h

@@ -288,10 +288,10 @@ public:
     bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); }
     unsigned get_extract_high(func_decl const * f) const { return f->get_parameter(0).get_int(); }
     unsigned get_extract_low(func_decl const * f) const { return f->get_parameter(1).get_int(); }
-    unsigned get_extract_high(expr const * n) { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
+    unsigned get_extract_high(expr const * n) const { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
-    unsigned get_extract_low(expr const * n) { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
+    unsigned get_extract_low(expr const * n) const { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
-    bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b);
+    bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b) const;
-    bool is_bv2int(expr const * e, expr * & r);
+    bool is_bv2int(expr const * e, expr * & r) const;
     bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
     bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }
     bool is_bv_mul(expr const * e) const { return is_app_of(e, get_fid(), OP_BMUL); }

src/ast/float_decl_plugin.cpp

@@ -491,6 +491,15 @@ void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbo
     sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT));
 }
 
+expr * float_decl_plugin::get_some_value(sort * s) {
+    SASSERT(s->is_sort_of(m_family_id, FLOAT_SORT));    
+    mpf tmp;
+    m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp);
+    expr * res = this->mk_value(tmp);
+    m_fm.del(tmp);
+    return res;
+}
+
 bool float_decl_plugin::is_value(app * e) const {
     if (e->get_family_id() != m_family_id) 
         return false;

src/ast/float_decl_plugin.h

@@ -140,6 +140,7 @@ public:
                                      unsigned arity, sort * const * domain, sort * range);
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
     virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
+    virtual expr * get_some_value(sort * s);
     virtual bool is_value(app* e) const;
     virtual bool is_unique_value(app* e) const { return is_value(e); }
     

src/smt/params/smt_params_helper.pyg

@@ -29,6 +29,7 @@ def_module_params(module_name='smt',
                           ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
                           ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
+                          ('bv.enable_int2bv', BOOL, False, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                           ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),

src/smt/params/theory_bv_params.cpp

@@ -22,4 +22,5 @@ Revision History:
 void theory_bv_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_bv_reflect = p.bv_reflect();
+    m_bv_enable_int2bv2int = p.bv_enable_int2bv(); 
 }

src/tactic/fpa/fpa2bv_converter.cpp

@@ -1263,6 +1263,9 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a
 
     expr * x = args[0], * y = args[1];
 
+    TRACE("fpa2bv_float_eq", tout << "X = " << mk_ismt2_pp(x, m) << std::endl; 
+                             tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;);
+
     expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m);
     mk_is_nan(x, x_is_nan);
     mk_is_nan(y, y_is_nan);
@@ -1290,6 +1293,8 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a
     m_simp.mk_ite(c2, m.mk_true(), c3t4, c2else);
 
     m_simp.mk_ite(c1, m.mk_false(), c2else, result);
+
+    TRACE("fpa2bv_float_eq", tout << "FLOAT_EQ = " << mk_ismt2_pp(result, m) << std::endl; );
 }
 
 void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -2314,9 +2319,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         unsigned ebits = fu.get_ebits(var->get_range());
         unsigned sbits = fu.get_sbits(var->get_range());
 
-        expr * sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
+        expr_ref sgn(m), sig(m), exp(m);
-        expr * sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
+        sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
-        expr * exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
+        sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
+        exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
 
         seen.insert(to_app(a->get_arg(0))->get_decl());
         seen.insert(to_app(a->get_arg(1))->get_decl());
@@ -2385,12 +2391,11 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
     for (unsigned i = 0; i < sz; i++)
     {
         func_decl * c = bv_mdl->get_constant(i);
-        if (seen.contains(c))
+        if (!seen.contains(c))            
-            continue;
+            float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
-        float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
     }
 
-// And keep everything else
+    // And keep everything else
     sz = bv_mdl->get_num_functions();
     for (unsigned i = 0; i < sz; i++)
     {

src/util/gparams.cpp

@@ -49,6 +49,7 @@ char const * g_params_renames[] = {
     "restart_factor", "smt.restart_factor",
     "arith_random_initial_value", "smt.arith.random_initial_value",
     "bv_reflect", "smt.bv.reflect",
+    "bv_enable_int2bv_propagation", "smt.bv.enable_int2bv",
     "qi_cost", "smt.qi.cost",
     "qi_eager_threshold", "smt.qi.eager_threshold",
     "nl_arith", "smt.arith.nl",