diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index b11e2c3ac..2600cb3ec 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -324,8 +324,12 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, family_id bvfid = m_bv_util.get_fid(); expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); - res_sgn_c1 = m.mk_app(bvfid, OP_BAND, m_bv_util.mk_bv_not(c_sgn), d_sgn, sign_bv); - res_sgn_c2 = m.mk_app(bvfid, OP_BAND, c_sgn, m_bv_util.mk_bv_not(d_sgn), m_bv_util.mk_bv_not(sign_bv)); + expr_ref not_c_sgn(m), not_d_sgn(m), not_sign_bv(m); + not_c_sgn = m_bv_util.mk_bv_not(c_sgn); + not_d_sgn = m_bv_util.mk_bv_not(d_sgn); + not_sign_bv = m_bv_util.mk_bv_not(sign_bv); + res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_c_sgn, d_sgn, sign_bv); + res_sgn_c2 = m.mk_app(bvfid, OP_BAND, c_sgn, not_d_sgn, not_sign_bv); res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn); expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); @@ -398,10 +402,14 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, m_simp.mk_and(x_is_inf, xy_is_neg, v3_and); mk_ite(v3_and, nan, y, v3); - expr_ref rm_is_to_neg(m), v4_and(m); + expr_ref rm_is_to_neg(m), signs_and(m), signs_xor(m), v4_and(m), rm_and_xor(m), neg_cond(m); m_simp.mk_and(x_is_zero, y_is_zero, c4); + m_simp.mk_and(x_is_neg, y_is_neg, signs_and); + m_simp.mk_xor(x_is_neg, y_is_neg, signs_xor); mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - mk_ite(rm_is_to_neg, nzero, pzero, v4); + m_simp.mk_and(rm_is_to_neg, signs_xor, rm_and_xor); + m_simp.mk_or(signs_and, rm_and_xor, neg_cond); + mk_ite(neg_cond, nzero, pzero, v4); m_simp.mk_and(x_is_neg, y_is_neg, v4_and); mk_ite(v4_and, x, v4, v4); @@ -665,8 +673,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_div_y_is_pos", y_is_pos); dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf); - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); + expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m); + expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m); // (x is NaN) || (y is NaN) -> NaN m_simp.mk_or(x_is_nan, y_is_nan, c1); @@ -701,6 +709,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); mk_ite(x_is_zero, nan, x_sgn_inf, v6); + // (x is 0) -> result is zero with sgn = x.sgn^y.sgn + // This is a special case to avoid problems with the unpacking of zero. + c7 = x_is_zero; + mk_ite(signs_xor, nzero, pzero, v7); + // else comes the actual division. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); @@ -738,10 +751,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4)); - round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); + round(f->get_range(), rm, res_sgn, res_sig, res_exp, v8); // And finally, we tie them together. - mk_ite(c6, v6, v7, result); + mk_ite(c7, v7, v8, result); + mk_ite(c6, v6, result, result); mk_ite(c5, v5, result, result); mk_ite(c4, v4, result, result); mk_ite(c3, v3, result, result); @@ -805,7 +819,7 @@ void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const * // (x is 0) -> x c4 = x_is_zero; - v4 = x; + v4 = pzero; // (y is 0) -> NaN. c5 = y_is_zero; @@ -1674,13 +1688,15 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref denormal_exp = m_bv_util.mk_numeral(1, ebits); mk_unbias(denormal_exp, denormal_exp); + dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp); + if (normalize) { expr_ref is_sig_zero(m), shift(m), lz(m), zero_s(m), zero_e(m); zero_s = m_bv_util.mk_numeral(0, sbits-1); zero_e = m_bv_util.mk_numeral(0, ebits); m_simp.mk_eq(zero_s, sig, is_sig_zero); mk_leading_zeros(sig, ebits, lz); - m_simp.mk_ite(is_sig_zero, zero_e, lz, shift); + m_simp.mk_ite(is_sig_zero, zero_e, lz, shift); SASSERT(is_well_sorted(m, is_sig_zero)); SASSERT(is_well_sorted(m, lz)); SASSERT(is_well_sorted(m, shift)); @@ -1688,7 +1704,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref if (ebits <= sbits) { expr_ref q(m); q = m_bv_util.mk_zero_extend(sbits-ebits, shift); - denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q); + denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q); } else { // the maximum shift is `sbits', because after that the mantissa @@ -1701,8 +1717,9 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref m_simp.mk_eq(zero_s, sh, is_sh_zero); short_shift = m_bv_util.mk_extract(sbits-1, 0, shift); m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl); - denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl); + denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl); } + denormal_exp = m_bv_util.mk_bv_sub(denormal_exp, shift); } SASSERT(is_well_sorted(m, normal_sig)); @@ -1710,6 +1727,8 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref SASSERT(is_well_sorted(m, normal_exp)); SASSERT(is_well_sorted(m, denormal_exp)); + dbg_decouple("fpa2bv_unpack_is_normal", is_normal); + m_simp.mk_ite(is_normal, normal_sig, denormal_sig, sig); m_simp.mk_ite(is_normal, normal_exp, denormal_exp, exp); diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 219172b34..8585e7eda 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -117,14 +117,14 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, char const * value) { std::string v(value); size_t e_pos = v.find('p'); if (e_pos == std::string::npos) e_pos = v.find('P'); - + std::string f, e; - + f = (e_pos != std::string::npos) ? v.substr(0, e_pos) : v; e = (e_pos != std::string::npos) ? v.substr(e_pos+1) : "0"; - + TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;); - + mpq q; m_mpq_manager.set(q, f.c_str()); @@ -132,14 +132,14 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, char const * value) { m_mpz_manager.set(ex, e.c_str()); set(o, rm, q, ex); - + TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;); } void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mpz const & exponent) { // Assumption: this represents significand * 2^exponent. set_rounding_mode(rm); - + mpq sig; m_mpq_manager.set(sig, significand); int64 exp = m_mpz_manager.get_int64(exponent); @@ -349,7 +349,7 @@ void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) { else o.value = fmod(x.value, y.value); -// Here is an x87 alternative if the above makes problems; this may also be faster. + // Here is an x87 alternative if the above makes problems; this may also be faster. #if 0 double xv = x.value; double yv = y.value; @@ -434,7 +434,7 @@ void hwf_manager::display_smt2(std::ostream & out, hwf const & a, bool decimal) void hwf_manager::to_rational(hwf const & x, unsynch_mpq_manager & qm, mpq & o) { SASSERT(is_normal(x) || is_denormal(x) || is_zero(x)); scoped_mpz n(qm), d(qm); - + if (is_normal(x)) qm.set(n, sig(x) | 0x0010000000000000ull); else @@ -466,7 +466,7 @@ bool hwf_manager::is_neg(hwf const & x) { bool hwf_manager::is_pos(hwf const & x) { return !sgn(x) && !is_nan(x); } - + bool hwf_manager::is_nzero(hwf const & x) { return RAW(x.value) == 0x8000000000000000ull; } @@ -581,20 +581,20 @@ void hwf_manager::mk_ninf(hwf & o) { #ifdef _WINDOWS #if defined(_AMD64_) || defined(_M_IA64) - #ifdef USE_INTRINSICS - #define SETRM(RM) _MM_SET_ROUNDING_MODE(RM) - #else - #define SETRM(RM) _controlfp_s(&sse2_state, RM, _MCW_RC); - #endif +#ifdef USE_INTRINSICS +#define SETRM(RM) _MM_SET_ROUNDING_MODE(RM) #else - #ifdef USE_INTRINSICS - #define SETRM(RM) _MM_SET_ROUNDING_MODE(RM) - #else - #define SETRM(RM) __control87_2(RM, _MCW_RC, &x86_state, &sse2_state) - #endif +#define SETRM(RM) _controlfp_s(&sse2_state, RM, _MCW_RC); #endif #else - #define SETRM(RM) fesetround(RM) +#ifdef USE_INTRINSICS +#define SETRM(RM) _MM_SET_ROUNDING_MODE(RM) +#else +#define SETRM(RM) __control87_2(RM, _MCW_RC, &x86_state, &sse2_state) +#endif +#endif +#else +#define SETRM(RM) fesetround(RM) #endif unsigned hwf_manager::prev_power_of_two(hwf const & a) { @@ -608,9 +608,28 @@ unsigned hwf_manager::prev_power_of_two(hwf const & a) { void hwf_manager::set_rounding_mode(mpf_rounding_mode rm) { -#ifdef _WINDOWS +#ifdef _WINDOWS +#ifdef USE_INTRINSICS switch (rm) { - case MPF_ROUND_NEAREST_TEVEN: + case MPF_ROUND_NEAREST_TEVEN: + SETRM(_MM_ROUND_NEAREST); + break; + case MPF_ROUND_TOWARD_POSITIVE: + SETRM(_MM_ROUND_UP); + break; + case MPF_ROUND_TOWARD_NEGATIVE: + SETRM(_MM_ROUND_DOWN); + break; + case MPF_ROUND_TOWARD_ZERO: + SETRM(_MM_ROUND_TOWARD_ZERO); + break; + case MPF_ROUND_NEAREST_TAWAY: + default: + UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware! + } +#else + switch (rm) { + case MPF_ROUND_NEAREST_TEVEN: SETRM(_RC_NEAR); break; case MPF_ROUND_TOWARD_POSITIVE: @@ -626,6 +645,7 @@ void hwf_manager::set_rounding_mode(mpf_rounding_mode rm) default: UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware! } +#endif #else // OSX/Linux switch (rm) { case MPF_ROUND_NEAREST_TEVEN: diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 6c542f1af..9618ffbce 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -520,9 +520,8 @@ void mpf_manager::add_sub(mpf_rounding_mode rm, mpf const & x, mpf const & y, mp } } else if (is_zero(x) && is_zero(y)) { - if (sgn(x) && sgn_y) - set(o, x); - else if (rm == MPF_ROUND_TOWARD_NEGATIVE) + if ((x.sign && sgn_y) || + ((rm == MPF_ROUND_TOWARD_NEGATIVE) && (x.sign != sgn_y))) mk_nzero(x.ebits, x.sbits, o); else mk_pzero(x.ebits, x.sbits, o); @@ -627,29 +626,28 @@ void mpf_manager::mul(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & if (is_zero(y)) mk_nan(x.ebits, x.sbits, o); else - mk_inf(x.ebits, x.sbits, sgn(y), o); + mk_inf(x.ebits, x.sbits, y.sign, o); } else if (is_pinf(y)) { if (is_zero(x)) mk_nan(x.ebits, x.sbits, o); else - mk_inf(x.ebits, x.sbits, sgn(x), o); + mk_inf(x.ebits, x.sbits, x.sign, o); } else if (is_ninf(x)) { if (is_zero(y)) mk_nan(x.ebits, x.sbits, o); else - mk_inf(x.ebits, x.sbits, !sgn(y), o); + mk_inf(x.ebits, x.sbits, !y.sign, o); } else if (is_ninf(y)) { if (is_zero(x)) mk_nan(x.ebits, x.sbits, o); else - mk_inf(x.ebits, x.sbits, !sgn(x), o); + mk_inf(x.ebits, x.sbits, !x.sign, o); } else if (is_zero(x) || is_zero(y)) { - set(o, x); - o.sign = x.sign ^ y.sign; + mk_zero(x.ebits, x.sbits, x.sign != y.sign, o); } else { o.ebits = x.ebits; @@ -699,31 +697,35 @@ void mpf_manager::div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & if (is_inf(y)) mk_nan(x.ebits, x.sbits, o); else - mk_inf(x.ebits, x.sbits, sgn(y), o); + mk_inf(x.ebits, x.sbits, y.sign, o); } else if (is_pinf(y)) { if (is_inf(x)) mk_nan(x.ebits, x.sbits, o); else - mk_zero(x.ebits, x.sbits, (x.sign ^ y.sign) == 1, o); + mk_zero(x.ebits, x.sbits, x.sign != y.sign, o); } else if (is_ninf(x)) { if (is_inf(y)) mk_nan(x.ebits, x.sbits, o); else - mk_inf(x.ebits, x.sbits, !sgn(y), o); + mk_inf(x.ebits, x.sbits, !y.sign, o); } else if (is_ninf(y)) { if (is_inf(x)) mk_nan(x.ebits, x.sbits, o); else - mk_zero(x.ebits, x.sbits, (x.sign ^ y.sign) == 1, o); + mk_zero(x.ebits, x.sbits, x.sign != y.sign, o); } else if (is_zero(y)) { if (is_zero(x)) mk_nan(x.ebits, x.sbits, o); else - mk_inf(x.ebits, x.sbits, sgn(x), o); + mk_inf(x.ebits, x.sbits, x.sign != y.sign, o); + } + else if (is_zero(x)) { + // Special case to avoid problems with unpacking of zeros. + mk_zero(x.ebits, x.sbits, x.sign != y.sign, o); } else { o.ebits = x.ebits; @@ -837,6 +839,10 @@ void mpf_manager::sqrt(mpf_rounding_mode rm, mpf const & x, mpf & o) { else mk_nzero(x.ebits, x.sbits, o); } + else if (is_pzero(x)) + mk_pzero(x.ebits, x.sbits, o); + else if (is_nzero(x)) + mk_nzero(x.ebits, x.sbits, o); else { o.ebits = x.ebits; o.sbits = x.sbits; @@ -933,7 +939,7 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { else if (is_inf(y)) set(o, x); else if (is_zero(x)) - set(o, x); + mk_pzero(x.ebits, x.sbits, o); else if (is_zero(y)) mk_nan(x.ebits, x.sbits, o); else { @@ -982,9 +988,9 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) { if (is_nan(x)) set(o, y); - else if (is_nan(y) || (sgn(y) && is_zero(x) && is_zero(y))) - set(o, x); - else if (gt(x, y)) + else if (is_nan(y)) + set(o, x); + else if (gt(x, y) || (is_zero(x) && is_nzero(y))) set(o, x); else set(o, y); @@ -993,9 +999,9 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) { void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) { if (is_nan(x)) set(o, y); - else if (is_nan(y) || (sgn(x) && is_zero(x) && is_zero(y))) + else if (is_nan(y)) set(o, x); - else if (lt(x, y)) + else if (lt(x, y) || (is_nzero(x) && is_zero(y))) set(o, x); else set(o, y);