mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Bugfix for fp.roundToIntegral.

Browse source 
Fixes #69
This commit is contained in:
Christoph M. Wintersteiger 2015-05-21 18:12:14 +01:00
parent c422b48bf4
commit 8c18bdcca9
2 changed files with 25 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1586,9 +1586,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
mk_nzero(f, nzero); mk_nzero(f, nzero);
mk_pzero(f, pzero); mk_pzero(f, pzero);
expr_ref x_is_zero(m), x_is_pos(m); expr_ref x_is_zero(m), x_is_pos(m), x_is_neg(m);
mk_is_zero(x, x_is_zero); mk_is_zero(x, x_is_zero);
mk_is_pos(x, x_is_pos); mk_is_pos(x, x_is_pos);
mk_is_neg(x, x_is_neg);
dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero); dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero);
dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos); dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos);
@ -1655,9 +1656,13 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
mk_ite(c422, xone, v42, v42); mk_ite(c422, xone, v42, v42);
mk_ite(c421, xzero, v42, v42); mk_ite(c421, xzero, v42, v42);
mk_ite(m.mk_eq(a_sgn, one_1), nzero, pone, v4); expr_ref v4_rtn(m), v4_rtp(m);
mk_ite(m.mk_or(rm_is_rte, rm_is_rta), v42, v4, v4); mk_ite(x_is_neg, nzero, pone, v4_rtp);
mk_ite(m.mk_or(rm_is_rtz, rm_is_rtn), xzero, v4, v4); mk_ite(x_is_neg, none, pzero, v4_rtn);
mk_ite(rm_is_rtp, v4_rtp, v42, v4);
mk_ite(rm_is_rtn, v4_rtn, v4, v4);
mk_ite(rm_is_rtz, xzero, v4, v4);
SASSERT(is_well_sorted(m, v4)); SASSERT(is_well_sorted(m, v4));

26
src/util/mpf.cpp
View file

@ -1006,11 +1006,22 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
else if (is_zero(x)) else if (is_zero(x))
mk_zero(x.ebits, x.sbits, x.sign, o); // -0.0 -> -0.0, says IEEE754, Sec 5.9. mk_zero(x.ebits, x.sbits, x.sign, o); // -0.0 -> -0.0, says IEEE754, Sec 5.9.
else if (x.exponent < 0) { else if (x.exponent < 0) {
if (rm == MPF_ROUND_TOWARD_ZERO || if (rm == MPF_ROUND_TOWARD_ZERO)
rm == MPF_ROUND_TOWARD_NEGATIVE)
mk_zero(x.ebits, x.sbits, x.sign, o); mk_zero(x.ebits, x.sbits, x.sign, o);
else if (rm == MPF_ROUND_NEAREST_TEVEN || else if (rm == MPF_ROUND_TOWARD_NEGATIVE) {
rm == MPF_ROUND_NEAREST_TAWAY) { if (x.sign)
mk_one(x.ebits, x.sbits, true, o);
else
mk_zero(x.ebits, x.sbits, false, o);
}
else if (rm == MPF_ROUND_TOWARD_POSITIVE) {
if (x.sign)
mk_zero(x.ebits, x.sbits, true, o);
else
mk_one(x.ebits, x.sbits, false, o);
}
else {
SASSERT(rm == MPF_ROUND_NEAREST_TEVEN || rm == MPF_ROUND_NEAREST_TAWAY);
bool tie = m_mpz_manager.is_zero(x.significand) && x.exponent == -1; bool tie = m_mpz_manager.is_zero(x.significand) && x.exponent == -1;
TRACE("mpf_dbg", tout << "tie = " << tie << std::endl;); TRACE("mpf_dbg", tout << "tie = " << tie << std::endl;);
if (tie && rm == MPF_ROUND_NEAREST_TEVEN) if (tie && rm == MPF_ROUND_NEAREST_TEVEN)
@ -1022,13 +1033,6 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
else else
mk_one(x.ebits, x.sbits, x.sign, o); mk_one(x.ebits, x.sbits, x.sign, o);
} }
else {
SASSERT(rm == MPF_ROUND_TOWARD_POSITIVE);
if (x.sign)
mk_nzero(x.ebits, x.sbits, o);
else
mk_one(x.ebits, x.sbits, false, o);
}
} }
else if (x.exponent >= x.sbits - 1) else if (x.exponent >= x.sbits - 1)
set(o, x); set(o, x);