mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 21:38:44 +00:00
Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable
This commit is contained in:
Nikolaj Bjorner
commit
193191e003
|
|
@ -180,7 +180,7 @@ def mk_dist_dir_core(x64):
|
|||
mk_util.JAVA_ENABLED = JAVA_ENABLED
|
||||
mk_win_dist(build_path, dist_path)
|
||||
if is_verbose():
|
||||
print("Generated %s distribution folder at '%s'") % (platform, dist_path)
|
||||
print("Generated %s distribution folder at '%s'" % (platform, dist_path))
|
||||
|
||||
def mk_dist_dir():
|
||||
mk_dist_dir_core(False)
|
||||
|
|
@ -208,7 +208,7 @@ def mk_zip_core(x64):
|
|||
ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
|
||||
os.path.walk(dist_path, mk_zip_visitor, '*')
|
||||
if is_verbose():
|
||||
print("Generated '%s'") % zfname
|
||||
print("Generated '%s'" % zfname)
|
||||
except:
|
||||
pass
|
||||
ZIPOUT = None
|
||||
|
|
@ -253,7 +253,7 @@ def cp_vs_runtime_core(x64):
|
|||
for f in VS_RUNTIME_FILES:
|
||||
shutil.copy(f, bin_dist_path)
|
||||
if is_verbose():
|
||||
print("Copied '%s' to '%s'") % (f, bin_dist_path)
|
||||
print("Copied '%s' to '%s'" % (f, bin_dist_path))
|
||||
|
||||
def cp_vs_runtime():
|
||||
cp_vs_runtime_core(True)
|
||||
|
|
|
|||
|
|
@ -359,6 +359,17 @@ void fpa2bv_converter::mk_pzero(func_decl *f, expr_ref & result) {
|
|||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_one(func_decl *f, expr_ref sign, expr_ref & result) {
|
||||
sort * srt = f->get_range();
|
||||
SASSERT(is_float(srt));
|
||||
unsigned sbits = m_util.get_sbits(srt);
|
||||
unsigned ebits = m_util.get_ebits(srt);
|
||||
mk_fp(sign,
|
||||
m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits),
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm,
|
||||
expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp,
|
||||
expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp)
|
||||
|
|
@ -1556,6 +1567,13 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
rm = args[0];
|
||||
x = args[1];
|
||||
|
||||
expr_ref rm_is_rta(m), rm_is_rte(m), rm_is_rtp(m), rm_is_rtn(m), rm_is_rtz(m);
|
||||
mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_rta);
|
||||
mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_rte);
|
||||
mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_rtp);
|
||||
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_rtn);
|
||||
mk_is_rm(rm, BV_RM_TO_ZERO, rm_is_rtz);
|
||||
|
||||
expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
|
||||
mk_nan(f, nan);
|
||||
mk_nzero(f, nzero);
|
||||
|
|
@ -1568,15 +1586,26 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero);
|
||||
dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos);
|
||||
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m);
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m);
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m);
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m);
|
||||
|
||||
// (x is NaN) -> NaN
|
||||
mk_is_nan(x, c1);
|
||||
v1 = nan;
|
||||
|
||||
// (x is +-oo) -> x
|
||||
mk_is_inf(x, c2);
|
||||
v2 = x;
|
||||
|
||||
// (x is +-0) -> x ; -0.0 -> -0.0, says IEEE754, Sec 5.9.
|
||||
mk_is_zero(x, c3);
|
||||
v3 = x;
|
||||
|
||||
|
||||
expr_ref one_1(m), zero_1(m);
|
||||
one_1 = m_bv_util.mk_numeral(1, 1);
|
||||
zero_1 = m_bv_util.mk_numeral(0, 1);
|
||||
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
|
||||
|
|
@ -1586,56 +1615,132 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig);
|
||||
dbg_decouple("fpa2bv_r2i_unpacked_exp", a_exp);
|
||||
|
||||
expr_ref exp_is_small(m), exp_h(m), one_1(m);
|
||||
exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp);
|
||||
one_1 = m_bv_util.mk_numeral(1, 1);
|
||||
m_simp.mk_eq(exp_h, one_1, exp_is_small);
|
||||
dbg_decouple("fpa2bv_r2i_exp_is_small", exp_is_small);
|
||||
c3 = exp_is_small;
|
||||
mk_ite(x_is_pos, pzero, nzero, v3);
|
||||
expr_ref xzero(m);
|
||||
mk_ite(m.mk_eq(a_sgn, one_1), nzero, pzero, xzero);
|
||||
|
||||
// exponent < 0 -> 0/1
|
||||
expr_ref exp_lt_zero(m), exp_h(m);
|
||||
exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp);
|
||||
m_simp.mk_eq(exp_h, one_1, exp_lt_zero);
|
||||
dbg_decouple("fpa2bv_r2i_exp_lt_zero", exp_lt_zero);
|
||||
c4 = exp_lt_zero;
|
||||
|
||||
expr_ref pone(m), none(m), xone(m), c421(m), c422(m), c423(m), t1(m), t2(m), tie(m), v42(m), exp_lt_m1(m);
|
||||
mk_one(f, zero_1, pone);
|
||||
mk_one(f, one_1, none);
|
||||
mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone);
|
||||
|
||||
m_simp.mk_eq(a_sig, m_bv_util.mk_numeral(fu().fm().m_powers2(sbits-1), sbits), t1);
|
||||
m_simp.mk_eq(a_exp, m_bv_util.mk_numeral(-1, ebits), t2);
|
||||
m_simp.mk_and(t1, t2, tie);
|
||||
dbg_decouple("fpa2bv_r2i_c42_tie", tie);
|
||||
|
||||
m_simp.mk_and(tie, rm_is_rte, c421);
|
||||
m_simp.mk_and(tie, rm_is_rta, c422);
|
||||
c423 = m_bv_util.mk_sle(a_exp, m_bv_util.mk_numeral(-2, ebits));
|
||||
|
||||
dbg_decouple("fpa2bv_r2i_c421", c421);
|
||||
dbg_decouple("fpa2bv_r2i_c422", c422);
|
||||
dbg_decouple("fpa2bv_r2i_c423", c423);
|
||||
|
||||
v42 = xone;
|
||||
mk_ite(c423, xzero, v42, v42);
|
||||
mk_ite(c422, xone, v42, v42);
|
||||
mk_ite(c421, xzero, v42, v42);
|
||||
|
||||
mk_ite(m.mk_eq(a_sgn, one_1), nzero, pone, v4);
|
||||
mk_ite(m.mk_or(rm_is_rte, rm_is_rta), v42, v4, v4);
|
||||
mk_ite(m.mk_or(rm_is_rtz, rm_is_rtn), xzero, v4, v4);
|
||||
|
||||
SASSERT(is_well_sorted(m, v4));
|
||||
|
||||
// exponent >= sbits-1
|
||||
expr_ref exp_is_large(m);
|
||||
exp_is_large = m_bv_util.mk_sle(m_bv_util.mk_numeral(sbits-1, ebits), a_exp);
|
||||
dbg_decouple("fpa2bv_r2i_exp_is_large", exp_is_large);
|
||||
c4 = exp_is_large;
|
||||
v4 = x;
|
||||
c5 = exp_is_large;
|
||||
v5 = x;
|
||||
|
||||
// Actual conversion with rounding.
|
||||
// x.exponent >= 0 && x.exponent < x.sbits - 1
|
||||
|
||||
// The actual rounding.
|
||||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
res_sgn = a_sgn;
|
||||
res_exp = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 2), a_exp);
|
||||
res_exp = a_exp;
|
||||
|
||||
expr_ref shift(m), r_shifted(m), l_shifted(m);
|
||||
shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits-1, ebits+1),
|
||||
m_bv_util.mk_sign_extend(1, a_exp));
|
||||
if (sbits > (ebits+1))
|
||||
r_shifted = m_bv_util.mk_bv_lshr(a_sig, m_bv_util.mk_zero_extend(sbits-(ebits+1), shift));
|
||||
else if (sbits < (ebits+1))
|
||||
r_shifted = m_bv_util.mk_extract(ebits, ebits-sbits+1, m_bv_util.mk_bv_lshr(m_bv_util.mk_zero_extend(ebits+1-sbits, a_sig), shift));
|
||||
else // sbits == ebits+1
|
||||
r_shifted = m_bv_util.mk_bv_lshr(a_sig, shift);
|
||||
SASSERT(is_well_sorted(m, r_shifted));
|
||||
SASSERT(m_bv_util.get_bv_size(r_shifted) == sbits);
|
||||
expr_ref shift(m), rshift(m), div(m), rem(m);
|
||||
shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits - 1, sbits + 1),
|
||||
m_bv_util.mk_sign_extend(sbits - ebits + 1, a_exp));
|
||||
rshift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits, sbits + 1), shift);
|
||||
div = m_bv_util.mk_bv_lshr(m_bv_util.mk_zero_extend(1, a_sig), shift);
|
||||
rem = m_bv_util.mk_bv_lshr(m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(1, a_sig), rshift), rshift);
|
||||
|
||||
if (sbits > (ebits+1))
|
||||
l_shifted = m_bv_util.mk_bv_shl(r_shifted, m_bv_util.mk_zero_extend(sbits-(ebits+1), shift));
|
||||
else if (sbits < (ebits+1))
|
||||
l_shifted = m_bv_util.mk_extract(ebits, ebits-sbits+1, m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(ebits+1-sbits, r_shifted), shift));
|
||||
else // sbits == ebits+1
|
||||
l_shifted = m_bv_util.mk_bv_shl(r_shifted, shift);
|
||||
SASSERT(is_well_sorted(m, l_shifted));
|
||||
SASSERT(m_bv_util.get_bv_size(l_shifted) == sbits);
|
||||
SASSERT(is_well_sorted(m, div));
|
||||
SASSERT(is_well_sorted(m, rem));
|
||||
SASSERT(m_bv_util.get_bv_size(div) == sbits + 1);
|
||||
SASSERT(m_bv_util.get_bv_size(rem) == sbits + 1);
|
||||
|
||||
res_sig = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1),
|
||||
m_bv_util.mk_concat(l_shifted,
|
||||
m_bv_util.mk_numeral(0, 3)));
|
||||
dbg_decouple("fpa2bv_r2i_shift", shift);
|
||||
dbg_decouple("fpa2bv_r2i_rshift", rshift);
|
||||
dbg_decouple("fpa2bv_r2i_div", div);
|
||||
dbg_decouple("fpa2bv_r2i_rem", rem);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
|
||||
expr_ref div_p1(m);
|
||||
div_p1 = m_bv_util.mk_bv_add(div, m_bv_util.mk_numeral(1, sbits+1));
|
||||
|
||||
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v5);
|
||||
expr_ref tie2(m), tie2_c(m), div_last(m), v51(m), rem_shl(m);
|
||||
rem_shl = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits - 1, 0, rem), zero_1);
|
||||
m_simp.mk_eq(rem_shl,
|
||||
m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits+1), shift),
|
||||
tie2);
|
||||
div_last = m_bv_util.mk_extract(0, 0, div);
|
||||
tie2_c = m.mk_or(m.mk_and(tie2,
|
||||
m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)),
|
||||
m.mk_and(rm_is_rta, m.mk_eq(div_last, zero_1)))),
|
||||
m.mk_xor(m.mk_eq(a_sgn, one_1),
|
||||
m_bv_util.mk_sle(m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits + 1), shift),
|
||||
rem_shl)));
|
||||
m_simp.mk_ite(tie2_c, div_p1, div, v51);
|
||||
|
||||
dbg_decouple("fpa2bv_r2i_v51", v51);
|
||||
dbg_decouple("fpa2bv_r2i_tie2", tie2);
|
||||
|
||||
SASSERT(is_well_sorted(m, tie2));
|
||||
SASSERT(is_well_sorted(m, tie2_c));
|
||||
SASSERT(is_well_sorted(m, v51));
|
||||
|
||||
expr_ref c521(m), v52(m);
|
||||
m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c521);
|
||||
m_simp.mk_and(c521, m.mk_eq(res_sgn, zero_1), c521);
|
||||
m_simp.mk_ite(c521, div_p1, div, v52);
|
||||
|
||||
expr_ref c531(m), v53(m);
|
||||
m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c531);
|
||||
m_simp.mk_and(c531, m.mk_eq(res_sgn, one_1), c531);
|
||||
m_simp.mk_ite(c531, div_p1, div, v53);
|
||||
|
||||
expr_ref c51(m), c52(m), c53(m);
|
||||
c51 = m.mk_or(rm_is_rte, rm_is_rta);
|
||||
c52 = rm_is_rtp;
|
||||
c53 = rm_is_rtn;
|
||||
|
||||
res_sig = div;
|
||||
m_simp.mk_ite(c53, v53, res_sig, res_sig);
|
||||
m_simp.mk_ite(c52, v52, res_sig, res_sig);
|
||||
m_simp.mk_ite(c51, v51, res_sig, res_sig);
|
||||
res_sig = m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3)); // rounding bits are all 0.
|
||||
res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), m_bv_util.mk_extract(ebits+1, 0, shift));
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(res_sgn) == 1);
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4);
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits+2);
|
||||
|
||||
// CMW: We use the rounder for normalization.
|
||||
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v6);
|
||||
|
||||
// And finally, we tie them together.
|
||||
mk_ite(c4, v4, v5, result);
|
||||
mk_ite(c5, v5, v6, result);
|
||||
mk_ite(c4, v4, result, result);
|
||||
mk_ite(c3, v3, result, result);
|
||||
mk_ite(c2, v2, result, result);
|
||||
mk_ite(c1, v1, result, result);
|
||||
|
|
@ -3239,7 +3344,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
|
|||
|
||||
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
|
||||
#ifdef Z3DEBUG
|
||||
return;
|
||||
// return;
|
||||
// CMW: This works only for quantifier-free formulas.
|
||||
expr_ref new_e(m);
|
||||
new_e = m.mk_fresh_const(prefix, m.get_sort(e));
|
||||
|
|
|
|||
|
|
@ -151,6 +151,8 @@ public:
|
|||
expr_ref_vector m_extra_assertions;
|
||||
|
||||
protected:
|
||||
void mk_one(func_decl *f, expr_ref sign, expr_ref & result);
|
||||
|
||||
void mk_is_nan(expr * e, expr_ref & result);
|
||||
void mk_is_inf(expr * e, expr_ref & result);
|
||||
void mk_is_pinf(expr * e, expr_ref & result);
|
||||
|
|
|
|||
|
|
@ -70,7 +70,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_FPA_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
|
||||
case OP_FPA_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break;
|
||||
case OP_FPA_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
|
||||
case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break;
|
||||
case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break;
|
||||
|
||||
case OP_FPA_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break;
|
||||
case OP_FPA_LT: SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break;
|
||||
|
|
@ -484,7 +484,7 @@ br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
|
|||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status fpa_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
mpf_rounding_mode rm;
|
||||
if (m_util.is_rm_numeral(arg1, rm)) {
|
||||
scoped_mpf v2(m_fm);
|
||||
|
|
|
|||
|
|
@ -57,7 +57,7 @@ public:
|
|||
br_status mk_max(expr * arg1, expr * arg2, expr_ref & result);
|
||||
br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
|
||||
br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result);
|
||||
br_status mk_round(expr * arg1, expr * arg2, expr_ref & result);
|
||||
br_status mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result);
|
||||
br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result);
|
||||
br_status mk_lt(expr * arg1, expr * arg2, expr_ref & result);
|
||||
br_status mk_gt(expr * arg1, expr * arg2, expr_ref & result);
|
||||
|
|
|
|||
|
|
@ -351,7 +351,7 @@ bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k) {
|
|||
}
|
||||
if (word_sz < sz) {
|
||||
unsigned bit_sz = k % (8 * sizeof(unsigned));
|
||||
unsigned mask = (1 << bit_sz) - 1;
|
||||
unsigned mask = (1u << bit_sz) - 1;
|
||||
return (data[word_sz] & mask) != 0;
|
||||
}
|
||||
return false;
|
||||
|
|
|
|||
|
|
@ -75,8 +75,11 @@ public:
|
|||
bit_vector(bit_vector const & source):
|
||||
m_num_bits(source.m_num_bits),
|
||||
m_capacity(source.m_capacity),
|
||||
m_data(alloc_svect(unsigned, source.m_capacity)) {
|
||||
memcpy(m_data, source.m_data, source.m_capacity * sizeof(unsigned));
|
||||
m_data(0) {
|
||||
if (source.m_data) {
|
||||
m_data = alloc_svect(unsigned, m_capacity);
|
||||
memcpy(m_data, source.m_data, m_capacity * sizeof(unsigned));
|
||||
}
|
||||
}
|
||||
|
||||
bit_vector(unsigned const * source, int num_bits):
|
||||
|
|
@ -184,6 +187,9 @@ public:
|
|||
|
||||
bit_vector & operator=(bit_vector const & source) {
|
||||
m_num_bits = source.m_num_bits;
|
||||
if (!source.m_data)
|
||||
return *this;
|
||||
|
||||
if (m_capacity < source.m_capacity) {
|
||||
dealloc_svect(m_data);
|
||||
m_data = alloc_svect(unsigned, source.m_capacity);
|
||||
|
|
|
|||
|
|
@ -1003,9 +1003,33 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
|
|||
mk_nan(x.ebits, x.sbits, o);
|
||||
else if (is_inf(x))
|
||||
set(o, x);
|
||||
else if (x.exponent < 0)
|
||||
else if (is_zero(x))
|
||||
mk_zero(x.ebits, x.sbits, x.sign, o); // -0.0 -> -0.0, says IEEE754, Sec 5.9.
|
||||
else if (x.exponent < 0) {
|
||||
if (rm == MPF_ROUND_TOWARD_ZERO ||
|
||||
rm == MPF_ROUND_TOWARD_NEGATIVE)
|
||||
mk_zero(x.ebits, x.sbits, x.sign, o);
|
||||
else if (x.exponent >= x.sbits-1)
|
||||
else if (rm == MPF_ROUND_NEAREST_TEVEN ||
|
||||
rm == MPF_ROUND_NEAREST_TAWAY) {
|
||||
bool tie = m_mpz_manager.is_zero(x.significand) && x.exponent == -1;
|
||||
if (tie && rm == MPF_ROUND_NEAREST_TEVEN)
|
||||
mk_zero(x.ebits, x.sbits, x.sign, o);
|
||||
else if (tie && rm == MPF_ROUND_NEAREST_TAWAY)
|
||||
mk_one(x.ebits, x.sbits, x.sign, o);
|
||||
else if (x.exponent < -1)
|
||||
mk_zero(x.ebits, x.sbits, x.sign, o);
|
||||
else
|
||||
mk_one(x.ebits, x.sbits, x.sign, o);
|
||||
}
|
||||
else {
|
||||
SASSERT(rm == MPF_ROUND_TOWARD_POSITIVE);
|
||||
if (x.sign)
|
||||
mk_nzero(x.ebits, x.sbits, o);
|
||||
else
|
||||
mk_one(x.ebits, x.sbits, false, o);
|
||||
}
|
||||
}
|
||||
else if (x.exponent >= x.sbits - 1)
|
||||
set(o, x);
|
||||
else {
|
||||
SASSERT(x.exponent >= 0 && x.exponent < x.sbits-1);
|
||||
|
|
@ -1016,20 +1040,61 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
|
|||
|
||||
scoped_mpf a(*this);
|
||||
set(a, x);
|
||||
unpack(a, true);
|
||||
unpack(a, true); // A includes hidden bit
|
||||
|
||||
TRACE("mpf_dbg", tout << "A = " << to_string(a) << std::endl;);
|
||||
|
||||
SASSERT(m_mpz_manager.lt(a.significand(), m_powers2(x.sbits)));
|
||||
SASSERT(m_mpz_manager.ge(a.significand(), m_powers2(x.sbits - 1)));
|
||||
|
||||
o.exponent = a.exponent();
|
||||
m_mpz_manager.set(o.significand, a.significand());
|
||||
|
||||
unsigned q = (unsigned) o.exponent;
|
||||
unsigned shift = o.sbits-q-1;
|
||||
TRACE("mpf_dbg", tout << "Q = " << q << " shift=" << shift << std::endl;);
|
||||
m_mpz_manager.machine_div2k(o.significand, shift);
|
||||
m_mpz_manager.mul2k(o.significand, shift+3);
|
||||
unsigned shift = o.sbits - ((unsigned)o.exponent) - 1;
|
||||
const mpz & shift_p = m_powers2(shift);
|
||||
TRACE("mpf_dbg", tout << "shift=" << shift << std::endl;);
|
||||
|
||||
round(rm, o);
|
||||
scoped_mpz div(m_mpz_manager), rem(m_mpz_manager);
|
||||
m_mpz_manager.machine_div_rem(o.significand, shift_p, div, rem);
|
||||
TRACE("mpf_dbg", tout << "div=" << m_mpz_manager.to_string(div) << " rem=" << m_mpz_manager.to_string(rem) << std::endl;);
|
||||
|
||||
switch (rm) {
|
||||
case MPF_ROUND_NEAREST_TEVEN:
|
||||
case MPF_ROUND_NEAREST_TAWAY: {
|
||||
scoped_mpz t(m_mpz_manager);
|
||||
m_mpz_manager.mul2k(rem, 1, t);
|
||||
bool tie = m_mpz_manager.eq(t, shift_p);
|
||||
if (tie &&
|
||||
(rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) ||
|
||||
(rm == MPF_ROUND_NEAREST_TAWAY && m_mpz_manager.is_even(div)))
|
||||
m_mpz_manager.inc(div);
|
||||
else if (x.sign ^ m_mpz_manager.gt(t, shift_p))
|
||||
m_mpz_manager.inc(div);
|
||||
break;
|
||||
}
|
||||
case MPF_ROUND_TOWARD_POSITIVE:
|
||||
if (!m_mpz_manager.is_zero(rem) && o.sign)
|
||||
m_mpz_manager.inc(div);
|
||||
break;
|
||||
case MPF_ROUND_TOWARD_NEGATIVE:
|
||||
if (!m_mpz_manager.is_zero(rem) && !o.sign)
|
||||
m_mpz_manager.inc(div);
|
||||
break;
|
||||
case MPF_ROUND_TOWARD_ZERO:
|
||||
default:
|
||||
/* nothing */;
|
||||
}
|
||||
|
||||
m_mpz_manager.mul2k(div, shift, o.significand);
|
||||
SASSERT(m_mpz_manager.ge(o.significand, m_powers2(o.sbits - 1)));
|
||||
|
||||
// re-normalize
|
||||
while (m_mpz_manager.ge(o.significand, m_powers2(o.sbits))) {
|
||||
m_mpz_manager.machine_div2k(o.significand, 1);
|
||||
o.exponent++;
|
||||
}
|
||||
|
||||
m_mpz_manager.sub(o.significand, m_powers2(o.sbits - 1), o.significand); // strip hidden bit
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "INTEGRAL = " << to_string(o) << std::endl;);
|
||||
|
|
@ -1449,6 +1514,14 @@ void mpf_manager::mk_nan(unsigned ebits, unsigned sbits, mpf & o) {
|
|||
o.sign = false;
|
||||
}
|
||||
|
||||
void mpf_manager::mk_one(unsigned ebits, unsigned sbits, bool sign, mpf & o) const {
|
||||
o.sbits = sbits;
|
||||
o.ebits = ebits;
|
||||
o.sign = sign;
|
||||
m_mpz_manager.set(o.significand, 0);
|
||||
o.exponent = 0;
|
||||
}
|
||||
|
||||
void mpf_manager::mk_max_value(unsigned ebits, unsigned sbits, bool sign, mpf & o) {
|
||||
o.sbits = sbits;
|
||||
o.ebits = ebits;
|
||||
|
|
|
|||
|
|
@ -209,6 +209,8 @@ public:
|
|||
void to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o);
|
||||
|
||||
protected:
|
||||
void mk_one(unsigned ebits, unsigned sbits, bool sign, mpf & o) const;
|
||||
|
||||
bool has_bot_exp(mpf const & x);
|
||||
bool has_top_exp(mpf const & x);
|
||||
|
||||
|
|
|
|||
|
|
@ -255,7 +255,7 @@ void mpff_manager::set(mpff & n, int64 v) {
|
|||
}
|
||||
else {
|
||||
if (v < 0) {
|
||||
set(n, static_cast<uint64>(-v));
|
||||
set(n, -static_cast<uint64>(v));
|
||||
n.m_sign = 1;
|
||||
}
|
||||
else {
|
||||
|
|
@ -680,7 +680,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c
|
|||
|
||||
// Make sure that a and b have the same exponent.
|
||||
if (exp_a > exp_b) {
|
||||
unsigned shift = exp_a - exp_b;
|
||||
unsigned shift = (unsigned)exp_a - (unsigned)exp_b;
|
||||
n_sig_b = m_buffers[0].c_ptr();
|
||||
shr(m_precision, sig_b, shift, m_precision, n_sig_b);
|
||||
if (sgn_b != m_to_plus_inf && has_one_at_first_k_bits(m_precision, sig_b, shift)) {
|
||||
|
|
|
|||
Loading…
Reference in a new issue