mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
FPA rewriter and MPF bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
5e60bcd920
commit
941d1063dd
|
@ -100,6 +100,11 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
|
||||
SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break;
|
||||
|
||||
case OP_FPA_INTERNAL_BVWRAP:
|
||||
case OP_FPA_INTERNAL_BVUNWRAP:
|
||||
st = BR_FAILED;
|
||||
break;
|
||||
|
||||
default:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
@ -183,8 +188,15 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
|
|||
|
||||
SASSERT(mpzm.is_int64(exp));
|
||||
mpf_exp_t mpf_exp = mpzm.get_int64(exp);
|
||||
mpf_exp = m_fm.unbias_exp(ebits, mpf_exp);
|
||||
|
||||
m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), sig, mpf_exp);
|
||||
TRACE("fp_rewriter",
|
||||
tout << "sgn: " << !mpzm.is_zero(z) << std::endl;
|
||||
tout << "sig: " << mpzm.to_string(sig) << std::endl;
|
||||
tout << "exp: " << mpf_exp << std::endl;
|
||||
tout << "v: " << m_fm.to_string(v) << std::endl;);
|
||||
|
||||
result = m_util.mk_value(v);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
@ -198,22 +210,24 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
|
|||
TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;);
|
||||
scoped_mpf v(m_fm);
|
||||
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq());
|
||||
result = m_util.mk_value(v);
|
||||
result = m_util.mk_value(v);
|
||||
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
|
||||
return BR_DONE;
|
||||
}
|
||||
else if (m_util.is_numeral(args[1], v)) {
|
||||
// rm + float -> float
|
||||
TRACE("fp_rewriter", tout << "v: " << m_fm.to_string(v) << std::endl; );
|
||||
scoped_mpf v(m_fm);
|
||||
m_fm.set(v, ebits, sbits, rmv, v);
|
||||
result = m_util.mk_value(v);
|
||||
scoped_mpf vf(m_fm);
|
||||
m_fm.set(vf, ebits, sbits, rmv, v);
|
||||
result = m_util.mk_value(vf);
|
||||
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
|
||||
return BR_DONE;
|
||||
}
|
||||
else if (bu.is_numeral(args[1], r1, bvs1)) {
|
||||
else if (bu.is_numeral(args[1], r1, bvs1)) {
|
||||
// rm + signed bv -> float
|
||||
scoped_mpf v(m_fm);
|
||||
TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;);
|
||||
r1 = bu.norm(r1, bvs1, true);
|
||||
TRACE("fp_rewriter", tout << "r1 norm: " << r1 << std::endl;);
|
||||
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq());
|
||||
result = m_util.mk_value(v);
|
||||
return BR_DONE;
|
||||
|
@ -229,8 +243,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
|
|||
!m_util.au().is_numeral(args[2], r2))
|
||||
return BR_FAILED;
|
||||
|
||||
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
|
||||
scoped_mpf v(m_fm);
|
||||
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
|
||||
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator());
|
||||
result = m_util.mk_value(v);
|
||||
return BR_DONE;
|
||||
|
@ -242,7 +255,6 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
|
|||
SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator()));
|
||||
SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator()));
|
||||
SASSERT(m_fm.mpz_manager().is_int64(r3.to_mpq().numerator()));
|
||||
scoped_mpf v(m_fm);
|
||||
mpf_exp_t biased_exp = m_fm.mpz_manager().get_int64(r2.to_mpq().numerator());
|
||||
m_fm.set(v, bvs2, bvs3 + 1,
|
||||
r1.is_one(),
|
||||
|
@ -711,8 +723,16 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
|
|||
bv_util bu(m());
|
||||
scoped_mpq q(m_fm.mpq_manager());
|
||||
m_fm.to_sbv_mpq(rmv, v, q);
|
||||
|
||||
rational r(q);
|
||||
result = bu.mk_numeral(r, bv_sz);
|
||||
unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
|
||||
rational ul, ll;
|
||||
ul = m_fm.m_powers2.m1(bv_sz);
|
||||
ll = rational(0);
|
||||
if (r >= ll && r <= ul)
|
||||
result = bu.mk_numeral(r, bv_sz);
|
||||
else
|
||||
result = m_util.mk_internal_to_ubv_unspecified(bv_sz);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
@ -737,8 +757,16 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
|
|||
bv_util bu(m());
|
||||
scoped_mpq q(m_fm.mpq_manager());
|
||||
m_fm.to_sbv_mpq(rmv, v, q);
|
||||
|
||||
rational r(q);
|
||||
result = bu.mk_numeral(r, bv_sz);
|
||||
unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
|
||||
rational ul, ll;
|
||||
ul = m_fm.m_powers2.m1(bv_sz - 1);
|
||||
ll = - m_fm.m_powers2(bv_sz - 1);
|
||||
if (r >= ll && r <= ul)
|
||||
result = bu.mk_numeral(r, bv_sz);
|
||||
else
|
||||
result = m_util.mk_internal_to_sbv_unspecified(bv_sz);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
|
|
@ -190,59 +190,9 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) {
|
|||
|
||||
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode rm, mpq const & value) {
|
||||
TRACE("mpf_dbg", tout << "set: " << m_mpq_manager.to_string(value) << " [" << ebits << "/" << sbits << "]"<< std::endl;);
|
||||
|
||||
if (m_mpq_manager.is_zero(value))
|
||||
mk_pzero(ebits, sbits, o);
|
||||
else {
|
||||
o.ebits = ebits;
|
||||
o.sbits = sbits;
|
||||
o.sign = m_mpq_manager.is_neg(value);
|
||||
|
||||
scoped_mpq x(m_mpq_manager);
|
||||
m_mpq_manager.set(x, value);
|
||||
m_mpq_manager.abs(x);
|
||||
|
||||
m_mpz_manager.set(o.significand, 0);
|
||||
|
||||
scoped_mpq v(m_mpq_manager);
|
||||
m_mpq_manager.set(v, x);
|
||||
o.exponent = 0;
|
||||
|
||||
// Normalize
|
||||
while (m_mpq_manager.ge(v, mpq(2)))
|
||||
{
|
||||
m_mpq_manager.div(v, mpq(2), v);
|
||||
o.exponent++;
|
||||
}
|
||||
|
||||
while (m_mpq_manager.lt(v, mpq(1)))
|
||||
{
|
||||
m_mpq_manager.mul(v, mpq(2), v);
|
||||
o.exponent--;
|
||||
}
|
||||
|
||||
m_mpz_manager.set(o.significand, 0);
|
||||
SASSERT(m_mpq_manager.lt(v, mpq(2)));
|
||||
SASSERT(m_mpq_manager.ge(v, mpq(1)));
|
||||
|
||||
// 1.0 <= v < 2.0 (* 2^o.exponent)
|
||||
// (and v != 0.0)
|
||||
for (unsigned i = 0; i < sbits + 3 ; i++)
|
||||
{
|
||||
m_mpz_manager.mul2k(o.significand, 1);
|
||||
if (m_mpq_manager.ge(v, mpq(1))) {
|
||||
m_mpz_manager.inc(o.significand);
|
||||
m_mpq_manager.dec(v); // v := v - 1.0
|
||||
}
|
||||
m_mpq_manager.mul(mpq(2), v, v); // v := 2.0 * v
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "rnd sig=" << m_mpz_manager.to_string(o.significand) <<
|
||||
" exp=" << o.exponent << std::endl;);
|
||||
|
||||
round(rm, o);
|
||||
}
|
||||
|
||||
scoped_mpz exp(m_mpz_manager);
|
||||
m_mpz_manager.set(exp, 0);
|
||||
set(o, ebits, sbits, rm, value, exp);
|
||||
TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;);
|
||||
}
|
||||
|
||||
|
@ -1109,15 +1059,13 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
|
|||
|
||||
SASSERT(t.exponent() < INT_MAX);
|
||||
|
||||
m_mpz_manager.set(z, t.significand());
|
||||
if (t.sign()) m_mpz_manager.neg(z);
|
||||
m_mpz_manager.set(z, t.significand());
|
||||
mpf_exp_t e = (mpf_exp_t)t.exponent() - t.sbits() + 1;
|
||||
if (e < 0) {
|
||||
bool last = false, round = false, guard = false, sticky = m_mpz_manager.is_odd(z);
|
||||
bool last = false, round = false, sticky = m_mpz_manager.is_odd(z);
|
||||
for (; e != 0; e++) {
|
||||
m_mpz_manager.machine_div2k(z, 1);
|
||||
sticky |= guard;
|
||||
guard = round;
|
||||
sticky |= round;
|
||||
round = last;
|
||||
last = m_mpz_manager.is_odd(z);
|
||||
}
|
||||
|
@ -1125,8 +1073,8 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
|
|||
switch (rm) {
|
||||
case MPF_ROUND_NEAREST_TEVEN: inc = round && (last || sticky); break;
|
||||
case MPF_ROUND_NEAREST_TAWAY: inc = round && (!last || sticky); break; // CMW: Check!
|
||||
case MPF_ROUND_TOWARD_POSITIVE: inc = (!m_mpz_manager.is_neg(z) && (round || sticky)); break;
|
||||
case MPF_ROUND_TOWARD_NEGATIVE: inc = (m_mpz_manager.is_neg(z) && (round || sticky)); break;
|
||||
case MPF_ROUND_TOWARD_POSITIVE: inc = (!x.sign && (round || sticky)); break;
|
||||
case MPF_ROUND_TOWARD_NEGATIVE: inc = (x.sign && (round || sticky)); break;
|
||||
case MPF_ROUND_TOWARD_ZERO: inc = false; break;
|
||||
default: UNREACHABLE();
|
||||
}
|
||||
|
@ -1136,6 +1084,7 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
|
|||
m_mpz_manager.mul2k(z, (unsigned) e);
|
||||
|
||||
m_mpq_manager.set(o, z);
|
||||
if (x.sign) m_mpq_manager.neg(o);
|
||||
}
|
||||
|
||||
void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
|
||||
|
|
Loading…
Reference in a new issue