From 03f6b465b968deb860943b020b3b5df55f1430ef Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 31 May 2016 16:14:50 +0100 Subject: [PATCH 1/6] comment typos --- src/ast/act_cache.cpp | 2 +- src/smt/smt_internalizer.cpp | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/act_cache.cpp b/src/ast/act_cache.cpp index 0ee0afaac..1d1341184 100644 --- a/src/ast/act_cache.cpp +++ b/src/ast/act_cache.cpp @@ -40,7 +40,7 @@ Notes: The number of unused entries (m_unused) is equal to the number of entries of the form t -> (s, 0) - That is, it is the number of keys that were never accessed by cliend code. + That is, it is the number of keys that were never accessed by client code. The cache maintains at most m_max_unused entries. When the maximum number of unused entries exceeds m_max_unused, then diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index a420d85d9..df80d3281 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -656,10 +656,10 @@ namespace smt { /** \brief Enable the flag m_merge_tf in the given enode. When the flag m_merge_tf is enabled, the enode n will be merged with the - true_enode (false_enode) whenever the boolean variable v is + true_enode (false_enode) whenever the Boolean variable v is assigned to true (false). - If is_new_var is true, then trail is not created for the flag uodate. + If is_new_var is true, then trail is not created for the flag update. */ void context::set_merge_tf(enode * n, bool_var v, bool is_new_var) { SASSERT(bool_var2enode(v) == n); @@ -674,8 +674,8 @@ namespace smt { } /** - \brief Trail object to disable the m_enode flag of a boolean - variable. The flag m_enode is true for a boolean variable v, + \brief Trail object to disable the m_enode flag of a Boolean + variable. The flag m_enode is true for a Boolean variable v, if there is an enode n associated with it. */ class set_enode_flag_trail : public trail { From 302c4915351b1a3fbbaf328d747230e9d3c2e8e8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 31 May 2016 16:22:24 +0100 Subject: [PATCH 2/6] theory_fpa refactoring --- src/smt/theory_fpa.cpp | 76 ++++++++++++++++++++---------------------- src/smt/theory_fpa.h | 1 - 2 files changed, 36 insertions(+), 41 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index ca939a1e8..215260607 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -35,6 +35,7 @@ namespace smt { virtual void undo(theory_fpa & th) { expr * val = m_map.find(key); m_map.remove(key); + m.dec_ref(key); m.dec_ref(val); key = 0; } @@ -125,18 +126,17 @@ namespace smt { if (m_is_initialized) { ast_manager & m = get_manager(); - dec_ref_map_values(m, m_conversions); - dec_ref_map_values(m, m_wraps); - dec_ref_collection_values(m, m_is_added_to_model); - } - else { - SASSERT(m_trail_stack.get_num_scopes() == 0); - SASSERT(m_conversions.empty()); - SASSERT(m_wraps.empty()); - SASSERT(m_is_added_to_model.empty()); - } + dec_ref_map_key_values(m, m_conversions); + dec_ref_collection_values(m, m_is_added_to_model); - m_is_initialized = false; + m_converter.reset(); + m_rw.reset(); + m_th_rw.reset(); + } + + SASSERT(m_trail_stack.get_num_scopes() == 0); + SASSERT(m_conversions.empty()); + SASSERT(m_is_added_to_model.empty()); } void theory_fpa::init(context * ctx) { @@ -261,28 +261,21 @@ namespace smt { m_th_rw((expr_ref&)res); } else { - sort * e_srt = m.get_sort(e); - func_decl * w; + sort * es = m.get_sort(e); - if (!m_wraps.find(e_srt, w)) { - SASSERT(!m_wraps.contains(e_srt)); - - sort * bv_srt; - if (m_converter.is_rm(e_srt)) - bv_srt = m_bv_util.mk_sort(3); - else { - SASSERT(m_converter.is_float(e_srt)); - unsigned ebits = m_fpa_util.get_ebits(e_srt); - unsigned sbits = m_fpa_util.get_sbits(e_srt); - bv_srt = m_bv_util.mk_sort(ebits + sbits); - } - - w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); - m_wraps.insert(e_srt, w); - m.inc_ref(w); + sort_ref bv_srt(m); + if (m_converter.is_rm(es)) + bv_srt = m_bv_util.mk_sort(3); + else { + SASSERT(m_converter.is_float(es)); + unsigned ebits = m_fpa_util.get_ebits(es); + unsigned sbits = m_fpa_util.get_sbits(es); + bv_srt = m_bv_util.mk_sort(ebits + sbits); } - res = m.mk_app(w, e); + func_decl_ref wrap_fd(m); + wrap_fd = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &es, bv_srt); + res = m.mk_app(wrap_fd, e); } return res; @@ -398,6 +391,7 @@ namespace smt { mk_ismt2_pp(res, m) << std::endl;); m_conversions.insert(e, res); + m.inc_ref(e); m.inc_ref(res); m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); } @@ -422,7 +416,6 @@ namespace smt { res = m.mk_and(res, t); } m_converter.m_extra_assertions.reset(); - m_th_rw(res); CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << std::endl;); @@ -678,19 +671,23 @@ namespace smt { mpf_rounding_mode rm; scoped_mpf val(mpfm); if (m_fpa_util.is_rm_numeral(n, rm)) { - c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3)); + expr_ref rm_num(m); + rm_num = m_bv_util.mk_numeral(rm, 3); + c = m.mk_eq(wrapped, rm_num); assert_cnstr(c); } else if (m_fpa_util.is_numeral(n, val)) { - expr_ref bv_val_e(m); + expr_ref bv_val_e(m), cc_args(m); bv_val_e = convert(n); SASSERT(is_app(bv_val_e)); SASSERT(to_app(bv_val_e)->get_num_args() == 3); - app_ref bv_val_a(to_app(bv_val_e.get()), m); + app_ref bv_val_a(m); + bv_val_a = to_app(bv_val_e.get()); expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) }; - c = m.mk_eq(wrapped, m_bv_util.mk_concat(3, args)); - c = m.mk_and(c, mk_side_conditions()); + cc_args = m_bv_util.mk_concat(3, args); + c = m.mk_eq(wrapped, cc_args); assert_cnstr(c); + assert_cnstr(mk_side_conditions()); } else { expr_ref wu(m); @@ -714,11 +711,10 @@ namespace smt { m_converter.reset(); m_rw.reset(); m_th_rw.reset(); - m_trail_stack.pop_scope(m_trail_stack.get_num_scopes()); - if (m_factory) dealloc(m_factory); m_factory = 0; + m_trail_stack.pop_scope(m_trail_stack.get_num_scopes()); ast_manager & m = get_manager(); - dec_ref_map_values(m, m_conversions); - dec_ref_map_values(m, m_wraps); + dec_ref_map_key_values(m, m_conversions); + dec_ref_collection_values(m, m_is_added_to_model); theory::reset_eh(); } diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 0a3ed94c6..32fcfcffc 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -144,7 +144,6 @@ namespace smt { fpa_util & m_fpa_util; bv_util & m_bv_util; arith_util & m_arith_util; - obj_map m_wraps; obj_map m_conversions; bool m_is_initialized; obj_hashtable m_is_added_to_model; From 47e75827ee6122e99f7631c92d21d3beae3db924 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 31 May 2016 16:22:48 +0100 Subject: [PATCH 3/6] theory_fpa refactoring --- src/smt/theory_fpa.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 215260607..6038867aa 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -132,13 +132,13 @@ namespace smt { m_converter.reset(); m_rw.reset(); m_th_rw.reset(); + m_is_initialized = false; } SASSERT(m_trail_stack.get_num_scopes() == 0); SASSERT(m_conversions.empty()); - SASSERT(m_is_added_to_model.empty()); - } - + SASSERT(m_is_added_to_model.empty()); + } void theory_fpa::init(context * ctx) { smt::theory::init(ctx); m_is_initialized = true; @@ -710,10 +710,11 @@ namespace smt { pop_scope_eh(m_trail_stack.get_num_scopes()); m_converter.reset(); m_rw.reset(); - m_th_rw.reset(); + m_th_rw.reset(); m_trail_stack.pop_scope(m_trail_stack.get_num_scopes()); + if (m_factory) dealloc(m_factory); m_factory = 0; ast_manager & m = get_manager(); - dec_ref_map_key_values(m, m_conversions); + dec_ref_map_key_values(m, m_conversions); dec_ref_collection_values(m, m_is_added_to_model); theory::reset_eh(); } From ade2dbe15a314e22fd124e7ec937d6505dc117ec Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 31 May 2016 16:47:14 +0100 Subject: [PATCH 4/6] Cache cleanup fix for bv_simplifier_plugin. Fixes #615 --- src/ast/simplifier/bv_simplifier_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp index 45fee07e4..11ed1b9e0 100644 --- a/src/ast/simplifier/bv_simplifier_plugin.cpp +++ b/src/ast/simplifier/bv_simplifier_plugin.cpp @@ -418,7 +418,7 @@ void bv_simplifier_plugin::mk_extract(unsigned high, unsigned low, expr* arg, ex mk_extract_core(high, low, arg, result); } if (m_extract_cache.size() > (1 << 12)) { - m_extract_cache.reset(); + flush_caches(); } TRACE("bv_simplifier_plugin", tout << "mk_extract [" << high << ":" << low << "]\n"; From b3b5c6226b8425d0bbc2f863e01eb8299ad8d820 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 2 Jun 2016 17:12:24 +0100 Subject: [PATCH 5/6] MPF code simplification --- src/util/mpf.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 0fcff0da0..d77b8c33f 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1304,7 +1304,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex // 3. Compute Y*Q / Y*QQ*2^{D-N} - bool YQ_sgn = y.sign ^ Q_sgn; + bool YQ_sgn = x.sign; scoped_mpz YQ_sig(m_mpz_manager); mpf_exp_t YQ_exp = Q_exp + y.exponent; m_mpz_manager.mul(y.significand, Q_sig, YQ_sig); @@ -1360,9 +1360,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex bool neg = m_mpz_manager.is_neg(X_YQ_sig); if (neg) m_mpz_manager.neg(X_YQ_sig); - bool X_YQ_sgn = ((!x.sign && !YQ_sgn && neg) || - (x.sign && YQ_sgn && !neg) || - (x.sign && !YQ_sgn)); + bool X_YQ_sgn = x.sign ^ neg; // 5. Rounding if (m_mpz_manager.is_zero(X_YQ_sig)) From 83ad5d65e4ad34fd9790d4c81fc4cd0a6d8a9362 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 2 Jun 2016 20:22:02 +0100 Subject: [PATCH 6/6] Replaced fp.rem conversion to bit-vectors with an SMT-compliant one. Fixes #561 --- src/ast/fpa/fpa2bv_converter.cpp | 201 +++++++++++++++++++++++++------ src/ast/fpa/fpa2bv_converter.h | 7 ++ 2 files changed, 168 insertions(+), 40 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 97d18bcf2..f32e82dd3 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -25,7 +25,6 @@ Notes: #include"fpa2bv_converter.h" #define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); } -#define BVSLT(X,Y,R) { expr_ref bvslt_eq(m), bvslt_not(m); m_simp.mk_eq(X, Y, bvslt_eq); m_simp.mk_not(bvslt_eq, bvslt_not); expr_ref t(m); t = m_bv_util.mk_sle(X,Y); m_simp.mk_and(t, bvslt_not, R); } fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m(m), @@ -125,10 +124,12 @@ void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * ar SASSERT(num == 0); SASSERT(f->get_num_parameters() == 1); SASSERT(f->get_parameter(0).is_external()); - unsigned p_id = f->get_parameter(0).get_ext_id(); mpf const & v = m_plugin->get_value(p_id); + mk_numeral(f->get_range(), v, result); +} +void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) { unsigned sbits = v.get_sbits(); unsigned ebits = v.get_ebits(); @@ -137,12 +138,12 @@ void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * ar mpf_exp_t const & exp = m_util.fm().exp(v); if (m_util.fm().is_nan(v)) - mk_nan(f, result); + mk_nan(s, result); else if (m_util.fm().is_inf(v)) { if (m_util.fm().sgn(v)) - mk_ninf(f, result); + mk_ninf(s, result); else - mk_pinf(f, result); + mk_pinf(s, result); } else { expr_ref bv_sgn(m), bv_sig(m), e(m), biased_exp(m); @@ -1012,15 +1013,17 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r mk_ninf(s, ninf); mk_pinf(s, pinf); - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); - expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); + expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m); + expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m); mk_is_nan(x, x_is_nan); mk_is_zero(x, x_is_zero); mk_is_pos(x, x_is_pos); + mk_is_neg(x, x_is_neg); mk_is_inf(x, x_is_inf); mk_is_nan(y, y_is_nan); mk_is_zero(y, y_is_zero); mk_is_pos(y, y_is_pos); + mk_is_neg(y, y_is_neg); mk_is_inf(y, y_is_inf); dbg_decouple("fpa2bv_rem_x_is_nan", x_is_nan); @@ -1054,34 +1057,120 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r // (x is 0) -> x c5 = x_is_zero; v5 = pzero; - + // exp(x) < exp(y) -> x + unsigned ebits = m_util.get_ebits(s); + unsigned sbits = m_util.get_sbits(s); expr * x_sgn, *x_sig, *x_exp; expr * y_sgn, *y_sig, *y_exp; split_fp(x, x_sgn, x_exp, x_sig); split_fp(y, y_sgn, y_exp, y_sig); - BVSLT(x_exp, y_exp, c6); + expr_ref one_ebits(m), y_exp_m1(m), xe_lt_yem1(m), ye_neq_zero(m); + one_ebits = m_bv_util.mk_numeral(1, ebits); + y_exp_m1 = m_bv_util.mk_bv_sub(y_exp, one_ebits); + BVULT(x_exp, y_exp_m1, xe_lt_yem1); + ye_neq_zero = m.mk_not(m.mk_eq(y_exp, m_bv_util.mk_numeral(0, ebits))); + c6 = m.mk_and(ye_neq_zero, xe_lt_yem1); v6 = x; - // else the actual remainder, r = x - y * n - expr_ref rne(m), nr(m), n(m), yn(m), r(m); - rne = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); - mk_div(s, rne, x, y, nr); - mk_round_to_integral(s, rne, nr, n); - mk_mul(s, rne, y, n, yn); - mk_sub(s, rne, x, yn, r); + expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); + expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m); + unpack(x, a_sgn, a_sig, a_exp, a_lz, true); + unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - expr_ref r_is_zero(m), x_sgn_ref(x_sgn, m), x_sgn_zero(m); - mk_is_zero(r, r_is_zero); - mk_zero(s, x_sgn_ref, x_sgn_zero); - mk_ite(r_is_zero, x_sgn_zero, r, v7); + dbg_decouple("fpa2bv_rem_a_sgn", a_sgn); + dbg_decouple("fpa2bv_rem_a_sig", a_sig); + dbg_decouple("fpa2bv_rem_a_exp", a_exp); + dbg_decouple("fpa2bv_rem_a_lz", a_lz); + dbg_decouple("fpa2bv_rem_b_sgn", b_sgn); + dbg_decouple("fpa2bv_rem_b_sig", b_sig); + dbg_decouple("fpa2bv_rem_b_exp", b_exp); + dbg_decouple("fpa2bv_rem_b_lz", b_lz); - dbg_decouple("fpa2bv_rem_nr", nr); - dbg_decouple("fpa2bv_rem_n", n); - dbg_decouple("fpa2bv_rem_yn", yn); - dbg_decouple("fpa2bv_rem_r", r); - dbg_decouple("fpa2bv_rem_v7", v7); + // else the actual remainder. + // max. exponent difference is (2^ebits) - 3 + const mpz & two_to_ebits = fu().fm().m_powers2(ebits); + mpz max_exp_diff; + m_mpz_manager.sub(two_to_ebits, 3, max_exp_diff); + SASSERT(m_mpz_manager.is_int64(max_exp_diff)); + SASSERT(m_mpz_manager.get_uint64(max_exp_diff) <= UINT_MAX); + uint64 max_exp_diff_ui64 = m_mpz_manager.get_uint64(max_exp_diff); + SASSERT(max_exp_diff_ui64 <= UINT32_MAX); + unsigned max_exp_diff_ui = (unsigned)max_exp_diff_ui64; + m_mpz_manager.del(max_exp_diff); + + expr_ref a_exp_ext(m), b_exp_ext(m); + a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp); + b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); + + expr_ref a_lz_ext(m), b_lz_ext(m); + a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); + b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); + + expr_ref exp_diff(m), neg_exp_diff(m), exp_diff_is_neg(m); + exp_diff = m_bv_util.mk_bv_sub( + m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), + m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); + neg_exp_diff = m_bv_util.mk_bv_neg(exp_diff); + exp_diff_is_neg = m_bv_util.mk_sle(exp_diff, m_bv_util.mk_numeral(0, ebits+2)); + dbg_decouple("fpa2bv_rem_exp_diff", exp_diff); + + // CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal, + // but calculating this via rem = x - y * nearest(x/y) creates huge + // circuits, too. Lazy instantiation seems the way to go in the long run + // (using the lazy bit-blaster helps on simple instances). + expr_ref a_sig_ext(m), b_sig_ext(m), lshift(m), rshift(m), shifted(m), huge_rem(m); + a_sig_ext = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(max_exp_diff_ui, a_sig), m_bv_util.mk_numeral(0, 3)); + b_sig_ext = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(max_exp_diff_ui, b_sig), m_bv_util.mk_numeral(0, 3)); + lshift = m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - (ebits+2) + 3, exp_diff); + rshift = m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - (ebits+2) + 3, neg_exp_diff); + shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift), + m_bv_util.mk_bv_shl(a_sig_ext, lshift)); + huge_rem = m_bv_util.mk_bv_urem(shifted, b_sig_ext); + dbg_decouple("fpa2bv_rem_huge_rem", huge_rem); + + expr_ref rndd_sgn(m), rndd_exp(m), rndd_sig(m), rne_bv(m), rndd(m); + rndd_sgn = a_sgn; + rndd_exp = m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext); + rndd_sig = m_bv_util.mk_extract(sbits+3, 0, huge_rem); + rne_bv = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); + round(s, rne_bv, rndd_sgn, rndd_sig, rndd_exp, rndd); + + expr_ref y_half(m), ny_half(m), zero_e(m), two_e(m); + expr_ref y_half_is_zero(m), y_half_is_nz(m); + expr_ref r_ge_y_half(m), r_gt_ny_half(m), r_le_y_half(m), r_lt_ny_half(m); + expr_ref r_ge_zero(m), r_le_zero(m); + expr_ref rounded_sub_y(m), rounded_add_y(m); + mpf zero, two; + m_mpf_manager.set(two, ebits, sbits, 2); + m_mpf_manager.set(zero, ebits, sbits, 0); + mk_numeral(s, two, two_e); + mk_numeral(s, zero, zero_e); + mk_div(s, rne_bv, y, two_e, y_half); + mk_neg(s, y_half, ny_half); + mk_is_zero(y_half, y_half_is_zero); + y_half_is_nz = m.mk_not(y_half_is_zero); + + mk_float_ge(s, rndd, y_half, r_ge_y_half); + mk_float_gt(s, rndd, ny_half, r_gt_ny_half); + mk_float_le(s, rndd, y_half, r_le_y_half); + mk_float_lt(s, rndd, ny_half, r_lt_ny_half); + + mk_sub(s, rne_bv, rndd, y, rounded_sub_y); + mk_add(s, rne_bv, rndd, y, rounded_add_y); + + expr_ref sub_cnd(m), add_cnd(m); + sub_cnd = m.mk_and(y_half_is_nz, + m.mk_or(m.mk_and(y_is_pos, r_ge_y_half), + m.mk_and(y_is_neg, r_le_y_half))); + add_cnd = m.mk_and(y_half_is_nz, + m.mk_or(m.mk_and(y_is_pos, r_lt_ny_half), + m.mk_and(y_is_neg, r_gt_ny_half))); + + mk_ite(add_cnd, rounded_add_y, rndd, v7); + mk_ite(sub_cnd, rounded_sub_y, v7, v7); + // And finally, we tie them together. mk_ite(c6, v6, v7, result); mk_ite(c5, v5, result, result); @@ -1102,9 +1191,15 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); - expr * sgn, * s, * e; - split_fp(args[0], sgn, e, s); - result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), e, s); + expr_ref x(m); + x = args[0]; + mk_abs(f->get_range(), x, result); +} + +void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) { + expr * sgn, *sig, *exp; + split_fp(x, sgn, exp, sig); + result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), exp, sig); } void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -1954,11 +2049,15 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); + expr_ref x(m), y(m); + x = args[0]; + y = args[1]; + mk_float_eq(f->get_range(), x, y, result); +} - expr * x = args[0], * y = args[1]; - +void fpa2bv_converter::mk_float_eq(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) { TRACE("fpa2bv_float_eq", tout << "X = " << mk_ismt2_pp(x, m) << std::endl; - tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;); + tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;); expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m); mk_is_nan(x, x_is_nan); @@ -1992,9 +2091,13 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); + expr_ref x(m), y(m); + x = args[0]; + y = args[1]; + mk_float_lt(f->get_range(), x, y, result); +} - expr * x = args[0], * y = args[1]; - +void fpa2bv_converter::mk_float_lt(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) { expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m); mk_is_nan(x, x_is_nan); mk_is_nan(y, y_is_nan); @@ -2039,11 +2142,15 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a void fpa2bv_converter::mk_float_gt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); + expr_ref x(m), y(m); + x = args[0]; + y = args[1]; + mk_float_gt(f->get_range(), x, y, result); +} - expr * x = args[0], * y = args[1]; - +void fpa2bv_converter::mk_float_gt(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) { expr_ref t3(m); - mk_float_le(f, num, args, t3); + mk_float_le(s, x, y, t3); expr_ref nan_or(m), xy_zero(m), not_t3(m), r_else(m); expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m); @@ -2060,17 +2167,31 @@ void fpa2bv_converter::mk_float_gt(func_decl * f, unsigned num, expr * const * a void fpa2bv_converter::mk_float_le(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); + expr_ref x(m), y(m); + x = args[0]; + y = args[1]; + mk_float_le(f->get_range(), x, y, result); +} + +void fpa2bv_converter::mk_float_le(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) { expr_ref a(m), b(m); - mk_float_lt(f, num, args, a); - mk_float_eq(f, num, args, b); + mk_float_lt(s, x, y, a); + mk_float_eq(s, x, y, b); m_simp.mk_or(a, b, result); } void fpa2bv_converter::mk_float_ge(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); + expr_ref x(m), y(m); + x = args[0]; + y = args[1]; + mk_float_ge(f->get_range(), x, y, result); +} + +void fpa2bv_converter::mk_float_ge(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) { expr_ref a(m), b(m); - mk_float_gt(f, num, args, a); - mk_float_eq(f, num, args, b); + mk_float_gt(s, x, y, a); + mk_float_eq(s, x, y, b); m_simp.mk_or(a, b, result); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index d056a3642..45030b301 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -79,6 +79,7 @@ public: void mk_rounding_mode(decl_kind k, expr_ref & result); void mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_numeral(sort * s, mpf const & v, expr_ref & result); virtual void mk_const(func_decl * f, expr_ref & result); virtual void mk_rm_const(func_decl * f, expr_ref & result); virtual void mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -100,12 +101,18 @@ public: void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_abs(sort * s, expr_ref & x, expr_ref & result); void mk_float_eq(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_float_gt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_float_le(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_float_ge(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_float_eq(sort * s, expr_ref & x, expr_ref & y, expr_ref & result); + void mk_float_lt(sort * s, expr_ref & x, expr_ref & y, expr_ref & result); + void mk_float_gt(sort *, expr_ref & x, expr_ref & y, expr_ref & result); + void mk_float_le(sort * s, expr_ref & x, expr_ref & y, expr_ref & result); + void mk_float_ge(sort * s, expr_ref & x, expr_ref & y, expr_ref & result); void mk_is_zero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);