mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Bugfix for mpf to_ieee_bv

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-07 20:17:04 +01:00
parent 773f90f122
commit f2ff071224
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/util/mpf.cpp
View file

@ -1176,12 +1176,14 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
SASSERT(!is_nan(x) && !is_inf(x));
SASSERT(exp(x) < INT_MAX);
unsigned sbits = x.get_sbits();
unsigned ebits = x.get_ebits();
scoped_mpz biased_exp(m_mpz_manager);
m_mpz_manager.set(biased_exp, bias_exp(ebits, exp(x)));
m_mpz_manager.set(o, sgn(x));
m_mpz_manager.mul2k(o, ebits);
m_mpz_manager.add(o, (int)exp(x), o);
m_mpz_manager.add(o, biased_exp, o);
m_mpz_manager.mul2k(o, sbits - 1);
m_mpz_manager.add(o, sig(x), o);
}
@ -1519,6 +1521,9 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) {
return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false));
}
mpf_exp_t mpf_manager::bias_exp(unsigned ebits, mpf_exp_t unbiased_exponent) {
return unbiased_exponent + m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
}
mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) {
return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
}

1
src/util/mpf.h
View file

@ -197,6 +197,7 @@ public:
mpf_exp_t mk_max_exp(unsigned ebits);
mpf_exp_t mk_min_exp(unsigned ebits);
mpf_exp_t bias_exp(unsigned ebits, mpf_exp_t unbiased_exponent);
mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent);
/**