mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-09-15 10:54:17 +02:00
commit 406cd00b3a
2 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2972,14 +2972,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
sig_sz = m_bv_util.get_bv_size(sig);
SASSERT(sig_sz >= (bv_sz + 3));
expr_ref exp_m_lz(m), shift(m), shift_neg(m), bv0_e2(m), shift_abs(m);
expr_ref exp_m_lz(m), shift(m), shift_neg(m), bv0_e2(m), shift_abs(m), shift_neg_dec(m);
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
m_bv_util.mk_zero_extend(2, lz));
shift = m_bv_util.mk_bv_sub(exp_m_lz,
m_bv_util.mk_numeral(bv_sz, ebits + 2));
shift_neg = m_bv_util.mk_bv_neg(shift);
bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
shift_neg_dec = m_bv_util.mk_sle(shift, bv0_e2);
shift_abs = m.mk_ite(shift_neg_dec, shift_neg, shift);
SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
@ -3001,7 +3002,9 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
expr_ref huge_sig(m), huge_shift(m), huge_shifted_sig(m);
huge_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_sz));
huge_shift = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sig_sz), shift_abs);
huge_shifted_sig = m_bv_util.mk_bv_lshr(huge_sig, huge_shift);
huge_shifted_sig = m.mk_ite(shift_neg_dec,
m_bv_util.mk_bv_shl(huge_sig, huge_shift),
m_bv_util.mk_bv_lshr(huge_sig, huge_shift));
dbg_decouple("fpa2bv_to_sbv_huge_shifted_sig", huge_shifted_sig);
SASSERT(m_bv_util.get_bv_size(huge_shifted_sig) == 2 * sig_sz);

7
src/util/mpf.cpp
View file

@ -877,10 +877,11 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
// Remove the extra bits, keeping a sticky bit.
m_mpz_manager.set(sticky_rem, 0);
if (o.sbits >= (4+extra))
m_mpz_manager.machine_div_rem(o.significand, m_powers2(4+extra), o.significand, sticky_rem);
unsigned minbits = (4 + extra);
if (o.sbits >= minbits)
m_mpz_manager.machine_div_rem(o.significand, m_powers2(o.sbits - minbits), o.significand, sticky_rem);
else
m_mpz_manager.mul2k(o.significand, (4+extra) - o.sbits, o.significand);
m_mpz_manager.mul2k(o.significand, minbits - o.sbits, o.significand);
if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(o.significand))
m_mpz_manager.inc(o.significand);