mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Optimization for initialization of mpf's from tiny reals.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-12 19:06:53 +00:00
parent db746e0c2f
commit f093ebe44c
1 changed files with 14 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/util/mpf.cpp
View file

@ -245,26 +245,30 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
m_mpz_manager.set(exp, exponent);
// Normalize such that 1.0 <= sig < 2.0
if (m_mpq_manager.ge(sig, mpq(2))) {
if (m_mpq_manager.lt(sig, 1)) {
m_mpq_manager.inv(sig);
unsigned int pp = m_mpq_manager.prev_power_of_two(sig);
if (!m_mpq_manager.is_power_of_two(sig, pp)) pp++;
scoped_mpz p2(m_mpz_manager);
m_mpq_manager.power(2, pp, p2);
m_mpq_manager.div(sig, p2, sig);
m_mpz_manager.sub(exp, mpz(pp), exp);
m_mpq_manager.inv(sig);
}
else if (m_mpq_manager.ge(sig, 2)) {
unsigned int pp = m_mpq_manager.prev_power_of_two(sig);
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)) {
m_mpq_manager.mul(sig, 2, sig);
m_mpz_manager.dec(exp);
}
// Check that 1.0 <= sig < 2.0
SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
TRACE("mpf_dbg", tout << "Normalized: sig = " << m_mpq_manager.to_string(sig) <<
" exp = " << m_mpz_manager.to_string(exp) << std::endl;);
// Check that 1.0 <= sig < 2.0
SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
scoped_mpz p(m_mpq_manager);
scoped_mpq t(m_mpq_manager), sq(m_mpq_manager);
m_mpz_manager.power(2, sbits + 3 - 1, p);