mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Assorted fixes for floats (#6968)
* Improve4be26eb543* Add-on to0f4f32c5d0* Fix mk_numeral * Fix corner-case in fp.div * Fixes for corner-cases in mk_to_fp_(un)signed * Fix out-of-range results in mpf_manager::fma * Further adjustments for fp.to_fp_(un)signed * fp.to_fp from real can't be NaN * fp.to_fp from reals: add bounds * Fix NaN encodings in theory_fpa. * Fix fp.fma rounding with tiny floats * Fix literal creation order in theory_fpa
This commit is contained in:
Christoph M. Wintersteiger
GitHub
parent
bd8e5eee4b
commit
9d57bdd2ef
|
|
@ -324,7 +324,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
|
|||
expr_ref else_value(m.mk_app(to_bv_i, dom.size(), dom.data()), m);
|
||||
result->set_else(else_value);
|
||||
}
|
||||
else if (m_fpa_util.is_to_real(f)) {
|
||||
else if (m_fpa_util.is_to_real(f)) {
|
||||
SASSERT(dom.size() == 1);
|
||||
func_decl_ref to_real_i(m.mk_func_decl(fid, OP_FPA_TO_REAL_I, 0, nullptr, dom.size(), dom.data()), m);
|
||||
expr_ref else_value(m.mk_app(to_real_i, dom.size(), dom.data()), m);
|
||||
|
|
@ -508,7 +508,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
|
|||
}
|
||||
}
|
||||
|
||||
TRACE("bv2fpa", tout << "Target model: " << *target_model; );
|
||||
TRACE("bv2fpa", tout << "Target model: " << *target_model << std::endl; );
|
||||
}
|
||||
|
||||
void bv2fpa_converter::display(std::ostream & out) {
|
||||
|
|
|
|||
|
|
@ -147,36 +147,11 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a
|
|||
|
||||
void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num == 0);
|
||||
sort* s = f->get_range();
|
||||
if (f->get_num_parameters() == 1) {
|
||||
SASSERT(f->get_parameter(0).is_external());
|
||||
unsigned p_id = f->get_parameter(0).get_ext_id();
|
||||
mpf const& v = m_plugin->get_value(p_id);
|
||||
mk_numeral(s, v, result);
|
||||
return;
|
||||
}
|
||||
scoped_mpf v(m_mpf_manager);
|
||||
unsigned ebits = m_util.get_ebits(s), sbits = m_util.get_sbits(s);
|
||||
switch (f->get_decl_kind()) {
|
||||
case OP_FPA_PLUS_INF:
|
||||
m_util.fm().mk_pinf(ebits, sbits, v);
|
||||
break;
|
||||
case OP_FPA_MINUS_INF:
|
||||
m_util.fm().mk_ninf(ebits, sbits, v);
|
||||
break;
|
||||
case OP_FPA_NAN:
|
||||
m_util.fm().mk_nan(ebits, sbits, v);
|
||||
break;
|
||||
case OP_FPA_PLUS_ZERO:
|
||||
m_util.fm().mk_pzero(ebits, sbits, v);
|
||||
break;
|
||||
case OP_FPA_MINUS_ZERO:
|
||||
m_util.fm().mk_nzero(ebits, sbits, v);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
mk_numeral(s, v, result);
|
||||
scoped_mpf v(m_mpf_manager);
|
||||
expr_ref a(m);
|
||||
a = m.mk_app(f, num, args);
|
||||
m_util.is_numeral(a, v);
|
||||
mk_numeral(f->get_range(), v, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) {
|
||||
|
|
@ -941,8 +916,8 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
|
|||
dbg_decouple("fpa2bv_div_y_is_pos", y_is_pos);
|
||||
dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf);
|
||||
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m);
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m);
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m), c8(m);
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m), v9(m);
|
||||
|
||||
// (x is NaN) || (y is NaN) -> NaN
|
||||
m_simp.mk_or(x_is_nan, y_is_nan, c1);
|
||||
|
|
@ -998,6 +973,9 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
|
|||
a_sig_ext = m_bv_util.mk_concat(a_sig, m_bv_util.mk_numeral(0, sbits + extra_bits));
|
||||
b_sig_ext = m_bv_util.mk_zero_extend(sbits + extra_bits, b_sig);
|
||||
|
||||
dbg_decouple("fpa2bv_div_a_sig_ext", a_sig_ext);
|
||||
dbg_decouple("fpa2bv_div_b_sig_ext", b_sig_ext);
|
||||
|
||||
expr_ref a_exp_ext(m), b_exp_ext(m);
|
||||
a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
|
||||
b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
|
||||
|
|
@ -1017,14 +995,21 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
|
|||
expr_ref quotient(m);
|
||||
// b_sig_ext can't be 0 here, so it's safe to use OP_BUDIV_I
|
||||
quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, a_sig_ext, b_sig_ext);
|
||||
|
||||
dbg_decouple("fpa2bv_div_quotient", quotient);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(quotient) == (sbits + sbits + extra_bits));
|
||||
|
||||
expr_ref sticky(m);
|
||||
expr_ref sticky(m), upper(m), upper_reduced(m), too_large(m);
|
||||
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(extra_bits-2, 0, quotient));
|
||||
res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(extra_bits+sbits+1, extra_bits-1, quotient), sticky);
|
||||
upper = m_bv_util.mk_extract(sbits + sbits + extra_bits-1, extra_bits+sbits+2, quotient);
|
||||
upper_reduced = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, upper.get());
|
||||
too_large = m.mk_eq(upper_reduced, m_bv_util.mk_numeral(1, 1));
|
||||
c8 = too_large;
|
||||
mk_ite(signs_xor, ninf, pinf, v8);
|
||||
dbg_decouple("fpa2bv_div_res_sig_p4", res_sig);
|
||||
dbg_decouple("fpa2bv_div_upper", upper);
|
||||
dbg_decouple("fpa2bv_div_too_large", too_large);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
|
||||
|
||||
|
|
@ -1042,10 +1027,14 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
|
|||
m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig);
|
||||
m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp);
|
||||
|
||||
round(s, rm, res_sgn, res_sig, res_exp, v8);
|
||||
dbg_decouple("fpa2bv_div_res_sig", res_sig);
|
||||
dbg_decouple("fpa2bv_div_res_exp", res_exp);
|
||||
|
||||
round(s, rm, res_sgn, res_sig, res_exp, v9);
|
||||
|
||||
// And finally, we tie them together.
|
||||
mk_ite(c7, v7, v8, result);
|
||||
mk_ite(c8, v8, v9, result);
|
||||
mk_ite(c7, v7, result, result);
|
||||
mk_ite(c6, v6, result, result);
|
||||
mk_ite(c5, v5, result, result);
|
||||
mk_ite(c4, v4, result, result);
|
||||
|
|
@ -2809,8 +2798,46 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
|
|||
|
||||
expr * e = m.mk_eq(m_util.mk_to_real(result), x);
|
||||
m_extra_assertions.push_back(e);
|
||||
// x = 0 -> result = 0+
|
||||
m_extra_assertions.push_back(m.mk_implies(m.mk_eq(x, zero), m.mk_eq(result, m_util.mk_pzero(result->get_sort()))));
|
||||
|
||||
expr_ref r_is_nan(m);
|
||||
mk_is_nan(result, r_is_nan);
|
||||
m_extra_assertions.push_back(m.mk_not(r_is_nan));
|
||||
|
||||
rational min_real, max_real;
|
||||
const mpz& max_exp_z = m_mpf_manager.m_powers2.m1(ebits-1);
|
||||
SASSERT(m_mpz_manager.is_uint(max_exp_z));
|
||||
unsigned max_exp = m_mpz_manager.get_uint(max_exp_z);
|
||||
rational max_sig = m_mpf_manager.m_powers2.m1(sbits) / m_mpf_manager.m_powers2(sbits-1);
|
||||
max_real = max_sig * rational(m_mpf_manager.m_powers2(max_exp));
|
||||
TRACE("fpa2bv_to_real", tout << "max exp: " << max_exp << " max real: " << max_real << std::endl;);
|
||||
|
||||
expr_ref r_is_pinf(m), r_is_ninf(m);
|
||||
mk_is_pinf(result, r_is_pinf);
|
||||
mk_is_ninf(result, r_is_ninf);
|
||||
|
||||
expr_ref e_max_real(m), e_max_real_neg(m);
|
||||
e_max_real = m_arith_util.mk_numeral(max_real, false);
|
||||
e_max_real_neg = m_arith_util.mk_numeral(-max_real, false);
|
||||
|
||||
expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
|
||||
mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_nta);
|
||||
mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_nte);
|
||||
mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_tp);
|
||||
mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_tn);
|
||||
mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_tz);
|
||||
|
||||
expr_ref implies_gt_max_real(m), implies_lt_min_real(m);
|
||||
implies_gt_max_real = m.mk_implies(r_is_pinf, m.mk_and(rm_tp, m_arith_util.mk_gt(x, e_max_real)));
|
||||
implies_lt_min_real = m.mk_implies(r_is_ninf, m.mk_and(rm_tn, m_arith_util.mk_lt(x, e_max_real_neg)));
|
||||
|
||||
m_extra_assertions.push_back(implies_gt_max_real);
|
||||
m_extra_assertions.push_back(implies_lt_min_real);
|
||||
|
||||
// x = 0 -> result = +0/-0
|
||||
expr_ref pzero(m), nzero(m);
|
||||
mk_pzero(result->get_sort(), pzero);
|
||||
mk_nzero(result->get_sort(), nzero);
|
||||
m_extra_assertions.push_back(m.mk_implies(m.mk_eq(x, zero), m.mk_or(m.mk_eq(result, pzero), m.mk_eq(result, nzero))));
|
||||
}
|
||||
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
|
|
@ -2854,19 +2881,13 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
|
|||
m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, e.to_mpq().numerator(), q.to_mpq());
|
||||
m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, e.to_mpq().numerator(), q.to_mpq());
|
||||
|
||||
app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m);
|
||||
a_nte = m_plugin->mk_numeral(nte);
|
||||
a_nta = m_plugin->mk_numeral(nta);
|
||||
a_tp = m_plugin->mk_numeral(tp);
|
||||
a_tn = m_plugin->mk_numeral(tn);
|
||||
a_tz = m_plugin->mk_numeral(tz);
|
||||
|
||||
expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
|
||||
mk_numeral(a_nte->get_decl(), 0, nullptr, bv_nte);
|
||||
mk_numeral(a_nta->get_decl(), 0, nullptr, bv_nta);
|
||||
mk_numeral(a_tp->get_decl(), 0, nullptr, bv_tp);
|
||||
mk_numeral(a_tn->get_decl(), 0, nullptr, bv_tn);
|
||||
mk_numeral(a_tz->get_decl(), 0, nullptr, bv_tz);
|
||||
sort *s = f->get_range();
|
||||
mk_numeral(s, nte, bv_nte);
|
||||
mk_numeral(s, nta, bv_nta);
|
||||
mk_numeral(s, tp, bv_tp);
|
||||
mk_numeral(s, tn, bv_tn);
|
||||
mk_numeral(s, tz, bv_tz);
|
||||
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m);
|
||||
c1 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3));
|
||||
|
|
@ -3003,30 +3024,42 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
|
|||
unsigned bv_sz = m_bv_util.get_bv_size(x);
|
||||
SASSERT(m_bv_util.get_bv_size(rm) == 3);
|
||||
|
||||
expr_ref rm_is_to_neg(m);
|
||||
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
|
||||
|
||||
expr_ref bv1_1(m), bv0_sz(m);
|
||||
bv1_1 = m_bv_util.mk_numeral(1, 1);
|
||||
bv0_sz = m_bv_util.mk_numeral(0, bv_sz);
|
||||
|
||||
expr_ref is_zero(m), pzero(m);
|
||||
expr_ref is_zero(m), pzero(m), nzero(m);
|
||||
is_zero = m.mk_eq(x, bv0_sz);
|
||||
mk_pzero(f, pzero);
|
||||
mk_nzero(f, nzero);
|
||||
|
||||
// Special case: x == 0 -> p/n zero
|
||||
// Special case: x == 0 -> +zero
|
||||
expr_ref c1(m), v1(m);
|
||||
c1 = is_zero;
|
||||
v1 = pzero;
|
||||
v1 = pzero; // No -zero? zeros_consistent_4.smt2 requires +zero.
|
||||
|
||||
// Special case: x != 0
|
||||
expr_ref is_neg_bit(m), exp_too_large(m), sig_4(m), exp_2(m);
|
||||
expr_ref sign_bit(m), exp_too_large(m), sig_4(m), exp_2(m), rest(m);
|
||||
expr_ref is_neg(m), x_abs(m), neg_x(m);
|
||||
is_neg_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x);
|
||||
is_neg = m.mk_eq(is_neg_bit, bv1_1);
|
||||
neg_x = m_bv_util.mk_bv_neg(x); // overflow problem?
|
||||
sign_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x);
|
||||
rest = m_bv_util.mk_extract(bv_sz - 2, 0, x);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_rest", rest);
|
||||
is_neg = m.mk_eq(sign_bit, bv1_1);
|
||||
neg_x = m_bv_util.mk_bv_neg(x);
|
||||
x_abs = m.mk_ite(is_neg, neg_x, x);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_is_neg", is_neg);
|
||||
// x_abs has an extra bit in the front.
|
||||
// x_abs is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2)
|
||||
// bv_sz-2 is the "1.0" bit for the rounder.
|
||||
expr_ref is_max_neg(m);
|
||||
is_max_neg = m.mk_and(is_neg, m.mk_eq(rest, m_bv_util.mk_numeral(0, bv_sz-1)));
|
||||
dbg_decouple("fpa2bv_to_fp_signed_is_max_neg", is_max_neg);
|
||||
|
||||
x_abs = m.mk_ite(is_max_neg, m_bv_util.mk_concat(bv1_1, m_bv_util.mk_numeral(0, bv_sz-1)), x_abs);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_x_abs", x_abs);
|
||||
|
||||
expr_ref lz(m);
|
||||
mk_leading_zeros(x_abs, bv_sz, lz);
|
||||
|
|
@ -3061,6 +3094,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
|
|||
expr_ref s_exp(m), exp_rest(m);
|
||||
s_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(bv_sz - 2, bv_sz), lz);
|
||||
// s_exp = (bv_sz-2) + (-lz) signed
|
||||
s_exp = m.mk_ite(is_max_neg, m_bv_util.mk_bv_sub(s_exp, m_bv_util.mk_numeral(1, bv_sz)), s_exp);
|
||||
SASSERT(m_bv_util.get_bv_size(s_exp) == bv_sz);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_s_exp", s_exp);
|
||||
|
||||
|
|
@ -3093,7 +3127,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
|
|||
dbg_decouple("fpa2bv_to_fp_signed_exp_too_large", exp_too_large);
|
||||
|
||||
expr_ref sgn(m), sig(m), exp(m);
|
||||
sgn = is_neg_bit;
|
||||
sgn = sign_bit;
|
||||
sig = sig_4;
|
||||
exp = exp_2;
|
||||
|
||||
|
|
@ -3132,6 +3166,9 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
|
|||
rm = to_app(args[0])->get_arg(0);
|
||||
x = args[1];
|
||||
|
||||
expr_ref rm_is_to_neg(m);
|
||||
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
|
||||
|
||||
dbg_decouple("fpa2bv_to_fp_unsigned_x", x);
|
||||
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
|
|
@ -3143,14 +3180,15 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
|
|||
bv0_1 = m_bv_util.mk_numeral(0, 1);
|
||||
bv0_sz = m_bv_util.mk_numeral(0, bv_sz);
|
||||
|
||||
expr_ref is_zero(m), pzero(m);
|
||||
expr_ref is_zero(m), pzero(m), nzero(m);
|
||||
is_zero = m.mk_eq(x, bv0_sz);
|
||||
mk_pzero(f, pzero);
|
||||
mk_nzero(f, nzero);
|
||||
|
||||
// Special case: x == 0 -> p/n zero
|
||||
// Special case: x == 0 -> +zero
|
||||
expr_ref c1(m), v1(m);
|
||||
c1 = is_zero;
|
||||
v1 = pzero;
|
||||
v1 = pzero; // No nzero?
|
||||
|
||||
// Special case: x != 0
|
||||
expr_ref exp_too_large(m), sig_4(m), exp_2(m);
|
||||
|
|
@ -3194,7 +3232,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
|
|||
unsigned exp_sz = ebits + 2; // (+2 for rounder)
|
||||
exp_2 = m_bv_util.mk_extract(exp_sz - 1, 0, s_exp);
|
||||
// the remaining bits are 0 if ebits is large enough.
|
||||
exp_too_large = m.mk_false(); // This is always in range.
|
||||
exp_too_large = m.mk_false();
|
||||
|
||||
// The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
|
||||
// exp < bv_sz (+sign bit which is [0])
|
||||
|
|
|
|||
|
|
@ -208,6 +208,7 @@ protected:
|
|||
|
||||
private:
|
||||
void mk_nan(sort * s, expr_ref & result);
|
||||
|
||||
void mk_nzero(sort * s, expr_ref & result);
|
||||
void mk_pzero(sort * s, expr_ref & result);
|
||||
void mk_zero(sort * s, expr_ref & sgn, expr_ref & result);
|
||||
|
|
|
|||
|
|
@ -220,7 +220,7 @@ namespace smt {
|
|||
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, m) << "\n";);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(e);
|
||||
ctx.internalize(e, false);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
literal lit(ctx.get_literal(e));
|
||||
ctx.mark_as_relevant(lit);
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
|
|
@ -239,11 +239,11 @@ namespace smt {
|
|||
if (ctx.b_internalized(atom))
|
||||
return true;
|
||||
|
||||
ctx.internalize(atom->get_args(), atom->get_num_args(), false);
|
||||
|
||||
literal l(ctx.mk_bool_var(atom));
|
||||
ctx.set_var_theory(l.var(), get_id());
|
||||
|
||||
ctx.internalize(atom->get_args(), atom->get_num_args(), false);
|
||||
|
||||
expr_ref bv_atom(m_rw.convert_atom(m_th_rw, atom));
|
||||
expr_ref bv_atom_w_side_c(m), atom_eq(m);
|
||||
bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions());
|
||||
|
|
@ -253,6 +253,18 @@ namespace smt {
|
|||
return true;
|
||||
}
|
||||
|
||||
void theory_fpa::mk_bv_nan(sort * s, expr_ref & result) {
|
||||
SASSERT(m_fpa_util.is_float(s));
|
||||
unsigned sbits = m_fpa_util.get_sbits(s);
|
||||
unsigned ebits = m_fpa_util.get_ebits(s);
|
||||
expr_ref exp(m), sgn(m), sig(m);
|
||||
exp = m_bv_util.mk_numeral(m_fpa_util.fm().m_powers2.m1(ebits), ebits);
|
||||
sgn = m_bv_util.mk_numeral(0, 1);
|
||||
sig = m_bv_util.mk_numeral(1, sbits - 1);
|
||||
expr * args[3] = {sgn, exp, sig};
|
||||
result = m_bv_util.mk_concat(3, args);
|
||||
}
|
||||
|
||||
bool theory_fpa::internalize_term(app * term) {
|
||||
TRACE("t_fpa_internalize", tout << "internalizing term: " << mk_ismt2_pp(term, m) << "\n";);
|
||||
SASSERT(term->get_family_id() == get_family_id());
|
||||
|
|
@ -286,6 +298,22 @@ namespace smt {
|
|||
default: /* ignore */;
|
||||
}
|
||||
|
||||
expr * owner = e->get_expr();
|
||||
sort * s = owner->get_sort();
|
||||
if (m_fpa_util.is_float(s))
|
||||
{
|
||||
TRACE("t_fpa", tout << "extra nan constraint for: " << mk_ismt2_pp(owner, m) << "\n";);
|
||||
expr_ref wrapped(m), is_nan(m), bv_nan(m);
|
||||
app_ref impl(m);
|
||||
wrapped = m_converter.wrap(owner);
|
||||
is_nan = m_fpa_util.mk_is_nan(owner);
|
||||
mk_bv_nan(s, bv_nan);
|
||||
impl = m.mk_or(m.mk_and(is_nan, m.mk_eq(wrapped, bv_nan)),
|
||||
m.mk_and(m.mk_not(is_nan), m.mk_not(m.mk_eq(wrapped, bv_nan))));
|
||||
assert_cnstr(impl);
|
||||
assert_cnstr(mk_side_conditions());
|
||||
}
|
||||
|
||||
if (!ctx.relevancy())
|
||||
relevant_eh(term);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -121,10 +121,11 @@ namespace smt {
|
|||
void attach_new_th_var(enode * n);
|
||||
void assert_cnstr(expr * e);
|
||||
|
||||
|
||||
enode* ensure_enode(expr* e);
|
||||
enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
|
||||
app* get_ite_value(expr* e);
|
||||
|
||||
void mk_bv_nan(sort * s, expr_ref & result);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -913,34 +913,38 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
|
||||
TRACE("mpf_dbg", tout << "R*= " << to_string_binary(res, 2, 0) << " (renormalized, delta=" << renorm_delta << ")" << std::endl;);
|
||||
|
||||
if (exp(res) <= mk_max_exp(x.ebits))
|
||||
{
|
||||
set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0));
|
||||
set(o, x.ebits, x.sbits, res.sign(), res.exponent(), mpz(0));
|
||||
|
||||
if (x.sbits >= 4) {
|
||||
m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4 + 3), o.significand, sticky_rem);
|
||||
renorm_sticky |= !m_mpz_manager.is_zero(sticky_rem);
|
||||
}
|
||||
else {
|
||||
m_mpz_manager.mul2k(res.significand(), 4 - x.sbits + 3, o.significand);
|
||||
}
|
||||
|
||||
if (renorm_sticky && m_mpz_manager.is_even(o.significand))
|
||||
m_mpz_manager.inc(o.significand);
|
||||
|
||||
TRACE("mpf_dbg", tout << "sum[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;
|
||||
tout << "R = " << to_string_binary(o, 1, 3) << std::endl;);
|
||||
|
||||
if (m_mpz_manager.is_zero(o.significand))
|
||||
mk_zero(x.ebits, x.sbits, rm == MPF_ROUND_TOWARD_NEGATIVE, o);
|
||||
else
|
||||
round(rm, o);
|
||||
if (x.sbits >= 4) {
|
||||
m_mpz_manager.machine_div_rem(res.significand(), m_powers2(x.sbits - 4 + 3), o.significand, sticky_rem);
|
||||
renorm_sticky |= !m_mpz_manager.is_zero(sticky_rem);
|
||||
}
|
||||
else {
|
||||
mk_inf(x.ebits, x.sbits, res.sign(), o);
|
||||
m_mpz_manager.mul2k(res.significand(), 4 - x.sbits + 3, o.significand);
|
||||
o.exponent -= 4 - x.sbits + 3;
|
||||
}
|
||||
|
||||
if (renorm_sticky && m_mpz_manager.is_even(o.significand))
|
||||
m_mpz_manager.inc(o.significand);
|
||||
|
||||
TRACE("mpf_dbg", tout << "sum[-1:sbits+2] = " << m_mpz_manager.to_string(o.significand) << std::endl;
|
||||
tout << "R = " << to_string_binary(o, 1, 3) << std::endl;);
|
||||
|
||||
unsigned max_size = o.sbits+4;
|
||||
unsigned sig_size = m_mpz_manager.bitsize(o.significand);
|
||||
if (sig_size > max_size) {
|
||||
unsigned d = sig_size - max_size;
|
||||
m_mpz_manager.machine_div2k(o.significand, d);
|
||||
o.exponent += d;
|
||||
}
|
||||
|
||||
if (m_mpz_manager.is_zero(o.significand))
|
||||
mk_zero(x.ebits, x.sbits, rm == MPF_ROUND_TOWARD_NEGATIVE, o);
|
||||
else
|
||||
round(rm, o);
|
||||
}
|
||||
|
||||
TRACE("mpf_dbg", tout << "FMA = " << to_string(o) << std::endl;);
|
||||
}
|
||||
|
||||
void my_mpz_sqrt(unsynch_mpz_manager & m, unsigned sbits, bool odd_exp, mpz & in, mpz & o) {
|
||||
|
|
|
|||
Loading…
Reference in a new issue