From 52cf80d63722ec6c322daa01c01fd7755306d9f8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Jul 2017 19:53:55 +0100 Subject: [PATCH] Simplified bit-vector bounds in fp.rem. Relates to #872. --- src/ast/fpa/fpa2bv_converter.cpp | 64 ++++++++++++++++---------------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 7e56df405..0f4d26739 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1535,12 +1535,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // Extend c expr_ref c_sig_ext(m); - c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits - 1 + 3))); + c_sig_ext = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits+2))); c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext); mul_sig = m_bv_util.mk_concat(mul_sig, m_bv_util.mk_numeral(0, 3)); - SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits + 3); - SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2 * sbits + 3); + SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits+3); + SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2*sbits+3); dbg_decouple("fpa2bv_fma_c_sig_ext", c_sig_ext); dbg_decouple("fpa2bv_fma_c_exp_ext", c_exp_ext); @@ -1564,8 +1564,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, SASSERT(is_well_sorted(m, f_sig)); SASSERT(is_well_sorted(m, f_exp)); - SASSERT(m_bv_util.get_bv_size(e_sig) == 2 * sbits + 3); - SASSERT(m_bv_util.get_bv_size(f_sig) == 2 * sbits + 3); + SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+3); + SASSERT(m_bv_util.get_bv_size(f_sig) == 2*sbits+3); SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2); SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2); @@ -1595,7 +1595,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, shifted_big = m_bv_util.mk_bv_lshr( m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)), m_bv_util.mk_zero_extend((3*sbits+3)-(ebits+2), exp_delta)); - shifted_f_sig = m_bv_util.mk_extract(3*sbits-1+3, sbits, shifted_big); + shifted_f_sig = m_bv_util.mk_extract(3*sbits+2, sbits, shifted_big); alignment_sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); alignment_sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, alignment_sticky_raw.get()); dbg_decouple("fpa2bv_fma_shifted_f_sig", shifted_f_sig); @@ -1613,14 +1613,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, m_simp.mk_eq(e_sgn, f_sgn, eq_sgn); dbg_decouple("fpa2bv_fma_eq_sgn", eq_sgn); - SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+2+3); - SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+2+3); + SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits+5); + SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits+5); dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); expr_ref sum(m), e_plus_f(m), e_minus_f(m), sticky_wide(m); - sticky_wide = m_bv_util.mk_zero_extend(2*sbits+1+3, alignment_sticky); + sticky_wide = m_bv_util.mk_zero_extend(2*sbits+4, alignment_sticky); e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig); e_plus_f = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(0, 0, e_plus_f), zero_1), m_bv_util.mk_bv_add(e_plus_f, sticky_wide), @@ -1633,12 +1633,12 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_f_sig_or_sticky", shifted_f_sig); m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum); - SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits+2+3); + SASSERT(m_bv_util.get_bv_size(sum) == 2*sbits+5); 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(2*sbits+1+3, 2*sbits+1+3, sum); + sign_bv = m_bv_util.mk_extract(2*sbits+4, 2*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); @@ -1662,14 +1662,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_res_sgn", res_sgn); expr_ref is_sig_neg(m); - is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2*sbits+1+3, 2*sbits+1+3, sig_abs)); + is_sig_neg = m.mk_eq(one_1, m_bv_util.mk_extract(2*sbits+4, 2*sbits+4, sig_abs)); sig_abs = m.mk_ite(is_sig_neg, m_bv_util.mk_bv_neg(sig_abs), sig_abs); dbg_decouple("fpa2bv_fma_is_sig_neg", is_sig_neg); // Result could have overflown into 4.xxx. - SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+2+3); + SASSERT(m_bv_util.get_bv_size(sig_abs) == 2*sbits+4); expr_ref extra(m), extra_is_zero(m); - extra = m_bv_util.mk_extract(2*sbits+1+3, 2*sbits+3, sig_abs); + extra = m_bv_util.mk_extract(2*sbits+4, 2*sbits+3, sig_abs); extra_is_zero = m.mk_eq(extra, m_bv_util.mk_numeral(0, 2)); dbg_decouple("fpa2bv_fma_extra", extra); @@ -1700,30 +1700,30 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, } expr_ref sig_abs_h1(m), sticky_h1(m), sticky_h1_red(m), sig_abs_h1_f(m), res_sig_1(m); - sticky_h1 = m_bv_util.mk_extract(sbits - 5 + too_short + 3, 0, sig_abs); - sig_abs_h1 = m_bv_util.mk_extract(2 * sbits + 1 + too_short + 3, sbits - 4 + too_short + 3, sig_abs); - sticky_h1_red = m_bv_util.mk_zero_extend(sbits + 5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); + sticky_h1 = m_bv_util.mk_extract(sbits+too_short-2, 0, sig_abs); + sig_abs_h1 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits-1+too_short, sig_abs); + sticky_h1_red = m_bv_util.mk_zero_extend(sbits+5, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); expr * sticky_h1_red_args[2] = { sig_abs_h1, sticky_h1_red }; sig_abs_h1_f = m_bv_util.mk_bv_or(2, sticky_h1_red_args); - res_sig_1 = m_bv_util.mk_extract(sbits + 3, 0, sig_abs_h1_f); - SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits - 4 + too_short + 3); - SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits + 6); - SASSERT(m_bv_util.get_bv_size(sticky_h1_red) == sbits + 6); - SASSERT(m_bv_util.get_bv_size(sig_abs_h1_f) == sbits + 6); - SASSERT(m_bv_util.get_bv_size(res_sig_1) == sbits + 4); + res_sig_1 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h1_f); + SASSERT(m_bv_util.get_bv_size(sticky_h1) == sbits+too_short-1); + SASSERT(m_bv_util.get_bv_size(sig_abs_h1) == sbits+6); + SASSERT(m_bv_util.get_bv_size(sticky_h1_red) == sbits+6); + SASSERT(m_bv_util.get_bv_size(sig_abs_h1_f) == sbits+6); + SASSERT(m_bv_util.get_bv_size(res_sig_1) == sbits+4); expr_ref sig_abs_h2(m), sticky_h2(m), sticky_h2_red(m), sig_abs_h2_f(m), res_sig_2(m); - sticky_h2 = m_bv_util.mk_extract(sbits - 4 + too_short + 3, 0, sig_abs); - sig_abs_h2 = m_bv_util.mk_extract(2 * sbits + 1 + too_short + 3, sbits - 3 + too_short + 3, sig_abs); - sticky_h2_red = m_bv_util.mk_zero_extend(sbits + 4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); + sticky_h2 = m_bv_util.mk_extract(sbits+too_short-1, 0, sig_abs); + sig_abs_h2 = m_bv_util.mk_extract(2*sbits+too_short+4, sbits+too_short, sig_abs); + sticky_h2_red = m_bv_util.mk_zero_extend(sbits+4, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_h1.get())); expr * sticky_h2_red_args[2] = { sig_abs_h2, sticky_h2_red }; sig_abs_h2_f = m_bv_util.mk_zero_extend(1, m_bv_util.mk_bv_or(2, sticky_h2_red_args)); - res_sig_2 = m_bv_util.mk_extract(sbits + 3, 0, sig_abs_h2_f); - SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits - 3 + too_short + 3); - SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits + 5); - SASSERT(m_bv_util.get_bv_size(sticky_h2_red) == sbits + 5); - SASSERT(m_bv_util.get_bv_size(sig_abs_h2_f) == sbits + 6); - SASSERT(m_bv_util.get_bv_size(res_sig_2) == sbits + 4); + res_sig_2 = m_bv_util.mk_extract(sbits+3, 0, sig_abs_h2_f); + SASSERT(m_bv_util.get_bv_size(sticky_h2) == sbits+too_short); + SASSERT(m_bv_util.get_bv_size(sig_abs_h2) == sbits+5); + SASSERT(m_bv_util.get_bv_size(sticky_h2_red) == sbits+5); + SASSERT(m_bv_util.get_bv_size(sig_abs_h2_f) == sbits+6); + SASSERT(m_bv_util.get_bv_size(res_sig_2) == sbits+4); res_sig = m.mk_ite(extra_is_zero, res_sig_1, res_sig_2);