mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

Bugfix for mpf sqrt.

Browse source 
Fixes #222.
This commit is contained in:
Christoph M. Wintersteiger 2015-09-21 19:44:53 +01:00
parent d4b66538f9
commit 0b15fc9402
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/util/mpf.cpp
View file

@ -980,8 +980,7 @@ void mpf_manager::sqrt(mpf_rounding_mode rm, mpf const & x, mpf & o) {
TRACE("mpf_dbg", tout << "A = " << to_string(a) << std::endl;); TRACE("mpf_dbg", tout << "A = " << to_string(a) << std::endl;);
m_mpz_manager.mul2k(a.significand(), x.sbits + ((a.exponent() % 2)?6:5)); m_mpz_manager.mul2k(a.significand(), x.sbits + ((a.exponent() % 2)?6:7));
// my_mpz_sqrt(m_mpz_manager, x.sbits, a.exponent % 2 ? true : false, a.significand, o.significand);
if (!m_mpz_manager.root(a.significand(), 2, o.significand)) if (!m_mpz_manager.root(a.significand(), 2, o.significand))
{ {
// If the result is inexact, it is 1 too large. // If the result is inexact, it is 1 too large.
@ -992,7 +991,7 @@ void mpf_manager::sqrt(mpf_rounding_mode rm, mpf const & x, mpf & o) {
} }
o.exponent = a.exponent() >> 1; o.exponent = a.exponent() >> 1;
round_sqrt(rm, o); round(rm, o);
} }
TRACE("mpf_dbg", tout << "SQRT = " << to_string(o) << std::endl;); TRACE("mpf_dbg", tout << "SQRT = " << to_string(o) << std::endl;);
@ -1589,6 +1588,13 @@ void mpf_manager::mk_ninf(unsigned ebits, unsigned sbits, mpf & o) {
} }
void mpf_manager::unpack(mpf & o, bool normalize) { void mpf_manager::unpack(mpf & o, bool normalize) {
TRACE("mpf_dbg", tout << "unpack " << to_string(o) << ": ebits=" <<
o.ebits << " sbits=" << o.sbits <<
" normalize=" << normalize <<
" has_top_exp=" << has_top_exp(o) << " (" << mk_top_exp(o.ebits) << ")" <<
" has_bot_exp=" << has_bot_exp(o) << " (" << mk_bot_exp(o.ebits) << ")" <<
" is_zero=" << is_zero(o) << std::endl;);
// Insert the hidden bit or adjust the exponent of denormal numbers. // Insert the hidden bit or adjust the exponent of denormal numbers.
if (is_zero(o)) if (is_zero(o))
return; return;