mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

Optimization for real to float conversion. Relates to #383.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-11 18:54:07 +00:00
parent e88ac377c5
commit d4efa3753c
1 changed files with 18 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/util/mpf.cpp
View file

@ -244,32 +244,35 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
m_mpq_manager.abs(sig); m_mpq_manager.abs(sig);
m_mpz_manager.set(exp, exponent); m_mpz_manager.set(exp, exponent);
// Normalize // Normalize such that 1.0 <= sig < 2.0
while (m_mpq_manager.ge(sig, 2)) { if (m_mpq_manager.ge(sig, mpq(2))) {
m_mpq_manager.div(sig, mpq(2), sig); unsigned int pp = m_mpq_manager.prev_power_of_two(sig);
m_mpz_manager.inc(exp); scoped_mpz p2(m_mpz_manager);
m_mpq_manager.power(2, pp, p2);
m_mpq_manager.div(sig, p2, sig);
m_mpz_manager.add(exp, mpz(pp), exp);
} }
SASSERT(m_mpq_manager.lt(sig, mpq(2)));
while (m_mpq_manager.lt(sig, 1)) { while (m_mpq_manager.lt(sig, 1)) {
m_mpq_manager.mul(sig, 2, sig); m_mpq_manager.mul(sig, 2, sig);
m_mpz_manager.dec(exp); m_mpz_manager.dec(exp);
} }
// 1.0 <= sig < 2.0 // Check that 1.0 <= sig < 2.0
SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2))); SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
TRACE("mpf_dbg", tout << "sig = " << m_mpq_manager.to_string(sig) << TRACE("mpf_dbg", tout << "Normalized: sig = " << m_mpq_manager.to_string(sig) <<
" exp = " << m_mpz_manager.to_string(exp) << std::endl;); " exp = " << m_mpz_manager.to_string(exp) << std::endl;);
m_mpz_manager.set(o.significand, 0); scoped_mpz p(m_mpq_manager);
for (unsigned i = 0; i < (sbits+3); i++) { scoped_mpq t(m_mpq_manager), sq(m_mpq_manager);
m_mpz_manager.mul2k(o.significand, 1); m_mpz_manager.power(2, sbits + 3 - 1, p);
if (m_mpq_manager.ge(sig, 1)) { m_mpq_manager.mul(p, sig, t);
m_mpz_manager.inc(o.significand); m_mpq_manager.floor(t, o.significand);
m_mpq_manager.dec(sig); m_mpq_manager.set(sq, o.significand);
} m_mpq_manager.div(sq, p, t);
m_mpq_manager.mul(sig, mpq(2), sig); m_mpq_manager.sub(sig, t, sig);
}
// sticky // sticky
if (!m_mpq_manager.is_zero(sig) && m_mpz_manager.is_even(o.significand)) if (!m_mpq_manager.is_zero(sig) && m_mpz_manager.is_even(o.significand))