From d1d49ef3a974ea9c86b15df4b32843f7fdfdca87 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 27 Mar 2019 17:13:00 +0000 Subject: [PATCH] Fix BV-conversion of fp.roundToIntegral. Fixes #2191. --- src/ast/fpa/fpa2bv_converter.cpp | 41 ++++++++++++++++++++++++++------ 1 file changed, 34 insertions(+), 7 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index eef2452db..f8879d6a1 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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);