mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Bugfix for rounding in FP to_sbv.

Browse source 
Fixes #113
This commit is contained in:
Christoph M. Wintersteiger 2015-05-30 14:50:15 +01:00
parent d47832d69c
commit fde873ac09
1 changed files with 35 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2953,9 +2953,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), 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);
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
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 ...]
@ -2964,34 +2963,48 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
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 shifted_sig(m);
shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs);
dbg_decouple("fpa2bv_to_sbv_shifted_sig", shifted_sig);
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_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(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, shifted_sig);
round = m_bv_util.mk_extract(sig_sz - bv_sz - 1, sig_sz - bv_sz - 1, shifted_sig);
sticky = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(sig_sz - bv_sz - 2, 0, shifted_sig),
m_bv_util.mk_numeral(0, sig_sz - (bv_sz + 3) + 2)),
bv0,
bv1);
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);
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_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));
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);
@ -3399,7 +3412,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#ifdef Z3DEBUG
return;
// return;
// CMW: This works only for quantifier-free formulas.
expr_ref new_e(m);
new_e = m.mk_fresh_const(prefix, m.get_sort(e));
@ -3409,6 +3422,12 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
}
expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) {
dbg_decouple("fpa2bv_rnd_dec_rm", expr_ref(rm, m));
dbg_decouple("fpa2bv_rnd_dec_sgn", expr_ref(sgn, m));
dbg_decouple("fpa2bv_rnd_dec_last", expr_ref(last, m));
dbg_decouple("fpa2bv_rnd_dec_round", expr_ref(round, m));
dbg_decouple("fpa2bv_rnd_dec_sticky", expr_ref(sticky, m));
expr_ref last_or_sticky(m), round_or_sticky(m), not_last(m), not_round(m), not_sticky(m), not_lors(m), not_rors(m), not_sgn(m);
expr * last_sticky[2] = { last, sticky };
expr * round_sticky[2] = { round, sticky };
@ -3446,6 +3465,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la
m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2);
m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, res);
dbg_decouple("fpa2bv_rnd_dec_res", res);
return res;
}