mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

FP: Fix for conversion functions from non-FP 0 to +0.0 even when the rounding mode is ToNegative.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-04-25 15:01:20 +01:00
parent b58d3f4335
commit 4768a360f8
1 changed files with 106 additions and 89 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2096,9 +2096,14 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
bool is_int;
m_util.au().is_numeral(x, q, is_int);
if (q.is_zero())
return mk_pzero(f, result);
else {
scoped_mpf v(m_mpf_manager);
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
@ -2107,11 +2112,15 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
mk_fp(sgn, e, s, result);
}
}
else if (m_util.au().is_numeral(x)) {
rational q;
bool is_int;
m_util.au().is_numeral(x, q, is_int);
if (m_util.au().is_zero(x))
mk_pzero(f, result);
else {
expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_nta);
mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_nte);
@ -2165,6 +2174,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
mk_ite(rm_nte, v2, result, result);
mk_ite(rm_nta, v1, result, result);
}
}
else {
bv_util & bu = m_bv_util;
arith_util & au = m_arith_util;
@ -2183,6 +2193,10 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
expr_ref rme(rm, m);
round(s, rme, sgn, sig, exp, result);
expr_ref c0(m);
mk_is_zero(x, c0);
mk_ite(c0, x, result, result);
expr * e = m.mk_eq(m_util.mk_to_real(result), x);
m_extra_assertions.push_back(e);
}
@ -2209,6 +2223,9 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
SASSERT(e.is_int64());
SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1));
if (q.is_zero())
return mk_pzero(f, result);
else {
scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager);
m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator());
m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator());
@ -2241,6 +2258,8 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
mk_ite(c3, bv_nta, result, result);
mk_ite(c4, bv_nte, result, result);
}
}
void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
TRACE("fpa2bv_to_real", for (unsigned i = 0; i < num; i++)
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
@ -2367,10 +2386,9 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
mk_pinf(f, pinf);
// Special case: x == 0 -> p/n zero
expr_ref c1(m), v1(m), rm_is_to_neg(m);
expr_ref c1(m), v1(m);
c1 = is_zero;
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_ite(rm_is_to_neg, nzero, pzero, v1);
v1 = pzero;
// Special case: x != 0
expr_ref is_neg_bit(m), exp_too_large(m), sig_4(m), exp_2(m);
@ -2508,10 +2526,9 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
mk_pinf(f, pinf);
// Special case: x == 0 -> p/n zero
expr_ref c1(m), v1(m), rm_is_to_neg(m);
expr_ref c1(m), v1(m);
c1 = is_zero;
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_ite(rm_is_to_neg, nzero, pzero, v1);
v1 = pzero;
// Special case: x != 0
expr_ref exp_too_large(m), sig_4(m), exp_2(m);