diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 015bce0ed..367fa3a4c 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -83,17 +83,21 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c rational q; mpf q_mpf; if (m_util.au().is_numeral(args[1], q)) { + TRACE("fp_rewriter", tout << "q: " << q << std::endl; ); mpf v; m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); result = m_util.mk_value(v); - m_util.fm().del(v); + m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else if (m_util.is_value(args[1], q_mpf)) { + else if (m_util.is_value(args[1], q_mpf)) { + TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; ); mpf v; m_util.fm().set(v, ebits, sbits, rm, q_mpf); result = m_util.mk_value(v); m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } else @@ -117,11 +121,11 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c return BR_FAILED; TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";); - mpf v; m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator()); result = m_util.mk_value(v); - m_util.fm().del(v); + m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } else { diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index dd40e8453..0913fbbcf 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1698,6 +1698,10 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a expr_ref sgn(m), sig(m), exp(m), lz(m); unpack(x, sgn, sig, exp, lz, true); + dbg_decouple("fpa2bv_to_float_x_sig", sig); + dbg_decouple("fpa2bv_to_float_x_exp", exp); + dbg_decouple("fpa2bv_to_float_lz", lz); + expr_ref res_sgn(m), res_sig(m), res_exp(m); res_sgn = sgn; @@ -1710,10 +1714,13 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a SASSERT(m_bv_util.get_bv_size(sgn) == 1); SASSERT(m_bv_util.get_bv_size(sig) == from_sbits); SASSERT(m_bv_util.get_bv_size(exp) == from_ebits); + SASSERT(m_bv_util.get_bv_size(lz) == from_ebits); - if (from_sbits < (to_sbits + 3)) + if (from_sbits < (to_sbits + 3)) + { // make sure that sig has at least to_sbits + 3 res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits)); + } else if (from_sbits > (to_sbits + 3)) { // collapse the extra bits into a sticky bit. @@ -1734,7 +1741,9 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a exponent_overflow = m.mk_false(); if (from_ebits < (to_ebits + 2)) - res_exp = m_bv_util.mk_sign_extend(to_ebits+2-from_ebits, exp); + { + res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp); + } else if (from_ebits > (to_ebits + 2)) { expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m); @@ -1747,7 +1756,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get()); zero1 = m_bv_util.mk_numeral(0, 1); - m_simp.mk_eq(high_red_and, one1, h_and_eq); + m_simp.mk_eq(high_red_and, one1, h_and_eq); m_simp.mk_eq(high_red_or, zero1, h_or_eq); m_simp.mk_eq(lows, zero1, s_is_zero); m_simp.mk_eq(lows, one1, s_is_one); @@ -1763,10 +1772,18 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a else res_exp = exp; + // subtract lz for subnormal numbers. + expr_ref lz_ext(m); + lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz); + res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext); SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2); + dbg_decouple("fpa2bv_to_float_res_sig", res_sig); + dbg_decouple("fpa2bv_to_float_res_exp", res_exp); + expr_ref rounded(m); round(s, rm, res_sgn, res_sig, res_exp, rounded); + expr_ref is_neg(m), sig_inf(m); m_simp.mk_eq(sgn, one1, is_neg); @@ -1781,7 +1798,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a mk_ite(c4, v4, result, result); mk_ite(c3, v3, result, result); mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); + mk_ite(c1, v1, result, result); } else { // .. other than that, we only support rationals for asFloat @@ -1826,7 +1843,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a m_util.fm().del(v); } - SASSERT(is_well_sorted(m, result)); + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index def9f4fd5..735d21c99 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -367,7 +367,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode o.ebits = ebits; o.sbits = sbits; - signed ds = sbits - x.sbits + 4; // plus rounding bits + signed ds = sbits - x.sbits + 3; // plus rounding bits if (ds > 0) { m_mpz_manager.mul2k(o.significand, ds);