mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Bugfix for FPA float to float conversion.

Browse source 
Fixes #337
This commit is contained in:
Christoph M. Wintersteiger 2015-11-24 17:21:40 +00:00
parent 5e37cf9bbf
commit 8eea6fd775
1 changed files with 29 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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));