mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Fix for fp.fma encoding. Relates to #872.
This commit is contained in:
parent
9d6be286d0
commit
f1c0ac72e7
|
@ -1516,7 +1516,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
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_add(m_bv_util.mk_bv_sub(a_exp_ext, a_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);
|
||||
|
||||
|
@ -1529,11 +1530,14 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
// 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)));
|
||||
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)));
|
||||
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);
|
||||
SASSERT(m_bv_util.get_bv_size(c_sig_ext) == 2 * sbits);
|
||||
dbg_decouple("fpa2bv_fma_c_sig_ext", c_sig_ext);
|
||||
dbg_decouple("fpa2bv_fma_c_exp_ext", c_exp_ext);
|
||||
|
||||
expr_ref swap_cond(m);
|
||||
swap_cond = m_bv_util.mk_sle(mul_exp, c_exp_ext);
|
||||
|
@ -1542,10 +1546,10 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
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_sig_ext, mul_sig, e_sig); // has 2 * sbits
|
||||
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_sig, c_sig_ext, f_sig); // has 2 * sbits
|
||||
m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2
|
||||
|
||||
SASSERT(is_well_sorted(m, e_sgn));
|
||||
|
@ -1560,6 +1564,11 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2);
|
||||
|
||||
dbg_decouple("fpa2bv_fma_e_sig", e_sig);
|
||||
dbg_decouple("fpa2bv_fma_e_exp", e_exp);
|
||||
dbg_decouple("fpa2bv_fma_f_sig", f_sig);
|
||||
dbg_decouple("fpa2bv_fma_f_exp", f_exp);
|
||||
|
||||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
|
||||
expr_ref exp_delta(m);
|
||||
|
@ -1582,6 +1591,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta));
|
||||
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);
|
||||
dbg_decouple("fpa2bv_fma_shifted_f_sig", shifted_f_sig);
|
||||
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits);
|
||||
SASSERT(is_well_sorted(m, shifted_f_sig));
|
||||
|
||||
|
@ -1594,14 +1604,16 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
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));
|
||||
dbg_decouple("fpa2bv_fma_f_sig_or_sticky", shifted_f_sig);
|
||||
|
||||
// Significant addition.
|
||||
// Two extra bits for catching the overflow.
|
||||
// Two extra bits for the sign and for catching overflows.
|
||||
e_sig = m_bv_util.mk_zero_extend(2, e_sig);
|
||||
shifted_f_sig = m_bv_util.mk_zero_extend(2, shifted_f_sig);
|
||||
|
||||
expr_ref eq_sgn(m);
|
||||
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);
|
||||
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits + 2);
|
||||
|
@ -1611,27 +1623,24 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
expr_ref sum(m), e_plus_f(m), e_minus_f(m);
|
||||
e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig);
|
||||
e_minus_f = m_bv_util.mk_bv_sub(e_sig, shifted_f_sig),
|
||||
m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum);
|
||||
|
||||
e_minus_f = m_bv_util.mk_bv_sub(e_sig, 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);
|
||||
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, 2*sbits+1, 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);
|
||||
|
||||
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_sign_bv", sign_bv);
|
||||
dbg_decouple("fpa2bv_fma_add_n_sum", n_sum);
|
||||
dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs);
|
||||
|
||||
res_exp = e_exp;
|
||||
|
||||
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);
|
||||
|
@ -1643,44 +1652,57 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
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);
|
||||
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, 2 * sbits + 1, 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);
|
||||
expr_ref ovfl_into_4(m);
|
||||
ovfl_into_4 = m.mk_eq(m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs),
|
||||
m_bv_util.mk_numeral(1, 2));
|
||||
dbg_decouple("fpa2bv_fma_ovfl_into_4", ovfl_into_4);
|
||||
if (sbits > 5) {
|
||||
expr_ref sticky_raw(m), sig_upper(m), sticky_redd(m), res_sig_norm(m);
|
||||
sticky_raw = m_bv_util.mk_extract(sbits - 4, 0, sig_abs);
|
||||
sig_upper = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_upper) == sbits + 4);
|
||||
sticky_redd = m.mk_app(bvfid, OP_BREDOR, sticky_raw.get());
|
||||
sticky = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd);
|
||||
expr * res_or_args[2] = { sig_upper, sticky };
|
||||
res_sig_norm = m_bv_util.mk_bv_or(2, res_or_args);
|
||||
expr_ref extra(m), extra_is_zero(m);
|
||||
extra = m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs);
|
||||
extra_is_zero = m.mk_eq(extra, m_bv_util.mk_numeral(0, 2));
|
||||
dbg_decouple("fpa2bv_fma_extra", extra);
|
||||
|
||||
expr_ref sticky_raw_ovfl(m), sig_upper_ovfl(m), sticky_redd_ovfl(m), sticky_ovfl(m), res_sig_ovfl(m);
|
||||
sticky_raw_ovfl = m_bv_util.mk_extract(sbits - 4, 0, sig_abs);
|
||||
sig_upper_ovfl = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs);
|
||||
SASSERT(m_bv_util.get_bv_size(sig_upper_ovfl) == sbits + 4);
|
||||
sticky_redd_ovfl = m.mk_app(bvfid, OP_BREDOR, sticky_raw_ovfl.get());
|
||||
sticky_ovfl = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd_ovfl);
|
||||
expr * res_or_args_ovfl[2] = { sig_upper_ovfl, sticky_ovfl };
|
||||
res_sig_ovfl = m_bv_util.mk_bv_or(2, res_or_args_ovfl);
|
||||
|
||||
res_sig = m.mk_ite(ovfl_into_4, res_sig_ovfl, res_sig_norm);
|
||||
res_exp = m.mk_ite(ovfl_into_4, m_bv_util.mk_bv_add(res_exp, m_bv_util.mk_numeral(1, ebits+2)),
|
||||
res_exp);
|
||||
}
|
||||
else {
|
||||
unsigned too_short = 6 - sbits;
|
||||
unsigned too_short = 0;
|
||||
if (sbits < 5) {
|
||||
too_short = 6 - sbits + 1;
|
||||
sig_abs = m_bv_util.mk_concat(sig_abs, m_bv_util.mk_numeral(0, too_short));
|
||||
res_sig = m_bv_util.mk_extract(sbits + 3, 0, sig_abs);
|
||||
}
|
||||
dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);
|
||||
dbg_decouple("fpa2bv_fma_sig_abs", sig_abs);
|
||||
|
||||
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, 0, sig_abs);
|
||||
sig_abs_h1 = m_bv_util.mk_extract(2 * sbits + 1 + too_short, sbits - 4 + 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);
|
||||
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, 0, sig_abs);
|
||||
sig_abs_h2 = m_bv_util.mk_extract(2 * sbits + 1 + too_short, sbits - 3 + 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);
|
||||
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);
|
||||
res_exp = m.mk_ite(extra_is_zero, e_exp, m_bv_util.mk_bv_add(e_exp, m_bv_util.mk_numeral(1, ebits + 2)));
|
||||
|
||||
dbg_decouple("fpa2bv_fma_res_sig", res_sig);
|
||||
dbg_decouple("fpa2bv_fma_res_exp", res_exp);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
|
||||
|
||||
expr_ref is_zero_sig(m), nil_sbits4(m);
|
||||
|
@ -3889,8 +3911,8 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
|
|||
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;
|
||||
tout << "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), one_1(m), h_exp(m), sh_exp(m), th_exp(m);
|
||||
|
@ -4106,7 +4128,6 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
|
|||
dbg_decouple("fpa2bv_rnd_rm_is_to_neg", rm_is_to_neg);
|
||||
dbg_decouple("fpa2bv_rnd_rm_is_to_pos", rm_is_to_pos);
|
||||
|
||||
|
||||
expr_ref sgn_is_zero(m), zero1(m);
|
||||
zero1 = m_bv_util.mk_numeral(0, 1);
|
||||
m_simp.mk_eq(sgn, zero1, sgn_is_zero);
|
||||
|
|
|
@ -886,7 +886,7 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
unsigned extra = 0;
|
||||
// Result could overflow into 4.xxx ...
|
||||
SASSERT(m_mpz_manager.lt(o.significand, m_powers2(2 * x.sbits + 2)));
|
||||
if(m_mpz_manager.ge(o.significand, m_powers2(2 * x.sbits + 1)))
|
||||
if (m_mpz_manager.ge(o.significand, m_powers2(2 * x.sbits + 1)))
|
||||
{
|
||||
extra++;
|
||||
o.exponent++;
|
||||
|
|
Loading…
Reference in a new issue