diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index a4961f555..234c343b8 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1134,6 +1134,9 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar mk_is_neg(z, z_is_neg); mk_is_inf(z, z_is_inf); + expr_ref rm_is_to_neg(m); + mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); + dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan); dbg_decouple("fpa2bv_fma_x_is_zero", x_is_zero); dbg_decouple("fpa2bv_fma_x_is_pos", x_is_pos); @@ -1187,31 +1190,28 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar 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. + // 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 + // (x is 0) || (y is 0) -> z 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, v7); + expr_ref ite_c(m); + m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c); + mk_ite(ite_c, pzero, z, v7); // else comes the fused multiplication. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); - SASSERT(ebits <= sbits); - - expr_ref rm_is_to_neg(m); - mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); + SASSERT(ebits <= sbits); expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m); expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m); 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, true); + unpack(z, c_sgn, c_sig, c_exp, c_lz, true); 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); @@ -1220,12 +1220,12 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar 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); + b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig); 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); + c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp); dbg_decouple("fpa2bv_fma_a_sig", a_sig_ext); dbg_decouple("fpa2bv_fma_b_sig", b_sig_ext); @@ -1233,6 +1233,9 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar dbg_decouple("fpa2bv_fma_a_exp", a_exp_ext); dbg_decouple("fpa2bv_fma_b_exp", b_exp_ext); dbg_decouple("fpa2bv_fma_c_exp", c_exp_ext); + dbg_decouple("fpa2bv_fma_a_lz", a_lz_ext); + dbg_decouple("fpa2bv_fma_b_lz", b_lz_ext); + dbg_decouple("fpa2bv_fma_c_lz", c_lz_ext); expr_ref mul_sgn(m), mul_sig(m), mul_exp(m); expr * signs[2] = { a_sgn, b_sgn }; @@ -1254,6 +1257,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar // 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))); + c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext); SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits); SASSERT(m_bv_util.get_bv_size(c_sig) == 2 * sbits); @@ -1269,7 +1273,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar 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_ext, 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)); @@ -1303,7 +1307,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar 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)-(ebits+2), exp_delta)); - shifted_f_sig = m_bv_util.mk_zero_extend(sbits, m_bv_util.mk_extract(3*sbits-1, 2*sbits, shifted_big)); + shifted_f_sig = m_bv_util.mk_extract(3*sbits-1, sbits, shifted_big); sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits); SASSERT(is_well_sorted(m, shifted_f_sig)); @@ -1334,7 +1338,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar 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_add(e_sig, shifted_f_sig), m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), sum); @@ -1354,7 +1358,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar dbg_decouple("fpa2bv_fma_add_n_sum", n_sum); dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs); - res_exp = m_bv_util.mk_bv_sub(e_exp, c_lz_ext); + res_exp = e_exp; // Result could overflow into 4.xxx ... @@ -1371,8 +1375,11 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs); - sticky = m_bv_util.mk_zero_extend(sbits+7, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get())); - res_sig = m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs); + sticky = m_bv_util.mk_zero_extend(sbits+3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get())); + dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky); + + expr * res_or_args[2] = { m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs), sticky }; + res_sig = m_bv_util.mk_bv_or(2, res_or_args); SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4); expr_ref is_zero_sig(m), nil_sbits4(m); @@ -2264,14 +2271,16 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref zero_e = m_bv_util.mk_numeral(0, ebits); if (normalize) { + expr_ref is_sig_zero(m), zero_s(m); + zero_s = m_bv_util.mk_numeral(0, sbits); + m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero); + expr_ref lz_d(m); - mk_leading_zeros(denormal_sig, ebits, lz_d); - m_simp.mk_ite(is_normal, zero_e, lz_d, lz); + mk_leading_zeros(denormal_sig, ebits, lz_d); + m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz); dbg_decouple("fpa2bv_unpack_lz", lz); - expr_ref is_sig_zero(m), shift(m), zero_s(m); - zero_s = m_bv_util.mk_numeral(0, sbits); - m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero); + expr_ref shift(m); m_simp.mk_ite(is_sig_zero, zero_e, lz, shift); dbg_decouple("fpa2bv_unpack_shift", shift); SASSERT(is_well_sorted(m, is_sig_zero));