From 941d1063dd13d9a0c44d62e23dc5eaa584211ef8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 6 Feb 2015 18:48:14 +0000 Subject: [PATCH] FPA rewriter and MPF bugfixes Signed-off-by: Christoph M. Wintersteiger --- src/ast/rewriter/fpa_rewriter.cpp | 50 +++++++++++++++++----- src/util/mpf.cpp | 69 ++++--------------------------- 2 files changed, 48 insertions(+), 71 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 394c2f117..291712805 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -100,6 +100,11 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break; + case OP_FPA_INTERNAL_BVWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: + st = BR_FAILED; + break; + default: NOT_IMPLEMENTED_YET(); } @@ -183,8 +188,15 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const SASSERT(mpzm.is_int64(exp)); mpf_exp_t mpf_exp = mpzm.get_int64(exp); + mpf_exp = m_fm.unbias_exp(ebits, mpf_exp); m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), sig, mpf_exp); + TRACE("fp_rewriter", + tout << "sgn: " << !mpzm.is_zero(z) << std::endl; + tout << "sig: " << mpzm.to_string(sig) << std::endl; + tout << "exp: " << mpf_exp << std::endl; + tout << "v: " << m_fm.to_string(v) << std::endl;); + result = m_util.mk_value(v); return BR_DONE; } @@ -198,22 +210,24 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;); scoped_mpf v(m_fm); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); - result = m_util.mk_value(v); + result = m_util.mk_value(v); // TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } else if (m_util.is_numeral(args[1], v)) { // rm + float -> float TRACE("fp_rewriter", tout << "v: " << m_fm.to_string(v) << std::endl; ); - scoped_mpf v(m_fm); - m_fm.set(v, ebits, sbits, rmv, v); - result = m_util.mk_value(v); + scoped_mpf vf(m_fm); + m_fm.set(vf, ebits, sbits, rmv, v); + result = m_util.mk_value(vf); // TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else if (bu.is_numeral(args[1], r1, bvs1)) { + else if (bu.is_numeral(args[1], r1, bvs1)) { // rm + signed bv -> float - scoped_mpf v(m_fm); + TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;); + r1 = bu.norm(r1, bvs1, true); + TRACE("fp_rewriter", tout << "r1 norm: " << r1 << std::endl;); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); result = m_util.mk_value(v); return BR_DONE; @@ -229,8 +243,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const !m_util.au().is_numeral(args[2], r2)) return BR_FAILED; - TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); - scoped_mpf v(m_fm); + TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator()); result = m_util.mk_value(v); return BR_DONE; @@ -242,7 +255,6 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator())); SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator())); SASSERT(m_fm.mpz_manager().is_int64(r3.to_mpq().numerator())); - scoped_mpf v(m_fm); mpf_exp_t biased_exp = m_fm.mpz_manager().get_int64(r2.to_mpq().numerator()); m_fm.set(v, bvs2, bvs3 + 1, r1.is_one(), @@ -711,8 +723,16 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); m_fm.to_sbv_mpq(rmv, v, q); + rational r(q); - result = bu.mk_numeral(r, bv_sz); + unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); + rational ul, ll; + ul = m_fm.m_powers2.m1(bv_sz); + ll = rational(0); + if (r >= ll && r <= ul) + result = bu.mk_numeral(r, bv_sz); + else + result = m_util.mk_internal_to_ubv_unspecified(bv_sz); return BR_DONE; } @@ -737,8 +757,16 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); m_fm.to_sbv_mpq(rmv, v, q); + rational r(q); - result = bu.mk_numeral(r, bv_sz); + unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); + rational ul, ll; + ul = m_fm.m_powers2.m1(bv_sz - 1); + ll = - m_fm.m_powers2(bv_sz - 1); + if (r >= ll && r <= ul) + result = bu.mk_numeral(r, bv_sz); + else + result = m_util.mk_internal_to_sbv_unspecified(bv_sz); return BR_DONE; } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 323ffa3af..4e452b1e8 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -190,59 +190,9 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) { void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpq const & value) { TRACE("mpf_dbg", tout << "set: " << m_mpq_manager.to_string(value) << " [" << ebits << "/" << sbits << "]"<< std::endl;); - - if (m_mpq_manager.is_zero(value)) - mk_pzero(ebits, sbits, o); - else { - o.ebits = ebits; - o.sbits = sbits; - o.sign = m_mpq_manager.is_neg(value); - - scoped_mpq x(m_mpq_manager); - m_mpq_manager.set(x, value); - m_mpq_manager.abs(x); - - m_mpz_manager.set(o.significand, 0); - - scoped_mpq v(m_mpq_manager); - m_mpq_manager.set(v, x); - o.exponent = 0; - - // Normalize - while (m_mpq_manager.ge(v, mpq(2))) - { - m_mpq_manager.div(v, mpq(2), v); - o.exponent++; - } - - while (m_mpq_manager.lt(v, mpq(1))) - { - m_mpq_manager.mul(v, mpq(2), v); - o.exponent--; - } - - m_mpz_manager.set(o.significand, 0); - SASSERT(m_mpq_manager.lt(v, mpq(2))); - SASSERT(m_mpq_manager.ge(v, mpq(1))); - - // 1.0 <= v < 2.0 (* 2^o.exponent) - // (and v != 0.0) - for (unsigned i = 0; i < sbits + 3 ; i++) - { - m_mpz_manager.mul2k(o.significand, 1); - if (m_mpq_manager.ge(v, mpq(1))) { - m_mpz_manager.inc(o.significand); - m_mpq_manager.dec(v); // v := v - 1.0 - } - m_mpq_manager.mul(mpq(2), v, v); // v := 2.0 * v - } - - TRACE("mpf_dbg", tout << "rnd sig=" << m_mpz_manager.to_string(o.significand) << - " exp=" << o.exponent << std::endl;); - - round(rm, o); - } - + scoped_mpz exp(m_mpz_manager); + m_mpz_manager.set(exp, 0); + set(o, ebits, sbits, rm, value, exp); TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;); } @@ -1109,15 +1059,13 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o SASSERT(t.exponent() < INT_MAX); - m_mpz_manager.set(z, t.significand()); - if (t.sign()) m_mpz_manager.neg(z); + m_mpz_manager.set(z, t.significand()); mpf_exp_t e = (mpf_exp_t)t.exponent() - t.sbits() + 1; if (e < 0) { - bool last = false, round = false, guard = false, sticky = m_mpz_manager.is_odd(z); + bool last = false, round = false, sticky = m_mpz_manager.is_odd(z); for (; e != 0; e++) { m_mpz_manager.machine_div2k(z, 1); - sticky |= guard; - guard = round; + sticky |= round; round = last; last = m_mpz_manager.is_odd(z); } @@ -1125,8 +1073,8 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o switch (rm) { case MPF_ROUND_NEAREST_TEVEN: inc = round && (last || sticky); break; case MPF_ROUND_NEAREST_TAWAY: inc = round && (!last || sticky); break; // CMW: Check! - case MPF_ROUND_TOWARD_POSITIVE: inc = (!m_mpz_manager.is_neg(z) && (round || sticky)); break; - case MPF_ROUND_TOWARD_NEGATIVE: inc = (m_mpz_manager.is_neg(z) && (round || sticky)); break; + case MPF_ROUND_TOWARD_POSITIVE: inc = (!x.sign && (round || sticky)); break; + case MPF_ROUND_TOWARD_NEGATIVE: inc = (x.sign && (round || sticky)); break; case MPF_ROUND_TOWARD_ZERO: inc = false; break; default: UNREACHABLE(); } @@ -1136,6 +1084,7 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o m_mpz_manager.mul2k(z, (unsigned) e); m_mpq_manager.set(o, z); + if (x.sign) m_mpq_manager.neg(o); } void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {