mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
This commit is contained in:
commit
de98426649
3 changed files with 31 additions and 10 deletions
|
@ -83,17 +83,21 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
|
|||
rational q;
|
||||
mpf q_mpf;
|
||||
if (m_util.au().is_numeral(args[1], q)) {
|
||||
TRACE("fp_rewriter", tout << "q: " << q << std::endl; );
|
||||
mpf v;
|
||||
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
|
||||
result = m_util.mk_value(v);
|
||||
m_util.fm().del(v);
|
||||
m_util.fm().del(v);
|
||||
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
|
||||
return BR_DONE;
|
||||
}
|
||||
else if (m_util.is_value(args[1], q_mpf)) {
|
||||
else if (m_util.is_value(args[1], q_mpf)) {
|
||||
TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; );
|
||||
mpf v;
|
||||
m_util.fm().set(v, ebits, sbits, rm, q_mpf);
|
||||
result = m_util.mk_value(v);
|
||||
m_util.fm().del(v);
|
||||
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
|
||||
return BR_DONE;
|
||||
}
|
||||
else
|
||||
|
@ -117,11 +121,11 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
|
|||
return BR_FAILED;
|
||||
|
||||
TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";);
|
||||
|
||||
mpf v;
|
||||
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
|
||||
result = m_util.mk_value(v);
|
||||
m_util.fm().del(v);
|
||||
m_util.fm().del(v);
|
||||
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
|
|
|
@ -1698,6 +1698,10 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
expr_ref sgn(m), sig(m), exp(m), lz(m);
|
||||
unpack(x, sgn, sig, exp, lz, true);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_x_sig", sig);
|
||||
dbg_decouple("fpa2bv_to_float_x_exp", exp);
|
||||
dbg_decouple("fpa2bv_to_float_lz", lz);
|
||||
|
||||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
|
||||
res_sgn = sgn;
|
||||
|
@ -1710,10 +1714,13 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
|
||||
SASSERT(m_bv_util.get_bv_size(sig) == from_sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == from_ebits);
|
||||
SASSERT(m_bv_util.get_bv_size(lz) == from_ebits);
|
||||
|
||||
if (from_sbits < (to_sbits + 3))
|
||||
if (from_sbits < (to_sbits + 3))
|
||||
{
|
||||
// make sure that sig has at least to_sbits + 3
|
||||
res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits));
|
||||
}
|
||||
else if (from_sbits > (to_sbits + 3))
|
||||
{
|
||||
// collapse the extra bits into a sticky bit.
|
||||
|
@ -1734,7 +1741,9 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
exponent_overflow = m.mk_false();
|
||||
|
||||
if (from_ebits < (to_ebits + 2))
|
||||
res_exp = m_bv_util.mk_sign_extend(to_ebits+2-from_ebits, exp);
|
||||
{
|
||||
res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp);
|
||||
}
|
||||
else if (from_ebits > (to_ebits + 2))
|
||||
{
|
||||
expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m);
|
||||
|
@ -1747,7 +1756,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
|
||||
|
||||
zero1 = m_bv_util.mk_numeral(0, 1);
|
||||
m_simp.mk_eq(high_red_and, one1, h_and_eq);
|
||||
m_simp.mk_eq(high_red_and, one1, h_and_eq);
|
||||
m_simp.mk_eq(high_red_or, zero1, h_or_eq);
|
||||
m_simp.mk_eq(lows, zero1, s_is_zero);
|
||||
m_simp.mk_eq(lows, one1, s_is_one);
|
||||
|
@ -1763,10 +1772,18 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
else
|
||||
res_exp = exp;
|
||||
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref lz_ext(m);
|
||||
lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz);
|
||||
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_res_sig", res_sig);
|
||||
dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
|
||||
|
||||
expr_ref rounded(m);
|
||||
round(s, rm, res_sgn, res_sig, res_exp, rounded);
|
||||
|
||||
|
||||
expr_ref is_neg(m), sig_inf(m);
|
||||
m_simp.mk_eq(sgn, one1, is_neg);
|
||||
|
@ -1781,7 +1798,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
mk_ite(c4, v4, result, result);
|
||||
mk_ite(c3, v3, result, result);
|
||||
mk_ite(c2, v2, result, result);
|
||||
mk_ite(c1, v1, result, result);
|
||||
mk_ite(c1, v1, result, result);
|
||||
}
|
||||
else {
|
||||
// .. other than that, we only support rationals for asFloat
|
||||
|
@ -1826,7 +1843,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
m_util.fm().del(v);
|
||||
}
|
||||
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
|
|
|
@ -367,7 +367,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
|
|||
o.ebits = ebits;
|
||||
o.sbits = sbits;
|
||||
|
||||
signed ds = sbits - x.sbits + 4; // plus rounding bits
|
||||
signed ds = sbits - x.sbits + 3; // plus rounding bits
|
||||
if (ds > 0)
|
||||
{
|
||||
m_mpz_manager.mul2k(o.significand, ds);
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue