mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

MPF conversion bugfix

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-28 17:57:21 +00:00
parent 12aaa0610b
commit 96c8bd7e91
1 changed files with 10 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/util/mpf.cpp
View file

@ -218,39 +218,24 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
o.exponent--; o.exponent--;
} }
m_mpz_manager.set(o.significand, 0); m_mpz_manager.set(o.significand, 0);
// o.exponent += sbits ;
SASSERT(m_mpq_manager.lt(v, mpq(2))); SASSERT(m_mpq_manager.lt(v, mpq(2)));
SASSERT(m_mpq_manager.ge(v, mpq(1))); SASSERT(m_mpq_manager.ge(v, mpq(1)));
// 1.0 <= v < 2.0 (* 2^o.exponent) // 1.0 <= v < 2.0 (* 2^o.exponent)
// (and v != 0.0) // (and v != 0.0)
for (unsigned i = 0; i < sbits + 3 ; i++) for (unsigned i = 0; i < sbits + 3 ; i++)
{ {
m_mpz_manager.mul(o.significand, mpz(2), o.significand); m_mpz_manager.mul2k(o.significand, 1);
if (m_mpq_manager.ge(v, mpq(1))) if (m_mpq_manager.ge(v, mpq(1))) {
m_mpz_manager.add(o.significand, mpz(1), o.significand); m_mpz_manager.inc(o.significand);
m_mpq_manager.sub(v, mpq(1), v); // v := v - 1.0 m_mpq_manager.dec(v); // v := v - 1.0
}
m_mpq_manager.mul(mpq(2), v, v); // v := 2.0 * v m_mpq_manager.mul(mpq(2), v, v); // v := 2.0 * v
} }
// Sticky
// m_mpz_manager.mul(o.significand, mpz(2), o.significand);
/*if (!m_mpq_manager.is_zero(v))
m_mpz_manager.add(o.significand, mpz(1), o.significand);*/
// bias? TRACE("mpf_dbg", tout << "rnd sig=" << m_mpz_manager.to_string(o.significand) <<
// o.exponent += m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false)); " exp=" << o.exponent << std::endl;);
// mpq pow;
// m_mpq_manager.power(mpq(2), sbits + 3, pow);
// m_mpq_manager.div(o.significand, pow, o.significand);
// SASSERT(m_mpz_manager.ge(o.significand, mpq(1.0)));
// SASSERT(m_mpz_manager.lt(o.significand, mpq(2.0)));
TRACE("mpf_dbg", tout << "sig=" << m_mpz_manager.to_string(o.significand) << " exp=" << o.exponent <<
" sticky=" << (!m_mpq_manager.is_zero(v)) << std::endl;);
round(rm, o); round(rm, o);
} }