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

Fix BV-conversion of fp.roundToIntegral. Fixes #2191.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2019-03-27 17:13:00 +00:00
parent 5c67c9d907
commit d1d49ef3a9
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 34 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1986,15 +1986,17 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
SASSERT(is_well_sorted(m, v4));
// exponent >= sbits-1
// exponent >= sbits-1 -> x
expr_ref exp_is_large(m);
exp_is_large = m_bv_util.mk_sle(m_bv_util.mk_numeral(sbits-1, ebits), a_exp);
exp_is_large = log2(sbits-1)+1 <= ebits-1 ?
m_bv_util.mk_sle(m_bv_util.mk_numeral(sbits-1, ebits), a_exp) :
m.mk_false();
dbg_decouple("fpa2bv_r2i_exp_is_large", exp_is_large);
c5 = exp_is_large;
v5 = x;
// Actual conversion with rounding.
// x.exponent >= 0 && x.exponent < x.sbits - 1
// exponent >= 0 && exponent < sbits - 1
expr_ref res_sgn(m), res_sig(m), res_exp(m);
res_sgn = a_sgn;
@ -2070,7 +2072,6 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
m_simp.mk_ite(c53, v53, res_sig, res_sig);
m_simp.mk_ite(c52, v52, res_sig, res_sig);
m_simp.mk_ite(c51, v51, res_sig, res_sig);
res_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3))); // rounding bits are all 0.
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
SASSERT(m_bv_util.get_bv_size(shift) == sbits);
@ -2082,11 +2083,37 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), e_shift);
SASSERT(m_bv_util.get_bv_size(res_sgn) == 1);
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits);
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits + 2);
// CMW: We use the rounder for normalization.
round(s, rm, res_sgn, res_sig, res_exp, v6);
// Renormalize
expr_ref zero_e2(m), min_exp(m), sig_lz(m), max_exp_delta(m), sig_lz_capped(m), renorm_delta(m);
zero_e2 = m_bv_util.mk_numeral(0, ebits+2);
mk_min_exp(ebits, min_exp);
min_exp = m_bv_util.mk_sign_extend(2, min_exp);
mk_leading_zeros(res_sig, ebits+2, sig_lz);
max_exp_delta = m_bv_util.mk_bv_sub(res_exp, min_exp);
sig_lz_capped = m.mk_ite(m_bv_util.mk_sle(sig_lz, max_exp_delta), sig_lz, max_exp_delta);
renorm_delta = m.mk_ite(m_bv_util.mk_sle(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2);
SASSERT(m_bv_util.get_bv_size(renorm_delta) == ebits + 2);
res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta);
res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta));
dbg_decouple("fpa2bv_r2i_renorm_delta", renorm_delta);
res_exp = m_bv_util.mk_extract(ebits-1, 0, res_exp);
mk_bias(res_exp, res_exp);
res_sig = m_bv_util.mk_extract(sbits-2, 0, res_sig);
v6 = m_util.mk_fp(res_sgn, res_exp, res_sig);
dbg_decouple("fpa2bv_r2i_res_sgn", res_sgn);
dbg_decouple("fpa2bv_r2i_res_sig", res_sig);
dbg_decouple("fpa2bv_r2i_res_exp", res_exp);
dbg_decouple("fpa2bv_r2i_c1", c1);
dbg_decouple("fpa2bv_r2i_c2", c2);
dbg_decouple("fpa2bv_r2i_c3", c3);
dbg_decouple("fpa2bv_r2i_c4", c4);
dbg_decouple("fpa2bv_r2i_c5", c5);
// And finally, we tie them together.
mk_ite(c5, v5, v6, result);