mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Fix corner case in MPF FMA (#6075)

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2022-06-04 15:55:26 +01:00 • committed by GitHub
parent 6422a6b5a7
commit d722c73d4c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 22 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/util/mpf.cpp
View file

@ -904,8 +904,6 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
SASSERT(m_mpz_manager.lt(res.significand(), m_powers2(2 * x.sbits + 1 + 3))); SASSERT(m_mpz_manager.lt(res.significand(), m_powers2(2 * x.sbits + 1 + 3)));
if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits + 3))) if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits + 3)))
{ {
SASSERT(exp(res) < mk_max_exp(x.ebits)); // NYI.
res.get().exponent++; res.get().exponent++;
renorm_sticky = !m_mpz_manager.is_even(res.significand()); renorm_sticky = !m_mpz_manager.is_even(res.significand());
m_mpz_manager.machine_div2k(res.significand(), 1); m_mpz_manager.machine_div2k(res.significand(), 1);
@ -923,26 +921,32 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
TRACE("mpf_dbg", tout << "R*= " << to_string_binary(res, 2, 0) << " (renormalized, delta=" << renorm_delta << ")" << std::endl;); TRACE("mpf_dbg", tout << "R*= " << to_string_binary(res, 2, 0) << " (renormalized, delta=" << renorm_delta << ")" << std::endl;);
set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0)); if (exp(res) <= mk_max_exp(x.ebits))
{
set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0));
if (x.sbits >= 4) { if (x.sbits >= 4) {
m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4 + 3), o.significand, sticky_rem); m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4 + 3), o.significand, sticky_rem);
renorm_sticky |= !m_mpz_manager.is_zero(sticky_rem); renorm_sticky |= !m_mpz_manager.is_zero(sticky_rem);
}
else {
m_mpz_manager.mul2k(res.significand(), 4 - x.sbits + 3, o.significand);
}
if (renorm_sticky && m_mpz_manager.is_even(o.significand))
m_mpz_manager.inc(o.significand);
TRACE("mpf_dbg", tout << "sum[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;
tout << "R = " << to_string_binary(o, 1, 3) << std::endl;);
if (m_mpz_manager.is_zero(o.significand))
mk_zero(x.ebits, x.sbits, rm == MPF_ROUND_TOWARD_NEGATIVE, o);
else
round(rm, o);
} }
else { else {
m_mpz_manager.mul2k(res.significand(), 4 - x.sbits + 3, o.significand); mk_inf(x.ebits, x.sbits, res.sign(), o);
} }
if (renorm_sticky && m_mpz_manager.is_even(o.significand))
m_mpz_manager.inc(o.significand);
TRACE("mpf_dbg", tout << "sum[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;
tout << "R = " << to_string_binary(o, 1, 3) << std::endl;);
if (m_mpz_manager.is_zero(o.significand))
mk_zero(x.ebits, x.sbits, rm == MPF_ROUND_TOWARD_NEGATIVE, o);
else
round(rm, o);
} }
} }