Skip to content

Commit

Permalink
Assorted fixes for floats (#6968)
Browse files Browse the repository at this point in the history 
* Improve 4be26eb

* Add-on to 0f4f32c

* 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
  • Loading branch information
@wintersteiger
wintersteiger committed Oct 30, 2023
1 parent bd8e5ee commit 9d57bdd
Show file tree
Hide file tree
Showing 6 changed files with 161 additions and 89 deletions.
4 changes: 2 additions & 2 deletions src/ast/fpa/bv2fpa_converter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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) {
Expand Down
162 changes: 100 additions & 62 deletions src/ast/fpa/fpa2bv_converter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand All @@ -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));

Expand All @@ -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);
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);

Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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());
Expand All @@ -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);
Expand Down Expand Up @@ -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])
Expand Down
1 change: 1 addition & 0 deletions src/ast/fpa/fpa2bv_converter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -208,6 +208,7 @@ class fpa2bv_converter {

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);
Expand Down
34 changes: 31 additions & 3 deletions src/smt/theory_fpa.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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());
Expand All @@ -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());
Expand Down Expand Up @@ -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);
}
Expand Down
3 changes: 2 additions & 1 deletion src/smt/theory_fpa.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
};

};
Expand Down
Loading

0 comments on commit 9d57bdd

Please sign in to comment.