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

Bugfix for FP casts (float to float conversion).

Browse source 
Fixes #331.
This commit is contained in:
Christoph M. Wintersteiger 2015-11-22 14:49:04 +00:00
parent d9bafc3fba
commit 59c1944f92
1 changed files with 20 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2277,6 +2277,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
}
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());
@ -2287,47 +2288,26 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
expr_ref exp_sub_lz(m);
exp_sub_lz = m_bv_util.mk_bv_sub(exp, 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);
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 high(m), low(m), low_msb(m);
expr_ref no_ovf(m), zero1(m);
high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp_sub_lz);
low = m_bv_util.mk_extract(to_ebits + 1, 0, exp_sub_lz);
low_msb = m_bv_util.mk_extract(to_ebits + 1, to_ebits + 1, low);
dbg_decouple("fpa2bv_to_float_exp_high", high);
dbg_decouple("fpa2bv_to_float_exp_low", low);
dbg_decouple("fpa2bv_to_float_exp_low_msb", low_msb);
res_exp = low;
expr_ref high_red_or(m), high_red_and(m);
high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get());
high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
expr_ref h_or_eq_0(m), h_and_eq_1(m), low_msb_is_one(m), low_msb_is_zero(m);
zero1 = m_bv_util.mk_numeral(0, 1);
m_simp.mk_eq(high_red_and, one1, h_and_eq_1);
m_simp.mk_eq(high_red_or, zero1, h_or_eq_0);
m_simp.mk_eq(low_msb, zero1, low_msb_is_zero);
m_simp.mk_eq(low_msb, one1, low_msb_is_one);
dbg_decouple("fpa2bv_to_float_exp_h_and_eq_1", h_and_eq_1);
dbg_decouple("fpa2bv_to_float_exp_h_or_eq_0", h_or_eq_0);
dbg_decouple("fpa2bv_to_float_exp_s_is_zero", low_msb_is_zero);
dbg_decouple("fpa2bv_to_float_exp_s_is_one", low_msb_is_one);
m_simp.mk_and(h_or_eq_0, low_msb_is_one, exponent_underflow);
m_simp.mk_and(h_and_eq_1, low_msb_is_zero, exponent_overflow);
m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow);
dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow);
dbg_decouple("fpa2bv_to_float_exp_udf", exponent_underflow);
// exponent underflow means that the result is the smallest
// representable float, rounded according to rm.
m_simp.mk_ite(exponent_underflow,
m_bv_util.mk_concat(m_bv_util.mk_numeral(1, 1),
m_bv_util.mk_numeral(1, to_ebits+1)),
res_exp,
res_exp);
m_simp.mk_ite(exponent_underflow, m_bv_util.mk_numeral(1, to_sbits+4), res_sig, res_sig);
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));
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);
}
else // from_ebits == (to_ebits + 2)
res_exp = m_bv_util.mk_bv_sub(exp, lz);