From 2a75f1d71e221f4984ecc2ca93c90ccf5b7f508d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Feb 2013 19:14:52 -0800 Subject: [PATCH 01/11] update logging for hilbert Signed-off-by: Nikolaj Bjorner --- src/muz_qe/heap_trie.h | 8 ++++---- src/muz_qe/hilbert_basis.cpp | 20 +++++++++++--------- 2 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/muz_qe/heap_trie.h b/src/muz_qe/heap_trie.h index e50a85505..a99861359 100644 --- a/src/muz_qe/heap_trie.h +++ b/src/muz_qe/heap_trie.h @@ -518,7 +518,7 @@ private: SASSERT(m_keys.size() == num_keys()); iterator it = begin(); trie* new_root = mk_trie(); - IF_VERBOSE(1, verbose_stream() << "before reshuffle: " << m_root->num_nodes() << " nodes\n";); + IF_VERBOSE(2, verbose_stream() << "before reshuffle: " << m_root->num_nodes() << " nodes\n";); for (; it != end(); ++it) { IF_VERBOSE(2, for (unsigned i = 0; i < num_keys(); ++i) { @@ -539,7 +539,7 @@ private: m_keys[i] = new_keys[i]; } - IF_VERBOSE(1, verbose_stream() << "after reshuffle: " << new_root->num_nodes() << " nodes\n";); + IF_VERBOSE(2, verbose_stream() << "after reshuffle: " << new_root->num_nodes() << " nodes\n";); IF_VERBOSE(2, it = begin(); for (; it != end(); ++it) { @@ -559,7 +559,7 @@ private: if (index == num_keys()) { SASSERT(n->ref_count() > 0); bool r = check(to_leaf(n)->get_value()); - IF_VERBOSE(1, + IF_VERBOSE(2, for (unsigned j = 0; j < index; ++j) { verbose_stream() << " "; } @@ -572,7 +572,7 @@ private: for (unsigned i = 0; i < nodes.size(); ++i) { ++m_stats.m_num_find_le_nodes; node* m = nodes[i].second; - IF_VERBOSE(1, + IF_VERBOSE(2, for (unsigned j = 0; j < index; ++j) { verbose_stream() << " "; } diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 49bf20746..bc06aa15e 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -21,6 +21,7 @@ Revision History: #include "heap.h" #include "map.h" #include "heap_trie.h" +#include "stopwatch.h" template class rational_map : public map {}; @@ -777,9 +778,18 @@ lbool hilbert_basis::saturate() { init_basis(); m_current_ineq = 0; while (!m_cancel && m_current_ineq < m_ineqs.size()) { - IF_VERBOSE(1, { statistics st; collect_statistics(st); st.display(verbose_stream()); }); select_inequality(); + stopwatch sw; + sw.start(); lbool r = saturate(m_ineqs[m_current_ineq], m_iseq[m_current_ineq]); + IF_VERBOSE(1, + { statistics st; + collect_statistics(st); + st.display(verbose_stream()); + sw.stop(); + verbose_stream() << "time: " << sw.get_seconds() << "\n"; + }); + ++m_stats.m_num_saturations; if (r != l_true) { return r; @@ -933,14 +943,6 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) { m_free_list.push_back(m_basis.back()); m_basis.pop_back(); } - for (unsigned i = 0; i < init_basis_size; ++i) { - offset_t idx = m_basis[i]; - if (vec(idx).weight().is_neg()) { - m_basis[i] = m_basis.back(); - m_basis.pop_back(); - - } - } m_basis.append(m_zero); std::sort(m_basis.begin(), m_basis.end(), vector_lt_t(*this)); m_zero.reset(); From 6f3850bfbcb7565043c08c6b32476d2c63b22358 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 28 Feb 2013 18:46:29 +0000 Subject: [PATCH 02/11] FPA bug and leak fixes (thanks to Gabriele Paganelli) Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 10 +- src/tactic/fpa/fpa2bv_converter.cpp | 634 ++++++++++++++++------------ src/tactic/fpa/fpa2bv_converter.h | 42 +- src/tactic/fpa/fpa2bv_rewriter.h | 4 +- src/tactic/fpa/fpa2bv_tactic.cpp | 2 +- 5 files changed, 397 insertions(+), 295 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 7f6d7f764..f2d6591dc 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -151,6 +151,10 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) { m_manager->raise_exception("expecting two integer parameters to floating point sort"); } + if (parameters[0].get_int() <= 1 || parameters[1].get_int() <= 1) + m_manager->raise_exception("floating point sorts need parameters > 1"); + if (parameters[0].get_int() > parameters[1].get_int()) + m_manager->raise_exception("floating point sorts with ebits > sbits are currently not supported"); return mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); case ROUNDING_MODE_SORT: return mk_rm_sort(); @@ -349,14 +353,14 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) m_manager->raise_exception("expecting two integer parameters to asFloat"); if (arity != 2 && arity != 3) - m_manager->raise_exception("invalid number of arguments to asFloat operator"); - if (!is_rm_sort(domain[0]) || domain[1] != m_real_sort) + m_manager->raise_exception("invalid number of arguments to asFloat operator"); + if (!is_rm_sort(domain[0]) || domain[1] != m_real_sort) m_manager->raise_exception("sort mismatch"); if (arity == 2) { sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 4afdc501f..b11e2c3ac 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -21,15 +21,15 @@ 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); m_simp.mk_and(m_bv_util.mk_ule(X,Y), 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); m_simp.mk_and(m_bv_util.mk_sle(X,Y), bvslt_not, R); } +#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), m_simp(m), m_util(m), - m_mpf_manager(m_util.fm()), - m_mpz_manager(m_mpf_manager.mpz_manager()), + m_mpf_manager(m_util.fm()), + m_mpz_manager(m_mpf_manager.mpz_manager()), m_bv_util(m), extra_assertions(m) { m_plugin = static_cast(m.get_plugin(m.mk_family_id("float"))); @@ -37,7 +37,7 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) : fpa2bv_converter::~fpa2bv_converter() { dec_ref_map_key_values(m, m_const2bv); - dec_ref_map_key_values(m, m_rm_const2bv); + dec_ref_map_key_values(m, m_rm_const2bv); } void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { @@ -123,17 +123,23 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) { unsigned ebits = m_util.get_ebits(srt); unsigned sbits = m_util.get_sbits(srt); + expr_ref sgn(m), s(m), e(m); + sort_ref s_sgn(m), s_sig(m), s_exp(m); + s_sgn = m_bv_util.mk_sort(1); + s_sig = m_bv_util.mk_sort(sbits-1); + s_exp = m_bv_util.mk_sort(ebits); + #ifdef _DEBUG std::string p("fpa2bv"); std::string name = f->get_name().str(); - expr * sgn = m.mk_fresh_const((p + "_sgn_" + name).c_str(), m_bv_util.mk_sort(1)); - expr * s = m.mk_fresh_const((p + "_sig_" + name).c_str(), m_bv_util.mk_sort(sbits-1)); - expr * e = m.mk_fresh_const((p + "_exp_" + name).c_str(), m_bv_util.mk_sort(ebits)); + sgn = m.mk_fresh_const((p + "_sgn_" + name).c_str(), s_sgn); + s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig); + e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp); #else - expr * sgn = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - expr * s = m.mk_fresh_const(0, m_bv_util.mk_sort(sbits-1)); - expr * e = m.mk_fresh_const(0, m_bv_util.mk_sort(ebits)); + sgn = m.mk_fresh_const(0, s_sgn); + s = m.mk_fresh_const(0, s_sig); + e = m.mk_fresh_const(0, s_exp); #endif mk_triple(sgn, s, e, result); @@ -153,7 +159,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) { result = r; } else { - SASSERT(is_rm_sort(f->get_range())); + SASSERT(is_rm_sort(f->get_range())); result = m.mk_fresh_const( #ifdef _DEBUG @@ -245,9 +251,10 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, dbg_decouple("fpa2bv_add_exp_delta", exp_delta); // cap the delta - expr_ref cap(m); + expr_ref cap(m), cap_le_delta(m); cap = m_bv_util.mk_numeral(sbits+2, ebits); - m_simp.mk_ite(m_bv_util.mk_ule(cap, exp_delta), cap, exp_delta, exp_delta); + cap_le_delta = m_bv_util.mk_ule(cap, exp_delta); + m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta); dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta); @@ -270,20 +277,22 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, SASSERT(is_well_sorted(m, shifted_d_sig)); sticky_raw = m_bv_util.mk_extract(sbits+2, 0, shifted_big); - expr_ref sticky_eq(m); - m_simp.mk_eq(sticky_raw, m_bv_util.mk_numeral(0, sbits+3), sticky_eq); - m_simp.mk_ite(sticky_eq, - m_bv_util.mk_numeral(0, sbits+3), - m_bv_util.mk_numeral(1, sbits+3), - sticky); + expr_ref sticky_eq(m), nil_sbit3(m), one_sbit3(m); + nil_sbit3 = m_bv_util.mk_numeral(0, sbits+3); + one_sbit3 = m_bv_util.mk_numeral(1, sbits+3); + m_simp.mk_eq(sticky_raw, nil_sbit3, sticky_eq); + m_simp.mk_ite(sticky_eq, nil_sbit3, one_sbit3, sticky); SASSERT(is_well_sorted(m, sticky)); - expr * or_args[2] = { shifted_d_sig.get(), sticky.get() }; + expr * or_args[2] = { shifted_d_sig, sticky }; shifted_d_sig = m_bv_util.mk_bv_or(2, or_args); SASSERT(is_well_sorted(m, shifted_d_sig)); - expr_ref eq_sgn(m), neq_sgn(m); - m_simp.mk_eq(c_sgn, d_sgn, eq_sgn); + expr_ref eq_sgn(m); + m_simp.mk_eq(c_sgn, d_sgn, eq_sgn); + + // dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn); + TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; ); // two extra bits for catching the overflow. c_sig = m_bv_util.mk_zero_extend(2, c_sig); @@ -311,19 +320,20 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, dbg_decouple("fpa2bv_add_sign_bv", sign_bv); dbg_decouple("fpa2bv_add_n_sum", n_sum); - - family_id bvfid = m_bv_util.get_fid(); + + 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)); res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn); - expr * res_sgn_or_args[3] = { res_sgn_c1.get(), res_sgn_c2.get(), res_sgn_c3.get() }; + 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); - expr_ref res_sig_eq(m), sig_abs(m); - m_simp.mk_eq(sign_bv, m_bv_util.mk_numeral(1, 1), res_sig_eq); - m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs); + expr_ref res_sig_eq(m), sig_abs(m), one_1(m); + one_1 = m_bv_util.mk_numeral(1, 1); + m_simp.mk_eq(sign_bv, one_1, res_sig_eq); + m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs); dbg_decouple("fpa2bv_add_sig_abs", sig_abs); @@ -333,9 +343,9 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm, void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; + + expr_ref rm(m), x(m), y(m); + rm = args[0]; x = args[1]; y = args[2]; @@ -391,7 +401,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref rm_is_to_neg(m), v4_and(m); m_simp.mk_and(x_is_zero, y_is_zero, c4); mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); - mk_ite(rm_is_to_neg, nzero, pzero, v4); + mk_ite(rm_is_to_neg, nzero, pzero, v4); m_simp.mk_and(x_is_neg, y_is_neg, v4_and); mk_ite(v4_and, x, v4, v4); @@ -432,8 +442,9 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp, res_sgn, res_sig, res_exp); - expr_ref is_zero_sig(m); - m_simp.mk_eq(res_sig, m_bv_util.mk_numeral(0, sbits+4), is_zero_sig); + expr_ref is_zero_sig(m), nil_sbit4(m); + nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4); + m_simp.mk_eq(res_sig, nil_sbit4, is_zero_sig); SASSERT(is_well_sorted(m, is_zero_sig)); @@ -463,7 +474,7 @@ void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, SASSERT(num == 3); expr_ref t(m); mk_uminus(f, 1, &args[2], t); - expr * nargs[3] = { args[0], args[1], t.get() }; + expr * nargs[3] = { args[0], args[1], t }; mk_add(f, 3, nargs, result); } @@ -481,9 +492,9 @@ void fpa2bv_converter::mk_uminus(func_decl * f, unsigned num, expr * const * arg void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; + + expr_ref rm(m), x(m), y(m); + rm = args[0]; x = args[1]; y = args[2]; @@ -589,9 +600,20 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(product) == 2*sbits); - expr_ref sticky(m); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product)); - res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(2*sbits-1, sbits-3, product), sticky); + expr_ref h_p(m), l_p(m), rbits(m); + h_p = m_bv_util.mk_extract(2*sbits-1, sbits, product); + l_p = m_bv_util.mk_extract(2*sbits-1, sbits, product); + + if (sbits >= 4) { + expr_ref sticky(m); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, l_p)); + rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, l_p), sticky); + } + else + rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - m_bv_util.get_bv_size(l_p))); + + SASSERT(m_bv_util.get_bv_size(rbits) == 4); + res_sig = m_bv_util.mk_concat(h_p, rbits); round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); @@ -610,9 +632,9 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); - - expr_ref rm(m), x(m), y(m); - rm = args[0]; + + expr_ref rm(m), x(m), y(m); + rm = args[0]; x = args[1]; y = args[2]; @@ -733,9 +755,9 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - + // Remainder is always exact, so there is no rounding mode. - expr_ref x(m), y(m); + expr_ref x(m), y(m); x = args[0]; y = args[1]; @@ -937,10 +959,10 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 4); - + // fusedma means (x * y) + z - expr_ref rm(m), x(m), y(m), z(m); - rm = args[0]; + expr_ref rm(m), x(m), y(m), z(m); + rm = args[0]; x = args[1]; y = args[2]; z = args[3]; @@ -1108,8 +1130,9 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar sig_size = m_bv_util.get_bv_size(res_sig); SASSERT(sig_size == sbits+4); - expr_ref is_zero_sig(m); - m_simp.mk_eq(res_sig, m_bv_util.mk_numeral(0, sbits+4), is_zero_sig); + expr_ref is_zero_sig(m), nil_sbits4(m); + nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4); + m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig); SASSERT(is_well_sorted(m, is_zero_sig)); @@ -1142,9 +1165,9 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - - expr_ref rm(m), x(m); - rm = args[0]; + + expr_ref rm(m), x(m); + rm = args[0]; x = args[1]; expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m); @@ -1175,10 +1198,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * expr_ref a_sgn(m), a_sig(m), a_exp(m); unpack(x, a_sgn, a_sig, a_exp, true); - expr_ref exp_is_small(m); - m_simp.mk_eq(m_bv_util.mk_extract(ebits-1, ebits-1, a_exp), - m_bv_util.mk_numeral(1, 1), - exp_is_small); + 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); @@ -1273,12 +1296,13 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a split(x, x_sgn, x_sig, x_exp); split(y, y_sgn, y_sig, y_exp); - expr_ref c3(m), t3(m), t4(m); - - m_simp.mk_eq(x_sgn, m_bv_util.mk_numeral(1, 1), c3); + expr_ref c3(m), t3(m), t4(m), one_1(m), nil_1(m); + one_1 = m_bv_util.mk_numeral(1, 1); + nil_1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(x_sgn, one_1, c3); expr_ref y_sgn_eq_0(m), y_lt_x_exp(m), y_lt_x_sig(m), y_eq_x_exp(m), y_le_x_sig_exp(m), t3_or(m); - m_simp.mk_eq(y_sgn, m_bv_util.mk_numeral(0, 1), y_sgn_eq_0); + m_simp.mk_eq(y_sgn, nil_1, y_sgn_eq_0); BVULT(y_exp, x_exp, y_lt_x_exp); BVULT(y_sig, x_sig, y_lt_x_sig); m_simp.mk_eq(y_exp, x_exp, y_eq_x_exp); @@ -1287,7 +1311,7 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a m_simp.mk_ite(y_sgn_eq_0, m.mk_true(), t3_or, t3); expr_ref y_sgn_eq_1(m), x_lt_y_exp(m), x_eq_y_exp(m), x_lt_y_sig(m), x_le_y_sig_exp(m), t4_or(m); - m_simp.mk_eq(y_sgn, m_bv_util.mk_numeral(1, 1), y_sgn_eq_1); + m_simp.mk_eq(y_sgn, one_1, y_sgn_eq_1); BVULT(x_exp, y_exp, x_lt_y_exp); m_simp.mk_eq(x_exp, y_exp, x_eq_y_exp); BVULT(x_sig, y_sig, x_lt_y_sig); @@ -1418,10 +1442,11 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { split(e, sgn, sig, exp); // exp == 1^n , sig != 0 - expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m); + expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m), zero(m); mk_top_exp(m_bv_util.get_bv_size(exp), top_exp); - m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), sig_is_zero); + zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)); + m_simp.mk_eq(sig, zero, sig_is_zero); 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); @@ -1430,9 +1455,10 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split(e, sgn, sig, exp); - expr_ref eq1(m), eq2(m), top_exp(m); + expr_ref eq1(m), eq2(m), top_exp(m), zero(m); mk_top_exp(m_bv_util.get_bv_size(exp), top_exp); - m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), eq1); + zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)); + m_simp.mk_eq(sig, zero, eq1); m_simp.mk_eq(exp, top_exp, eq2); m_simp.mk_and(eq1, eq2, result); } @@ -1455,22 +1481,27 @@ void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); expr * a0 = to_app(e)->get_arg(0); - m_simp.mk_eq(a0, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(a0)), result); + expr_ref zero(m); + zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(a0)); + m_simp.mk_eq(a0, zero, result); } void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); expr * a0 = to_app(e)->get_arg(0); - m_simp.mk_eq(a0, m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(a0)), result); + expr_ref one(m); + one = m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(a0)); + m_simp.mk_eq(a0, one, result); } void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split(e, sgn, sig, exp); - expr_ref eq1(m), eq2(m), bot_exp(m); + expr_ref eq1(m), eq2(m), bot_exp(m), zero(m); mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp); - m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), eq1); + zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)); + m_simp.mk_eq(sig, zero, eq1); m_simp.mk_eq(exp, bot_exp, eq2); m_simp.mk_and(eq1, eq2, result); } @@ -1478,35 +1509,40 @@ void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split(e, sgn, sig, exp); - expr_ref e_is_zero(m), eq(m); + expr_ref e_is_zero(m), eq(m), one_1(m); mk_is_zero(e, e_is_zero); - m_simp.mk_eq(sgn, m_bv_util.mk_numeral(1, 1), eq); + one_1 = m_bv_util.mk_numeral(1, 1); + m_simp.mk_eq(sgn, one_1, eq); m_simp.mk_and(eq, e_is_zero, result); } void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split(e, sgn, sig, exp); - expr_ref e_is_zero(m), eq(m); + expr_ref e_is_zero(m), eq(m), nil_1(m); mk_is_zero(e, e_is_zero); - m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), eq); + nil_1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(sgn, nil_1, eq); m_simp.mk_and(eq, e_is_zero, result); } void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split(e, sgn, sig, exp); - m_simp.mk_eq(exp, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp)), result); + expr_ref zero(m); + zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp)); + m_simp.mk_eq(exp, zero, result); } void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split(e, sgn, sig, exp); - expr_ref is_special(m), is_denormal(m); + expr_ref is_special(m), is_denormal(m), p(m); mk_is_denormal(e, is_denormal); unsigned ebits = m_bv_util.get_bv_size(exp); - m_simp.mk_eq(exp, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits), is_special); + p = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits); + m_simp.mk_eq(exp, p, is_special); expr_ref or_ex(m); m_simp.mk_or(is_special, is_denormal, or_ex); @@ -1514,21 +1550,21 @@ void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { } void fpa2bv_converter::mk_is_rm(expr * e, BV_RM_VAL rm, expr_ref & result) { - SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3); + SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3); expr_ref rm_num(m); rm_num = m_bv_util.mk_numeral(rm, 3); - switch(rm) - { - case BV_RM_TIES_TO_AWAY: - case BV_RM_TIES_TO_EVEN: - case BV_RM_TO_NEGATIVE: - case BV_RM_TO_POSITIVE: return m_simp.mk_eq(e, rm_num, result); - case BV_RM_TO_ZERO: - default: + switch(rm) + { + case BV_RM_TIES_TO_AWAY: + case BV_RM_TIES_TO_EVEN: + case BV_RM_TO_NEGATIVE: + case BV_RM_TO_POSITIVE: return m_simp.mk_eq(e, rm_num, result); + case BV_RM_TO_ZERO: + default: rm_num = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); expr_ref r(m); r = m_bv_util.mk_ule(e, rm_num); return m_simp.mk_not(r, result); - } + } } void fpa2bv_converter::mk_top_exp(unsigned sz, expr_ref & result) { @@ -1546,7 +1582,7 @@ void fpa2bv_converter::mk_min_exp(unsigned ebits, expr_ref & result) { } void fpa2bv_converter::mk_max_exp(unsigned ebits, expr_ref & result) { - SASSERT(ebits > 0); + SASSERT(ebits > 0); result = m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(ebits-1, false), ebits); } @@ -1557,9 +1593,12 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & if (bv_sz == 0) result = m_bv_util.mk_numeral(0, max_bits); else if (bv_sz == 1) { - expr_ref eq(m); - m_simp.mk_eq(e, m_bv_util.mk_numeral(0, 1), eq); - m_simp.mk_ite(eq, m_bv_util.mk_numeral(1, max_bits), m_bv_util.mk_numeral(0, max_bits), result); + expr_ref eq(m), nil_1(m), one_m(m), nil_m(m); + nil_1 = m_bv_util.mk_numeral(0, 1); + one_m = m_bv_util.mk_numeral(1, max_bits); + nil_m = m_bv_util.mk_numeral(0, max_bits); + m_simp.mk_eq(e, nil_1, eq); + m_simp.mk_ite(eq, one_m, nil_m, result); } else { expr_ref H(m), L(m); @@ -1573,11 +1612,13 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & mk_leading_zeros(H, max_bits, lzH); /* recursive! */ mk_leading_zeros(L, max_bits, lzL); - expr_ref H_is_zero(m); - m_simp.mk_eq(H, m_bv_util.mk_numeral(0, H_size), H_is_zero); + expr_ref H_is_zero(m), nil_h(m); + nil_h = m_bv_util.mk_numeral(0, H_size); + m_simp.mk_eq(H, nil_h, H_is_zero); - expr_ref sum(m); - sum = m_bv_util.mk_bv_add(m_bv_util.mk_numeral(H_size, max_bits), lzL); + expr_ref sum(m), h_m(m); + h_m = m_bv_util.mk_numeral(H_size, max_bits); + sum = m_bv_util.mk_bv_add(h_m, lzL); m_simp.mk_ite(H_is_zero, sum, lzH, result); } @@ -1634,25 +1675,40 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref mk_unbias(denormal_exp, denormal_exp); if (normalize) { - expr_ref is_sig_zero(m), shift(m), lz(m); - m_simp.mk_eq(m_bv_util.mk_numeral(0, sbits-1), sig, is_sig_zero); + 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, m_bv_util.mk_numeral(0, ebits), 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)); - if (ebits < sbits) { + SASSERT(m_bv_util.get_bv_size(shift) == ebits); + if (ebits <= sbits) { expr_ref q(m); - q = m_bv_util.mk_zero_extend(sbits-ebits, shift); + q = m_bv_util.mk_zero_extend(sbits-ebits, shift); denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q); } else { - denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, shift); + // the maximum shift is `sbits', because after that the mantissa + // would be zero anyways. So we can safely cut the shift variable down, + // as long as we check the higher bits. + expr_ref sh(m), is_sh_zero(m), sl(m), zero_s(m), sbits_s(m), short_shift(m); + zero_s = m_bv_util.mk_numeral(0, sbits-1); + sbits_s = m_bv_util.mk_numeral(sbits, sbits); + sh = m_bv_util.mk_extract(ebits-1, sbits, shift); + 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); } } SASSERT(is_well_sorted(m, normal_sig)); SASSERT(is_well_sorted(m, denormal_sig)); + SASSERT(is_well_sorted(m, normal_exp)); + SASSERT(is_well_sorted(m, denormal_exp)); m_simp.mk_ite(is_normal, normal_sig, denormal_sig, sig); m_simp.mk_ite(is_normal, normal_exp, denormal_exp, exp); @@ -1672,19 +1728,20 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) { - switch(f->get_decl_kind()) - { - case OP_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break; + switch(f->get_decl_kind()) + { + case OP_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break; case OP_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break; case OP_RM_TOWARD_NEGATIVE: result = m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3); break; case OP_RM_TOWARD_POSITIVE: result = m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3); break; - case OP_RM_TOWARD_ZERO: result = m_bv_util.mk_numeral(BV_RM_TO_ZERO, 3); break; - default: UNREACHABLE(); - } + case OP_RM_TOWARD_ZERO: result = m_bv_util.mk_numeral(BV_RM_TO_ZERO, 3); break; + default: UNREACHABLE(); + } } -void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { +void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef _DEBUG + // return; expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e)); extra_assertions.push_back(m.mk_eq(new_e, e)); @@ -1701,144 +1758,158 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & dbg_decouple("fpa2bv_rnd_sig", sig); dbg_decouple("fpa2bv_rnd_exp", exp); - SASSERT(is_well_sorted(m, rm)); - SASSERT(is_well_sorted(m, sgn)); - SASSERT(is_well_sorted(m, sig)); - SASSERT(is_well_sorted(m, exp)); + SASSERT(is_well_sorted(m, rm)); + SASSERT(is_well_sorted(m, sgn)); + SASSERT(is_well_sorted(m, sig)); + SASSERT(is_well_sorted(m, exp)); - TRACE("fpa2bv_dbg", tout << "RND: " << std::endl << - "ebits = " << ebits << std::endl << - "sbits = " << sbits << std::endl << - "sgn = " << mk_ismt2_pp(sgn, m) << std::endl << - "sig = " << mk_ismt2_pp(sig, m) << std::endl << - "exp = " << mk_ismt2_pp(exp, m) << std::endl; ); + TRACE("fpa2bv_dbg", tout << "RND: " << std::endl << + "ebits = " << ebits << std::endl << + "sbits = " << sbits << std::endl << + "sgn = " << mk_ismt2_pp(sgn, m) << std::endl << + "sig = " << mk_ismt2_pp(sig, m) << std::endl << + "exp = " << mk_ismt2_pp(exp, m) << std::endl; ); - // Assumptions: sig is of the form f[-1:0] . f[1:sbits-1] [guard,round,sticky], + // Assumptions: sig is of the form f[-1:0] . f[1:sbits-1] [guard,round,sticky], // i.e., it has 2 + (sbits-1) + 3 = sbits + 4 bits, where the first one is in sgn. - // Furthermore, note that sig is an unsigned bit-vector, while exp is signed. + // Furthermore, note that sig is an unsigned bit-vector, while exp is signed. - SASSERT(ebits <= sbits); - SASSERT(m_bv_util.is_bv(rm) && m_bv_util.get_bv_size(rm) == 3); - SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); - SASSERT(m_bv_util.is_bv(sig) && m_bv_util.get_bv_size(sig) >= 5); - SASSERT(m_bv_util.is_bv(exp) && m_bv_util.get_bv_size(exp) >= 4); + SASSERT(ebits <= sbits); + SASSERT(m_bv_util.is_bv(rm) && m_bv_util.get_bv_size(rm) == 3); + SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); + SASSERT(m_bv_util.is_bv(sig) && m_bv_util.get_bv_size(sig) >= 5); + SASSERT(m_bv_util.is_bv(exp) && m_bv_util.get_bv_size(exp) >= 4); SASSERT(m_bv_util.get_bv_size(sig) == sbits+4); SASSERT(m_bv_util.get_bv_size(exp) == ebits+2); - // bool UNFen = false; + // bool UNFen = false; // bool OVFen = false; - expr_ref e_min(m), e_max(m); - mk_min_exp(ebits, e_min); - mk_max_exp(ebits, e_max); + expr_ref e_min(m), e_max(m); + mk_min_exp(ebits, e_min); + mk_max_exp(ebits, e_max); - TRACE("fpa2bv_dbg", tout << "e_min = " << mk_ismt2_pp(e_min, m) << std::endl << - "e_max = " << mk_ismt2_pp(e_max, m) << std::endl;); + TRACE("fpa2bv_dbg", tout << "e_min = " << mk_ismt2_pp(e_min, m) << std::endl << + "e_max = " << mk_ismt2_pp(e_max, m) << std::endl;); - expr_ref OVF1(m), e_top_three(m), sigm1(m), e_eq_emax_and_sigm1(m), e_eq_emax(m); - expr_ref e3(m), ne3(m), e2(m), e1(m), e21(m); - m_simp.mk_eq(m_bv_util.mk_extract(ebits+1, ebits+1, exp), m_bv_util.mk_numeral(1, 1), e3); - m_simp.mk_eq(m_bv_util.mk_extract(ebits, ebits, exp), m_bv_util.mk_numeral(1, 1), e2); - m_simp.mk_eq(m_bv_util.mk_extract(ebits-1, ebits-1, exp), m_bv_util.mk_numeral(1, 1), e1); + expr_ref OVF1(m), e_top_three(m), sigm1(m), e_eq_emax_and_sigm1(m), e_eq_emax(m); + expr_ref e3(m), ne3(m), e2(m), e1(m), e21(m), one_1(m), h_exp(m), sh_exp(m), th_exp(m); + one_1 = m_bv_util.mk_numeral(1, 1); + h_exp = m_bv_util.mk_extract(ebits+1, ebits+1, exp); + sh_exp = m_bv_util.mk_extract(ebits, ebits, exp); + th_exp = m_bv_util.mk_extract(ebits-1, ebits-1, exp); + m_simp.mk_eq(h_exp, one_1, e3); + m_simp.mk_eq(sh_exp, one_1, e2); + m_simp.mk_eq(th_exp, one_1, e1); m_simp.mk_or(e2, e1, e21); m_simp.mk_not(e3, ne3); m_simp.mk_and(ne3, e21, e_top_three); - m_simp.mk_eq(m_bv_util.mk_zero_extend(2, e_max), exp, e_eq_emax); - m_simp.mk_eq(m_bv_util.mk_extract(sbits+3, sbits+3, sig), m_bv_util.mk_numeral(1, 1), sigm1); + + expr_ref ext_emax(m), t_sig(m); + ext_emax = m_bv_util.mk_zero_extend(2, e_max); + t_sig = m_bv_util.mk_extract(sbits+3, sbits+3, sig); + m_simp.mk_eq(ext_emax, exp, e_eq_emax); + m_simp.mk_eq(t_sig, one_1, sigm1); m_simp.mk_and(e_eq_emax, sigm1, e_eq_emax_and_sigm1); m_simp.mk_or(e_top_three, e_eq_emax_and_sigm1, OVF1); dbg_decouple("fpa2bv_rnd_OVF1", OVF1); - TRACE("fpa2bv_dbg", tout << "OVF1 = " << mk_ismt2_pp(OVF1, m) << std::endl;); - SASSERT(is_well_sorted(m, OVF1)); + TRACE("fpa2bv_dbg", tout << "OVF1 = " << mk_ismt2_pp(OVF1, m) << std::endl;); + SASSERT(is_well_sorted(m, OVF1)); - expr_ref lz(m); - mk_leading_zeros(sig, ebits+2, lz); // CMW: is this always large enough? + expr_ref lz(m); + mk_leading_zeros(sig, ebits+2, lz); // CMW: is this always large enough? dbg_decouple("fpa2bv_rnd_lz", lz); - TRACE("fpa2bv_dbg", tout << "LZ = " << mk_ismt2_pp(lz, m) << std::endl;); + TRACE("fpa2bv_dbg", tout << "LZ = " << mk_ismt2_pp(lz, m) << std::endl;); - expr_ref t(m); - t = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2)); + expr_ref t(m); + t = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2)); t = m_bv_util.mk_bv_sub(t, lz); - t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min)); + t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min)); expr_ref TINY(m); - TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral(-1, ebits+2)); + TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral(-1, ebits+2)); - TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;); - SASSERT(is_well_sorted(m, TINY)); + TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;); + SASSERT(is_well_sorted(m, TINY)); dbg_decouple("fpa2bv_rnd_TINY", TINY); - expr_ref beta(m); + expr_ref beta(m); beta = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(exp, lz), m_bv_util.mk_numeral(1, ebits+2)); - TRACE("fpa2bv_dbg", tout << "beta = " << mk_ismt2_pp(beta, m)<< std::endl; ); - SASSERT(is_well_sorted(m, beta)); + TRACE("fpa2bv_dbg", tout << "beta = " << mk_ismt2_pp(beta, m)<< std::endl; ); + SASSERT(is_well_sorted(m, beta)); dbg_decouple("fpa2bv_rnd_beta", beta); - expr_ref sigma(m), sigma_add(m); + expr_ref sigma(m), sigma_add(m); sigma_add = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits+2)); - m_simp.mk_ite(TINY, sigma_add, lz, sigma); + m_simp.mk_ite(TINY, sigma_add, lz, sigma); dbg_decouple("fpa2bv_rnd_sigma", sigma); - TRACE("fpa2bv_dbg", tout << "Shift distance: " << mk_ismt2_pp(sigma, m) << std::endl;); + TRACE("fpa2bv_dbg", tout << "Shift distance: " << mk_ismt2_pp(sigma, m) << std::endl;); SASSERT(is_well_sorted(m, sigma)); - // Normalization shift + // Normalization shift dbg_decouple("fpa2bv_rnd_sig_before_shift", sig); - unsigned sig_size = m_bv_util.get_bv_size(sig); + unsigned sig_size = m_bv_util.get_bv_size(sig); SASSERT(sig_size == sbits+4); - unsigned sigma_size = m_bv_util.get_bv_size(sigma); + unsigned sigma_size = m_bv_util.get_bv_size(sigma); - expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m), rs_sig(m), ls_sig(m), big_sh_sig(m); - sigma_neg = m_bv_util.mk_bv_neg(sigma); + expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m), + rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m); + sigma_neg = m_bv_util.mk_bv_neg(sigma); sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size); - m_simp.mk_ite(m_bv_util.mk_sle(sigma_neg, sigma_cap), sigma_neg, sigma_cap, sigma_neg_capped); + sigma_le_cap = m_bv_util.mk_sle(sigma_neg, sigma_cap); + m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped); dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg); dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped); - sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size)); + sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size)); dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero); - sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size)); - rs_sig = m_bv_util.mk_bv_lshr(sig_ext, m_bv_util.mk_zero_extend(2*sig_size - sigma_size, sigma_neg_capped)); - ls_sig = m_bv_util.mk_bv_shl(sig_ext, m_bv_util.mk_zero_extend(2*sig_size - sigma_size, sigma)); - m_simp.mk_ite(sigma_lt_zero, rs_sig, ls_sig, big_sh_sig); + sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size)); + rs_sig = m_bv_util.mk_bv_lshr(sig_ext, m_bv_util.mk_zero_extend(2*sig_size - sigma_size, sigma_neg_capped)); + ls_sig = m_bv_util.mk_bv_shl(sig_ext, m_bv_util.mk_zero_extend(2*sig_size - sigma_size, sigma)); + m_simp.mk_ite(sigma_lt_zero, rs_sig, ls_sig, big_sh_sig); SASSERT(m_bv_util.get_bv_size(big_sh_sig) == 2*sig_size); dbg_decouple("fpa2bv_rnd_big_sh_sig", big_sh_sig); unsigned sig_extract_low_bit = (2*sig_size-1)-(sbits+2)+1; - sig = m_bv_util.mk_extract(2*sig_size-1, sig_extract_low_bit, big_sh_sig); + sig = m_bv_util.mk_extract(2*sig_size-1, sig_extract_low_bit, big_sh_sig); SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); dbg_decouple("fpa2bv_rnd_shifted_sig", sig); - expr_ref sticky(m); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sig_extract_low_bit-1, 0, big_sh_sig)); - SASSERT(is_well_sorted(m, sticky)); - SASSERT(is_well_sorted(m, sig)); - - // put the sticky bit into the significand. - expr * tmp[] = { sig, m_bv_util.mk_zero_extend(sbits+1, sticky) }; - sig = m_bv_util.mk_bv_or(2, tmp); + expr_ref sticky(m); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sig_extract_low_bit-1, 0, big_sh_sig)); + SASSERT(is_well_sorted(m, sticky)); SASSERT(is_well_sorted(m, sig)); - SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); - - // CMW: The (OVF1 && OVFen) and (TINY && UNFen) cases are never taken. - m_simp.mk_ite(TINY, m_bv_util.mk_zero_extend(2, e_min), beta, exp); - SASSERT(is_well_sorted(m, exp)); - // Significand rounding + // put the sticky bit into the significand. + expr_ref ext_sticky(m); + ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky); + expr * tmp[] = { sig, ext_sticky }; + sig = m_bv_util.mk_bv_or(2, tmp); + SASSERT(is_well_sorted(m, sig)); + SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); + + // CMW: The (OVF1 && OVFen) and (TINY && UNFen) cases are never taken. + expr_ref ext_emin(m); + ext_emin = m_bv_util.mk_zero_extend(2, e_min); + m_simp.mk_ite(TINY, ext_emin, beta, exp); + SASSERT(is_well_sorted(m, exp)); + + // Significand rounding expr_ref round(m), last(m); - sticky = m_bv_util.mk_extract(0, 0, sig); // new sticky bit! - round = m_bv_util.mk_extract(1, 1, sig); + sticky = m_bv_util.mk_extract(0, 0, sig); // new sticky bit! + round = m_bv_util.mk_extract(1, 1, sig); last = m_bv_util.mk_extract(2, 2, sig); TRACE("fpa2bv_dbg", tout << "sticky = " << mk_ismt2_pp(sticky, m) << std::endl;); @@ -1847,70 +1918,76 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & dbg_decouple("fpa2bv_rnd_round", round); dbg_decouple("fpa2bv_rnd_last", last); - sig = m_bv_util.mk_extract(sbits+1, 2, sig); + sig = m_bv_util.mk_extract(sbits+1, 2, sig); - expr * last_sticky[2] = { last, sticky }; - expr * round_sticky[2] = { round, sticky }; - expr * last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky); - expr * round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky); - expr * round_lors[2] = { m_bv_util.mk_bv_not(round), m_bv_util.mk_bv_not(last_or_sticky) }; - expr * pos_args[2] = { sgn, m_bv_util.mk_bv_not(round_or_sticky) }; - expr * neg_args[2] = { m_bv_util.mk_bv_not(sgn), m_bv_util.mk_bv_not(round_or_sticky) }; + expr_ref last_or_sticky(m), round_or_sticky(m), not_round(m), not_lors(m), not_rors(m), not_sgn(m); + expr * last_sticky[2] = { last, sticky }; + expr * round_sticky[2] = { round, sticky }; + last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky); + round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky); + not_round = m_bv_util.mk_bv_not(round); + not_lors = m_bv_util.mk_bv_not(last_or_sticky); + not_rors = m_bv_util.mk_bv_not(round_or_sticky); + not_sgn = m_bv_util.mk_bv_not(sgn); + expr * round_lors[2] = { not_round, not_lors }; + expr * pos_args[2] = { sgn, not_rors }; + expr * neg_args[2] = { not_sgn, not_rors }; expr_ref inc_teven(m), inc_taway(m), inc_pos(m), inc_neg(m); - inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, round_lors)); - inc_taway = round; - inc_pos = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, pos_args)); - inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args)); + inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, round_lors)); + inc_taway = round; + inc_pos = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, pos_args)); + inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args)); expr_ref inc(m), inc_c2(m), inc_c3(m), inc_c4(m); - expr_ref rm_is_to_neg(m), rm_is_to_pos(m), rm_is_away(m), rm_is_even(m); + expr_ref rm_is_to_neg(m), rm_is_to_pos(m), rm_is_away(m), rm_is_even(m), nil_1(m); + nil_1 = m_bv_util.mk_numeral(0, 1); mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_to_pos); mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_away); mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_even); - m_simp.mk_ite(rm_is_to_neg, inc_neg, m_bv_util.mk_numeral(0, 1), inc_c4); + m_simp.mk_ite(rm_is_to_neg, inc_neg, nil_1, inc_c4); m_simp.mk_ite(rm_is_to_pos, inc_pos, inc_c4, inc_c3); m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2); - m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, inc); + m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, inc); - SASSERT(m_bv_util.get_bv_size(inc) == 1 && is_well_sorted(m, inc)); + SASSERT(m_bv_util.get_bv_size(inc) == 1 && is_well_sorted(m, inc)); dbg_decouple("fpa2bv_rnd_inc", inc); - sig = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(1, sig), - m_bv_util.mk_zero_extend(sbits, inc)); - SASSERT(is_well_sorted(m, sig)); + sig = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(1, sig), + m_bv_util.mk_zero_extend(sbits, inc)); + SASSERT(is_well_sorted(m, sig)); dbg_decouple("fpa2bv_rnd_sig_plus_inc", sig); - // Post normalization - SASSERT(m_bv_util.get_bv_size(sig) == sbits + 1); + // Post normalization + SASSERT(m_bv_util.get_bv_size(sig) == sbits + 1); expr_ref SIGovf(m); - m_simp.mk_eq(m_bv_util.mk_extract(sbits, sbits, sig), m_bv_util.mk_numeral(1, 1), SIGovf); + t_sig = m_bv_util.mk_extract(sbits, sbits, sig); + m_simp.mk_eq(t_sig, one_1, SIGovf); SASSERT(is_well_sorted(m, SIGovf)); dbg_decouple("fpa2bv_rnd_SIGovf", SIGovf); - m_simp.mk_ite(SIGovf, - m_bv_util.mk_extract(sbits, 1, sig), - m_bv_util.mk_extract(sbits-1, 0, sig), - sig); + expr_ref hallbut1_sig(m), lallbut1_sig(m); + hallbut1_sig = m_bv_util.mk_extract(sbits, 1, sig); + lallbut1_sig = m_bv_util.mk_extract(sbits-1, 0, sig); + m_simp.mk_ite(SIGovf, hallbut1_sig, lallbut1_sig, sig); - SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); + SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); - m_simp.mk_ite(SIGovf, - m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2)), - exp, - exp); + expr_ref exp_p1(m); + exp_p1 = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2)); + m_simp.mk_ite(SIGovf, exp_p1, exp, exp); - SASSERT(is_well_sorted(m, sig)); - SASSERT(is_well_sorted(m, exp)); + SASSERT(is_well_sorted(m, sig)); + SASSERT(is_well_sorted(m, exp)); dbg_decouple("fpa2bv_rnd_sig_postnormalized", sig); dbg_decouple("fpa2bv_rnd_exp_postnormalized", exp); - - SASSERT(m_bv_util.get_bv_size(sig) == sbits); - SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); - SASSERT(m_bv_util.get_bv_size(e_max) == ebits); + + SASSERT(m_bv_util.get_bv_size(sig) == sbits); + SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); + SASSERT(m_bv_util.get_bv_size(e_max) == ebits); - // Exponent adjustment and rounding + // Exponent adjustment and rounding expr_ref biased_exp(m); mk_bias(m_bv_util.mk_extract(ebits-1, 0, exp), biased_exp); dbg_decouple("fpa2bv_rnd_unbiased_exp", exp); @@ -1920,12 +1997,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & SASSERT(is_well_sorted(m, OVF1)); SASSERT(m.is_bool(OVF1)); - expr_ref preOVF2(m), OVF2(m), OVF(m); - m_simp.mk_eq(m.mk_app(m_bv_util.get_fid(), OP_BREDAND, biased_exp.get()), m_bv_util.mk_numeral(1, 1), preOVF2); + expr_ref preOVF2(m), OVF2(m), OVF(m), exp_redand(m), pem2m1(m); + exp_redand = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, biased_exp.get()); + m_simp.mk_eq(exp_redand, one_1, preOVF2); m_simp.mk_and(SIGovf, preOVF2, OVF2); - m_simp.mk_ite(OVF2, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-2), ebits), - biased_exp, - biased_exp); + pem2m1 = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-2), ebits); + m_simp.mk_ite(OVF2, pem2m1, biased_exp, biased_exp); m_simp.mk_or(OVF1, OVF2, OVF); SASSERT(is_well_sorted(m, OVF2)); @@ -1950,11 +2027,11 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), sgn_is_zero); expr_ref max_sig(m), max_exp(m), inf_sig(m), inf_exp(m); - max_sig = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(sbits-1, false), sbits-1); - max_exp = m_bv_util.mk_concat(m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1, false), ebits-1), + max_sig = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(sbits-1, false), sbits-1); + max_exp = m_bv_util.mk_concat(m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1, false), ebits-1), m_bv_util.mk_numeral(0, 1)); - inf_sig = m_bv_util.mk_numeral(0, sbits-1); - inf_exp = top_exp; + inf_sig = m_bv_util.mk_numeral(0, sbits-1); + inf_exp = top_exp; dbg_decouple("fpa2bv_rnd_max_exp", max_exp); @@ -1962,15 +2039,17 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & m_simp.mk_ite(rm_zero_or_neg, max_exp, inf_exp, max_inf_exp_neg); m_simp.mk_ite(rm_zero_or_pos, max_exp, inf_exp, max_inf_exp_pos); m_simp.mk_ite(sgn_is_zero, max_inf_exp_neg, max_inf_exp_pos, ovfl_exp); - m_simp.mk_eq(m_bv_util.mk_extract(sbits-1, sbits-1, sig), m_bv_util.mk_numeral(0, 1), n_d_check); + t_sig = m_bv_util.mk_extract(sbits-1, sbits-1, sig); + m_simp.mk_eq(t_sig, nil_1, n_d_check); m_simp.mk_ite(n_d_check, bot_exp /* denormal */, biased_exp, n_d_exp); m_simp.mk_ite(OVF, ovfl_exp, n_d_exp, exp); - expr_ref max_inf_sig_neg(m), max_inf_sig_pos(m), ovfl_sig(m); + expr_ref max_inf_sig_neg(m), max_inf_sig_pos(m), ovfl_sig(m), rest_sig(m); m_simp.mk_ite(rm_zero_or_neg, max_sig, inf_sig, max_inf_sig_neg); m_simp.mk_ite(rm_zero_or_pos, max_sig, inf_sig, max_inf_sig_pos); m_simp.mk_ite(sgn_is_zero, max_inf_sig_neg, max_inf_sig_pos, ovfl_sig); - m_simp.mk_ite(OVF, ovfl_sig, m_bv_util.mk_extract(sbits-2, 0, sig), sig); + rest_sig = m_bv_util.mk_extract(sbits-2, 0, sig); + m_simp.mk_ite(OVF, ovfl_sig, rest_sig, sig); dbg_decouple("fpa2bv_rnd_sgn_final", sgn); dbg_decouple("fpa2bv_rnd_sig_final", sig); @@ -1978,26 +2057,21 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & expr_ref res_sgn(m), res_sig(m), res_exp(m); res_sgn = sgn; - res_sig = sig; - res_exp = exp; - - SASSERT(m_bv_util.get_bv_size(res_sgn) == 1); - SASSERT(is_well_sorted(m, res_sgn)); + res_sig = sig; + res_exp = exp; + + SASSERT(m_bv_util.get_bv_size(res_sgn) == 1); + SASSERT(is_well_sorted(m, res_sgn)); SASSERT(m_bv_util.get_bv_size(res_sig) == sbits-1); - SASSERT(is_well_sorted(m, res_sig)); + SASSERT(is_well_sorted(m, res_sig)); SASSERT(m_bv_util.get_bv_size(res_exp) == ebits); - SASSERT(is_well_sorted(m, res_exp)); + SASSERT(is_well_sorted(m, res_exp)); - mk_triple(res_sgn, res_sig, res_exp, result); + mk_triple(res_sgn, res_sig, res_exp, result); TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; ); } - -fpa2bv_model_converter * fpa2bv_converter::mk_model_converter() { - return alloc(fpa2bv_model_converter, m, m_const2bv, m_rm_const2bv); -} - void fpa2bv_model_converter::display(std::ostream & out) { out << "(fpa2bv-model-converter"; for (obj_map::iterator it = m_const2bv.begin(); @@ -2008,7 +2082,7 @@ void fpa2bv_model_converter::display(std::ostream & out) { unsigned indent = n.size() + 4; out << mk_ismt2_pp(it->m_value, m, indent) << ")"; } - for (obj_map::iterator it = m_rm_const2bv.begin(); + for (obj_map::iterator it = m_rm_const2bv.begin(); it != m_rm_const2bv.end(); it++) { const symbol & n = it->m_key->get_name(); @@ -2024,11 +2098,23 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); it++) - res->m_const2bv.insert(translator(it->m_key), translator(it->m_value)); - for (obj_map::iterator it = m_rm_const2bv.begin(); + { + func_decl * k = translator(it->m_key); + expr * v = translator(it->m_value); + res->m_const2bv.insert(k, v); + translator.to().inc_ref(k); + translator.to().inc_ref(v); + } + for (obj_map::iterator it = m_rm_const2bv.begin(); it != m_rm_const2bv.end(); it++) - res->m_rm_const2bv.insert(translator(it->m_key), translator(it->m_value)); + { + func_decl * k = translator(it->m_key); + expr * v = translator(it->m_value); + res->m_rm_const2bv.insert(k, v); + translator.to().inc_ref(k); + translator.to().inc_ref(v); + } return res; } @@ -2098,30 +2184,30 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { mpzm.del(sig_z); } - for (obj_map::iterator it = m_rm_const2bv.begin(); + for (obj_map::iterator it = m_rm_const2bv.begin(); it != m_rm_const2bv.end(); it++) { - func_decl * var = it->m_key; + func_decl * var = it->m_key; app * a = to_app(it->m_value); SASSERT(fu.is_rm(var->get_range())); - rational val(0); - unsigned sz = 0; - if (a && bu.is_numeral(a, val, sz)) { - TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl; ); - SASSERT(val.is_uint64()); - switch (val.get_uint64()) - { - case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break; - case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break; - case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break; - case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break; - case BV_RM_TO_ZERO: - default: float_mdl->register_decl(var, fu.mk_round_toward_zero()); - } + rational val(0); + unsigned sz = 0; + if (a && bu.is_numeral(a, val, sz)) { + TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl; ); + SASSERT(val.is_uint64()); + switch (val.get_uint64()) + { + case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break; + case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break; + case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break; + case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break; + case BV_RM_TO_ZERO: + default: float_mdl->register_decl(var, fu.mk_round_toward_zero()); + } seen.insert(var); - } - } + } + } fu.fm().del(fp_val); @@ -2135,7 +2221,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); } - // And keep everything else +// And keep everything else sz = bv_mdl->get_num_functions(); for (unsigned i = 0; i < sz; i++) { @@ -2151,3 +2237,9 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { float_mdl->register_usort(s, u.size(), u.c_ptr()); } } + +model_converter * mk_fpa2bv_model_converter(ast_manager & m, + obj_map const & const2bv, + obj_map const & rm_const2bv) { + return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv); +} \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 1ee374941..6ac1d2b8b 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -35,13 +35,13 @@ class fpa2bv_converter { ast_manager & m; basic_simplifier_plugin m_simp; float_util m_util; - mpf_manager & m_mpf_manager; - unsynch_mpz_manager & m_mpz_manager; + mpf_manager & m_mpf_manager; + unsynch_mpz_manager & m_mpz_manager; bv_util m_bv_util; float_decl_plugin * m_plugin; obj_map m_const2bv; - obj_map m_rm_const2bv; + obj_map m_rm_const2bv; public: fpa2bv_converter(ast_manager & m); @@ -52,22 +52,22 @@ public: bool is_float(sort * s) { return m_util.is_float(s); } bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); } bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); } - bool is_rm_sort(sort * s) { return m_util.is_rm(s); } + bool is_rm_sort(sort * s) { return m_util.is_rm(s); } void mk_triple(expr * sign, expr * significand, expr * exponent, expr_ref & result) { - SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1); - SASSERT(m_bv_util.is_bv(significand)); - SASSERT(m_bv_util.is_bv(exponent)); + SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1); + SASSERT(m_bv_util.is_bv(significand)); + SASSERT(m_bv_util.is_bv(exponent)); result = m.mk_app(m_util.get_family_id(), OP_TO_FLOAT, sign, significand, exponent); } void mk_eq(expr * a, expr * b, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); - void mk_rounding_mode(func_decl * f, expr_ref & result); + void mk_rounding_mode(func_decl * f, expr_ref & result); void mk_value(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_const(func_decl * f, expr_ref & result); - void mk_rm_const(func_decl * f, expr_ref & result); + void mk_rm_const(func_decl * f, expr_ref & result); void mk_plus_inf(func_decl * f, expr_ref & result); void mk_minus_inf(func_decl * f, expr_ref & result); @@ -102,7 +102,8 @@ public: void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - fpa2bv_model_converter * mk_model_converter(); + obj_map const & const2bv() const { return m_const2bv; } + obj_map const & rm_const2bv() const { return m_rm_const2bv; } void dbg_decouple(const char * prefix, expr_ref & e); expr_ref_vector extra_assertions; @@ -122,11 +123,11 @@ protected: void mk_is_denormal(expr * e, expr_ref & result); void mk_is_normal(expr * e, expr_ref & result); - void mk_is_rm(expr * e, BV_RM_VAL rm, expr_ref & result); + void mk_is_rm(expr * e, BV_RM_VAL rm, expr_ref & result); void mk_top_exp(unsigned sz, expr_ref & result); void mk_bot_exp(unsigned sz, expr_ref & result); - void mk_min_exp(unsigned ebits, expr_ref & result); + void mk_min_exp(unsigned ebits, expr_ref & result); void mk_max_exp(unsigned ebits, expr_ref & result); void mk_leading_zeros(expr * e, unsigned max_bits, expr_ref & result); @@ -135,7 +136,7 @@ protected: void mk_unbias(expr * e, expr_ref & result); void unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, bool normalize); - void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result); + void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result); void 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, @@ -146,11 +147,11 @@ protected: class fpa2bv_model_converter : public model_converter { ast_manager & m; obj_map m_const2bv; - obj_map m_rm_const2bv; + obj_map m_rm_const2bv; public: - fpa2bv_model_converter(ast_manager & m, obj_map & const2bv, - obj_map & rm_const2bv) : + fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, + obj_map const & rm_const2bv) : m(m) { // Just create a copy? for (obj_map::iterator it = const2bv.begin(); @@ -161,7 +162,7 @@ public: m.inc_ref(it->m_key); m.inc_ref(it->m_value); } - for (obj_map::iterator it = rm_const2bv.begin(); + for (obj_map::iterator it = rm_const2bv.begin(); it != rm_const2bv.end(); it++) { @@ -173,7 +174,7 @@ public: virtual ~fpa2bv_model_converter() { dec_ref_map_key_values(m, m_const2bv); - dec_ref_map_key_values(m, m_rm_const2bv); + dec_ref_map_key_values(m, m_rm_const2bv); } virtual void operator()(model_ref & md, unsigned goal_idx) { @@ -198,4 +199,9 @@ protected: void convert(model * bv_mdl, model * float_mdl); }; + +model_converter * mk_fpa2bv_model_converter(ast_manager & m, + obj_map const & const2bv, + obj_map const & rm_const2bv); + #endif diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 94694867a..4b3525a32 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -73,7 +73,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { return BR_DONE; } - if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) { + if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) { m_conv.mk_rm_const(f, result); return BR_DONE; } @@ -102,7 +102,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_RM_NEAREST_TIES_TO_EVEN: case OP_RM_TOWARD_NEGATIVE: case OP_RM_TOWARD_POSITIVE: - case OP_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; + case OP_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE; case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE; case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE; diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 79f41518e..a90ff9317 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -90,7 +90,7 @@ class fpa2bv_tactic : public tactic { } if (g->models_enabled()) - mc = m_conv.mk_model_converter(); + mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv()); g->inc_depth(); result.push_back(g.get()); From 7822b86b532abdd75b7e7aad2b6383464ab8658b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 1 Mar 2013 19:06:01 +0000 Subject: [PATCH 03/11] FPA: multiple bugfixes for HWF, MPF and a bugfix for FPA2BV (many thanks to Gabriele Paganelli) Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 43 +++++++++++++------ src/util/hwf.cpp | 64 +++++++++++++++++++---------- src/util/mpf.cpp | 46 ++++++++++++--------- 3 files changed, 99 insertions(+), 54 deletions(-) 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); From 6c3e2e67643757811b7123e87d7dad04902689be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Mar 2013 21:03:08 -0800 Subject: [PATCH 04/11] add default simplifications as tactic Signed-off-by: Nikolaj Bjorner --- src/muz_qe/hilbert_basis.cpp | 7 +-- src/muz_qe/horn_tactic.cpp | 85 ++++++++++++++++++++++++++++++++---- src/muz_qe/horn_tactic.h | 5 +++ 3 files changed, 86 insertions(+), 11 deletions(-) diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index c1d941c1c..e7c7928a3 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -23,8 +23,6 @@ Revision History: #include "heap_trie.h" #include "stopwatch.h" -template -class rational_map : public map {}; typedef int_hashtable > int_table; @@ -264,7 +262,10 @@ class hilbert_basis::index { void reset() { memset(this, 0, sizeof(*this)); } }; - typedef rational_map value_map; + template + class numeral_map : public map {}; + + typedef numeral_map value_map; hilbert_basis& hb; value_map m_neg; value_index m_pos; diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 0637148d6..a8ace78aa 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -21,15 +21,18 @@ Revision History: #include"proof_converter.h" #include"horn_tactic.h" #include"dl_context.h" +#include"expr_replacer.h" class horn_tactic : public tactic { struct imp { ast_manager& m; + bool m_is_simplify; datalog::context m_ctx; smt_params m_fparams; - imp(ast_manager & m, params_ref const & p): + imp(bool is_simplify, ast_manager & m, params_ref const & p): m(m), + m_is_simplify(is_simplify), m_ctx(m, m_fparams) { updt_params(p); } @@ -180,6 +183,9 @@ class horn_tactic : public tactic { expr_ref_vector queries(m); std::stringstream msg; + m_ctx.reset(); + m_ctx.ensure_opened(); + for (unsigned i = 0; i < sz; i++) { f = g->form(i); formula_kind k = get_formula_kind(f); @@ -196,7 +202,7 @@ class horn_tactic : public tactic { } } - if (queries.size() != 1) { + if (queries.size() != 1 || m_is_simplify) { q = m.mk_fresh_const("query", m.mk_bool_sort()); register_predicate(q); for (unsigned i = 0; i < queries.size(); ++i) { @@ -208,8 +214,26 @@ class horn_tactic : public tactic { } SASSERT(queries.size() == 1); q = queries[0].get(); + if (m_is_simplify) { + simplify(q, g, result, mc, pc); + } + else { + verify(q, g, result, mc, pc); + } + } + + void verify(expr* q, + goal_ref const& g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc) { + lbool is_reachable = m_ctx.query(q); g->inc_depth(); + + bool produce_models = g->models_enabled(); + bool produce_proofs = g->proofs_enabled(); + result.push_back(g.get()); switch (is_reachable) { case l_true: { @@ -237,19 +261,60 @@ class horn_tactic : public tactic { TRACE("horn", g->display(tout);); SASSERT(g->is_well_sorted()); } + + void simplify(expr* q, + goal_ref const& g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc) { + + expr_ref fml(m); + bool produce_models = g->models_enabled(); + bool produce_proofs = g->proofs_enabled(); + + if (produce_models) { + mc = datalog::mk_skip_model_converter(); + } + if (produce_proofs) { + pc = datalog::mk_skip_proof_converter(); + } + + func_decl* query_pred = to_app(q)->get_decl(); + m_ctx.set_output_predicate(query_pred); + m_ctx.get_rules(); // flush adding rules. + m_ctx.apply_default_transformation(mc, pc); + + expr_substitution sub(m); + sub.insert(q, m.mk_false()); + scoped_ptr rep = mk_default_expr_replacer(m); + g->inc_depth(); + g->reset(); + result.push_back(g.get()); + datalog::rule_set const& rules = m_ctx.get_rules(); + datalog::rule_set::iterator it = rules.begin(), end = rules.end(); + for (; it != end; ++it) { + datalog::rule* r = *it; + r->to_formula(fml); + (*rep)(fml); + g->assert_expr(fml); + } + } + }; - + + bool m_is_simplify; params_ref m_params; statistics m_stats; imp * m_imp; public: - horn_tactic(ast_manager & m, params_ref const & p): + horn_tactic(bool is_simplify, ast_manager & m, params_ref const & p): + m_is_simplify(is_simplify), m_params(p) { - m_imp = alloc(imp, m, p); + m_imp = alloc(imp, is_simplify, m, p); } virtual tactic * translate(ast_manager & m) { - return alloc(horn_tactic, m, m_params); + return alloc(horn_tactic, m_is_simplify, m, m_params); } virtual ~horn_tactic() { @@ -293,7 +358,7 @@ public: m_imp = 0; } dealloc(d); - d = alloc(imp, m, m_params); + d = alloc(imp, m_is_simplify, m, m_params); #pragma omp critical (tactic_cancel) { m_imp = d; @@ -308,6 +373,10 @@ protected: }; tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(horn_tactic, m, p)); + return clean(alloc(horn_tactic, false, m, p)); +} + +tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(horn_tactic, true, m, p)); } diff --git a/src/muz_qe/horn_tactic.h b/src/muz_qe/horn_tactic.h index 7f56a77ba..f041321ea 100644 --- a/src/muz_qe/horn_tactic.h +++ b/src/muz_qe/horn_tactic.h @@ -27,4 +27,9 @@ tactic * mk_horn_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("horn", "apply tactic for horn clauses.", "mk_horn_tactic(m, p)") */ + +tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("horn-simplify", "simplify horn clauses.", "mk_horn_simplify_tactic(m, p)") +*/ #endif From 352912c6b55448e348e97f9a69c27df580a65455 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Mar 2013 21:06:13 -0800 Subject: [PATCH 05/11] add default simplifications as tactic Signed-off-by: Nikolaj Bjorner --- src/muz_qe/horn_tactic.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index a8ace78aa..cd03e522e 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -287,6 +287,7 @@ class horn_tactic : public tactic { expr_substitution sub(m); sub.insert(q, m.mk_false()); scoped_ptr rep = mk_default_expr_replacer(m); + rep->set_substitution(&sub); g->inc_depth(); g->reset(); result.push_back(g.get()); From 523dc0fb36e6c52f4118641bfb1598b9f7e25229 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Mar 2013 21:24:21 -0800 Subject: [PATCH 06/11] add slicing Signed-off-by: Nikolaj Bjorner --- src/muz_qe/horn_tactic.cpp | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index cd03e522e..c22474a7c 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -22,6 +22,8 @@ Revision History: #include"horn_tactic.h" #include"dl_context.h" #include"expr_replacer.h" +#include"dl_rule_transformer.h" +#include"dl_mk_slice.h" class horn_tactic : public tactic { struct imp { @@ -30,9 +32,9 @@ class horn_tactic : public tactic { datalog::context m_ctx; smt_params m_fparams; - imp(bool is_simplify, ast_manager & m, params_ref const & p): + imp(bool t, ast_manager & m, params_ref const & p): m(m), - m_is_simplify(is_simplify), + m_is_simplify(t), m_ctx(m, m_fparams) { updt_params(p); } @@ -283,6 +285,13 @@ class horn_tactic : public tactic { m_ctx.set_output_predicate(query_pred); m_ctx.get_rules(); // flush adding rules. m_ctx.apply_default_transformation(mc, pc); + + if (m_ctx.get_params().slice()) { + datalog::rule_transformer transformer(m_ctx); + datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); + transformer.register_plugin(slice); + m_ctx.transform_rules(transformer, mc, pc); + } expr_substitution sub(m); sub.insert(q, m.mk_false()); @@ -308,10 +317,10 @@ class horn_tactic : public tactic { statistics m_stats; imp * m_imp; public: - horn_tactic(bool is_simplify, ast_manager & m, params_ref const & p): - m_is_simplify(is_simplify), + horn_tactic(bool t, ast_manager & m, params_ref const & p): + m_is_simplify(t), m_params(p) { - m_imp = alloc(imp, is_simplify, m, p); + m_imp = alloc(imp, t, m, p); } virtual tactic * translate(ast_manager & m) { From 197b2e8ddb9186693057eb6d6bc5e7e707b4f61e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Mar 2013 13:55:41 -0800 Subject: [PATCH 07/11] fix bugs reported by Arie Gurfinkel Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_context.cpp | 142 ++++++++++++++++++++++++++----------- src/muz_qe/pdr_context.h | 4 +- 2 files changed, 103 insertions(+), 43 deletions(-) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 73bffd4e4..7df4a2b64 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -410,6 +410,15 @@ namespace pdr { add_property(result, level); } + void pred_transformer::propagate_to_infinity(unsigned invariant_level) { + expr_ref inv = get_formulas(invariant_level, false); + add_property(inv, infty_level); + // cleanup + for (unsigned i = invariant_level; i < m_levels.size(); ++i) { + m_levels[i].reset(); + } + } + lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level) { TRACE("pdr", tout << "is-reachable: " << head()->get_name() << " level: " << n.level() << "\n"; @@ -723,26 +732,6 @@ namespace pdr { m_closed = true; } - expr_ref model_node::get_trace() const { - pred_transformer& p = pt(); - ast_manager& m = p.get_manager(); - manager& pm = p.get_pdr_manager(); - TRACE("pdr", model_smt2_pp(tout, m, get_model(), 0);); - func_decl* f = p.head(); - unsigned arity = f->get_arity(); - model_ref model = get_model_ptr(); - expr_ref_vector args(m); - expr_ref v(m); - model_evaluator mev(m); - - for (unsigned i = 0; i < arity; ++i) { - v = m.mk_const(pm.o2n(p.sig(i),0)); - expr_ref e = mev.eval(model, v); - args.push_back(e); - } - return expr_ref(m.mk_app(f, args.size(), args.c_ptr()), m); - } - static bool is_ini(datalog::rule const& r) { return r.get_uninterpreted_tail_size() == 0; } @@ -961,21 +950,80 @@ namespace pdr { return out; } - expr_ref model_search::get_trace() const { + /** + Extract trace comprising of constraints + and predicates that are satisfied from facts to the query. + The resulting trace + */ + + expr_ref model_search::get_trace(context const& ctx) const { pred_transformer& pt = get_root().pt(); ast_manager& m = pt.get_manager(); manager& pm = pt.get_pdr_manager(); - expr_ref result(m.mk_true(),m); - expr_ref_vector rules(m); - ptr_vector nodes; - nodes.push_back(m_root); - while (!nodes.empty()) { - model_node* current = nodes.back(); - nodes.pop_back(); - rules.push_back(current->get_trace()); - nodes.append(current->children()); - } - return pm.mk_and(rules); + datalog::context& dctx = ctx.get_context(); + datalog::rule_manager& rm = dctx.get_rule_manager(); + expr_ref_vector constraints(m), predicates(m); + expr_ref tmp(m); + ptr_vector children; + unsigned deltas[2]; + datalog::rule_ref rule(rm), r0(rm); + model_node* n = m_root; + datalog::var_counter& vc = rm.get_var_counter(); + substitution subst(m); + unifier unif(m); + rule = n->get_rule(); + unsigned max_var = vc.get_max_var(*rule); + predicates.push_back(rule->get_head()); + children.append(n); + bool first = true; + while (!children.empty()) { + SASSERT(children.size() == predicates.size()); + expr_ref_vector binding(m); + n = children.back(); + children.pop_back(); + n->mk_instantiate(r0, rule, binding); + + max_var = std::max(max_var, vc.get_max_var(*rule)); + subst.reset(); + subst.reserve(2, max_var+1); + deltas[0] = 0; + deltas[1] = max_var+1; + + VERIFY(unif(predicates.back(), rule->get_head(), subst)); + for (unsigned i = 0; i < constraints.size(); ++i) { + subst.apply(2, deltas, expr_offset(constraints[i].get(), 0), tmp); + dctx.get_rewriter()(tmp); + constraints[i] = tmp; + } + for (unsigned i = 0; i < predicates.size(); ++i) { + subst.apply(2, deltas, expr_offset(predicates[i].get(), 0), tmp); + predicates[i] = tmp; + } + if (!first) { + constraints.push_back(predicates.back()); + } + first = false; + predicates.pop_back(); + for (unsigned i = 0; i < rule->get_uninterpreted_tail_size(); ++i) { + subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp); + predicates.push_back(tmp); + } + for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) { + subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp); + dctx.get_rewriter()(tmp); + if (!m.is_true(tmp)) { + constraints.push_back(tmp); + } + } + for (unsigned i = 0; i < constraints.size(); ++i) { + max_var = std::max(vc.get_max_var(constraints[i].get()), max_var); + } + for (unsigned i = 0; i < predicates.size(); ++i) { + max_var = std::max(vc.get_max_var(predicates[i].get()), max_var); + } + children.append(n->children()); + } + return pm.mk_and(constraints); } proof_ref model_search::get_proof_trace(context const& ctx) const { @@ -1367,6 +1415,8 @@ namespace pdr { if (!m_params.validate_result()) { return; } + std::stringstream msg; + switch(m_last_result) { case l_true: { proof_ref pr = get_proof(); @@ -1374,7 +1424,8 @@ namespace pdr { expr_ref_vector side_conditions(m); bool ok = checker.check(pr, side_conditions); if (!ok) { - IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";); + msg << "proof validation failed"; + throw default_exception(msg.str()); } for (unsigned i = 0; i < side_conditions.size(); ++i) { expr* cond = side_conditions[i].get(); @@ -1385,9 +1436,8 @@ namespace pdr { solver.assert_expr(tmp); lbool res = solver.check(); if (res != l_false) { - IF_VERBOSE(0, verbose_stream() << "rule validation failed\n"; - verbose_stream() << mk_pp(cond, m) << "\n"; - ); + msg << "rule validation failed when checking: " << mk_pp(cond, m); + throw default_exception(msg.str()); } } break; @@ -1430,14 +1480,15 @@ namespace pdr { names.push_back(symbol(i)); } sorts.reverse(); - tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp); + if (!sorts.empty()) { + tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp); + } smt::kernel solver(m, get_fparams()); solver.assert_expr(tmp); lbool res = solver.check(); if (res != l_false) { - IF_VERBOSE(0, verbose_stream() << "rule validation failed\n"; - verbose_stream() << mk_pp(tmp, m) << "\n"; - ); + msg << "rule validation failed when checking: " << mk_pp(tmp, m); + throw default_exception(msg.str()); } } } @@ -1530,6 +1581,14 @@ namespace pdr { inductive_property ex(m, mc, rs); verbose_stream() << ex.to_string(); }); + + // upgrade invariants that are known to be inductive. + decl2rel::iterator it = m_rels.begin (), end = m_rels.end (); + for (; m_inductive_lvl > 0 && it != end; ++it) { + if (it->m_value->head() != m_query_pred) { + it->m_value->propagate_to_infinity (m_inductive_lvl); + } + } validate(); return l_false; } @@ -1594,7 +1653,7 @@ namespace pdr { proof_ref pr = get_proof(); return expr_ref(pr.get(), m); } - return m_search.get_trace(); + return m_search.get_trace(*this); } expr_ref context::mk_unsat_answer() const { @@ -1939,6 +1998,7 @@ namespace pdr { } st.update("PDR num unfoldings", m_stats.m_num_nodes); st.update("PDR max depth", m_stats.m_max_depth); + st.update("PDR inductive level", m_inductive_lvl); m_pm.collect_statistics(st); for (unsigned i = 0; i < m_core_generalizers.size(); ++i) { diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 7491327dd..32f13cdd4 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -138,6 +138,7 @@ namespace pdr { ptr_vector& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); } bool propagate_to_next_level(unsigned level); + void propagate_to_infinity(unsigned level); void add_property(expr * lemma, unsigned lvl); // add property 'p' to state at level. lbool is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level); @@ -223,7 +224,6 @@ namespace pdr { void set_rule(datalog::rule const* r) { m_rule = r; } datalog::rule* get_rule(); - expr_ref get_trace() const; void mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding); std::ostream& display(std::ostream& out, unsigned indent); @@ -253,7 +253,7 @@ namespace pdr { void set_root(model_node* n); model_node& get_root() const { return *m_root; } std::ostream& display(std::ostream& out) const; - expr_ref get_trace() const; + expr_ref get_trace(context const& ctx) const; proof_ref get_proof_trace(context const& ctx) const; void backtrack_level(bool uses_level, model_node& n); }; From e5f03f999abb3af7743163975301bbfc9f9b6d34 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 4 Mar 2013 20:21:14 +0000 Subject: [PATCH 08/11] FPA: Added conversion operator float -> float. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 23 ++-- src/ast/rewriter/float_rewriter.cpp | 23 ++-- src/tactic/fpa/fpa2bv_converter.cpp | 169 ++++++++++++++++++++++++++-- src/util/mpf.cpp | 2 +- 4 files changed, 188 insertions(+), 29 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index f2d6591dc..62ec3a4cf 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -353,27 +353,22 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) m_manager->raise_exception("expecting two integer parameters to asFloat"); if (arity != 2 && arity != 3) m_manager->raise_exception("invalid number of arguments to asFloat operator"); - if (!is_rm_sort(domain[0]) || domain[1] != m_real_sort) + if (arity == 3 && domain[2] != m_int_sort) + m_manager->raise_exception("sort mismatch"); + if (!is_rm_sort(domain[0]) || + !(domain[1] == m_real_sort || is_sort_of(domain[1], m_family_id, FLOAT_SORT))) m_manager->raise_exception("sort mismatch"); - if (arity == 2) { - sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); - symbol name("asFloat"); - return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } - else { - if (domain[2] != m_int_sort) - m_manager->raise_exception("sort mismatch"); - sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); - symbol name("asFloat"); - return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("asFloat"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); } } diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 482e280e3..18fea6c47 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -77,14 +77,23 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c return BR_FAILED; rational q; - if (!m_util.au().is_numeral(args[1], q)) + mpf q_mpf; + if (m_util.au().is_numeral(args[1], q)) { + mpf v; + m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); + result = m_util.mk_value(v); + m_util.fm().del(v); + return BR_DONE; + } + else if (m_util.is_value(args[1], q_mpf)) { + mpf v; + m_util.fm().set(v, ebits, sbits, rm, q_mpf); + result = m_util.mk_value(v); + m_util.fm().del(v); + return BR_DONE; + } + else return BR_FAILED; - - mpf v; - m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); - result = m_util.mk_value(v); - m_util.fm().del(v); - return BR_DONE; } else if (num_args == 3 && m_util.is_rm(m().get_sort(args[0])) && diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 2600cb3ec..37eaa365a 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1403,23 +1403,176 @@ void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * cons } void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - if (num == 3 && m_bv_util.is_bv(args[0]) && - m_bv_util.is_bv(args[1]) && m_bv_util.is_bv(args[2])) { + TRACE("fpa2bv_to_float", for (unsigned i=0; i < num; i++) + tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; ); + + if (num == 3 && + m_bv_util.is_bv(args[0]) && + m_bv_util.is_bv(args[1]) && + m_bv_util.is_bv(args[2])) { // Theoretically, the user could have thrown in it's own triple of bit-vectors. // Just keep it here, as there will be something else that uses it. mk_triple(args[0], args[1], args[2], result); } + else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) { + // We also support float to float conversion + expr_ref rm(m), x(m); + rm = args[0]; + x = args[1]; + + 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); + expr_ref one1(m); + + one1 = m_bv_util.mk_numeral(1, 1); + expr_ref ninf(m), pinf(m); + mk_plus_inf(f, pinf); + mk_minus_inf(f, ninf); + + // NaN -> NaN + mk_is_nan(x, c1); + mk_nan(f, v1); + + // +0 -> +0 + mk_is_pzero(x, c2); + mk_pzero(f, v2); + + // -0 -> -0 + mk_is_nzero(x, c3); + mk_nzero(f, v3); + + // +oo -> +oo + mk_is_pinf(x, c4); + v4 = pinf; + + // -oo -> -oo + mk_is_ninf(x, c5); + v5 = ninf; + + // otherwise: the actual conversion with rounding. + sort * s = f->get_range(); + expr_ref sgn(m), sig(m), exp(m); + unpack(x, sgn, sig, exp, true); + + expr_ref res_sgn(m), res_sig(m), res_exp(m); + + res_sgn = sgn; + + unsigned from_sbits = m_util.get_sbits(m.get_sort(args[1])); + unsigned from_ebits = m_util.get_ebits(m.get_sort(args[1])); + unsigned to_sbits = m_util.get_sbits(s); + unsigned to_ebits = m_util.get_ebits(s); + + SASSERT(m_bv_util.get_bv_size(sgn) == 1); + SASSERT(m_bv_util.get_bv_size(sig) == from_sbits); + SASSERT(m_bv_util.get_bv_size(exp) == from_ebits); + + if (from_sbits < (to_sbits + 3)) + // make sure that sig has at least to_sbits + 3 + res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits)); + else if (from_sbits > (to_sbits + 3)) + { + // collapse the extra bits into a sticky bit. + expr_ref sticky(m), low(m), high(m); + low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); + high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig); + unsigned high_sz = m_bv_util.get_bv_size(high); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low); + res_sig = m_bv_util.mk_concat(high, sticky); + } + else + res_sig = sig; + + res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder. + unsigned sig_sz = m_bv_util.get_bv_size(res_sig); + SASSERT(sig_sz == to_sbits+4); + + expr_ref exponent_overflow(m); + exponent_overflow = m.mk_false(); + + if (from_ebits < (to_ebits + 2)) + res_exp = m_bv_util.mk_sign_extend(to_ebits+2-from_ebits, exp); + else if (from_ebits > (to_ebits + 2)) + { + expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), or_eq(m), not_or_eq(m), and_eq(m); + expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m); + high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp); + low = m_bv_util.mk_extract(to_ebits+1, 0, exp); + lows = m_bv_util.mk_extract(to_ebits+1, to_ebits+1, low); + + high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high); + high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high); + + zero1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(high_red_and, one1, and_eq); + m_simp.mk_eq(high_red_or, zero1, or_eq); + m_simp.mk_eq(lows, zero1, s_is_zero); + m_simp.mk_eq(lows, one1, s_is_one); + + expr_ref c2(m); + m_simp.mk_ite(or_eq, s_is_one, m.mk_false(), c2); + m_simp.mk_ite(and_eq, s_is_zero, c2, exponent_overflow); + + // Note: Upon overflow, we _could_ try to shift the significand around... + + res_exp = low; + } + else + res_exp = exp; + + SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2); + + expr_ref rounded(m); + round(s, rm, res_sgn, res_sig, res_exp, rounded); + + expr_ref is_neg(m), sig_inf(m); + m_simp.mk_eq(sgn, one1, is_neg); + mk_ite(is_neg, ninf, pinf, sig_inf); + + dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow); + + mk_ite(exponent_overflow, sig_inf, rounded, v6); + + // And finally, we tie them together. + 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); + } else { + // .. other than that, we only support rationals for asFloat SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - - SASSERT(m_util.is_rm(to_app(args[0])->get_decl()->get_range())); + unsigned sbits = m_util.get_sbits(f->get_range()); + + //SASSERT(m_bv_util.is_numeral(args[0])); + //rational tmp_rat; unsigned sz; + //m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz); + //SASSERT(tmp_rat.is_int32()); + //SASSERT(sz == 3); + //BV_RM_VAL rm = (BV_RM_VAL) tmp_rat.get_unsigned(); + + /*mpf_rounding_mode rm; + switch(bv_rm) + { + case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break; + case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break; + case BV_RM_TO_NEGATIVE: rm = MPF_ROUND_TOWARD_NEGATIVE; break; + case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break; + case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break; + default: UNREACHABLE(); + }*/ + + SASSERT(m_util.au().is_numeral(args[1])); + + sort * rm_rng = to_app(args[0])->get_decl()->get_range(); + SASSERT(m_util.is_rm(rm_rng)); mpf_rounding_mode rm = static_cast(to_app(args[1])->get_decl_kind()); - + rational q; - SASSERT(m_util.au().is_numeral(args[1])); + SASSERT(m_util.au().is_numeral(args[1])); m_util.au().is_numeral(args[1], q); mpf v; @@ -1433,6 +1586,8 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a m_util.fm().del(v); } + + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 9618ffbce..dfac97626 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -367,7 +367,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode o.ebits = ebits; o.sbits = sbits; - signed ds = sbits - x.sbits; + signed ds = sbits - x.sbits + 4; // plus rounding bits if (ds > 0) { m_mpz_manager.mul2k(o.significand, ds); From 35906889b60753ca34b931c0465607d46d3d1c88 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 5 Mar 2013 13:49:42 +0000 Subject: [PATCH 09/11] FPA: compilation bugfixes Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 37eaa365a..42fdd0a62 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1476,8 +1476,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a expr_ref sticky(m), low(m), high(m); low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig); - unsigned high_sz = m_bv_util.get_bv_size(high); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get()); res_sig = m_bv_util.mk_concat(high, sticky); } else @@ -1494,24 +1493,24 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a res_exp = m_bv_util.mk_sign_extend(to_ebits+2-from_ebits, exp); else if (from_ebits > (to_ebits + 2)) { - expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), or_eq(m), not_or_eq(m), and_eq(m); + expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m); expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m); high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp); low = m_bv_util.mk_extract(to_ebits+1, 0, exp); lows = m_bv_util.mk_extract(to_ebits+1, to_ebits+1, low); - high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high); - high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high); + high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get()); + high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get()); zero1 = m_bv_util.mk_numeral(0, 1); - m_simp.mk_eq(high_red_and, one1, and_eq); - m_simp.mk_eq(high_red_or, zero1, or_eq); + m_simp.mk_eq(high_red_and, one1, h_and_eq); + m_simp.mk_eq(high_red_or, zero1, h_or_eq); m_simp.mk_eq(lows, zero1, s_is_zero); m_simp.mk_eq(lows, one1, s_is_one); expr_ref c2(m); - m_simp.mk_ite(or_eq, s_is_one, m.mk_false(), c2); - m_simp.mk_ite(and_eq, s_is_zero, c2, exponent_overflow); + m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2); + m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow); // Note: Upon overflow, we _could_ try to shift the significand around... @@ -2416,4 +2415,4 @@ model_converter * mk_fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, obj_map const & rm_const2bv) { return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv); -} \ No newline at end of file +} From 9a4331995e1e3b2fe779becfbb9185e3bda113c7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 5 Mar 2013 14:11:50 +0000 Subject: [PATCH 10/11] FPA: bugfix for bitblaster. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 42fdd0a62..d7d4458f8 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1546,14 +1546,14 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); - //SASSERT(m_bv_util.is_numeral(args[0])); - //rational tmp_rat; unsigned sz; - //m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz); - //SASSERT(tmp_rat.is_int32()); - //SASSERT(sz == 3); - //BV_RM_VAL rm = (BV_RM_VAL) tmp_rat.get_unsigned(); + SASSERT(m_bv_util.is_numeral(args[0])); + rational tmp_rat; unsigned sz; + m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz); + SASSERT(tmp_rat.is_int32()); + SASSERT(sz == 3); + BV_RM_VAL bv_rm = (BV_RM_VAL) tmp_rat.get_unsigned(); - /*mpf_rounding_mode rm; + mpf_rounding_mode rm; switch(bv_rm) { case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break; @@ -1562,14 +1562,10 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break; case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break; default: UNREACHABLE(); - }*/ + } SASSERT(m_util.au().is_numeral(args[1])); - sort * rm_rng = to_app(args[0])->get_decl()->get_range(); - SASSERT(m_util.is_rm(rm_rng)); - mpf_rounding_mode rm = static_cast(to_app(args[1])->get_decl_kind()); - rational q; SASSERT(m_util.au().is_numeral(args[1])); m_util.au().is_numeral(args[1], q); From bdc675b1dfef87fcffeb7f3e5143128492d3bd89 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 Mar 2013 09:04:03 -0800 Subject: [PATCH 11/11] Fix bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/ast/macros/macro_util.cpp | 15 +++++++++++---- src/model/model_v2_pp.cpp | 5 +++++ 3 files changed, 18 insertions(+), 4 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 7aaaf2f8d..643c9b26f 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -63,6 +63,8 @@ Version 4.3.2 - Fixed bug reported at http://z3.codeplex.com/workitem/23 (Thanks to Paul Jackson). +- Fixed bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 (Thanks to Tianhai Liu). + Version 4.3.1 ============= diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index e9b9c831e..bd21aa1ac 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -597,8 +597,9 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref is_hint_head(head, vars) must also return true */ bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) { - TRACE("macro_util_hint", tout << "is_poly_hint n:\n" << mk_pp(n, m_manager) << "\nhead:\n" << mk_pp(head, m_manager) << "\nexception:\n" - << mk_pp(exception, m_manager) << "\n";); + TRACE("macro_util_hint", tout << "is_poly_hint n:\n" << mk_pp(n, m_manager) << "\nhead:\n" << mk_pp(head, m_manager) << "\nexception:\n"; + if (exception) tout << mk_pp(exception, m_manager); else tout << ""; + tout << "\n";); ptr_buffer vars; if (!is_hint_head(head, vars)) { TRACE("macro_util_hint", tout << "failed because head is not hint head\n";); @@ -792,7 +793,10 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a mk_add(args.size(), args.c_ptr(), m_manager.get_sort(arg), rest); expr_ref def(m_manager); mk_sub(rhs, rest, def); - add_arith_macro_candidate(to_app(arg), num_decls, def, atom, is_ineq, _is_poly_hint, r); + // If is_poly_hint, rhs may contain variables that do not occur in to_app(arg). + // So, we should re-check. + if (!_is_poly_hint || is_poly_hint(def, to_app(arg), 0)) + add_arith_macro_candidate(to_app(arg), num_decls, def, atom, is_ineq, _is_poly_hint, r); } else if (is_times_minus_one(arg, neg_arg) && is_app(neg_arg)) { f = to_app(neg_arg)->get_decl(); @@ -810,7 +814,10 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a mk_add(args.size(), args.c_ptr(), m_manager.get_sort(arg), rest); expr_ref def(m_manager); mk_sub(rest, rhs, def); - add_arith_macro_candidate(to_app(neg_arg), num_decls, def, atom, is_ineq, _is_poly_hint, r); + // If is_poly_hint, rhs may contain variables that do not occur in to_app(neg_arg). + // So, we should re-check. + if (!_is_poly_hint || is_poly_hint(def, to_app(neg_arg), 0)) + add_arith_macro_candidate(to_app(neg_arg), num_decls, def, atom, is_ineq, _is_poly_hint, r); } } } diff --git a/src/model/model_v2_pp.cpp b/src/model/model_v2_pp.cpp index 9073ddece..4600ccc9e 100644 --- a/src/model/model_v2_pp.cpp +++ b/src/model/model_v2_pp.cpp @@ -80,3 +80,8 @@ void model_v2_pp(std::ostream & out, model_core const & md, bool partial) { display_constants(out, md); display_functions(out, md, partial); } + +// debugging support +void pp(model_core const & md) { + model_v2_pp(std::cout, md, false); +}