diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 83ba843ac..cc0fef3c3 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1072,7 +1072,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, result = y; mk_ite(lt, x, result, result); - mk_ite(both_zero, pzero, result, result); + mk_ite(both_zero, y, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1102,7 +1102,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, result = y; mk_ite(gt, x, result, result); - mk_ite(both_zero, pzero, result, result); + mk_ite(both_zero, y, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1586,9 +1586,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_nzero(f, nzero); 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_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_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(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); + expr_ref v4_rtn(m), v4_rtp(m); + mk_ite(x_is_neg, nzero, pone, v4_rtp); + 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)); @@ -3039,6 +3044,13 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { m_simp.mk_not(sig_is_zero, sig_is_not_zero); m_simp.mk_eq(exp, top_exp, exp_is_top); m_simp.mk_and(exp_is_top, sig_is_not_zero, result); + + // Inject auxiliary lemmas that fix e to the one and only NaN value, + // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation + // has a value to propagate. + m_extra_assertions.push_back(m.mk_eq(sgn, m_bv_util.mk_numeral(0, 1))); + m_extra_assertions.push_back(m.mk_eq(exp, top_exp)); + m_extra_assertions.push_back(m.mk_eq(sig, m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(sig)))); } void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) { diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 40021e330..37c42b494 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -412,7 +412,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) { - result = m_util.mk_pzero(m().get_sort(arg1)); + result = arg2; return BR_DONE; } @@ -421,7 +421,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { m().mk_ite(mk_eq_nan(arg2), arg1, m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), - m_util.mk_pzero(m().get_sort(arg1)), + arg2, m().mk_ite(m_util.mk_lt(arg1, arg2), arg1, arg2)))); @@ -438,7 +438,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) { - result = m_util.mk_pzero(m().get_sort(arg1)); + result = arg2; return BR_DONE; } @@ -447,7 +447,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { m().mk_ite(mk_eq_nan(arg2), arg1, m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), - m_util.mk_pzero(m().get_sort(arg1)), + arg2, m().mk_ite(m_util.mk_gt(arg1, arg2), arg1, arg2)))); diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 5a7f71987..78dd6f174 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -556,6 +556,20 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& rats){ extract_lcd(rats); } +void iz3mgr::get_broken_gcd_test_coeffs(const ast &proof, std::vector& rats){ + symb s = sym(proof); + int numps = s->get_num_parameters(); + rats.resize(numps-2); + for(int i = 2; i < numps; i++){ + rational r; + bool ok = s->get_parameter(i).is_rational(r); + if(!ok) + throw "Bad Farkas coefficient"; + rats[i-2] = r; + } + extract_lcd(rats); +} + void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& coeffs){ std::vector rats; get_assign_bounds_coeffs(proof,rats); diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 54fb35a0f..8d4479f8f 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -424,6 +424,8 @@ class iz3mgr { void get_farkas_coeffs(const ast &proof, std::vector& rats); + void get_broken_gcd_test_coeffs(const ast &proof, std::vector& rats); + void get_assign_bounds_coeffs(const ast &proof, std::vector& rats); void get_assign_bounds_coeffs(const ast &proof, std::vector& rats); diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index d1479e4cc..f510f4070 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1021,6 +1021,12 @@ public: my_coeffs.push_back(make_int(c)); my_prem_cons.push_back(conc(prem(proof,i))); } + else if(c.is_neg()){ + int j = (i % 2 == 0) ? i + 1 : i - 1; + my_prems.push_back(prems[j]); + my_coeffs.push_back(make_int(-coeffs[j])); + my_prem_cons.push_back(conc(prem(proof,j))); + } } ast my_con = sum_inequalities(my_coeffs,my_prem_cons); @@ -1884,7 +1890,7 @@ public: } case GCDTestKind: { std::vector farkas_coeffs; - get_farkas_coeffs(proof,farkas_coeffs); + get_broken_gcd_test_coeffs(proof,farkas_coeffs); if(farkas_coeffs.size() != nprems){ pfgoto(proof); throw unsupported(); diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.h b/src/muz/transforms/dl_mk_quantifier_instantiation.h index 138d5abee..37a5b8a6c 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.h +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.h @@ -26,8 +26,9 @@ Revision History: #define _DL_MK_QUANTIFIER_INSTANTIATION_H_ -#include"dl_rule_transformer.h" -#include"expr_safe_replace.h" +#include "dl_rule_transformer.h" +#include "expr_safe_replace.h" +#include "union_find.h" namespace datalog { @@ -37,75 +38,12 @@ namespace datalog { class mk_quantifier_instantiation : public rule_transformer::plugin { typedef svector > term_pairs; - class union_find { - unsigned_vector m_find; - unsigned_vector m_size; - unsigned_vector m_next; - - void ensure_size(unsigned v) { - while (v >= get_num_vars()) { - mk_var(); - } - } - public: - unsigned mk_var() { - unsigned r = m_find.size(); - m_find.push_back(r); - m_size.push_back(1); - m_next.push_back(r); - return r; - } - unsigned get_num_vars() const { return m_find.size(); } - - unsigned find(unsigned v) const { - if (v >= get_num_vars()) { - return v; - } - while (true) { - unsigned new_v = m_find[v]; - if (new_v == v) - return v; - v = new_v; - } - } - - unsigned next(unsigned v) const { - if (v >= get_num_vars()) { - return v; - } - return m_next[v]; - } - - bool is_root(unsigned v) const { - return v >= get_num_vars() || m_find[v] == v; - } - - void merge(unsigned v1, unsigned v2) { - unsigned r1 = find(v1); - unsigned r2 = find(v2); - if (r1 == r2) - return; - ensure_size(v1); - ensure_size(v2); - if (m_size[r1] > m_size[r2]) - std::swap(r1, r2); - m_find[r1] = r2; - m_size[r2] += m_size[r1]; - std::swap(m_next[r1], m_next[r2]); - } - - void reset() { - m_find.reset(); - m_next.reset(); - m_size.reset(); - } - }; ast_manager& m; context& m_ctx; expr_safe_replace m_var2cnst; expr_safe_replace m_cnst2var; - union_find m_uf; + basic_union_find m_uf; ptr_vector m_todo; ptr_vector m_terms; ptr_vector m_binding; diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index c45898cc7..4854b3c07 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -37,6 +37,7 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { mk_smt_tactic(), and_then( mk_fpa2bv_tactic(m, p), + mk_propagate_values_tactic(m, p), using_params(mk_simplify_tactic(m, p), simp_p), mk_bit_blaster_tactic(m, p), using_params(mk_simplify_tactic(m, p), simp_p), diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 40d20b644..b159cbdb6 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -338,8 +338,39 @@ void hwf_manager::sqrt(mpf_rounding_mode rm, hwf const & x, hwf & o) { void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o) { set_rounding_mode(rm); - modf(x.value, &o.value); - // Note: on x64, this sometimes produces an SNAN instead of a QNAN? + // CMW: modf is not the right function here. + // modf(x.value, &o.value); + + // According to the Intel Architecture manual, the x87-instrunction FRNDINT is the + // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions. + +#ifdef USE_INTRINSICS + switch (rm) { + case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break; + case 2: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_POS_INF)); break; + case 3: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEG_INF)); break; + case 4: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_ZERO)); break; + case 1: + UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware! + break; + default: + UNREACHABLE(); // Unknown rounding mode. + } +#else + NOT_IMPLEMENTED_YET(); +#endif + +#if 0 + double xv = x.value; + double & ov = o.value; + + __asm { + fld xv + frndint + fstp ov // Store result away. + } + +#endif } void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 1dab7b995..e66f6d270 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1006,11 +1006,22 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o else if (is_zero(x)) 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) + if (rm == MPF_ROUND_TOWARD_ZERO) mk_zero(x.ebits, x.sbits, x.sign, o); - else if (rm == MPF_ROUND_NEAREST_TEVEN || - rm == MPF_ROUND_NEAREST_TAWAY) { + else if (rm == MPF_ROUND_TOWARD_NEGATIVE) { + 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; TRACE("mpf_dbg", tout << "tie = " << tie << std::endl;); if (tie && rm == MPF_ROUND_NEAREST_TEVEN) @@ -1019,15 +1030,8 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & 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, 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); + mk_one(x.ebits, x.sbits, x.sign, o); } } else if (x.exponent >= x.sbits - 1) diff --git a/src/util/union_find.h b/src/util/union_find.h index 32de6846a..23d33a442 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -173,5 +173,71 @@ public: #endif }; + +class basic_union_find { + unsigned_vector m_find; + unsigned_vector m_size; + unsigned_vector m_next; + + void ensure_size(unsigned v) { + while (v >= get_num_vars()) { + mk_var(); + } + } + public: + unsigned mk_var() { + unsigned r = m_find.size(); + m_find.push_back(r); + m_size.push_back(1); + m_next.push_back(r); + return r; + } + unsigned get_num_vars() const { return m_find.size(); } + + unsigned find(unsigned v) const { + if (v >= get_num_vars()) { + return v; + } + while (true) { + unsigned new_v = m_find[v]; + if (new_v == v) + return v; + v = new_v; + } + } + + unsigned next(unsigned v) const { + if (v >= get_num_vars()) { + return v; + } + return m_next[v]; + } + + bool is_root(unsigned v) const { + return v >= get_num_vars() || m_find[v] == v; + } + + void merge(unsigned v1, unsigned v2) { + unsigned r1 = find(v1); + unsigned r2 = find(v2); + if (r1 == r2) + return; + ensure_size(v1); + ensure_size(v2); + if (m_size[r1] > m_size[r2]) + std::swap(r1, r2); + m_find[r1] = r2; + m_size[r2] += m_size[r1]; + std::swap(m_next[r1], m_next[r2]); + } + + void reset() { + m_find.reset(); + m_next.reset(); + m_size.reset(); + } +}; + + #endif /* _UNION_FIND_H_ */