mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 21:38:44 +00:00
Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872.
This commit is contained in:
Christoph M. Wintersteiger
parent
75b533f050
commit
33ebdc8adc
|
|
@ -3904,9 +3904,6 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
|
|||
SASSERT(m_bv_util.get_bv_size(sig) == sbits+4);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == ebits+2);
|
||||
|
||||
// bool UNFen = false;
|
||||
// bool OVFen = false;
|
||||
|
||||
expr_ref e_min(m), e_max(m);
|
||||
mk_min_exp(ebits, e_min);
|
||||
mk_max_exp(ebits, e_max);
|
||||
|
|
@ -4025,7 +4022,6 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
|
|||
SASSERT(is_well_sorted(m, sig));
|
||||
SASSERT(m_bv_util.get_bv_size(sig) == sbits+2);
|
||||
|
||||
// CMW: The (OVF1 && OVFen) and (TINY && UNFen) cases are never taken.
|
||||
expr_ref ext_emin(m);
|
||||
ext_emin = m_bv_util.mk_zero_extend(2, e_min);
|
||||
m_simp.mk_ite(TINY, ext_emin, beta, exp);
|
||||
|
|
|
|||
344
src/util/mpf.cpp
344
src/util/mpf.cpp
|
|
@ -805,7 +805,7 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
o.ebits = x.ebits;
|
||||
o.sbits = x.sbits;
|
||||
|
||||
scoped_mpf mul_res(*this, x.ebits+2, 2*x.sbits);
|
||||
scoped_mpf mul_res(*this, x.ebits+2, 2*x.sbits-1);
|
||||
scoped_mpf a(*this, x.ebits, x.sbits), b(*this, x.ebits, x.sbits), c(*this, x.ebits, x.sbits);
|
||||
set(a, x);
|
||||
set(b, y);
|
||||
|
|
@ -814,9 +814,12 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
unpack(b, true);
|
||||
unpack(c, true);
|
||||
|
||||
TRACE("mpf_dbg", tout << "A = " << to_string(a) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "B = " << to_string(b) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "C = " << to_string(c) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "A = " << to_string(a) << std::endl;
|
||||
tout << "B = " << to_string(b) << std::endl;
|
||||
tout << "C = " << to_string(c) << std::endl;
|
||||
tout << "A = " << to_string_binary(a, 1, 0) << std::endl;
|
||||
tout << "B = " << to_string_binary(b, 1, 0) << std::endl;
|
||||
tout << "C = " << to_string_binary(c, 1, 0) << std::endl;);
|
||||
|
||||
SASSERT(m_mpz_manager.lt(a.significand(), m_powers2(x.sbits)));
|
||||
SASSERT(m_mpz_manager.lt(b.significand(), m_powers2(x.sbits)));
|
||||
|
|
@ -824,99 +827,115 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
SASSERT(m_mpz_manager.ge(a.significand(), m_powers2(x.sbits-1)));
|
||||
SASSERT(m_mpz_manager.ge(b.significand(), m_powers2(x.sbits-1)));
|
||||
|
||||
// A/B in _1.[sbits-1].
|
||||
mul_res.get().sign = (a.sign() != b.sign());
|
||||
mul_res.get().exponent = a.exponent() + b.exponent();
|
||||
m_mpz_manager.mul(a.significand(), b.significand(), mul_res.get().significand);
|
||||
m_mpz_manager.mul(a.significand(), b.significand(), mul_res.significand());
|
||||
|
||||
TRACE("mpf_dbg", tout << "PRODUCT = " << to_string(mul_res) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "M = " << to_string(mul_res) << std::endl;
|
||||
tout << "M = " << to_string_binary(mul_res, 1, 0) << std::endl;);
|
||||
|
||||
// mul_res is [-1][0].[2*sbits - 2], i.e., between 2*sbits-1 and 2*sbits.
|
||||
// mul_res is [-1][0].[2*sbits - 2], i.e., >= 2^(2*sbits-2) and < 2^(2*sbits).
|
||||
SASSERT(m_mpz_manager.lt(mul_res.significand(), m_powers2(2*x.sbits)));
|
||||
SASSERT(m_mpz_manager.ge(mul_res.significand(), m_powers2(2*x.sbits - 2)));
|
||||
|
||||
// Introduce extra bits into c.
|
||||
m_mpz_manager.mul2k(c.significand(), x.sbits-1, c.significand());
|
||||
// Introduce extra bits into c in _[0].[sbits-1] s.t. c in _[0].[2*sbits-2]
|
||||
c.get().ebits = x.ebits + 2;
|
||||
c.get().sbits = 2 * x.sbits - 1;
|
||||
m_mpz_manager.mul2k(c.significand(), x.sbits - 1);
|
||||
|
||||
SASSERT(m_mpz_manager.lt(c.significand(), m_powers2(2 * x.sbits - 1)));
|
||||
TRACE("mpf_dbg", tout << "C_= " << to_string(c) << std::endl;
|
||||
tout << "C_= " << to_string_binary(c, 1, 0) << std::endl;);
|
||||
|
||||
SASSERT(m_mpz_manager.lt(c.significand(), m_powers2(2*x.sbits)));
|
||||
SASSERT(m_mpz_manager.is_zero(c.significand()) ||
|
||||
m_mpz_manager.ge(c.significand(), m_powers2(2 * x.sbits - 2)));
|
||||
m_mpz_manager.ge(c.significand(), m_powers2(2*x.sbits - 2)));
|
||||
|
||||
TRACE("mpf_dbg", tout << "C = " << to_string(c) << std::endl;);
|
||||
|
||||
if (exp(c) > exp(mul_res))
|
||||
if (exp(c) > exp(mul_res)) {
|
||||
TRACE("mpf_dbg", tout << "Swap!" << std::endl;);
|
||||
mul_res.swap(c);
|
||||
}
|
||||
|
||||
mpf_exp_t exp_delta = exp(mul_res) - exp(c);
|
||||
mpf_exp_t exp_delta_w = exp(mul_res) - exp(c);
|
||||
|
||||
SASSERT(exp(mul_res) >= exp(c) && exp_delta >= 0);
|
||||
SASSERT(exp(mul_res) >= exp(c) && exp_delta_w >= 0);
|
||||
|
||||
if (exp_delta > 2 * x.sbits)
|
||||
exp_delta = 2 * x.sbits;
|
||||
if (exp_delta_w > 2 * x.sbits)
|
||||
exp_delta_w = 2 * x.sbits;
|
||||
unsigned exp_delta = (unsigned)exp_delta_w;
|
||||
TRACE("mpf_dbg", tout << "exp_delta = " << exp_delta << std::endl;);
|
||||
|
||||
// Alignment shift with sticky bit computation.
|
||||
scoped_mpz sticky_rem(m_mpz_manager);
|
||||
m_mpz_manager.machine_div_rem(c.significand(), m_powers2((int)exp_delta), c.significand(), sticky_rem);
|
||||
m_mpz_manager.machine_div_rem(c.significand(), m_powers2(exp_delta), c.significand(), sticky_rem);
|
||||
TRACE("mpf_dbg", tout << "alignment shift -> sig = " << m_mpz_manager.to_string(c.significand()) <<
|
||||
" sticky_rem = " << m_mpz_manager.to_string(sticky_rem) << std::endl;);
|
||||
if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(c.significand()))
|
||||
m_mpz_manager.inc(c.significand());
|
||||
|
||||
TRACE("mpf_dbg", tout << "M' = " << m_mpz_manager.to_string(mul_res.significand()) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "C' = " << m_mpz_manager.to_string(c.significand()) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "M'= " << m_mpz_manager.to_string(mul_res.significand()) << std::endl;
|
||||
tout << "M'= " << to_string_binary(mul_res, 1, 0) << std::endl; );
|
||||
TRACE("mpf_dbg", tout << "C'= " << m_mpz_manager.to_string(c.significand()) << std::endl;
|
||||
tout << "C'= " << to_string_binary(c, 1, 0) << std::endl; );
|
||||
|
||||
scoped_mpf res(c);
|
||||
|
||||
res.get().sign = mul_res.sign();
|
||||
res.get().exponent = mul_res.exponent();
|
||||
|
||||
// Significand addition
|
||||
|
||||
if (sgn(mul_res) != sgn(c)) {
|
||||
TRACE("mpf_dbg", tout << "SUBTRACTING" << std::endl;);
|
||||
m_mpz_manager.sub(mul_res.significand(), c.significand(), o.significand);
|
||||
m_mpz_manager.sub(mul_res.significand(), c.significand(), res.significand());
|
||||
|
||||
if (m_mpz_manager.is_neg(res.significand())) {
|
||||
m_mpz_manager.abs(res.significand());
|
||||
res.get().sign |= !mul_res.sign() && c.sign();
|
||||
}
|
||||
}
|
||||
else {
|
||||
TRACE("mpf_dbg", tout << "ADDING" << std::endl;);
|
||||
m_mpz_manager.add(mul_res.significand(), c.significand(), o.significand);
|
||||
m_mpz_manager.add(mul_res.significand(), c.significand(), res.significand());
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "sum[-1:] = " << m_mpz_manager.to_string(o.significand) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "S'= " << m_mpz_manager.to_string(res.significand()) << std::endl;
|
||||
tout << "S'= " << to_string_binary(res, 1, 0) << std::endl; );
|
||||
|
||||
bool neg = m_mpz_manager.is_neg(o.significand);
|
||||
TRACE("mpf_dbg", tout << "NEG=" << neg << std::endl;);
|
||||
if (neg) m_mpz_manager.abs(o.significand);
|
||||
|
||||
o.exponent = mul_res.exponent();
|
||||
|
||||
unsigned extra = 0;
|
||||
// Result could overflow into 4.xxx ...
|
||||
SASSERT(m_mpz_manager.lt(o.significand, m_powers2(2 * x.sbits + 2)));
|
||||
if (m_mpz_manager.ge(o.significand, m_powers2(2 * x.sbits + 1)))
|
||||
SASSERT(m_mpz_manager.lt(res.significand(), m_powers2(2 * x.sbits + 1)));
|
||||
if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits)))
|
||||
{
|
||||
extra++;
|
||||
o.exponent++;
|
||||
TRACE("mpf_dbg", tout << "Addition overflew!" << std::endl;);
|
||||
SASSERT(exp(res) < mk_max_exp(x.ebits)); // NYI.
|
||||
|
||||
res.get().exponent++;
|
||||
bool sticky = !m_mpz_manager.is_even(res.significand());
|
||||
m_mpz_manager.machine_div2k(res.significand(), 1);
|
||||
if (sticky && m_mpz_manager.is_even(res.significand()))
|
||||
m_mpz_manager.inc(res.significand());
|
||||
TRACE("mpf_dbg", tout << "Add/Sub overflew into 4.xxx!" << std::endl;
|
||||
tout << "S*= " << to_string_binary(res, 2, 0) << std::endl;);
|
||||
}
|
||||
|
||||
// Remove the extra bits, keeping a sticky bit.
|
||||
m_mpz_manager.set(sticky_rem, 0);
|
||||
unsigned minbits = (4 + extra);
|
||||
if (o.sbits >= minbits)
|
||||
m_mpz_manager.machine_div_rem(o.significand, m_powers2(o.sbits - minbits), o.significand, sticky_rem);
|
||||
else
|
||||
m_mpz_manager.mul2k(o.significand, minbits - o.sbits, o.significand);
|
||||
set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0));
|
||||
|
||||
if (x.sbits >= 4) {
|
||||
m_mpz_manager.set(sticky_rem, 0);
|
||||
m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4), o.significand, sticky_rem);
|
||||
if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(o.significand))
|
||||
m_mpz_manager.inc(o.significand);
|
||||
}
|
||||
else {
|
||||
m_mpz_manager.mul2k(res.significand(), 4 - x.sbits, o.significand);
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "sum[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "sum[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;
|
||||
tout << "R = " << to_string_binary(o, 2, 3) << std::endl;);
|
||||
|
||||
if (m_mpz_manager.is_zero(o.significand))
|
||||
mk_zero(x.ebits, x.sbits, rm == MPF_ROUND_TOWARD_NEGATIVE, o);
|
||||
else {
|
||||
o.sign = ((!mul_res.sign() && c.sign() && neg) ||
|
||||
( mul_res.sign() && !c.sign() && !neg) ||
|
||||
( mul_res.sign() && c.sign()));
|
||||
TRACE("mpf_dbg", tout << "before round = " << to_string(o) << std::endl <<
|
||||
"fs[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;);
|
||||
else
|
||||
round(rm, o);
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
|
@ -1596,6 +1615,64 @@ std::string mpf_manager::to_string_hexfloat(mpf const & x) {
|
|||
return ss.str();
|
||||
}
|
||||
|
||||
std::string mpf_manager::to_string_binary(mpf const & x, unsigned upper_extra, unsigned lower_extra) {
|
||||
std::string res;
|
||||
|
||||
if (is_nan(x))
|
||||
res = std::string("") + "#b0 " +
|
||||
"#b" + std::string(x.ebits, '1') + " " +
|
||||
"#b" + std::string(x.sbits-2, '0') + "1 " +
|
||||
"(NaN)";
|
||||
else if (is_inf(x))
|
||||
res = std::string("") + "#b" + (sgn(x)?"1":"0") + " " +
|
||||
"#b" + std::string(x.ebits, '1') + " " +
|
||||
"#b" + std::string(x.sbits - 1, '0') + "1 " +
|
||||
"(" + (sgn(x)?"-":"+") + "oo)";
|
||||
else if (is_zero(x))
|
||||
res = std::string("") + "#b" + (sgn(x) ? "1" : "0") + " " +
|
||||
"#b" + std::string(x.ebits, '0') + " " +
|
||||
"#b" + std::string(x.sbits - 1, '0') + " " +
|
||||
"(" + (sgn(x) ? "-" : "+") + "zero)";
|
||||
else {
|
||||
res = std::string("") + "#b" + (sgn(x) ? "1" : "0") + " ";
|
||||
|
||||
scoped_mpz tmp(m_mpz_manager);
|
||||
|
||||
if (is_denormal(x))
|
||||
m_mpz_manager.set(tmp, bias_exp(x.ebits, mk_min_exp(x.ebits)));
|
||||
else {
|
||||
m_mpz_manager.set(tmp, bias_exp(x.ebits, exp(x)));
|
||||
}
|
||||
|
||||
std::string tmp_str = "";
|
||||
for (unsigned i = 0; i < x.ebits; i++) {
|
||||
tmp_str += m_mpz_manager.is_odd(tmp) ? "1" : "0";
|
||||
tmp /= 2;
|
||||
}
|
||||
std::reverse(tmp_str.begin(), tmp_str.end());
|
||||
res += "#b" + tmp_str + " ";
|
||||
|
||||
tmp_str = "";
|
||||
m_mpz_manager.set(tmp, sig(x));
|
||||
unsigned num_bits = upper_extra + x.sbits + lower_extra;
|
||||
for (unsigned i = 0; i < num_bits || !tmp.is_zero(); i++) {
|
||||
tmp_str += m_mpz_manager.is_odd(tmp) ? "1" : "0";
|
||||
tmp /= 2;
|
||||
if (i == lower_extra - 1)
|
||||
tmp_str += ",";
|
||||
if (i == x.sbits + lower_extra - 2) {
|
||||
tmp_str += ".";
|
||||
if (i == num_bits - 1)
|
||||
tmp_str += " ";
|
||||
}
|
||||
}
|
||||
std::reverse(tmp_str.begin(), tmp_str.end());
|
||||
res += "#b" + tmp_str;
|
||||
}
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
void mpf_manager::to_rational(mpf const & x, unsynch_mpq_manager & qm, mpq & o) {
|
||||
scoped_mpf a(*this);
|
||||
scoped_mpz n(m_mpq_manager), d(m_mpq_manager);
|
||||
|
|
@ -1865,129 +1942,76 @@ void mpf_manager::mk_round_inf(mpf_rounding_mode rm, mpf & o) {
|
|||
}
|
||||
|
||||
void mpf_manager::round(mpf_rounding_mode rm, mpf & o) {
|
||||
// Assumptions: o.significand is of the form f[-1:0] . f[1:sbits-1] [guard,round,sticky],
|
||||
// Assumptions: o.significand is of the form f[-1:0] . f[1:sbits-1] [round,extra,sticky],
|
||||
// i.e., it has 2 + (sbits-1) + 3 = sbits + 4 bits.
|
||||
|
||||
TRACE("mpf_dbg", tout << "RND: " << to_string(o) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "RND: " << to_string(o) << std::endl;
|
||||
tout << to_string_binary(o, 1, 3) << std::endl;);
|
||||
|
||||
DEBUG_CODE({
|
||||
const mpz & p_m3 = m_powers2(o.sbits+5);
|
||||
const mpz & p_m3 = m_powers2(o.sbits+4);
|
||||
SASSERT(m_mpz_manager.lt(o.significand, p_m3));
|
||||
});
|
||||
|
||||
// Structure of the rounder:
|
||||
// (s, e_out, f_out) == (s, exprd(s, post(e, sigrd(s, f)))).
|
||||
mpf_exp_t e_max = mk_max_exp(o.ebits);
|
||||
mpf_exp_t e_min = mk_min_exp(o.ebits);
|
||||
|
||||
bool UNFen = false; // Are these supposed to be persistent flags accross calls?
|
||||
bool OVFen = false;
|
||||
|
||||
mpf_exp_t e_max_norm = mk_max_exp(o.ebits);
|
||||
mpf_exp_t e_min_norm = mk_min_exp(o.ebits);
|
||||
scoped_mpz temporary(m_mpq_manager);
|
||||
|
||||
TRACE("mpf_dbg", tout << "e_min_norm = " << e_min_norm << std::endl <<
|
||||
"e_max_norm = " << e_max_norm << std::endl;);
|
||||
|
||||
const mpz & p_m1 = m_powers2(o.sbits+2);
|
||||
const mpz & p_m2 = m_powers2(o.sbits+3);
|
||||
(void)p_m1;
|
||||
|
||||
TRACE("mpf_dbg", tout << "p_m1 = " << m_mpz_manager.to_string(p_m1) << std::endl <<
|
||||
"p_m2 = " << m_mpz_manager.to_string(p_m2) << std::endl;);
|
||||
|
||||
bool OVF1 = o.exponent > e_max_norm || // Exponent OVF
|
||||
(o.exponent == e_max_norm && m_mpz_manager.ge(o.significand, p_m2));
|
||||
|
||||
TRACE("mpf_dbg", tout << "OVF1 = " << OVF1 << std::endl;);
|
||||
|
||||
int lz = 0;
|
||||
scoped_mpz t(m_mpq_manager);
|
||||
m_mpz_manager.set(t, p_m2);
|
||||
while (m_mpz_manager.gt(t, o.significand)) {
|
||||
m_mpz_manager.machine_div2k(t, 1);
|
||||
lz++;
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "LZ = " << lz << std::endl;);
|
||||
|
||||
m_mpz_manager.set(t, o.exponent);
|
||||
m_mpz_manager.inc(t);
|
||||
m_mpz_manager.sub(t, lz, t);
|
||||
m_mpz_manager.set(temporary, e_min_norm);
|
||||
m_mpz_manager.sub(t, temporary, t);
|
||||
bool TINY = m_mpz_manager.is_neg(t);
|
||||
|
||||
TRACE("mpf_dbg", tout << "TINY = " << TINY << std::endl;);
|
||||
|
||||
mpf_exp_t alpha = 3 << (o.ebits-2);
|
||||
unsigned sig_width = m_mpz_manager.prev_power_of_two(o.significand) + 1;
|
||||
mpf_exp_t lz = o.sbits + 4 - sig_width;
|
||||
mpf_exp_t beta = o.exponent - lz + 1;
|
||||
|
||||
TRACE("mpf_dbg", tout << "alpha = " << alpha << std::endl <<
|
||||
"beta = " << beta << std::endl; );
|
||||
scoped_mpz sigma(m_mpz_manager);
|
||||
|
||||
scoped_mpz sigma(m_mpq_manager);
|
||||
sigma = 0;
|
||||
|
||||
if (TINY && !UNFen) {
|
||||
m_mpz_manager.set(sigma, o.exponent);
|
||||
m_mpz_manager.sub(sigma, temporary, sigma);
|
||||
m_mpz_manager.inc(sigma);
|
||||
if (beta < e_min) {
|
||||
// denormal significand/TINY
|
||||
m_mpz_manager.set(sigma, o.exponent - e_min);
|
||||
o.exponent = e_min;
|
||||
}
|
||||
else
|
||||
m_mpz_manager.set(sigma, lz);
|
||||
|
||||
scoped_mpz limit(m_mpq_manager);
|
||||
limit = o.sbits + 2;
|
||||
m_mpz_manager.neg(limit);
|
||||
if (m_mpz_manager.lt(sigma, limit)) {
|
||||
m_mpz_manager.set(sigma, limit);
|
||||
else {
|
||||
m_mpz_manager.set(sigma, lz - 1);
|
||||
o.exponent = beta;
|
||||
}
|
||||
|
||||
scoped_mpz sigma_cap(m_mpz_manager);
|
||||
sigma_cap = o.sbits + 2;
|
||||
m_mpz_manager.neg(sigma_cap);
|
||||
if (m_mpz_manager.lt(sigma, sigma_cap))
|
||||
m_mpz_manager.set(sigma, sigma_cap);
|
||||
|
||||
TRACE("mpf_dbg", tout << "e_min_norm = " << e_min << std::endl;
|
||||
tout << "e_max_norm = " << e_max << std::endl;
|
||||
tout << "beta = " << beta << ", (beta < e_min) = " << (beta < e_min) << std::endl;
|
||||
tout << "LZ = " << lz << std::endl;
|
||||
tout << "sigma = " << m_mpz_manager.to_string(sigma) << std::endl;
|
||||
tout << "sigma_cap = " << m_mpz_manager.to_string(sigma_cap) << std::endl;);
|
||||
|
||||
// Normalization shift
|
||||
|
||||
TRACE("mpf_dbg", tout << "Shift distance: " << m_mpz_manager.to_string(sigma) << " " << ((m_mpz_manager.is_nonneg(sigma))?"(LEFT)":"(RIGHT)") << std::endl;);
|
||||
|
||||
if (m_mpz_manager.le(sigma, 0)) { // Right shift
|
||||
if (m_mpz_manager.le(sigma, -1)) {
|
||||
// Right shift
|
||||
scoped_mpz sticky_rem(m_mpz_manager);
|
||||
unsigned sigma_uint = (unsigned)-m_mpz_manager.get_int64(sigma); // sigma is capped, this is safe.
|
||||
sigma_uint += 2;
|
||||
m_mpz_manager.machine_div_rem(o.significand, m_powers2(sigma_uint), o.significand, sticky_rem);
|
||||
unsigned nsigma_uint = (unsigned)-m_mpz_manager.get_int64(sigma); // sigma is capped, this is safe.
|
||||
m_mpz_manager.machine_div_rem(o.significand, m_powers2(nsigma_uint), o.significand, sticky_rem);
|
||||
bool sticky = !m_mpz_manager.is_zero(sticky_rem);
|
||||
if (sticky && m_mpz_manager.is_even(o.significand))
|
||||
m_mpz_manager.inc(o.significand);
|
||||
}
|
||||
else { // Left shift
|
||||
else {
|
||||
// Left shift
|
||||
unsigned sigma_uint = static_cast<unsigned>(m_mpz_manager.get_int64(sigma));
|
||||
m_mpz_manager.mul2k(o.significand, sigma_uint - 1, o.significand);
|
||||
bool sticky = !m_mpz_manager.is_even(o.significand);
|
||||
m_mpz_manager.machine_div2k(o.significand, 1);
|
||||
if (sticky && m_mpz_manager.is_even(o.significand))
|
||||
m_mpz_manager.inc(o.significand);
|
||||
m_mpz_manager.mul2k(o.significand, sigma_uint, o.significand);
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "After sticky: " << to_string(o) << std::endl;);
|
||||
|
||||
if (OVF1 && OVFen) {
|
||||
o.exponent = beta;
|
||||
o.exponent -= alpha;
|
||||
}
|
||||
else if (TINY && UNFen) {
|
||||
o.exponent = beta;
|
||||
o.exponent += alpha;
|
||||
}
|
||||
else if (TINY && !UNFen)
|
||||
o.exponent = e_min_norm;
|
||||
else
|
||||
o.exponent = beta;
|
||||
|
||||
TRACE("mpf_dbg", tout << "Shifted: " << to_string(o) << std::endl;);
|
||||
|
||||
const mpz & p_sig = m_powers2(o.sbits);
|
||||
SASSERT(TINY || (m_mpz_manager.ge(o.significand, p_sig)));
|
||||
TRACE("mpf_dbg", tout << "Shifted: " << to_string(o) << std::endl;
|
||||
tout << to_string_binary(o, 1, 3) << std::endl;);
|
||||
|
||||
// Significand rounding (sigrd)
|
||||
|
||||
bool sticky = !m_mpz_manager.is_even(o.significand); // new sticky bit!
|
||||
bool sticky = !m_mpz_manager.is_even(o.significand);
|
||||
m_mpz_manager.machine_div2k(o.significand, 1);
|
||||
sticky = sticky || !m_mpz_manager.is_even(o.significand);
|
||||
m_mpz_manager.machine_div2k(o.significand, 1);
|
||||
bool round = !m_mpz_manager.is_even(o.significand);
|
||||
m_mpz_manager.machine_div2k(o.significand, 1);
|
||||
|
|
@ -2002,56 +2026,47 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) {
|
|||
bool inc = false;
|
||||
switch (rm) {
|
||||
case MPF_ROUND_NEAREST_TEVEN: inc = round && (last || sticky); break;
|
||||
// case MPF_ROUND_NEAREST_TAWAY: inc = round; break; // CMW: Check
|
||||
case MPF_ROUND_NEAREST_TAWAY: inc = round && (!last || sticky); break; // CMW: Fix ok?
|
||||
case MPF_ROUND_NEAREST_TAWAY: inc = round && (!last || sticky); break;
|
||||
case MPF_ROUND_TOWARD_POSITIVE: inc = (!o.sign && (round || sticky)); break;
|
||||
case MPF_ROUND_TOWARD_NEGATIVE: inc = (o.sign && (round || sticky)); break;
|
||||
case MPF_ROUND_TOWARD_ZERO: inc = false; break;
|
||||
default: UNREACHABLE();
|
||||
}
|
||||
|
||||
if (inc) {
|
||||
TRACE("mpf_dbg", tout << "Rounding increment -> significand +1" << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "Rounding increment -> significand +" << (int)inc << std::endl;);
|
||||
if (inc)
|
||||
m_mpz_manager.inc(o.significand);
|
||||
}
|
||||
else
|
||||
TRACE("mpf_dbg", tout << "Rounding increment -> significand +0" << std::endl;);
|
||||
|
||||
TRACE("mpf_dbg", tout << "Rounded significand: " << to_string(o) << std::endl;);
|
||||
|
||||
bool SIGovf = false;
|
||||
|
||||
// Post normalization (post)
|
||||
|
||||
const mpz & p_sig = m_powers2(o.sbits);
|
||||
if (m_mpz_manager.ge(o.significand, p_sig)) {
|
||||
m_mpz_manager.machine_div2k(o.significand, 1);
|
||||
o.exponent++;
|
||||
}
|
||||
|
||||
if (o.exponent > e_max_norm)
|
||||
SIGovf = true;
|
||||
|
||||
bool SIGovf = o.exponent > e_max;
|
||||
TRACE("mpf_dbg", tout << "Post-normalized: " << to_string(o) << std::endl;);
|
||||
|
||||
TRACE("mpf_dbg", tout << "SIGovf = " << SIGovf << std::endl;);
|
||||
|
||||
// Exponent rounding (exprd)
|
||||
|
||||
bool o_has_max_exp = (o.exponent > e_max_norm);
|
||||
bool o_has_max_exp = (o.exponent > e_max);
|
||||
bool OVF2 = SIGovf && o_has_max_exp;
|
||||
|
||||
TRACE("mpf_dbg", tout << "OVF2 = " << OVF2 << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "o_has_max_exp = " << o_has_max_exp << std::endl;);
|
||||
|
||||
if (!OVFen && OVF2)
|
||||
if (OVF2)
|
||||
mk_round_inf(rm, o);
|
||||
else {
|
||||
const mpz & p = m_powers2(o.sbits-1);
|
||||
TRACE("mpf_dbg", tout << "P: " << m_mpz_manager.to_string(p_m1) << std::endl;);
|
||||
|
||||
if (m_mpz_manager.ge(o.significand, p)) {
|
||||
TRACE("mpf_dbg", tout << "NORMAL: " << m_mpz_manager.to_string(o.significand) << std::endl;);
|
||||
m_mpz_manager.sub(o.significand, p, o.significand);
|
||||
m_mpz_manager.sub(o.significand, p, o.significand); // Strips the hidden bit.
|
||||
}
|
||||
else {
|
||||
TRACE("mpf_dbg", tout << "DENORMAL: " << m_mpz_manager.to_string(o.significand) << std::endl;);
|
||||
|
|
@ -2059,7 +2074,8 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) {
|
|||
}
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "ROUNDED = " << to_string(o) << std::endl;);
|
||||
TRACE("mpf_dbg", tout << "ROUNDED = " << to_string(o) << std::endl;
|
||||
tout << to_string_binary(o, -1, 0) << " (hidden bit, unbiased exp)." << std::endl;);
|
||||
}
|
||||
|
||||
void mpf_manager::round_sqrt(mpf_rounding_mode rm, mpf & o) {
|
||||
|
|
|
|||
|
|
@ -287,6 +287,7 @@ protected:
|
|||
std::string to_string_raw(mpf const & a);
|
||||
std::string to_string_hexfloat(mpf const & a);
|
||||
std::string to_string_hexfloat(bool sgn, mpf_exp_t exp, scoped_mpz const & sig, unsigned ebits, unsigned sbits, unsigned rbits);
|
||||
std::string to_string_binary(mpf const & x, unsigned upper_extra, unsigned lower_extra);
|
||||
public:
|
||||
powers2 m_powers2;
|
||||
};
|
||||
|
|
|
|||
Loading…
Reference in a new issue