From 6f3850bfbcb7565043c08c6b32476d2c63b22358 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 28 Feb 2013 18:46:29 +0000 Subject: [PATCH] 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());