From 73eb7cbf5c04869c171f190d00125449333ea095 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 5 May 2015 23:53:33 +0100 Subject: [PATCH 1/8] Bugfix for mpf roundToIntegral. Partially fixes #69 --- src/ast/rewriter/fpa_rewriter.cpp | 4 +- src/ast/rewriter/fpa_rewriter.h | 2 +- src/util/mpf.cpp | 92 +++++++++++++++++++++++++++---- src/util/mpf.h | 4 +- 4 files changed, 87 insertions(+), 15 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 5fb9dfd37..40021e330 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -70,7 +70,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break; case OP_FPA_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break; case OP_FPA_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break; - case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break; + case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break; case OP_FPA_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; case OP_FPA_LT: SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break; @@ -484,7 +484,7 @@ br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { return BR_FAILED; } -br_status fpa_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_fm); diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 2c76fad6a..2da839718 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -57,7 +57,7 @@ public: br_status mk_max(expr * arg1, expr * arg2, expr_ref & result); br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result); br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result); - br_status mk_round(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result); br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result); br_status mk_lt(expr * arg1, expr * arg2, expr_ref & result); br_status mk_gt(expr * arg1, expr * arg2, expr_ref & result); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 9de56773a..9b6db5213 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1003,9 +1003,30 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o mk_nan(x.ebits, x.sbits, o); else if (is_inf(x)) set(o, x); - else if (x.exponent < 0) + else if (is_zero(x)) mk_zero(x.ebits, x.sbits, x.sign, o); - else if (x.exponent >= x.sbits-1) + else if (x.exponent < 0) { + if (rm == MPF_ROUND_TOWARD_ZERO || + rm == MPF_ROUND_TOWARD_NEGATIVE) + mk_pzero(x.ebits, x.sbits, o); + else if (rm == MPF_ROUND_NEAREST_TEVEN || + rm == MPF_ROUND_NEAREST_TAWAY) { + bool tie = m_mpz_manager.is_zero(x.significand) && x.exponent == -1; + if (tie && rm == MPF_ROUND_NEAREST_TEVEN) + mk_pzero(x.ebits, x.sbits, o); + else if (tie && rm == MPF_ROUND_NEAREST_TAWAY) + mk_one(x.ebits, x.sbits, o); + else if (x.exponent < -1 || m_mpz_manager.lt(x.significand, m_powers2(x.sbits-2))) + mk_pzero(x.ebits, x.sbits, o); + else + mk_one(x.ebits, x.sbits, o); + } + else { + SASSERT(rm == MPF_ROUND_TOWARD_POSITIVE); + mk_one(x.ebits, x.sbits, o); + } + } + else if (x.exponent >= x.sbits - 1) set(o, x); else { SASSERT(x.exponent >= 0 && x.exponent < x.sbits-1); @@ -1016,21 +1037,62 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o scoped_mpf a(*this); set(a, x); - unpack(a, true); + unpack(a, true); // A includes hidden bit TRACE("mpf_dbg", tout << "A = " << to_string(a) << std::endl;); - + + SASSERT(m_mpz_manager.lt(a.significand(), m_powers2(x.sbits))); + SASSERT(m_mpz_manager.ge(a.significand(), m_powers2(x.sbits - 1))); + o.exponent = a.exponent(); m_mpz_manager.set(o.significand, a.significand()); - unsigned q = (unsigned) o.exponent; - unsigned shift = o.sbits-q-1; - TRACE("mpf_dbg", tout << "Q = " << q << " shift=" << shift << std::endl;); - m_mpz_manager.machine_div2k(o.significand, shift); - m_mpz_manager.mul2k(o.significand, shift+3); + unsigned shift = o.sbits - ((unsigned)o.exponent) - 1; + const mpz & shift_p = m_powers2(shift); + TRACE("mpf_dbg", tout << "shift=" << shift << std::endl;); + + scoped_mpz div(m_mpz_manager), rem(m_mpz_manager); + m_mpz_manager.machine_div_rem(o.significand, shift_p, div, rem); + TRACE("mpf_dbg", tout << "div=" << m_mpz_manager.to_string(div) << " rem=" << m_mpz_manager.to_string(rem) << std::endl;); - round(rm, o); - } + switch (rm) { + case MPF_ROUND_NEAREST_TEVEN: + case MPF_ROUND_NEAREST_TAWAY: { + scoped_mpz t(m_mpz_manager); + m_mpz_manager.mul2k(rem, 1, t); + bool tie = m_mpz_manager.eq(t, shift_p); + if (tie && + (rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) || + (rm == MPF_ROUND_NEAREST_TAWAY && m_mpz_manager.is_even(div))) + m_mpz_manager.inc(div); + else if (m_mpz_manager.gt(t, shift_p)) + m_mpz_manager.inc(div); + break; + } + case MPF_ROUND_TOWARD_POSITIVE: + if (!m_mpz_manager.is_zero(rem) && !o.sign) + m_mpz_manager.inc(div); + break; + case MPF_ROUND_TOWARD_NEGATIVE: + if (!m_mpz_manager.is_zero(rem) && o.sign) + m_mpz_manager.inc(div); + break; + case MPF_ROUND_TOWARD_ZERO: + default: + /* nothing */; + } + + m_mpz_manager.mul2k(div, shift, o.significand); + SASSERT(m_mpz_manager.ge(o.significand, m_powers2(o.sbits - 1))); + + // re-normalize + while (m_mpz_manager.ge(o.significand, m_powers2(o.sbits))) { + m_mpz_manager.machine_div2k(o.significand, 1); + o.exponent++; + } + + m_mpz_manager.sub(o.significand, m_powers2(o.sbits - 1), o.significand); // strip hidden bit + } TRACE("mpf_dbg", tout << "INTEGRAL = " << to_string(o) << std::endl;); } @@ -1449,6 +1511,14 @@ void mpf_manager::mk_nan(unsigned ebits, unsigned sbits, mpf & o) { o.sign = false; } +void mpf_manager::mk_one(unsigned ebits, unsigned sbits, mpf & o) const { + o.sbits = sbits; + o.ebits = ebits; + o.sign = false; + m_mpz_manager.set(o.significand, 0); + o.exponent = 0; +} + void mpf_manager::mk_max_value(unsigned ebits, unsigned sbits, bool sign, mpf & o) { o.sbits = sbits; o.ebits = ebits; diff --git a/src/util/mpf.h b/src/util/mpf.h index bac502c58..533944172 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -208,7 +208,9 @@ public: void to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o); -protected: +protected: + void mk_one(unsigned ebits, unsigned sbits, mpf & o) const; + bool has_bot_exp(mpf const & x); bool has_top_exp(mpf const & x); From 53b479e1c3dd79e4bdc64f96ea1a960132d9fae3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 6 May 2015 12:24:18 +0100 Subject: [PATCH 2/8] Bugfix for fp.rem(0, 0). Fixes #70. --- src/ast/fpa/fpa2bv_converter.cpp | 12 ++++++------ src/util/mpf.cpp | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 60120bea2..1543ce629 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -959,14 +959,14 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, c3 = y_is_inf; v3 = x; - // (x is 0) -> x - c4 = x_is_zero; - v4 = pzero; - // (y is 0) -> NaN. - c5 = y_is_zero; - v5 = nan; + c4 = y_is_zero; + v4 = nan; + // (x is 0) -> x + c5 = x_is_zero; + v5 = pzero; + // else the actual remainder. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 9b6db5213..428cfb318 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1161,10 +1161,10 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { mk_nan(x.ebits, x.sbits, o); else if (is_inf(y)) set(o, x); - else if (is_zero(x)) - set(o, x); else if (is_zero(y)) mk_nan(x.ebits, x.sbits, o); + else if (is_zero(x)) + set(o, x); else { o.ebits = x.ebits; o.sbits = x.sbits; From a63481de85d1237c5084d80479fc26b1f5ccafb9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 6 May 2015 19:18:29 +0100 Subject: [PATCH 3/8] New implementations of fp.roundToIntegral in mpf and fpa2bv. Partially fixes #69 --- src/ast/fpa/fpa2bv_converter.cpp | 189 ++++++++++++++++++++++++------- src/ast/fpa/fpa2bv_converter.h | 4 +- src/util/mpf.cpp | 31 ++--- src/util/mpf.h | 2 +- 4 files changed, 168 insertions(+), 58 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 1543ce629..cc189f462 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -359,6 +359,17 @@ void fpa2bv_converter::mk_pzero(func_decl *f, expr_ref & result) { result); } +void fpa2bv_converter::mk_one(func_decl *f, expr_ref sign, expr_ref & result) { + sort * srt = f->get_range(); + SASSERT(is_float(srt)); + unsigned sbits = m_util.get_sbits(srt); + unsigned ebits = m_util.get_ebits(srt); + mk_fp(sign, + m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits), + m_bv_util.mk_numeral(0, sbits-1), + result); +} + void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp, expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp) @@ -828,7 +839,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, mk_is_ninf(y, c5); mk_ite(x_is_inf, nan, xy_zero, v5); - // (y is 0) -> if (x is 0) then NaN else inf with xor sign. + // (y is 0) -> if (x is 0) then NaN else inf with xor sign. c6 = y_is_zero; expr_ref sgn_inf(m); mk_ite(signs_xor, ninf, pinf, sgn_inf); @@ -1556,10 +1567,17 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * rm = args[0]; x = args[1]; + expr_ref rm_is_rta(m), rm_is_rte(m), rm_is_rtp(m), rm_is_rtn(m), rm_is_rtz(m); + mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_rta); + mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_rte); + mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_rtp); + mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_rtn); + mk_is_rm(rm, BV_RM_TO_ZERO, rm_is_rtz); + expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); mk_nan(f, nan); mk_nzero(f, nzero); - mk_pzero(f, pzero); + mk_pzero(f, pzero); expr_ref x_is_zero(m), x_is_pos(m); mk_is_zero(x, x_is_zero); @@ -1568,74 +1586,161 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero); dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos); - expr_ref c1(m), c2(m), c3(m), c4(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m); + expr_ref c1(m), c2(m), c3(m), c4(m), c5(m); + expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m); + // (x is NaN) -> NaN mk_is_nan(x, c1); v1 = nan; + // (x is +-oo) -> x mk_is_inf(x, c2); v2 = x; + + // (x is +-0) -> x ; -0.0 -> -0.0, says IEEE754, Sec 5.9. + mk_is_zero(x, c3); + v3 = x; + + + expr_ref one_1(m), zero_1(m); + one_1 = m_bv_util.mk_numeral(1, 1); + zero_1 = m_bv_util.mk_numeral(0, 1); unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); - + dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig); dbg_decouple("fpa2bv_r2i_unpacked_exp", a_exp); - expr_ref exp_is_small(m), exp_h(m), one_1(m); - exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp); - one_1 = m_bv_util.mk_numeral(1, 1); - m_simp.mk_eq(exp_h, one_1, exp_is_small); - dbg_decouple("fpa2bv_r2i_exp_is_small", exp_is_small); - c3 = exp_is_small; - mk_ite(x_is_pos, pzero, nzero, v3); + expr_ref xzero(m); + mk_ite(m.mk_eq(a_sgn, one_1), nzero, pzero, xzero); + + // exponent < 0 -> 0/1 + expr_ref exp_lt_zero(m), exp_h(m); + exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp); + m_simp.mk_eq(exp_h, one_1, exp_lt_zero); + dbg_decouple("fpa2bv_r2i_exp_lt_zero", exp_lt_zero); + c4 = exp_lt_zero; + + expr_ref pone(m), none(m), xone(m), c421(m), c422(m), c423(m), t1(m), t2(m), tie(m), v42(m), exp_lt_m1(m); + mk_one(f, zero_1, pone); + mk_one(f, one_1, none); + mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone); + m_simp.mk_eq(a_sig, m_bv_util.mk_numeral(fu().fm().m_powers2(sbits-1), sbits), t1); + m_simp.mk_eq(a_exp, m_bv_util.mk_numeral(-1, ebits), t2); + m_simp.mk_and(t1, t2, tie); + dbg_decouple("fpa2bv_r2i_c42_tie", tie); + + m_simp.mk_and(tie, rm_is_rte, c421); + m_simp.mk_and(tie, rm_is_rta, c422); + c423 = m_bv_util.mk_sle(a_exp, m_bv_util.mk_numeral(-2, ebits)); + + dbg_decouple("fpa2bv_r2i_c421", c421); + dbg_decouple("fpa2bv_r2i_c422", c422); + dbg_decouple("fpa2bv_r2i_c423", c423); + + v42 = xone; + mk_ite(c423, xzero, v42, v42); + mk_ite(c422, xone, v42, v42); + mk_ite(c421, xzero, v42, v42); + + mk_ite(m.mk_eq(a_sgn, one_1), nzero, pone, v4); + mk_ite(m.mk_or(rm_is_rte, rm_is_rta), v42, v4, v4); + mk_ite(m.mk_or(rm_is_rtz, rm_is_rtn), xzero, v4, v4); + + SASSERT(is_well_sorted(m, v4)); + + // exponent >= sbits-1 expr_ref exp_is_large(m); exp_is_large = m_bv_util.mk_sle(m_bv_util.mk_numeral(sbits-1, ebits), a_exp); dbg_decouple("fpa2bv_r2i_exp_is_large", exp_is_large); - c4 = exp_is_large; - v4 = x; + c5 = exp_is_large; + v5 = x; + + // Actual conversion with rounding. + // x.exponent >= 0 && x.exponent < x.sbits - 1 - // The actual rounding. expr_ref res_sgn(m), res_sig(m), res_exp(m); res_sgn = a_sgn; - res_exp = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 2), a_exp); + res_exp = a_exp; - expr_ref shift(m), r_shifted(m), l_shifted(m); - shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits-1, ebits+1), - m_bv_util.mk_sign_extend(1, a_exp)); - if (sbits > (ebits+1)) - r_shifted = m_bv_util.mk_bv_lshr(a_sig, m_bv_util.mk_zero_extend(sbits-(ebits+1), shift)); - else if (sbits < (ebits+1)) - r_shifted = m_bv_util.mk_extract(ebits, ebits-sbits+1, m_bv_util.mk_bv_lshr(m_bv_util.mk_zero_extend(ebits+1-sbits, a_sig), shift)); - else // sbits == ebits+1 - r_shifted = m_bv_util.mk_bv_lshr(a_sig, shift); - SASSERT(is_well_sorted(m, r_shifted)); - SASSERT(m_bv_util.get_bv_size(r_shifted) == sbits); + expr_ref shift(m), rshift(m), div(m), rem(m); + shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits - 1, sbits + 1), + m_bv_util.mk_sign_extend(sbits - ebits + 1, a_exp)); + rshift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits, sbits + 1), shift); + div = m_bv_util.mk_bv_lshr(m_bv_util.mk_zero_extend(1, a_sig), shift); + rem = m_bv_util.mk_bv_lshr(m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(1, a_sig), rshift), rshift); - if (sbits > (ebits+1)) - l_shifted = m_bv_util.mk_bv_shl(r_shifted, m_bv_util.mk_zero_extend(sbits-(ebits+1), shift)); - else if (sbits < (ebits+1)) - l_shifted = m_bv_util.mk_extract(ebits, ebits-sbits+1, m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(ebits+1-sbits, r_shifted), shift)); - else // sbits == ebits+1 - l_shifted = m_bv_util.mk_bv_shl(r_shifted, shift); - SASSERT(is_well_sorted(m, l_shifted)); - SASSERT(m_bv_util.get_bv_size(l_shifted) == sbits); + SASSERT(is_well_sorted(m, div)); + SASSERT(is_well_sorted(m, rem)); + SASSERT(m_bv_util.get_bv_size(div) == sbits + 1); + SASSERT(m_bv_util.get_bv_size(rem) == sbits + 1); - res_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), - m_bv_util.mk_concat(l_shifted, - m_bv_util.mk_numeral(0, 3))); + dbg_decouple("fpa2bv_r2i_shift", shift); + dbg_decouple("fpa2bv_r2i_rshift", rshift); + dbg_decouple("fpa2bv_r2i_div", div); + dbg_decouple("fpa2bv_r2i_rem", rem); - SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4)); + expr_ref div_p1(m); + div_p1 = m_bv_util.mk_bv_add(div, m_bv_util.mk_numeral(1, sbits+1)); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v5); + expr_ref tie2(m), tie2_c(m), div_last(m), v51(m), rem_shl(m); + rem_shl = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits - 1, 0, rem), zero_1); + m_simp.mk_eq(rem_shl, + m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits+1), shift), + tie2); + div_last = m_bv_util.mk_extract(0, 0, div); + tie2_c = m.mk_or(m.mk_and(tie2, + m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)), + m.mk_and(rm_is_rta, m.mk_eq(div_last, zero_1)))), + m.mk_xor(m.mk_eq(a_sgn, one_1), + m_bv_util.mk_sle(m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits + 1), shift), + rem_shl))); + m_simp.mk_ite(tie2_c, div_p1, div, v51); + + dbg_decouple("fpa2bv_r2i_v51", v51); + dbg_decouple("fpa2bv_r2i_tie2", tie2); + + SASSERT(is_well_sorted(m, tie2)); + SASSERT(is_well_sorted(m, tie2_c)); + SASSERT(is_well_sorted(m, v51)); + + expr_ref c521(m), v52(m); + m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c521); + m_simp.mk_and(c521, m.mk_eq(res_sgn, zero_1), c521); + m_simp.mk_ite(c521, div_p1, div, v52); + + expr_ref c531(m), v53(m); + m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c531); + m_simp.mk_and(c531, m.mk_eq(res_sgn, one_1), c531); + m_simp.mk_ite(c531, div_p1, div, v53); + + expr_ref c51(m), c52(m), c53(m); + c51 = m.mk_or(rm_is_rte, rm_is_rta); + c52 = rm_is_rtp; + c53 = rm_is_rtn; + + res_sig = div; + m_simp.mk_ite(c53, v53, res_sig, res_sig); + m_simp.mk_ite(c52, v52, res_sig, res_sig); + m_simp.mk_ite(c51, v51, res_sig, res_sig); + res_sig = m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3)); // rounding bits are all 0. + res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), m_bv_util.mk_extract(ebits+1, 0, shift)); + + SASSERT(m_bv_util.get_bv_size(res_sgn) == 1); + SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4); + SASSERT(m_bv_util.get_bv_size(res_exp) == ebits+2); + + // CMW: We use the rounder for normalization. + round(f->get_range(), rm, res_sgn, res_sig, res_exp, v6); // And finally, we tie them together. - mk_ite(c4, v4, v5, result); + mk_ite(c5, v5, v6, result); + mk_ite(c4, v4, result, result); mk_ite(c3, v3, result, result); mk_ite(c2, v2, result, result); mk_ite(c1, v1, result, result); @@ -3239,7 +3344,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef Z3DEBUG - return; + // return; // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e)); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index fa797b610..4b3c1a6ca 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -92,7 +92,7 @@ public: void mk_ninf(func_decl * f, expr_ref & result); void mk_nan(func_decl * f, expr_ref & result); void mk_nzero(func_decl *f, expr_ref & result); - void mk_pzero(func_decl *f, expr_ref & result); + void mk_pzero(func_decl *f, expr_ref & result); void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -151,6 +151,8 @@ public: expr_ref_vector m_extra_assertions; protected: + void mk_one(func_decl *f, expr_ref sign, expr_ref & result); + void mk_is_nan(expr * e, expr_ref & result); void mk_is_inf(expr * e, expr_ref & result); void mk_is_pinf(expr * e, expr_ref & result); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 428cfb318..4940fa448 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1004,26 +1004,29 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o else if (is_inf(x)) set(o, x); else if (is_zero(x)) - mk_zero(x.ebits, x.sbits, x.sign, o); + mk_zero(x.ebits, x.sbits, x.sign, o); // -0.0 -> -0.0, says IEEE754, Sec 5.9. else if (x.exponent < 0) { if (rm == MPF_ROUND_TOWARD_ZERO || rm == MPF_ROUND_TOWARD_NEGATIVE) - mk_pzero(x.ebits, x.sbits, o); + mk_zero(x.ebits, x.sbits, x.sign, o); else if (rm == MPF_ROUND_NEAREST_TEVEN || rm == MPF_ROUND_NEAREST_TAWAY) { bool tie = m_mpz_manager.is_zero(x.significand) && x.exponent == -1; if (tie && rm == MPF_ROUND_NEAREST_TEVEN) - mk_pzero(x.ebits, x.sbits, o); + mk_zero(x.ebits, x.sbits, x.sign, o); else if (tie && rm == MPF_ROUND_NEAREST_TAWAY) - mk_one(x.ebits, x.sbits, o); - else if (x.exponent < -1 || m_mpz_manager.lt(x.significand, m_powers2(x.sbits-2))) - mk_pzero(x.ebits, x.sbits, o); + mk_one(x.ebits, x.sbits, x.sign, o); + else if (x.exponent < -1) + mk_zero(x.ebits, x.sbits, x.sign, o); else - mk_one(x.ebits, x.sbits, o); + mk_one(x.ebits, x.sbits, x.sign, o); } else { SASSERT(rm == MPF_ROUND_TOWARD_POSITIVE); - mk_one(x.ebits, x.sbits, o); + 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) @@ -1049,7 +1052,7 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o unsigned shift = o.sbits - ((unsigned)o.exponent) - 1; const mpz & shift_p = m_powers2(shift); - TRACE("mpf_dbg", tout << "shift=" << shift << std::endl;); + TRACE("mpf_dbg", tout << "shift=" << shift << std::endl;); scoped_mpz div(m_mpz_manager), rem(m_mpz_manager); m_mpz_manager.machine_div_rem(o.significand, shift_p, div, rem); @@ -1065,16 +1068,16 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o (rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) || (rm == MPF_ROUND_NEAREST_TAWAY && m_mpz_manager.is_even(div))) m_mpz_manager.inc(div); - else if (m_mpz_manager.gt(t, shift_p)) + else if (x.sign ^ m_mpz_manager.gt(t, shift_p)) m_mpz_manager.inc(div); break; } case MPF_ROUND_TOWARD_POSITIVE: - if (!m_mpz_manager.is_zero(rem) && !o.sign) + if (!m_mpz_manager.is_zero(rem) && o.sign) m_mpz_manager.inc(div); break; case MPF_ROUND_TOWARD_NEGATIVE: - if (!m_mpz_manager.is_zero(rem) && o.sign) + if (!m_mpz_manager.is_zero(rem) && !o.sign) m_mpz_manager.inc(div); break; case MPF_ROUND_TOWARD_ZERO: @@ -1511,10 +1514,10 @@ void mpf_manager::mk_nan(unsigned ebits, unsigned sbits, mpf & o) { o.sign = false; } -void mpf_manager::mk_one(unsigned ebits, unsigned sbits, mpf & o) const { +void mpf_manager::mk_one(unsigned ebits, unsigned sbits, bool sign, mpf & o) const { o.sbits = sbits; o.ebits = ebits; - o.sign = false; + o.sign = sign; m_mpz_manager.set(o.significand, 0); o.exponent = 0; } diff --git a/src/util/mpf.h b/src/util/mpf.h index 533944172..ef87ca0b7 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -209,7 +209,7 @@ public: void to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o); protected: - void mk_one(unsigned ebits, unsigned sbits, mpf & o) const; + void mk_one(unsigned ebits, unsigned sbits, bool sign, mpf & o) const; bool has_bot_exp(mpf const & x); bool has_top_exp(mpf const & x); From 6645358fedb36e7966e3d1a8d22d834d04430e6d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 10 May 2015 22:30:07 +0000 Subject: [PATCH 4/8] fix issue #57: undefined behavior in bit_vector.h --- src/util/bit_vector.h | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 6738ba0aa..43b0e9619 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -75,8 +75,11 @@ public: bit_vector(bit_vector const & source): m_num_bits(source.m_num_bits), m_capacity(source.m_capacity), - m_data(alloc_svect(unsigned, source.m_capacity)) { - memcpy(m_data, source.m_data, source.m_capacity * sizeof(unsigned)); + m_data(0) { + if (source.m_data) { + m_data = alloc_svect(unsigned, m_capacity); + memcpy(m_data, source.m_data, m_capacity * sizeof(unsigned)); + } } bit_vector(unsigned const * source, int num_bits): @@ -183,6 +186,9 @@ public: bool operator!=(bit_vector const & other) const { return !operator==(other); } bit_vector & operator=(bit_vector const & source) { + if (!source.m_data) + return *this; + m_num_bits = source.m_num_bits; if (m_capacity < source.m_capacity) { dealloc_svect(m_data); From 091ae37c06eb8875f4cf939d676ac15fd455cd0d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 11 May 2015 04:44:11 +0100 Subject: [PATCH 5/8] Fix bug in my previous patch in bit_vector::operator=() Signed-off-by: Nuno Lopes --- src/util/bit_vector.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 43b0e9619..f7af2019d 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -186,10 +186,10 @@ public: bool operator!=(bit_vector const & other) const { return !operator==(other); } bit_vector & operator=(bit_vector const & source) { + m_num_bits = source.m_num_bits; if (!source.m_data) return *this; - m_num_bits = source.m_num_bits; if (m_capacity < source.m_capacity) { dealloc_svect(m_data); m_data = alloc_svect(unsigned, source.m_capacity); From 379ce66391a2d1de57424b8b99dfa22dc290130b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 11 May 2015 06:30:24 +0100 Subject: [PATCH 6/8] fix a few undefined behaviors exposed by the unit tests Signed-off-by: Nuno Lopes --- src/util/bit_util.cpp | 2 +- src/util/mpff.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/bit_util.cpp b/src/util/bit_util.cpp index 0f1fd294d..fde66b054 100644 --- a/src/util/bit_util.cpp +++ b/src/util/bit_util.cpp @@ -351,7 +351,7 @@ bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k) { } if (word_sz < sz) { unsigned bit_sz = k % (8 * sizeof(unsigned)); - unsigned mask = (1 << bit_sz) - 1; + unsigned mask = (1u << bit_sz) - 1; return (data[word_sz] & mask) != 0; } return false; diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index b979b32ff..14c67e7c0 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -255,7 +255,7 @@ void mpff_manager::set(mpff & n, int64 v) { } else { if (v < 0) { - set(n, static_cast(-v)); + set(n, -static_cast(v)); n.m_sign = 1; } else { @@ -680,7 +680,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c // Make sure that a and b have the same exponent. if (exp_a > exp_b) { - unsigned shift = exp_a - exp_b; + unsigned shift = (unsigned)exp_a - (unsigned)exp_b; n_sig_b = m_buffers[0].c_ptr(); shr(m_precision, sig_b, shift, m_precision, n_sig_b); if (sgn_b != m_to_plus_inf && has_one_at_first_k_bits(m_precision, sig_b, shift)) { From 043f441a4c1c37cbbc253a6d41446cbeca74040f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 12 May 2015 10:29:37 +0100 Subject: [PATCH 7/8] Python 3.x compatibility. Fixes problems reported in comments to 1abeb825a35a620ff27a409a8d09d676e1395d95 --- scripts/mk_win_dist.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index db4cc48e3..fb42750e3 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -180,7 +180,7 @@ def mk_dist_dir_core(x64): mk_util.JAVA_ENABLED = JAVA_ENABLED mk_win_dist(build_path, dist_path) if is_verbose(): - print("Generated %s distribution folder at '%s'") % (platform, dist_path) + print("Generated %s distribution folder at '%s'" % (platform, dist_path)) def mk_dist_dir(): mk_dist_dir_core(False) @@ -208,7 +208,7 @@ def mk_zip_core(x64): ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED) os.path.walk(dist_path, mk_zip_visitor, '*') if is_verbose(): - print("Generated '%s'") % zfname + print("Generated '%s'" % zfname) except: pass ZIPOUT = None @@ -253,7 +253,7 @@ def cp_vs_runtime_core(x64): for f in VS_RUNTIME_FILES: shutil.copy(f, bin_dist_path) if is_verbose(): - print("Copied '%s' to '%s'") % (f, bin_dist_path) + print("Copied '%s' to '%s'" % (f, bin_dist_path)) def cp_vs_runtime(): cp_vs_runtime_core(True) From ce749240d7f1951244131e2365276813b04db2d8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 12 May 2015 18:43:51 +0100 Subject: [PATCH 8/8] more fixes for python 3 Signed-off-by: Nuno Lopes --- scripts/mk_util.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 72d432eab..207ac4c8c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -248,16 +248,16 @@ def test_fpmath(cc): t.add('int main() { return 42; }\n') t.commit() if exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0: - FPMATH_FLAGS="-mfpmath=sse -msse -msse2" + FPMATH_FLAGS="-mfpmath=sse -msse -msse2" return "SSE2-GCC" elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0: - FPMATH_FLAGS="-msse -msse2" + FPMATH_FLAGS="-msse -msse2" return "SSE2-CLANG" elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0: - FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard" + FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard" return "ARM-VFP" else: - FPMATH_FLAGS="" + FPMATH_FLAGS="" return "UNKNOWN" @@ -1841,7 +1841,7 @@ def mk_config(): CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH) CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS FPMATH = test_fpmath(CXX) - CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) + CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) HAS_OMP = test_openmp(CXX) if HAS_OMP: CXXFLAGS = '%s -fopenmp' % CXXFLAGS