From 7c32df93a4627f78c6be0dba6d6817967ce28c4d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 3 Jun 2013 18:17:41 +0100 Subject: [PATCH 01/14] SLS tactic: compilation fixes Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/sls_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index f49ce8422..69e1c8bc3 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -1370,7 +1370,7 @@ class sls_tactic : public tactic { void updt_params(params_ref const & p) { m_produce_models = p.get_bool("produce_models", false); - m_max_restarts = p.get_uint("sls_restarts", -1); + m_max_restarts = p.get_uint("sls_restarts", (unsigned)-1); m_tracker.set_random_seed(p.get_uint("random_seed", 0)); m_plateau_limit = p.get_uint("plateau_limit", 100); } @@ -1612,7 +1612,7 @@ class sls_tactic : public tactic { lbool search(goal_ref const & g) { lbool res = l_undef; double score = 0.0, old_score = 0.0; - unsigned new_const = -1, new_bit = 0; + unsigned new_const = (unsigned)-1, new_bit = 0; mpz new_value; move_type move; @@ -1631,7 +1631,7 @@ class sls_tactic : public tactic { checkpoint(); old_score = score; - new_const = -1; + new_const = (unsigned)-1; ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g); From 093fe945bc3e57d5d8c1f9f4afdf597549ef8ab2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 3 Jun 2013 18:19:45 +0100 Subject: [PATCH 02/14] FPA: min/max/fma bugfixes + partial quantifier support Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 223 ++++++++++++++++++++-------- src/tactic/fpa/fpa2bv_rewriter.h | 16 +- 2 files changed, 165 insertions(+), 74 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 363cf1df8..02aff67c6 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1022,13 +1022,15 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, split(x, x_sgn, x_sig, x_exp); split(y, y_sgn, y_sig, y_exp); - expr_ref c1(m), c2(m), y_is_nan(m), x_is_nzero(m), y_is_zero(m), c2_and(m); - mk_is_nan(x, c1); - mk_is_nan(y, y_is_nan); - mk_is_nzero(x, x_is_nzero); + expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), c1_and(m); + mk_is_zero(x, x_is_zero); mk_is_zero(y, y_is_zero); - m_simp.mk_and(x_is_nzero, y_is_zero, c2_and); - m_simp.mk_or(y_is_nan, c2_and, c2); + m_simp.mk_and(x_is_zero, y_is_zero, c1_and); + mk_is_nan(x, x_is_nan); + m_simp.mk_or(x_is_nan, c1_and, c1); + + mk_is_nan(y, y_is_nan); + c2 = y_is_nan; expr_ref c3(m); mk_float_lt(f, num, args, c3); @@ -1063,13 +1065,15 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, split(x, x_sgn, x_sig, x_exp); split(y, y_sgn, y_sig, y_exp); - expr_ref c1(m), c2(m), y_is_nan(m), y_is_nzero(m), x_is_zero(m), xy_is_zero(m); - mk_is_nan(x, c1); - mk_is_nan(y, y_is_nan); - mk_is_nzero(y, y_is_nzero); + expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), y_is_zero(m), x_is_zero(m), c1_and(m); + mk_is_zero(y, y_is_zero); mk_is_zero(x, x_is_zero); - m_simp.mk_and(y_is_nzero, x_is_zero, xy_is_zero); - m_simp.mk_or(y_is_nan, xy_is_zero, c2); + m_simp.mk_and(y_is_zero, x_is_zero, c1_and); + mk_is_nan(x, x_is_nan); + m_simp.mk_or(x_is_nan, c1_and, c1); + + mk_is_nan(y, y_is_nan); + c2 = y_is_nan; expr_ref c3(m); mk_float_gt(f, num, args, c3); @@ -1111,20 +1115,23 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar mk_minus_inf(f, ninf); mk_plus_inf(f, pinf); - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); - expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); - expr_ref z_is_nan(m), z_is_zero(m), z_is_pos(m), z_is_inf(m); + expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m); + expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m); + expr_ref z_is_nan(m), z_is_zero(m), z_is_pos(m), z_is_neg(m), z_is_inf(m); mk_is_nan(x, x_is_nan); mk_is_zero(x, x_is_zero); mk_is_pos(x, x_is_pos); + mk_is_neg(x, x_is_neg); mk_is_inf(x, x_is_inf); mk_is_nan(y, y_is_nan); mk_is_zero(y, y_is_zero); mk_is_pos(y, y_is_pos); + mk_is_neg(y, y_is_neg); mk_is_inf(y, y_is_inf); mk_is_nan(z, z_is_nan); mk_is_zero(z, z_is_zero); mk_is_pos(z, z_is_pos); + mk_is_neg(z, z_is_neg); mk_is_inf(z, z_is_inf); dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan); @@ -1140,42 +1147,56 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar dbg_decouple("fpa2bv_fma_z_is_pos", z_is_pos); dbg_decouple("fpa2bv_fma_z_is_inf", z_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); + expr_ref inf_xor(m), inf_cond(m); + m_simp.mk_xor(x_is_neg, y_is_neg, inf_xor); + m_simp.mk_xor(inf_xor, z_is_neg, inf_xor); + m_simp.mk_and(z_is_inf, inf_xor, inf_cond); + + // (x is NaN) || (y is NaN) || (z is Nan) -> NaN + m_simp.mk_or(x_is_nan, y_is_nan, z_is_nan, c1); v1 = nan; // (x is +oo) -> if (y is 0) then NaN else inf with y's sign. mk_is_pinf(x, c2); - expr_ref y_sgn_inf(m); + expr_ref y_sgn_inf(m), inf_or(m); mk_ite(y_is_pos, pinf, ninf, y_sgn_inf); - mk_ite(y_is_zero, nan, y_sgn_inf, v2); + m_simp.mk_or(y_is_zero, inf_cond, inf_or); + mk_ite(inf_or, nan, y_sgn_inf, v2); // (y is +oo) -> if (x is 0) then NaN else inf with x's sign. mk_is_pinf(y, c3); expr_ref x_sgn_inf(m); mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); - mk_ite(x_is_zero, nan, x_sgn_inf, v3); + m_simp.mk_or(x_is_zero, inf_cond, inf_or); + mk_ite(inf_or, nan, x_sgn_inf, v3); // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign. mk_is_ninf(x, c4); expr_ref neg_y_sgn_inf(m); mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf); - mk_ite(y_is_zero, nan, neg_y_sgn_inf, v4); + m_simp.mk_or(y_is_zero, inf_cond, inf_or); + mk_ite(inf_or, nan, neg_y_sgn_inf, v4); // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign. mk_is_ninf(y, c5); expr_ref neg_x_sgn_inf(m); mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf); - mk_ite(x_is_zero, nan, neg_x_sgn_inf, v5); + m_simp.mk_or(x_is_zero, inf_cond, inf_or); + mk_ite(inf_or, nan, neg_x_sgn_inf, v5); + + // z is +-INF -> Z. + mk_is_inf(z, c6); + v6 = z; // (x is 0) || (y is 0) -> x but with sign = x.sign ^ y.sign - m_simp.mk_or(x_is_zero, y_is_zero, c6); + m_simp.mk_or(x_is_zero, y_is_zero, c7); expr_ref sign_xor(m); m_simp.mk_xor(x_is_pos, y_is_pos, sign_xor); - mk_ite(sign_xor, nzero, pzero, v6); + mk_ite(sign_xor, nzero, pzero, v7); + // else comes the fused multiplication. unsigned ebits = m_util.get_ebits(f->get_range()); @@ -1190,54 +1211,57 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar expr_ref c_sgn(m), c_sig(m), c_exp(m), c_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - unpack(z, c_sgn, c_sig, c_exp, c_lz, false); + unpack(z, c_sgn, c_sig, c_exp, c_lz, true); - expr_ref a_lz_ext(m), b_lz_ext(m); + expr_ref a_lz_ext(m), b_lz_ext(m), c_lz_ext(m); a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); + c_lz_ext = m_bv_util.mk_zero_extend(2, c_lz); expr_ref a_sig_ext(m), b_sig_ext(m); a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig); b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig); - expr_ref a_exp_ext(m), b_exp_ext(m); + expr_ref a_exp_ext(m), b_exp_ext(m), c_exp_ext(m); a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp); b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); + c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp); expr_ref mul_sgn(m), mul_sig(m), mul_exp(m); expr * signs[2] = { a_sgn, b_sgn }; - mul_sgn = m_bv_util.mk_bv_xor(2, signs); + mul_sgn = m_bv_util.mk_bv_xor(2, signs); dbg_decouple("fpa2bv_fma_mul_sgn", mul_sgn); - mul_exp = m_bv_util.mk_bv_sub( - m_bv_util.mk_bv_add(a_exp_ext, b_exp_ext), - m_bv_util.mk_bv_add(a_lz_ext, b_lz_ext)); + mul_exp = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), + m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); + dbg_decouple("fpa2bv_fma_mul_exp", mul_exp); mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext); - dbg_decouple("fpa2bv_fma_mul_sig", mul_sig); SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits); + SASSERT(m_bv_util.get_bv_size(mul_exp) == ebits + 2); - // The result in `product' represents a number of the form 1.*** (unpacked) - // (product = mul_sgn/mul_sig/mul_exp and c_sgn/c_sig/c_exp is unpacked w/o normalization). + // The product has the form [-1][0].[2*sbits - 2]. + + // Extend c + c_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits-1))); - // extend c. - c_sig = m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits)); - c_exp = m_bv_util.mk_sign_extend(2, c_exp); + SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits); + SASSERT(m_bv_util.get_bv_size(c_sig) == 2 * sbits); expr_ref swap_cond(m); - swap_cond = m_bv_util.mk_sle(mul_exp, c_exp); + swap_cond = m_bv_util.mk_sle(mul_exp, c_exp_ext); SASSERT(is_well_sorted(m, swap_cond)); expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m); m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn); m_simp.mk_ite(swap_cond, c_sig, mul_sig, e_sig); // has 2 * sbits - m_simp.mk_ite(swap_cond, c_exp, mul_exp, e_exp); // has ebits + 2 + m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2 m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn); m_simp.mk_ite(swap_cond, mul_sig, c_sig, f_sig); // has 2 * sbits - m_simp.mk_ite(swap_cond, mul_exp, c_exp, f_exp); // has ebits + 2 + m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2 SASSERT(is_well_sorted(m, e_sgn)); SASSERT(is_well_sorted(m, e_sig)); @@ -1247,26 +1271,94 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar SASSERT(is_well_sorted(m, f_exp)); expr_ref res_sgn(m), res_sig(m), res_exp(m); - add_core(2 * sbits, ebits + 2, rm, - e_sgn, e_sig, e_exp, f_sgn, f_sig, f_exp, - res_sgn, res_sig, res_exp); + + expr_ref exp_delta(m); + exp_delta = m_bv_util.mk_bv_sub(e_exp, f_exp); + dbg_decouple("fpa2bv_fma_add_exp_delta", exp_delta); - // Note: res_sig is now 2 * sbits + 4, i.e., `sbits' too much, which should go into a sticky bit. - unsigned sig_size = m_bv_util.get_bv_size(res_sig); - SASSERT(sig_size == (2*sbits+4)); + // cap the delta + expr_ref cap(m), cap_le_delta(m); + cap = m_bv_util.mk_numeral(sbits+3, ebits+2); + cap_le_delta = m_bv_util.mk_ule(exp_delta, cap); + m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta); + SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2); + dbg_decouple("fpa2bv_fma_add_exp_delta_capped", exp_delta); + + // Alignment shift with sticky bit computation. + expr_ref big_f_sig(m); + big_f_sig = m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits+4)); + SASSERT(is_well_sorted(m, big_f_sig)); - // Note: res_exp is 2 bits too wide. - unsigned exp_size = m_bv_util.get_bv_size(res_exp); - SASSERT(exp_size == ebits+4); - res_exp = m_bv_util.mk_extract(ebits+1, 0, res_exp); + expr_ref shifted_big(m), shifted_f_sig(m), sticky_raw(m); + shifted_big = m_bv_util.mk_bv_lshr(big_f_sig, m_bv_util.mk_concat(m_bv_util.mk_numeral(0, (2*(sbits+4))-(ebits+2)), exp_delta)); + shifted_f_sig = m_bv_util.mk_extract((2*(sbits+4)-1), (sbits+4), shifted_big); + SASSERT(is_well_sorted(m, shifted_f_sig)); - expr_ref sticky(m); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits, 0, res_sig)); - res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(2*sbits+3, sbits+1, res_sig), sticky); + sticky_raw = m_bv_util.mk_extract(sbits+3, 0, shifted_big); + expr_ref sticky(m), sticky_eq(m), nil_sbit4(m), one_sbit4(m); + nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4); + one_sbit4 = m_bv_util.mk_numeral(1, sbits+4); + m_simp.mk_eq(sticky_raw, nil_sbit4, sticky_eq); + m_simp.mk_ite(sticky_eq, nil_sbit4, one_sbit4, sticky); + SASSERT(is_well_sorted(m, sticky)); + + expr * or_args[2] = { shifted_f_sig, sticky }; + shifted_f_sig = m_bv_util.mk_bv_or(2, or_args); + SASSERT(is_well_sorted(m, shifted_f_sig)); - sig_size = m_bv_util.get_bv_size(res_sig); - SASSERT(sig_size == sbits+4); + expr_ref eq_sgn(m); + m_simp.mk_eq(e_sgn, f_sgn, eq_sgn); + + // two extra bits for catching the overflow. + e_sig = m_bv_util.mk_zero_extend(2, e_sig); + shifted_f_sig = m_bv_util.mk_zero_extend(2, shifted_f_sig); + SASSERT(m_bv_util.get_bv_size(e_sig) == sbits+6); + SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == sbits+6); + + dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); + dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); + + expr_ref sum(m); + m_simp.mk_ite(eq_sgn, + m_bv_util.mk_bv_add(e_sig, shifted_f_sig), // ADD LZ + m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), + sum); + + SASSERT(is_well_sorted(m, sum)); + + dbg_decouple("fpa2bv_fma_add_sum", sum); + + expr_ref sign_bv(m), n_sum(m); + sign_bv = m_bv_util.mk_extract(sbits+4, sbits+4, sum); + n_sum = m_bv_util.mk_bv_neg(sum); + + dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv); + dbg_decouple("fpa2bv_fma_add_n_sum", n_sum); + + family_id bvfid = m_bv_util.get_fid(); + + expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); + expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m); + not_e_sgn = m_bv_util.mk_bv_not(e_sgn); + not_f_sgn = m_bv_util.mk_bv_not(f_sgn); + not_sign_bv = m_bv_util.mk_bv_not(sign_bv); + res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, e_sgn, sign_bv); + res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv); + res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_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); + + 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_fma_add_sig_abs", sig_abs); + + res_sig = m_bv_util.mk_extract(sbits+3, 0, sig_abs); + res_exp = m_bv_util.mk_bv_sub(e_exp, c_lz_ext); + 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); @@ -1281,10 +1373,11 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar expr_ref rounded(m); round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded); - mk_ite(is_zero_sig, zero_case, rounded, v7); + mk_ite(is_zero_sig, zero_case, rounded, 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); @@ -1293,7 +1386,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_mul", tout << "MUL = " << mk_ismt2_pp(result, m) << std::endl; ); + TRACE("fpa2bv_fma_", tout << "FMA = " << mk_ismt2_pp(result, m) << std::endl; ); } void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -2571,9 +2664,13 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { sz = bv_mdl->get_num_functions(); for (unsigned i = 0; i < sz; i++) { - func_decl * c = bv_mdl->get_function(i); - if (!seen.contains(c)) - float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); + func_decl * f = bv_mdl->get_function(i); + if (!seen.contains(f)) + { + TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl; ); + func_interp * val = bv_mdl->get_func_interp(f); + float_mdl->register_decl(f, val); + } } sz = bv_mdl->get_num_uninterpreted_sorts(); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 3398874f5..d8a141b62 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -29,9 +29,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { ast_manager & m_manager; expr_ref_vector m_out; fpa2bv_converter & m_conv; - sort_ref_vector m_bindings; - expr_ref_vector m_mappings; - + sort_ref_vector m_bindings; unsigned long long m_max_memory; unsigned m_max_steps; @@ -42,8 +40,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { m_manager(m), m_out(m), m_conv(c), - m_bindings(m), - m_mappings(m) { + m_bindings(m) { updt_params(p); // We need to make sure that the mananger has the BV plugin loaded. symbol s_bv("bv"); @@ -177,7 +174,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { new_bindings.push_back(q->get_decl_sort(i)); SASSERT(new_bindings.size() == q->get_num_decls()); m_bindings.append(new_bindings); - m_mappings.resize(m_bindings.size(), 0); } return true; } @@ -215,8 +211,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); result_pr = 0; - m_bindings.shrink(old_sz); - m_mappings.shrink(old_sz); + m_bindings.shrink(old_sz); TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; @@ -243,10 +238,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { new_exp); } else - new_exp = m().mk_var(t->get_idx(), s); - m_mappings[inx] = new_exp; + new_exp = m().mk_var(t->get_idx(), s); - result = m_mappings[inx].get(); + result = new_exp; result_pr = 0; TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); return true; From e5c720de29f146f3380b7069b3e102a044f3a295 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Jun 2013 17:36:34 +0100 Subject: [PATCH 03/14] FPA: bugfix for abs Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 4ec17addf..5c18e1241 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -223,7 +223,7 @@ public: app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_REM, arg1, arg2); } app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MAX, arg1, arg2); } app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); } - app * mk_abs(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1, arg2); } + app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1); } app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_SQRT, arg1, arg2); } app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); } app * mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) { From 123d3ec3a765ff57b449526f49808efef3a9f36b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Jun 2013 17:55:29 +0100 Subject: [PATCH 04/14] New FPA operators added. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 11 ++++++++++- src/ast/float_decl_plugin.h | 8 +++++++- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 2a090fc39..21d4d6a86 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -255,7 +255,10 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param case OP_FLOAT_IS_ZERO: name = "isZero"; break; case OP_FLOAT_IS_NZERO: name = "isNZero"; break; case OP_FLOAT_IS_PZERO: name = "isPZero"; break; - case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break; + case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break; + case OP_FLOAT_IS_INF: name = "isInfinite"; break; + case OP_FLOAT_IS_NORMAL: name = "isNormal"; break; + case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal"; break; default: UNREACHABLE(); break; @@ -415,6 +418,9 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_FLOAT_IS_NZERO: case OP_FLOAT_IS_PZERO: case OP_FLOAT_IS_SIGN_MINUS: + case OP_FLOAT_IS_INF: + case OP_FLOAT_IS_NORMAL: + case OP_FLOAT_IS_SUBNORMAL: return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range); case OP_FLOAT_ABS: case OP_FLOAT_UMINUS: @@ -473,9 +479,12 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("<=", OP_FLOAT_LE)); op_names.push_back(builtin_name(">=", OP_FLOAT_GE)); + op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF)); op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO)); op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO)); op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO)); + op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL)); + op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL)); op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS)); op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 5c18e1241..fd632a8a1 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -61,9 +61,12 @@ enum float_op_kind { OP_FLOAT_GT, OP_FLOAT_LE, OP_FLOAT_GE, + OP_FLOAT_IS_INF, OP_FLOAT_IS_ZERO, - OP_FLOAT_IS_NZERO, + OP_FLOAT_IS_NORMAL, + OP_FLOAT_IS_SUBNORMAL, OP_FLOAT_IS_PZERO, + OP_FLOAT_IS_NZERO, OP_FLOAT_IS_SIGN_MINUS, OP_TO_FLOAT, @@ -237,7 +240,10 @@ public: app * mk_le(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_LE, arg1, arg2); } app * mk_ge(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_GE, arg1, arg2); } + app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_INF, arg1); } app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_ZERO, arg1); } + app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NORMAL, arg1); } + app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); } app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); } app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); } app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); } From d7639557d2867e8cade627237fc686ff76e59580 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Jun 2013 18:03:46 +0100 Subject: [PATCH 05/14] FPA: added rewriting and fpa2bv conversion rules for new operations. Signed-off-by: Christoph M. Wintersteiger --- src/ast/rewriter/float_rewriter.cpp | 33 +++++++++++++++++++++++++++++ src/ast/rewriter/float_rewriter.h | 3 +++ src/tactic/fpa/fpa2bv_converter.cpp | 15 +++++++++++++ src/tactic/fpa/fpa2bv_converter.h | 3 +++ src/tactic/fpa/fpa2bv_rewriter.h | 3 +++ 5 files changed, 57 insertions(+) diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index b43f07b65..bfcfbcbfc 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -58,6 +58,9 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_ZERO: SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break; case OP_FLOAT_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break; case OP_FLOAT_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break; + case OP_FLOAT_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break; + case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break; + case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; } @@ -428,6 +431,36 @@ br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { return BR_FAILED; } +br_status float_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_inf(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_normal(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_denormal(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 7c86a5bc3..6968d96cf 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -66,6 +66,9 @@ public: br_status mk_is_zero(expr * arg1, expr_ref & result); br_status mk_is_nzero(expr * arg1, expr_ref & result); br_status mk_is_pzero(expr * arg1, expr_ref & result); + br_status mk_is_inf(expr * arg1, expr_ref & result); + br_status mk_is_normal(expr * arg1, expr_ref & result); + br_status mk_is_subnormal(expr * arg1, expr_ref & result); br_status mk_is_sign_minus(expr * arg1, expr_ref & result); br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 02aff67c6..d95709813 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1621,6 +1621,21 @@ void fpa2bv_converter::mk_is_pzero(func_decl * f, unsigned num, expr * const * a m_simp.mk_and(a0_is_pos, a0_is_zero, result); } +void fpa2bv_converter::mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_inf(args[0], result); +} + +void fpa2bv_converter::mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_normal(args[0], result); +} + +void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_denormal(args[0], result); +} + void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); mk_is_neg(args[0], result); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 2a68342f8..9f9c74c38 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -116,6 +116,9 @@ public: void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); 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); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index d8a141b62..59d068626 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -132,6 +132,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; From 455618bb2b1564eb026b0984c2fe022150efcf02 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Jun 2013 18:34:31 +0100 Subject: [PATCH 06/14] FPA: added is_nan Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 3 +++ src/ast/float_decl_plugin.h | 2 ++ src/ast/rewriter/float_rewriter.cpp | 11 +++++++++++ src/ast/rewriter/float_rewriter.h | 1 + src/tactic/fpa/fpa2bv_converter.cpp | 5 +++++ src/tactic/fpa/fpa2bv_converter.h | 1 + src/tactic/fpa/fpa2bv_rewriter.h | 1 + 7 files changed, 24 insertions(+) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 21d4d6a86..4aab6ab32 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -256,6 +256,7 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param case OP_FLOAT_IS_NZERO: name = "isNZero"; break; case OP_FLOAT_IS_PZERO: name = "isPZero"; break; case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break; + case OP_FLOAT_IS_NAN: name = "isNaN"; break; case OP_FLOAT_IS_INF: name = "isInfinite"; break; case OP_FLOAT_IS_NORMAL: name = "isNormal"; break; case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal"; break; @@ -418,6 +419,7 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_FLOAT_IS_NZERO: case OP_FLOAT_IS_PZERO: case OP_FLOAT_IS_SIGN_MINUS: + case OP_FLOAT_IS_NAN: case OP_FLOAT_IS_INF: case OP_FLOAT_IS_NORMAL: case OP_FLOAT_IS_SUBNORMAL: @@ -479,6 +481,7 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("<=", OP_FLOAT_LE)); op_names.push_back(builtin_name(">=", OP_FLOAT_GE)); + op_names.push_back(builtin_name("isNaN", OP_FLOAT_IS_NAN)); op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF)); op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO)); op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO)); diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index fd632a8a1..f1b60a91b 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -61,6 +61,7 @@ enum float_op_kind { OP_FLOAT_GT, OP_FLOAT_LE, OP_FLOAT_GE, + OP_FLOAT_IS_NAN, OP_FLOAT_IS_INF, OP_FLOAT_IS_ZERO, OP_FLOAT_IS_NORMAL, @@ -240,6 +241,7 @@ public: app * mk_le(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_LE, arg1, arg2); } app * mk_ge(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_GE, arg1, arg2); } + app * mk_is_nan(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NAN, arg1); } app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_INF, arg1); } app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_ZERO, arg1); } app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NORMAL, arg1); } diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index bfcfbcbfc..015bce0ed 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -58,6 +58,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_ZERO: SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break; case OP_FLOAT_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break; case OP_FLOAT_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break; + case OP_FLOAT_IS_NAN: SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break; case OP_FLOAT_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break; case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break; case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; @@ -431,6 +432,16 @@ br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { return BR_FAILED; } +br_status float_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_nan(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + br_status float_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 6968d96cf..4a0879d4b 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -66,6 +66,7 @@ public: br_status mk_is_zero(expr * arg1, expr_ref & result); br_status mk_is_nzero(expr * arg1, expr_ref & result); br_status mk_is_pzero(expr * arg1, expr_ref & result); + br_status mk_is_nan(expr * arg1, expr_ref & result); br_status mk_is_inf(expr * arg1, expr_ref & result); br_status mk_is_normal(expr * arg1, expr_ref & result); br_status mk_is_subnormal(expr * arg1, expr_ref & result); diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index d95709813..dd40e8453 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1621,6 +1621,11 @@ void fpa2bv_converter::mk_is_pzero(func_decl * f, unsigned num, expr * const * a m_simp.mk_and(a0_is_pos, a0_is_zero, result); } +void fpa2bv_converter::mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_nan(args[0], result); +} + void fpa2bv_converter::mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); mk_is_inf(args[0], result); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 9f9c74c38..821618bae 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -116,6 +116,7 @@ public: void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 59d068626..24e275c0d 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -132,6 +132,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; From 0210156bf0c59844a65aacb4957ce49cd65e3761 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Jun 2013 10:51:56 -0400 Subject: [PATCH 07/14] add convex interior generalizer Signed-off-by: Nikolaj Bjorner --- src/muz_qe/fixedpoint_params.pyg | 1 + src/muz_qe/pdr_context.cpp | 3 + src/muz_qe/pdr_generalizers.cpp | 171 +++++++++++++++++++++++++++++++ src/muz_qe/pdr_generalizers.h | 17 +++ 4 files changed, 192 insertions(+) diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index d38c3c9b0..c2996dd8f 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -48,6 +48,7 @@ def_module_params('fixedpoint', ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"), ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"), ('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"), + ('use_convex_hull_generalizer', BOOL, False, "PDR: generalize using convex hulls of lemmas"), ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"), ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when " "checking for reachability (not only during cube weakening)"), diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 76f744325..1c49e0c83 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1572,6 +1572,9 @@ namespace pdr { } } + if (m_params.use_convex_hull_generalizer()) { + m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this)); + } if (!use_mc && m_params.use_inductive_generalizer()) { m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0)); } diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index 1b8ea22f9..800a21eaf 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -147,6 +147,177 @@ namespace pdr { } + core_convex_hull_generalizer::core_convex_hull_generalizer(context& ctx): + core_generalizer(ctx), + m(ctx.get_manager()), + a(m), + m_sigma(m), + m_trail(m) { + m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real())); + m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real())); + } + + void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { + manager& pm = n.pt().get_pdr_manager(); + expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m); + if (core.empty()) { + return; + } + if (!m_left.contains(n.pt().head())) { + expr_ref left(m), right(m); + m_left.insert(n.pt().head(), 0); + unsigned sz = n.pt().sig_size(); + for (unsigned i = 0; i < sz; ++i) { + func_decl* fn0 = n.pt().sig(i); + sort* srt = fn0->get_range(); + if (a.is_int_real(srt)) { + func_decl* fn1 = pm.o2n(fn0, 0); + left = m.mk_fresh_const(fn1->get_name().str().c_str(), srt); + right = m.mk_fresh_const(fn1->get_name().str().c_str(), srt); + m_left.insert(fn1, left); + m_right.insert(fn1, right); + m_trail.push_back(left); + m_trail.push_back(right); + } + } + } + unsigned sz = n.pt().sig_size(); + for (unsigned i = 0; i < sz; ++i) { + expr* left, *right; + func_decl* fn0 = n.pt().sig(i); + func_decl* fn1 = pm.o2n(fn0, 0); + if (m_left.find(fn1, left) && m_right.find(fn1, right)) { + eqs.push_back(m.mk_eq(m.mk_const(fn1), a.mk_add(left, right))); + } + } + if (!mk_convex(core, 0, conv1)) { + IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";); + return; + } + conv1.append(eqs); + conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real()))); + conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real()))); + conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get()))); + expr_ref fml = n.pt().get_formulas(n.level(), false); + expr_ref_vector fmls(m); + datalog::flatten_and(fml, fmls); + for (unsigned i = 0; i < fmls.size(); ++i) { + fml = m.mk_not(fmls[i].get()); + core2.reset(); + datalog::flatten_and(fml, core2); + if (!mk_convex(core2, 1, conv2)) { + IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core2), m) << "\n";); + continue; + } + conv2.append(conv1); + expr_ref state = pm.mk_and(conv2); + TRACE("pdr", tout << "Check:\n" << mk_pp(state, m) << "\n"; + tout << "New formula:\n" << mk_pp(pm.mk_and(core), m) << "\n"; + tout << "Old formula:\n" << mk_pp(fml, m) << "\n"; + + ); + model_node nd(0, state, n.pt(), n.level()); + if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) { + TRACE("pdr", + tout << mk_pp(state, m) << "\n"; + tout << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";); + IF_VERBOSE(0, + verbose_stream() << mk_pp(state, m) << "\n"; + verbose_stream() << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";); + core.reset(); + core.append(conv2); + } + } + } + + bool core_convex_hull_generalizer::mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv) { + conv.reset(); + for (unsigned i = 0; i < core.size(); ++i) { + mk_convex(core[i], index, conv); + } + return !conv.empty(); + } + + void core_convex_hull_generalizer::mk_convex(expr* fml, unsigned index, expr_ref_vector& conv) { + expr_ref result(m), r1(m), r2(m); + expr* e1, *e2; + bool is_not = m.is_not(fml, fml); + if (a.is_le(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = a.mk_le(r1, r2); + } + else if (a.is_ge(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = a.mk_ge(r1, r2); + } + else if (a.is_gt(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = a.mk_gt(r1, r2); + } + else if (a.is_lt(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = a.mk_lt(r1, r2); + } + else if (m.is_eq(fml, e1, e2) && a.is_int_real(e1) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = m.mk_eq(r1, r2); + } + else { + TRACE("pdr", tout << "Did not handle " << mk_pp(fml, m) << "\n";); + return; + } + if (is_not) { + result = m.mk_not(result); + } + conv.push_back(result); + } + + + bool core_convex_hull_generalizer::translate(func_decl* f, unsigned index, expr_ref& result) { + expr* tmp; + if (index == 0 && m_left.find(f, tmp)) { + result = tmp; + return true; + } + if (index == 1 && m_right.find(f, tmp)) { + result = tmp; + return true; + } + return false; + } + + + bool core_convex_hull_generalizer::mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result) { + if (!is_app(term)) { + return false; + } + app* app = to_app(term); + expr* e1, *e2; + expr_ref r1(m), r2(m); + if (translate(app->get_decl(), index, result)) { + return true; + } + if (a.is_add(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) { + result = a.mk_add(r1, r2); + return true; + } + if (a.is_sub(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) { + result = a.mk_sub(r1, r2); + return true; + } + if (a.is_mul(term, e1, e2) && mk_convex(e1, index, true, r1) && mk_convex(e2, index, true, r2)) { + result = a.mk_mul(r1, r2); + return true; + } + if (a.is_numeral(term)) { + if (is_mul) { + result = term; + } + else { + result = a.mk_mul(m_sigma[index].get(), term); + } + return true; + } + IF_VERBOSE(0, verbose_stream() << "Not handled: " << mk_pp(term, m) << "\n";); + return false; + } + + // --------------------------------- // core_arith_inductive_generalizer // NB. this is trying out some ideas for generalization in diff --git a/src/muz_qe/pdr_generalizers.h b/src/muz_qe/pdr_generalizers.h index 03bd89c4d..a4be9d1fa 100644 --- a/src/muz_qe/pdr_generalizers.h +++ b/src/muz_qe/pdr_generalizers.h @@ -73,6 +73,23 @@ namespace pdr { virtual void collect_statistics(statistics& st) const; }; + class core_convex_hull_generalizer : public core_generalizer { + ast_manager& m; + arith_util a; + expr_ref_vector m_sigma; + expr_ref_vector m_trail; + obj_map m_left; + obj_map m_right; + bool mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv); + void mk_convex(expr* fml, unsigned index, expr_ref_vector& conv); + bool mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result); + bool translate(func_decl* fn, unsigned index, expr_ref& result); + public: + core_convex_hull_generalizer(context& ctx); + virtual ~core_convex_hull_generalizer() {} + virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); + }; + class core_multi_generalizer : public core_generalizer { core_bool_inductive_generalizer m_gen; public: From 6184c5fdbcad3ad666f8220cdebcae4601b03bd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Jun 2013 15:29:22 -0400 Subject: [PATCH 08/14] reorder attibutes to match initialization order Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_instruction.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index 6b16968c2..637d9a17f 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -528,9 +528,9 @@ namespace datalog { class instr_filter_interpreted_and_project : public instruction { reg_idx m_src; - reg_idx m_res; app_ref m_cond; unsigned_vector m_cols; + reg_idx m_res; public: instr_filter_interpreted_and_project(reg_idx src, app_ref & condition, unsigned col_cnt, const unsigned * removed_cols, reg_idx result) From 2c8b314a15ba1bfc79e508b0266df1405782656b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Jun 2013 13:34:20 -0700 Subject: [PATCH 09/14] Fix issue https://z3.codeplex.com/workitem/48 Signed-off-by: Leonardo de Moura --- src/sat/sat_simplifier.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 623c73758..47c4b6150 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -625,7 +625,8 @@ namespace sat { case 1: TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";); propagate_unit(c[0]); - remove_clause(c); + // propagate_unit will delete c. + // remove_clause(c); return; case 2: TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";); @@ -816,7 +817,8 @@ namespace sat { } if (sz == 1) { propagate_unit(c[0]); - remove_clause(c); + // propagate_unit will delete c. + // remove_clause(c); continue; } if (sz == 2) { From 40b1137b30da4914c233001a704928662567f60d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Jun 2013 13:45:14 -0700 Subject: [PATCH 10/14] Fix issue https://z3.codeplex.com/workitem/47 Signed-off-by: Leonardo de Moura --- src/sat/sat_asymm_branch.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 81d631e4e..b8ac520b2 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -72,11 +72,14 @@ namespace sat { int limit = -static_cast(m_asymm_branch_limit); std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt()); m_counter -= s.m_clauses.size(); + SASSERT(s.m_qhead == s.m_trail.size()); clause_vector::iterator it = s.m_clauses.begin(); clause_vector::iterator it2 = it; clause_vector::iterator end = s.m_clauses.end(); try { for (; it != end; ++it) { + if (s.inconsistent()) + break; SASSERT(s.m_qhead == s.m_trail.size()); if (m_counter < limit || s.inconsistent()) { *it2 = *it; @@ -111,6 +114,7 @@ namespace sat { bool asymm_branch::process(clause & c) { TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";); SASSERT(s.scope_lvl() == 0); + SASSERT(s.m_qhead == s.m_trail.size()); #ifdef Z3DEBUG unsigned trail_sz = s.m_trail.size(); #endif @@ -143,6 +147,7 @@ namespace sat { SASSERT(!s.inconsistent()); SASSERT(s.scope_lvl() == 0); SASSERT(trail_sz == s.m_trail.size()); + SASSERT(s.m_qhead == s.m_trail.size()); if (i == sz - 1) { // clause size can't be reduced. s.attach_clause(c); @@ -181,15 +186,18 @@ namespace sat { s.assign(c[0], justification()); s.del_clause(c); s.propagate_core(false); + SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size()); return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. case 2: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); s.mk_bin_clause(c[0], c[1], false); s.del_clause(c); + SASSERT(s.m_qhead == s.m_trail.size()); return false; default: c.shrink(new_sz); s.attach_clause(c); + SASSERT(s.m_qhead == s.m_trail.size()); return true; } } From 1a26c9726bafca21cdba95f7a9f709ec087f43a0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 14 Jun 2013 13:15:48 +0100 Subject: [PATCH 11/14] .NET API: bugfix Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Solver.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 274f8dc4a..555a2466f 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -210,7 +210,7 @@ namespace Microsoft.Z3 public Status Check(params Expr[] assumptions) { Z3_lbool r; - if (assumptions == null) + if (assumptions == null || assumptions.Length == 0) r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject); else r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions)); From 76c59cb85c0637c32989f40a85c8c5364afb3e8f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 14 Jun 2013 17:22:25 +0100 Subject: [PATCH 12/14] MPF conversion bugfix. Signed-off-by: Christoph M. Wintersteiger --- src/ast/rewriter/float_rewriter.cpp | 12 ++++++++---- src/util/mpf.cpp | 2 +- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 015bce0ed..367fa3a4c 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -83,17 +83,21 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c rational q; mpf q_mpf; if (m_util.au().is_numeral(args[1], q)) { + TRACE("fp_rewriter", tout << "q: " << q << std::endl; ); mpf v; m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); result = m_util.mk_value(v); - m_util.fm().del(v); + m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else if (m_util.is_value(args[1], q_mpf)) { + else if (m_util.is_value(args[1], q_mpf)) { + TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; ); mpf v; m_util.fm().set(v, ebits, sbits, rm, q_mpf); result = m_util.mk_value(v); m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } else @@ -117,11 +121,11 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c return BR_FAILED; TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";); - mpf v; m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator()); result = m_util.mk_value(v); - m_util.fm().del(v); + m_util.fm().del(v); + TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } else { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index def9f4fd5..735d21c99 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 + 4; // plus rounding bits + signed ds = sbits - x.sbits + 3; // plus rounding bits if (ds > 0) { m_mpz_manager.mul2k(o.significand, ds); From 92c1b2597869f1bb65cdf68559b45f02127bbb0f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 14 Jun 2013 20:14:00 +0100 Subject: [PATCH 13/14] FPA: bugfix for float to float conversion (subnormal numbers). Thanks to Gabriele Paganelli for reporting this bug! Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 29 +++++++++++++++++++++++------ 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index dd40e8453..53ac5a58f 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1698,6 +1698,10 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a expr_ref sgn(m), sig(m), exp(m), lz(m); unpack(x, sgn, sig, exp, lz, true); + dbg_decouple("fpa2bv_to_float_x_sig", sig); + dbg_decouple("fpa2bv_to_float_x_exp", exp); + dbg_decouple("fpa2bv_to_float_lz", lz); + expr_ref res_sgn(m), res_sig(m), res_exp(m); res_sgn = sgn; @@ -1710,10 +1714,13 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a 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); + SASSERT(m_bv_util.get_bv_size(lz) == from_ebits); - if (from_sbits < (to_sbits + 3)) + 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. @@ -1734,7 +1741,9 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a 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); + { + res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp); + } else if (from_ebits > (to_ebits + 2)) { expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m); @@ -1747,7 +1756,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a 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, h_and_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); @@ -1763,10 +1772,18 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a else res_exp = exp; + // subtract lz for subnormal numbers. + expr_ref lz_ext(m); + lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz); + res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext); SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2); + dbg_decouple("fpa2bv_to_float_res_sig", res_sig); + dbg_decouple("fpa2bv_to_float_res_exp", res_exp); + 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); @@ -1781,7 +1798,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a mk_ite(c4, v4, result, result); mk_ite(c3, v3, result, result); mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); + mk_ite(c1, v1, result, result); } else { // .. other than that, we only support rationals for asFloat @@ -1826,7 +1843,7 @@ 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)); + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -2161,7 +2178,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef _DEBUG - return; + // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e)); From ecceb0accc455fcb0ee6eaf95ad33a91e2783b0c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 14 Jun 2013 20:16:02 +0100 Subject: [PATCH 14/14] FPA: debug output disabled. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 53ac5a58f..0913fbbcf 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -2178,7 +2178,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef _DEBUG - + return; // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e));