mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Bugfixes for fp.to_* operators
This commit is contained in:
parent
4267f304a4
commit
05447d612a
|
@ -285,7 +285,21 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
|
|||
bv_fres = bv_fe->get_result();
|
||||
ft_fres = rebuild_floats(mc, rng, to_app(bv_fres));
|
||||
m_th_rw(ft_fres);
|
||||
result->insert_new_entry(new_args.c_ptr(), ft_fres);
|
||||
TRACE("bv2fpa",
|
||||
for (unsigned i = 0; i < new_args.size(); i++)
|
||||
tout << mk_ismt2_pp(bv_args[i], m) << " == " <<
|
||||
mk_ismt2_pp(new_args[i], m) << std::endl;
|
||||
tout << mk_ismt2_pp(bv_fres, m) << " == " << mk_ismt2_pp(ft_fres, m) << std::endl;);
|
||||
func_entry * fe = result->get_entry(new_args.c_ptr());
|
||||
if (fe == 0)
|
||||
result->insert_new_entry(new_args.c_ptr(), ft_fres);
|
||||
else {
|
||||
// The BV model may have multiple equivalent entries using different
|
||||
// representations of NaN. We can only keep one and we check that
|
||||
// the results for all those entries are the same.
|
||||
if (ft_fres != fe->get_result())
|
||||
throw default_exception("BUG: UF function entries disagree with each other");
|
||||
}
|
||||
}
|
||||
|
||||
app_ref bv_els(m);
|
||||
|
@ -462,6 +476,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
|
|||
args.push_back(m.mk_var(i, f->get_domain()[i]));
|
||||
fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr()));
|
||||
#else
|
||||
|
||||
fmv->set_else(0);
|
||||
#endif
|
||||
target_model->register_decl(f, fmv);
|
||||
|
@ -476,7 +491,6 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
|
|||
}
|
||||
|
||||
void bv2fpa_converter::display(std::ostream & out) {
|
||||
out << "(fpa2bv-model-converter";
|
||||
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
|
||||
it != m_const2bv.end();
|
||||
it++) {
|
||||
|
@ -510,7 +524,6 @@ void bv2fpa_converter::display(std::ostream & out) {
|
|||
out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
|
||||
mk_ismt2_pp(it->m_value.second, m, indent) << ")";
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
|
||||
bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
|
||||
|
|
|
@ -3312,11 +3312,11 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m);
|
||||
big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift),
|
||||
m_bv_util.mk_bv_shl(big_sig, shift));
|
||||
int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-bv_sz-3, big_sig_shifted);
|
||||
int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted);
|
||||
SASSERT(m_bv_util.get_bv_size(int_part) == bv_sz+3);
|
||||
last = m_bv_util.mk_extract(big_sig_sz-bv_sz-4, big_sig_sz-bv_sz-4, big_sig_shifted);
|
||||
round = m_bv_util.mk_extract(big_sig_sz-bv_sz-5, big_sig_sz-bv_sz-5, big_sig_shifted);
|
||||
stickies = m_bv_util.mk_extract(big_sig_sz-bv_sz-6, 0, big_sig_shifted);
|
||||
last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted);
|
||||
round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted);
|
||||
stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted);
|
||||
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies);
|
||||
dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted);
|
||||
dbg_decouple("fpa2bv_to_bv_int_part", int_part);
|
||||
|
@ -3335,25 +3335,25 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
dbg_decouple("fpa2bv_to_bv_inc", inc);
|
||||
dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
|
||||
|
||||
expr_ref out_of_range(m);
|
||||
expr_ref in_range(m);
|
||||
if (!is_signed) {
|
||||
expr_ref ul(m);
|
||||
ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
|
||||
out_of_range = m_bv_util.mk_ule(ul, pre_rounded);
|
||||
ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz));
|
||||
in_range = m_bv_util.mk_ule(pre_rounded, ul);
|
||||
}
|
||||
else {
|
||||
expr_ref ll(m), ul(m);
|
||||
ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
|
||||
ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1));
|
||||
out_of_range = m.mk_not(m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul)));
|
||||
in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
|
||||
}
|
||||
dbg_decouple("fpa2bv_to_bv_out_of_range", out_of_range);
|
||||
dbg_decouple("fpa2bv_to_bv_in_range", in_range);
|
||||
|
||||
expr_ref rounded(m);
|
||||
rounded = m_bv_util.mk_extract(bv_sz-1, 0, pre_rounded);
|
||||
dbg_decouple("fpa2bv_to_bv_rounded", rounded);
|
||||
|
||||
result = m.mk_ite(out_of_range, unspec_v, rounded);
|
||||
result = m.mk_ite(m.mk_not(in_range), unspec_v, rounded);
|
||||
result = m.mk_ite(c2, v2, result);
|
||||
result = m.mk_ite(c1, v1, result);
|
||||
|
||||
|
|
|
@ -854,13 +854,11 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
|
|||
scoped_mpf v(m_fm);
|
||||
|
||||
if (m_util.is_numeral(arg, v)) {
|
||||
if (!m_fm.is_nan(v) && !m_fm.is_inf(v)) {
|
||||
if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
|
||||
if (m_hi_fp_unspecified) {
|
||||
result = m_util.arith_util().mk_numeral(rational(0), false);
|
||||
return BR_DONE;
|
||||
}
|
||||
else
|
||||
return BR_FAILED;
|
||||
}
|
||||
else {
|
||||
scoped_mpq r(m_fm.mpq_manager());
|
||||
|
|
|
@ -1217,12 +1217,18 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
|
|||
default: UNREACHABLE();
|
||||
}
|
||||
if (inc) m_mpz_manager.inc(z);
|
||||
TRACE("mpf_dbg_sbv",
|
||||
tout << "SBV: (" << to_string(x) << ") == " << m_mpq_manager.to_string(z) << std::endl;
|
||||
tout << "sign=" << t.sign() << " last=" << last << " round=" << round <<
|
||||
" sticky=" << sticky << " inc=" << inc << std::endl; );
|
||||
}
|
||||
else
|
||||
m_mpz_manager.mul2k(z, (unsigned) e);
|
||||
|
||||
m_mpq_manager.set(o, z);
|
||||
if (x.sign) m_mpq_manager.neg(o);
|
||||
|
||||
TRACE("mpf_dbg", tout << "SBV = " << m_mpq_manager.to_string(o) << std::endl;);
|
||||
}
|
||||
|
||||
void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
|
||||
|
@ -1248,6 +1254,8 @@ void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
|
|||
m_mpz_manager.mul2k(o, sbits - 1);
|
||||
m_mpz_manager.add(o, sig(x), o);
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "IEEE_BV = " << m_mpz_manager.to_string(o) << std::endl;);
|
||||
}
|
||||
|
||||
void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig) {
|
||||
|
|
Loading…
Reference in a new issue