mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
MPF bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
defb6158fe
commit
2258988b37
|
@ -301,28 +301,36 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
|
|||
m_mpq_manager.mul(sig, 2, sig);
|
||||
m_mpz_manager.dec(exp);
|
||||
}
|
||||
|
||||
|
||||
// 1.0 <= sig < 2.0
|
||||
SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
|
||||
|
||||
TRACE("mpf_dbg", tout << "sig = " << m_mpq_manager.to_string(sig) << " exp = " << m_mpz_manager.to_string(exp) << std::endl;);
|
||||
|
||||
TRACE("mpf_dbg", tout << "sig = " << m_mpq_manager.to_string(sig) <<
|
||||
" exp = " << m_mpz_manager.to_string(exp) << std::endl;);
|
||||
|
||||
m_mpz_manager.set(o.significand, 0);
|
||||
for (unsigned i = 0; i < (sbits+3); i++) {
|
||||
m_mpz_manager.mul2k(o.significand, 1);
|
||||
if (!m_mpq_manager.lt(sig, 1)) {
|
||||
m_mpz_manager.inc(o.significand);
|
||||
if (m_mpq_manager.ge(sig, 1)) {
|
||||
m_mpz_manager.inc(o.significand);
|
||||
m_mpq_manager.dec(sig);
|
||||
}
|
||||
m_mpq_manager.mul(sig, 2, sig);
|
||||
m_mpq_manager.mul(sig, mpq(2), sig);
|
||||
}
|
||||
|
||||
// sticky
|
||||
if (!m_mpq_manager.is_zero(sig) && m_mpz_manager.is_even(o.significand))
|
||||
m_mpz_manager.inc(o.significand);
|
||||
|
||||
TRACE("mpf_dbg", tout << "sig = " << m_mpz_manager.to_string(o.significand) <<
|
||||
" exp = " << o.exponent << std::endl;);
|
||||
|
||||
if (m_mpz_manager.is_small(exp)) {
|
||||
o.exponent = m_mpz_manager.get_int64(exp);
|
||||
round(rm, o);
|
||||
}
|
||||
else
|
||||
mk_inf(ebits, sbits, o.sign, o); // CMW: output warning message? throw exception?
|
||||
mk_inf(ebits, sbits, o.sign, o);
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;);
|
||||
|
|
Loading…
Reference in a new issue