From 8eea6fd775e2d6720d2b9d793d4e98614e0b8171 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 24 Nov 2015 17:21:40 +0000 Subject: [PATCH] Bugfix for FPA float to float conversion. Fixes #337 --- src/ast/fpa/fpa2bv_converter.cpp | 50 ++++++++++++++++++-------------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d931fda9b..c4ca4c03d 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2278,39 +2278,47 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * } else if (from_ebits > (to_ebits + 2)) { unsigned ebits_diff = from_ebits - (to_ebits + 2); - expr_ref lz_rest(m), lz_redor(m), lz_redor_bool(m); - lz_rest = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, lz); - lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get()); - m_simp.mk_eq(lz_redor, one1, lz_redor_bool); - dbg_decouple("fpa2bv_to_float_exp_lz_redor", lz_redor); // subtract lz for subnormal numbers. expr_ref exp_sub_lz(m); - exp_sub_lz = m_bv_util.mk_bv_sub(exp, lz); + exp_sub_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), m_bv_util.mk_sign_extend(2, lz)); dbg_decouple("fpa2bv_to_float_exp_sub_lz", exp_sub_lz); - + // check whether exponent is within roundable (to_ebits+2) range. - expr_ref exp_sgn(m), exp_max(m), exp_min(m), exp_in_range(m); - exp_sgn = m_bv_util.mk_extract(from_ebits - 1, from_ebits - 1, exp_sub_lz); - mk_max_exp(to_ebits + 2, exp_max); - mk_min_exp(to_ebits + 2, exp_min); + expr_ref max_exp(m), min_exp(m), exp_in_range(m); + const mpz & z = m_mpf_manager.m_powers2(to_ebits + 1, true); + max_exp = m_bv_util.mk_concat( + m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(to_ebits, false), to_ebits + 1), + m_bv_util.mk_numeral(0, 1)); + min_exp = m_bv_util.mk_numeral(z + mpz(2), to_ebits+2); + dbg_decouple("fpa2bv_to_float_max_exp", max_exp); + dbg_decouple("fpa2bv_to_float_min_exp", min_exp); + + expr_ref first_ovf_exp(m), first_udf_exp(m); + const mpz & ovft = m_mpf_manager.m_powers2.m1(to_ebits+1, false); + first_ovf_exp = m_bv_util.mk_numeral(ovft, from_ebits+2); + first_udf_exp = m_bv_util.mk_concat( + m_bv_util.mk_numeral(-1, ebits_diff + 3), + m_bv_util.mk_numeral(1, to_ebits + 1)); + dbg_decouple("fpa2bv_to_float_first_ovf_exp", first_ovf_exp); + dbg_decouple("fpa2bv_to_float_first_udf_exp", first_udf_exp); + exp_in_range = m_bv_util.mk_extract(to_ebits + 1, 0, exp_sub_lz); - SASSERT(m_bv_util.get_bv_size(exp_max) == to_ebits + 2); - SASSERT(m_bv_util.get_bv_size(exp_min) == to_ebits + 2); SASSERT(m_bv_util.get_bv_size(exp_in_range) == to_ebits + 2); - dbg_decouple("fpa2bv_to_float_exp_max", exp_max); - dbg_decouple("fpa2bv_to_float_exp_min", exp_min); expr_ref ovf_cond(m), udf_cond(m); - ovf_cond = m_bv_util.mk_sle(m_bv_util.mk_sign_extend(ebits_diff, exp_max), exp_sub_lz); - udf_cond = m_bv_util.mk_sle(exp_sub_lz, m_bv_util.mk_sign_extend(ebits_diff, exp_min)); - + ovf_cond = m_bv_util.mk_sle(first_ovf_exp, exp_sub_lz); + udf_cond = m_bv_util.mk_sle(exp_sub_lz, first_udf_exp); + dbg_decouple("fpa2bv_to_float_exp_ovf", ovf_cond); + dbg_decouple("fpa2bv_to_float_exp_udf", udf_cond); + res_exp = exp_in_range; - res_exp = m.mk_ite(ovf_cond, exp_max, res_exp); - res_exp = m.mk_ite(udf_cond, exp_min, res_exp); + res_exp = m.mk_ite(ovf_cond, max_exp, res_exp); + res_exp = m.mk_ite(udf_cond, min_exp, res_exp); } - else // from_ebits == (to_ebits + 2) + else { // from_ebits == (to_ebits + 2) res_exp = m_bv_util.mk_bv_sub(exp, lz); + } SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits + 2); SASSERT(is_well_sorted(m, res_exp));