Added FP to_ieee_bv to fpa_rewriter to enable model evaluation.

src/api/api_fpa.cpp

@@ -838,7 +838,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_ieee_bv(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_float_to_ieee_bv(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_to_ieee_bv(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }

src/ast/fpa_decl_plugin.cpp

@@ -642,7 +642,7 @@ func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, pa
     return m_manager->mk_func_decl(name, 1, domain, m_real_sort, func_decl_info(m_family_id, k));
 }
 
-func_decl * fpa_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                                    unsigned arity, sort * const * domain, sort * range) {
     if (arity != 1)
         m_manager->raise_exception("invalid number of arguments to to_ieee_bv");
@@ -791,7 +791,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_FPA_TO_FP_UNSIGNED:
         return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_TO_IEEE_BV:
-        return mk_float_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
+        return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_INTERNAL_BVWRAP:
         return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_INTERNAL_BVUNWRAP:
@@ -1013,7 +1013,13 @@ app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) {
     return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range);
 }
 
+app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned width) {
+    parameter ps[] = { parameter(width) };
+    sort * range = m_bv_util.mk_sort(width);
+    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range);
+}
+
 app * fpa_util::mk_internal_to_real_unspecified() {
     sort * range = m_a_util.mk_real();
     return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range);
-}
+}

src/ast/fpa_decl_plugin.h

@@ -89,6 +89,7 @@ enum fpa_op_kind {
     OP_FPA_INTERNAL_BVUNWRAP,
     OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED,
     OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED,    
+    OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED,
     OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED,    
 
     LAST_FLOAT_OP
@@ -152,8 +153,8 @@ class fpa_decl_plugin : public decl_plugin {
                           unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,
                            unsigned arity, sort * const * domain, sort * range);
-    func_decl * mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                    unsigned arity, sort * const * domain, sort * range);
+                              unsigned arity, sort * const * domain, sort * range);
 
     func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                     unsigned arity, sort * const * domain, sort * range);
@@ -329,10 +330,11 @@ public:
 
     bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FPA_NEG); }
 
-    app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); }
+    app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); }
 
     app * mk_internal_to_ubv_unspecified(unsigned width);
     app * mk_internal_to_sbv_unspecified(unsigned width);
+    app * mk_internal_to_ieee_bv_unspecified(unsigned width);
     app * mk_internal_to_real_unspecified();
 
     bool is_wrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); }

src/ast/rewriter/fpa_rewriter.cpp

@@ -90,8 +90,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(f, args[0], args[1], result); break;
     case OP_FPA_TO_UBV:    SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break;
     case OP_FPA_TO_SBV:    SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break;
-    case OP_FPA_TO_REAL:   SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
+    case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break;
-    case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;    
+    case OP_FPA_TO_REAL:   SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;    
 
     case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: 
         SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break;
@@ -121,7 +121,7 @@ br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result)
         // The "hardware interpretation" is 0.
         result = bu.mk_numeral(0, bv_sz);
     else
-        result = m_util.mk_internal_to_real_unspecified();
+        result = m_util.mk_internal_to_ubv_unspecified(bv_sz);
 
     return BR_DONE;
 }
@@ -136,7 +136,22 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result)
         // The "hardware interpretation" is 0.
         result = bu.mk_numeral(0, bv_sz);
     else
-        result = m_util.mk_internal_to_real_unspecified();
+        result = m_util.mk_internal_to_sbv_unspecified(bv_sz);
+
+    return BR_DONE;
+}
+
+br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) {
+    SASSERT(f->get_num_parameters() == 1);
+    SASSERT(f->get_parameter(0).is_int());
+    unsigned bv_sz = f->get_parameter(0).get_int();
+
+    bv_util bu(m());
+    if (m_hi_fp_unspecified)
+        // The "hardware interpretation" is 0.
+        result = bu.mk_numeral(0, bv_sz);
+    else
+        result = m_util.mk_internal_to_ieee_bv_unspecified(bv_sz);
 
     return BR_DONE;
 }
@@ -698,10 +713,6 @@ br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result)
     return BR_FAILED;
 }
 
-br_status fpa_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) {
-    return BR_FAILED;
-}
-
 br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
     unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
     bv_util bu(m());
@@ -794,6 +805,26 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
     return BR_FAILED;
 }
 
+br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) {
+    scoped_mpf v(m_fm);
+
+    if (m_util.is_numeral(arg, v)) {
+
+        if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
+            mk_to_ieee_bv_unspecified(f, result);
+            return BR_REWRITE_FULL;
+        }
+        
+        bv_util bu(m());
+        scoped_mpz rz(m_fm.mpq_manager());
+        m_fm.to_ieee_bv_mpz(v, rz);
+        result = bu.mk_numeral(rational(rz), v.get().get_ebits() + v.get().get_sbits());
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
 br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
     scoped_mpf v(m_fm);
     

src/ast/rewriter/fpa_rewriter.h

@@ -81,10 +81,12 @@ public:
     br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result);
     br_status mk_to_real(expr * arg, expr_ref & result);
 
     br_status mk_to_ubv_unspecified(func_decl * f, expr_ref & result);
     br_status mk_to_sbv_unspecified(func_decl * f, expr_ref & result);
+    br_status mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result);
     br_status mk_to_real_unspecified(expr_ref & result);
 };
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -58,7 +58,7 @@ class inc_sat_solver : public solver {
     proof_converter_ref m_pc;   
     model_converter_ref m_mc2;   
     expr_dependency_ref m_dep_core;
-    svector<double>       m_weights;
+    svector<double>     m_weights;
 
     typedef obj_map<expr, sat::literal> dep2asm_t;
 public:

src/util/mpf.cpp

@@ -1179,6 +1179,19 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
     if (x.sign) m_mpq_manager.neg(o);
 }
 
+void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
+    SASSERT(!is_nan(x) && !is_inf(x));
+    SASSERT(exp(x) < INT_MAX);
+
+    unsigned sbits = x.get_sbits();
+    unsigned ebits = x.get_ebits();
+    m_mpz_manager.set(o, sgn(x));
+    m_mpz_manager.mul2k(o, ebits);
+    m_mpz_manager.add(o, exp(x), o);
+    m_mpz_manager.mul2k(o, sbits - 1);
+    m_mpz_manager.add(o, sig(x), o);
+}
+
 void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
     SASSERT(x.sbits == y.sbits && x.ebits == y.ebits);
 

src/util/mpf.h

@@ -207,6 +207,7 @@ public:
     unsigned prev_power_of_two(mpf const & a);
 
     void to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o);
+    void to_ieee_bv_mpz(const mpf & x, scoped_mpz & o);
 
 protected:
     void mk_one(unsigned ebits, unsigned sbits, bool sign, mpf & o) const;