mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

FPA bugfixes for denormal numbers.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-04-05 12:45:28 +01:00
parent 5ef0fdc9c8
commit 26efb3c7f1
2 changed files with 85 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

139
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -423,9 +423,9 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr_ref a_sgn(m), a_sig(m), a_exp(m), b_sgn(m), b_sig(m), b_exp(m);
unpack(x, a_sgn, a_sig, a_exp, true);
unpack(y, b_sgn, b_sig, b_exp, false);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, false);
unpack(y, b_sgn, b_sig, b_exp, b_lz, false);
dbg_decouple("fpa2bv_add_unpack_a_sgn", a_sgn);
dbg_decouple("fpa2bv_add_unpack_a_sig", a_sig);
@ -511,7 +511,7 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
mk_nzero(f, nzero);
mk_pzero(f, pzero);
mk_minus_inf(f, ninf);
mk_plus_inf(f, pinf);
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);
@ -575,13 +575,21 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), b_sgn(m), b_sig(m), b_exp(m);
unpack(x, a_sgn, a_sig, a_exp, true);
unpack(y, b_sgn, b_sig, b_exp, true);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
expr_ref lz_a(m), lz_b(m);
mk_leading_zeros(a_sig, ebits+2, lz_a);
mk_leading_zeros(b_sig, ebits+2, lz_b);
dbg_decouple("fpa2bv_mul_a_sig", a_sig);
dbg_decouple("fpa2bv_mul_a_exp", a_exp);
dbg_decouple("fpa2bv_mul_b_sig", b_sig);
dbg_decouple("fpa2bv_mul_b_exp", b_exp);
expr_ref a_lz_ext(m), b_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);
dbg_decouple("fpa2bv_mul_lz_a", a_lz);
dbg_decouple("fpa2bv_mul_lz_b", b_lz);
expr_ref a_sig_ext(m), b_sig_ext(m);
a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig);
@ -597,9 +605,9 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_mul_res_sgn", res_sgn);
res_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(lz_a, lz_b));
res_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));
expr_ref product(m);
product = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext);
@ -614,11 +622,11 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
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);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product));
rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, product), 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)));
rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - sbits));
SASSERT(m_bv_util.get_bv_size(rbits) == 4);
res_sig = m_bv_util.mk_concat(h_p, rbits);
@ -719,9 +727,9 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), b_sgn(m), b_sig(m), b_exp(m);
unpack(x, a_sgn, a_sig, a_exp, true);
unpack(y, b_sgn, b_sig, b_exp, true);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
unsigned extra_bits = sbits+2;
expr_ref a_sig_ext(m), b_sig_ext(m);
@ -736,7 +744,13 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
expr * signs[2] = { a_sgn, b_sgn };
res_sgn = m_bv_util.mk_bv_xor(2, signs);
res_exp = m_bv_util.mk_bv_sub(a_exp_ext, b_exp_ext);
expr_ref a_lz_ext(m), b_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);
res_exp = m_bv_util.mk_bv_sub(
m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
expr_ref quotient(m);
quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV, a_sig_ext, b_sig_ext);
@ -829,10 +843,10 @@ void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const *
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr_ref a_sgn(m), a_sig(m), a_exp(m);
expr_ref b_sgn(m), b_sig(m), b_exp(m);
unpack(x, a_sgn, a_sig, a_exp, true);
unpack(y, b_sgn, b_sig, b_exp, true);
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);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
BVSLT(a_exp, b_exp, c6);
v6 = x;
@ -1062,16 +1076,16 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
expr_ref rm_is_to_neg(m);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
expr_ref a_sgn(m), a_sig(m), a_exp(m);
expr_ref b_sgn(m), b_sig(m), b_exp(m);
expr_ref c_sgn(m), c_sig(m), c_exp(m);
unpack(x, a_sgn, a_sig, a_exp, true);
unpack(y, b_sgn, b_sig, b_exp, true);
unpack(z, c_sgn, c_sig, c_exp, false);
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, false);
expr_ref lz_a(m), lz_b(m);
mk_leading_zeros(a_sig, ebits+2, lz_a);
mk_leading_zeros(b_sig, ebits+2, lz_b);
expr_ref a_lz_ext(m), b_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);
expr_ref a_sig_ext(m), b_sig_ext(m);
a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig);
@ -1089,7 +1103,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
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(lz_a, lz_b));
m_bv_util.mk_bv_add(a_lz_ext, b_lz_ext));
mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext);
@ -1209,8 +1223,11 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
unsigned sbits = m_util.get_sbits(f->get_range());
SASSERT(ebits < sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m);
unpack(x, a_sgn, a_sig, a_exp, true);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig);
dbg_decouple("fpa2bv_r2i_unpacked_exp", a_exp);
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);
@ -1456,8 +1473,8 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
// otherwise: the actual conversion with rounding.
sort * s = f->get_range();
expr_ref sgn(m), sig(m), exp(m);
unpack(x, sgn, sig, exp, true);
expr_ref sgn(m), sig(m), exp(m), lz(m);
unpack(x, sgn, sig, exp, lz, true);
expr_ref res_sgn(m), res_sig(m), res_exp(m);
@ -1818,7 +1835,7 @@ void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) {
result = m_bv_util.mk_concat(n_leading, rest);
}
void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, bool normalize) {
void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize) {
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
SASSERT(to_app(e)->get_num_args() == 3);
@ -1837,23 +1854,29 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
expr_ref normal_sig(m), normal_exp(m);
normal_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(1, 1), sig);
mk_unbias(exp, normal_exp);
dbg_decouple("fpa2bv_unpack_normal_exp", normal_exp);
expr_ref denormal_sig(m), denormal_exp(m);
denormal_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), sig);
denormal_sig = m_bv_util.mk_zero_extend(1, sig);
denormal_exp = m_bv_util.mk_numeral(1, ebits);
mk_unbias(denormal_exp, denormal_exp);
dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp);
dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp);
expr_ref zero_e(m);
zero_e = m_bv_util.mk_numeral(0, ebits);
if (normalize) {
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, zero_e, lz, shift);
SASSERT(is_well_sorted(m, is_sig_zero));
SASSERT(is_well_sorted(m, lz));
expr_ref lz_d(m);
mk_leading_zeros(denormal_sig, ebits, lz_d);
m_simp.mk_ite(is_normal, 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);
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));
SASSERT(is_well_sorted(m, shift));
SASSERT(m_bv_util.get_bv_size(shift) == ebits);
if (ebits <= sbits) {
@ -1872,10 +1895,11 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
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);
}
denormal_exp = m_bv_util.mk_bv_sub(denormal_exp, shift);
denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl);
}
}
else
lz = zero_e;
SASSERT(is_well_sorted(m, normal_sig));
SASSERT(is_well_sorted(m, denormal_sig));
@ -2020,8 +2044,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
dbg_decouple("fpa2bv_rnd_beta", beta);
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));
dbg_decouple("fpa2bv_rnd_e_min", e_min);
dbg_decouple("fpa2bv_rnd_e_max", e_max);
expr_ref sigma(m), sigma_add(m), e_min_p2(m);
sigma_add = m_bv_util.mk_bv_sub(exp, m_bv_util.mk_sign_extend(2, e_min));
sigma_add = m_bv_util.mk_bv_add(sigma_add, m_bv_util.mk_numeral(1, ebits+2));
m_simp.mk_ite(TINY, sigma_add, lz, sigma);
dbg_decouple("fpa2bv_rnd_sigma", sigma);
@ -2034,7 +2062,8 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
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);
SASSERT(m_bv_util.get_bv_size(sigma) == ebits+2);
unsigned sigma_size = ebits+2;
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);

2
src/tactic/fpa/fpa2bv_converter.h
View file

@ -135,7 +135,7 @@ protected:
void mk_bias(expr * e, expr_ref & result);
void mk_unbias(expr * e, expr_ref & result);
void unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, bool normalize);
void unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize);
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,