mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Bugfix for fp.to_sbv and fp.to_ubv.

Browse source 
Fixes #162.
This commit is contained in:
Christoph M. Wintersteiger 2015-09-15 19:03:31 +01:00
parent a1073206f9
commit 869cd6074d
2 changed files with 59 additions and 179 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

234
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -2783,8 +2783,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
}
void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_to_ubv", for (unsigned i = 0; i < num; i++)
void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {
TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
SASSERT(f->get_num_parameters() == 1);
@ -2815,25 +2815,34 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
// NaN, Inf, or negative (except -0) -> unspecified
expr_ref c1(m), v1(m);
c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
if (!is_signed)
c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
else
c1 = m.mk_or(x_is_nan, x_is_inf);
v1 = mk_to_ubv_unspecified(bv_sz);
dbg_decouple("fpa2bv_to_bv_c1", c1);
// +-Zero -> 0
expr_ref c2(m), v2(m);
c2 = x_is_zero;
v2 = m_bv_util.mk_numeral(rational(0), bv_srt);
dbg_decouple("fpa2bv_to_ubv_c2", c2);
dbg_decouple("fpa2bv_to_bv_c2", c2);
// Otherwise...
expr_ref sgn(m), sig(m), exp(m), lz(m);
unpack(x, sgn, sig, exp, lz, true);
dbg_decouple("fpa2bv_to_bv_sgn", sgn);
dbg_decouple("fpa2bv_to_bv_sig", sig);
dbg_decouple("fpa2bv_to_bv_exp", exp);
dbg_decouple("fpa2bv_to_bv_lz", lz);
// sig is of the form +- [1].[sig] * 2^(exp-lz)
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
SASSERT(m_bv_util.get_bv_size(sig) == sbits);
SASSERT(m_bv_util.get_bv_size(exp) == ebits);
SASSERT(m_bv_util.get_bv_size(lz) == ebits);
dbg_decouple("fpa2bv_to_ubv_sig", sig);
SASSERT(m_bv_util.get_bv_size(lz) == ebits);
unsigned sig_sz = m_bv_util.get_bv_size(sig);
SASSERT(sig_sz == sbits);
if (sig_sz < (bv_sz + 3))
@ -2841,35 +2850,38 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
sig_sz = m_bv_util.get_bv_size(sig);
SASSERT(sig_sz >= (bv_sz + 3));
expr_ref exp_m_lz(m), shift(m), shift_neg(m), bv0_e2(m), shift_abs(m);
expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), bv0_e2(m), shift_abs(m);
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
m_bv_util.mk_zero_extend(2, lz));
shift = m_bv_util.mk_bv_sub(exp_m_lz,
m_bv_util.mk_numeral(bv_sz - 1, ebits + 2));
shift_neg = m_bv_util.mk_bv_neg(shift);
e_m_lz_m_bv_sz = m_bv_util.mk_bv_sub(exp_m_lz,
m_bv_util.mk_numeral(bv_sz - 1, ebits + 2));
shift = m_bv_util.mk_bv_neg(e_m_lz_m_bv_sz);
bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), e_m_lz_m_bv_sz, shift);
SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
dbg_decouple("fpa2bv_to_ubv_shift", shift);
dbg_decouple("fpa2bv_to_ubv_shift_abs", shift_abs);
dbg_decouple("fpa2bv_to_bv_shift", shift);
dbg_decouple("fpa2bv_to_bv_shift_abs", shift_abs);
// x is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
// [1][ ... sig ... ][r][g][ ... s ...]
// [ ... ubv ... ][r][g][ ... s ... ]
expr_ref max_shift(m);
max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
expr_ref c_in_limits(m);
c_in_limits = m_bv_util.mk_sle(shift, m_bv_util.mk_numeral(0, ebits + 2));
dbg_decouple("fpa2bv_to_ubv_in_limits", c_in_limits);
if (!is_signed)
c_in_limits = m_bv_util.mk_sle(bv0_e2, shift);
else
c_in_limits = m.mk_or(m_bv_util.mk_sle(m_bv_util.mk_numeral(1, ebits + 2), shift),
m.mk_and(m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift),
m.mk_eq(sig, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sbits-1)))));
dbg_decouple("fpa2bv_to_bv_in_limits", c_in_limits);
expr_ref shifted_sig(m);
shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs);
dbg_decouple("fpa2bv_to_ubv_shifted_sig", shifted_sig);
dbg_decouple("fpa2bv_to_bv_shifted_sig", shifted_sig);
expr_ref last(m), round(m), sticky(m);
last = m_bv_util.mk_extract(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, shifted_sig);
@ -2878,25 +2890,32 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
m_bv_util.mk_numeral(0, sig_sz - (bv_sz + 3) + 2)),
bv0,
bv1);
dbg_decouple("fpa2bv_to_ubv_last", last);
dbg_decouple("fpa2bv_to_ubv_round", round);
dbg_decouple("fpa2bv_to_ubv_sticky", sticky);
dbg_decouple("fpa2bv_to_bv_last", last);
dbg_decouple("fpa2bv_to_bv_round", round);
dbg_decouple("fpa2bv_to_bv_sticky", sticky);
expr_ref rounding_decision(m);
rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky);
SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1);
dbg_decouple("fpa2bv_to_ubv_rounding_decision", rounding_decision);
dbg_decouple("fpa2bv_to_bv_rounding_decision", rounding_decision);
expr_ref unrounded_sig(m), pre_rounded(m), inc(m);
unrounded_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz, shifted_sig));
inc = m_bv_util.mk_zero_extend(1, m_bv_util.mk_zero_extend(bv_sz - 1, rounding_decision));
pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc);
dbg_decouple("fpa2bv_to_bv_inc", inc);
dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
expr_ref rnd_overflow(m), rnd(m), rnd_has_overflown(m);
rnd_overflow = m_bv_util.mk_extract(bv_sz, bv_sz, pre_rounded);
rnd = m_bv_util.mk_extract(bv_sz - 1, 0, pre_rounded);
rnd_has_overflown = m.mk_eq(rnd_overflow, bv1);
dbg_decouple("fpa2bv_to_ubv_rnd_has_overflown", rnd_has_overflown);
dbg_decouple("fpa2bv_to_bv_rnd_has_overflown", rnd_has_overflown);
if (is_signed)
rnd = m.mk_ite(m.mk_eq(sgn, bv1), m_bv_util.mk_bv_neg(rnd), rnd);
dbg_decouple("fpa2bv_to_bv_rnd", rnd);
result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(bv_sz), rnd);
result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(bv_sz));
@ -2906,160 +2925,16 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
SASSERT(is_well_sorted(m, result));
}
void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_to_ubv", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
mk_to_bv(f, num, args, false, result);
}
void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_to_sbv", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
SASSERT(num == 2);
SASSERT(m_bv_util.get_bv_size(args[0]) == 3);
SASSERT(m_util.is_float(args[1]));
expr * rm = args[0];
expr * x = args[1];
sort * xs = m.get_sort(x);
sort * bv_srt = f->get_range();
unsigned ebits = m_util.get_ebits(xs);
unsigned sbits = m_util.get_sbits(xs);
unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
expr_ref bv0(m), bv1(m), bv0_2(m), bv1_2(m), bv3_2(m);
bv0 = m_bv_util.mk_numeral(0, 1);
bv1 = m_bv_util.mk_numeral(1, 1);
bv0_2 = m_bv_util.mk_numeral(0, 2);
bv1_2 = m_bv_util.mk_numeral(1, 2);
bv3_2 = m_bv_util.mk_numeral(3, 2);
expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m);
mk_is_nan(x, x_is_nan);
mk_is_inf(x, x_is_inf);
mk_is_zero(x, x_is_zero);
mk_is_neg(x, x_is_neg);
mk_is_nzero(x, x_is_nzero);
// NaN, Inf -> unspecified
expr_ref c1(m), v1(m);
c1 = m.mk_or(x_is_nan, x_is_inf);
v1 = mk_to_sbv_unspecified(bv_sz);
dbg_decouple("fpa2bv_to_sbv_c1", c1);
// +-Zero -> 0
expr_ref c2(m), v2(m);
c2 = x_is_zero;
v2 = m_bv_util.mk_numeral(rational(0), bv_srt);
dbg_decouple("fpa2bv_to_sbv_c2", c2);
// Otherwise...
expr_ref sgn(m), sig(m), exp(m), lz(m);
unpack(x, sgn, sig, exp, lz, true);
dbg_decouple("fpa2bv_to_sbv_sgn", sgn);
dbg_decouple("fpa2bv_to_sbv_sig", sig);
dbg_decouple("fpa2bv_to_sbv_exp", exp);
// x is of the form +- [1].[sig] * 2^(exp-lz)
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
SASSERT(m_bv_util.get_bv_size(sig) == sbits);
SASSERT(m_bv_util.get_bv_size(exp) == ebits);
SASSERT(m_bv_util.get_bv_size(lz) == ebits);
dbg_decouple("fpa2bv_to_sbv_sig", sig);
unsigned sig_sz = m_bv_util.get_bv_size(sig);
SASSERT(sig_sz == sbits);
if (sig_sz < (bv_sz + 3))
sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, bv_sz - sig_sz + 3));
sig_sz = m_bv_util.get_bv_size(sig);
SASSERT(sig_sz >= (bv_sz + 3));
expr_ref exp_m_lz(m), shift(m), shift_neg(m), bv0_e2(m), shift_abs(m), shift_neg_dec(m);
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
m_bv_util.mk_zero_extend(2, lz));
shift = m_bv_util.mk_bv_sub(exp_m_lz,
m_bv_util.mk_numeral(bv_sz, ebits + 2));
shift_neg = m_bv_util.mk_bv_neg(shift);
bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
shift_neg_dec = m_bv_util.mk_sle(shift, bv0_e2);
shift_abs = m.mk_ite(shift_neg_dec, shift_neg, shift);
SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
dbg_decouple("fpa2bv_to_sbv_shift", shift);
// sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
// [1][ ... sig ... ][r][g][ ... s ...]
// [ ... ubv ... ][r][g][ ... s ... ]
// expr_ref max_shift(m);
// max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
expr_ref c_in_limits(m);
c_in_limits = m_bv_util.mk_sle(shift, m_bv_util.mk_numeral(0, ebits + 2));
dbg_decouple("fpa2bv_to_sbv_in_limits", c_in_limits);
expr_ref huge_sig(m), huge_shift(m), huge_shifted_sig(m);
huge_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_sz));
huge_shift = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sig_sz), shift_abs);
huge_shifted_sig = m.mk_ite(shift_neg_dec,
m_bv_util.mk_bv_shl(huge_sig, huge_shift),
m_bv_util.mk_bv_lshr(huge_sig, huge_shift));
dbg_decouple("fpa2bv_to_sbv_huge_shifted_sig", huge_shifted_sig);
SASSERT(m_bv_util.get_bv_size(huge_shifted_sig) == 2 * sig_sz);
expr_ref upper_hss(m), lower_hss(m);
upper_hss = m_bv_util.mk_extract(2 * sig_sz - 1, sig_sz + 1, huge_shifted_sig);
lower_hss = m_bv_util.mk_extract(sig_sz, 0, huge_shifted_sig);
SASSERT(m_bv_util.get_bv_size(upper_hss) == sig_sz - 1);
SASSERT(m_bv_util.get_bv_size(lower_hss) == sig_sz + 1);
dbg_decouple("fpa2bv_to_sbv_upper_hss", upper_hss);
dbg_decouple("fpa2bv_to_sbv_lower_hss", lower_hss);
expr_ref last(m), round(m), sticky(m);
last = m_bv_util.mk_extract(1, 1, upper_hss);
round = m_bv_util.mk_extract(0, 0, upper_hss);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lower_hss.get());
dbg_decouple("fpa2bv_to_sbv_last", last);
dbg_decouple("fpa2bv_to_sbv_round", round);
dbg_decouple("fpa2bv_to_sbv_sticky", sticky);
expr_ref upper_hss_w_sticky(m);
upper_hss_w_sticky = m_bv_util.mk_concat(upper_hss, sticky);
dbg_decouple("fpa2bv_to_sbv_upper_hss_w_sticky", upper_hss_w_sticky);
SASSERT(m_bv_util.get_bv_size(upper_hss_w_sticky) == sig_sz);
expr_ref rounding_decision(m);
rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky);
SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1);
dbg_decouple("fpa2bv_to_sbv_rounding_decision", rounding_decision);
expr_ref unrounded_sig(m), pre_rounded(m), inc(m);
unrounded_sig = m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz - 1, upper_hss_w_sticky);
inc = m_bv_util.mk_zero_extend(bv_sz, rounding_decision);
pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc);
dbg_decouple("fpa2bv_to_sbv_inc", inc);
dbg_decouple("fpa2bv_to_sbv_unrounded_sig", unrounded_sig);
dbg_decouple("fpa2bv_to_sbv_pre_rounded", pre_rounded);
expr_ref rnd_overflow(m), rnd_abs(m), rnd_signed(m), rnd_has_overflown(m), extra_neg(m);
rnd_overflow = m_bv_util.mk_extract(bv_sz, bv_sz - 1, pre_rounded);
rnd_abs = m_bv_util.mk_extract(bv_sz - 1, 0, pre_rounded);
rnd_signed = m.mk_ite(m.mk_eq(sgn, bv1), m_bv_util.mk_bv_neg(rnd_abs), rnd_abs);
extra_neg = m_bv_util.mk_numeral(fu().fm().m_powers2(bv_sz-1), bv_sz+1);
rnd_has_overflown = m.mk_and(m.mk_not(m.mk_eq(rnd_overflow, bv0_2)),
m.mk_not(m.mk_and(m.mk_eq(sgn, bv1), m.mk_eq(pre_rounded, extra_neg))));
dbg_decouple("fpa2bv_to_sbv_extra_neg", extra_neg);
dbg_decouple("fpa2bv_to_sbv_rnd_overflow", rnd_overflow);
dbg_decouple("fpa2bv_to_sbv_rnd_abs", rnd_abs);
dbg_decouple("fpa2bv_to_sbv_rnd_has_overflown", rnd_has_overflown);
result = m.mk_ite(rnd_has_overflown, mk_to_sbv_unspecified(bv_sz), rnd_signed);
result = m.mk_ite(c_in_limits, result, mk_to_sbv_unspecified(bv_sz));
result = m.mk_ite(c2, v2, result);
result = m.mk_ite(c1, v1, result);
SASSERT(is_well_sorted(m, result));
mk_to_bv(f, num, args, true, result);
}
expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned width) {
@ -3326,7 +3201,7 @@ void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) {
expr_ref e_plus_one(m);
e_plus_one = m_bv_util.mk_bv_add(e, m_bv_util.mk_numeral(1, ebits));
expr_ref leading(m), n_leading(m), rest(m);
leading = m_bv_util.mk_extract(ebits-1, ebits-1, e_plus_one);
n_leading = m_bv_util.mk_bv_not(leading);
@ -3350,6 +3225,10 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
SASSERT(m_bv_util.get_bv_size(exp) == ebits);
SASSERT(m_bv_util.get_bv_size(sig) == sbits-1);
dbg_decouple("fpa2bv_unpack_sgn", sgn);
dbg_decouple("fpa2bv_unpack_exp", exp);
dbg_decouple("fpa2bv_unpack_sig", sig);
expr_ref is_normal(m);
mk_is_normal(e, is_normal);
@ -3359,8 +3238,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
dbg_decouple("fpa2bv_unpack_normal_exp", normal_exp);
expr_ref denormal_sig(m), denormal_exp(m);
denormal_sig = m_bv_util.mk_zero_extend(1, sig);
// SASSERT(ebits >= 3); // Note: when ebits=2 there is no 1-exponent, so mk_unbias will produce a 0.
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);

4
src/ast/fpa/fpa2bv_converter.h
View file

@ -186,7 +186,9 @@ protected:
expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp,
expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp);
app * mk_fresh_const(char const * prefix, unsigned sz);
app * mk_fresh_const(char const * prefix, unsigned sz);
void mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result);
};
#endif