mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge pull request #5550 from wintersteiger/cwinter_fpa_fixes

Browse source 
Assorted fixes for floats
This commit is contained in:
Christoph M. Wintersteiger 2021-10-12 18:24:49 +01:00 committed by GitHub
parent 52032b9ef8 b471ebdf1c
commit 58fd4fc860
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 33 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -102,7 +102,7 @@ expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr
rational exp_unbiased_q;
exp_unbiased_q = exp_q - m_fpa_util.fm().m_powers2.m1(ebits - 1);
scoped_mpz sig_z(mpzm);
scoped_mpz sig_z(mpzm);
mpf_exp_t exp_z;
mpzm.set(sig_z, sig_q.to_mpq().numerator());
exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
@ -346,7 +346,7 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
app * a0 = to_app(val->get_arg(0));
expr_ref v0(m), v1(m), v2(m);
#ifdef Z3DEBUG
#ifdef Z3DEBUG_FPA2BV_NAMES
app * a1 = to_app(val->get_arg(1));
app * a2 = to_app(val->get_arg(2));
v0 = mc->get_const_interp(a0->get_decl());
@ -378,7 +378,7 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP));
#ifdef Z3DEBUG
#ifdef Z3DEBUG_FPA2BV_NAMES
SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0);
SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0);
SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0);
@ -386,9 +386,10 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
seen.insert(to_app(val->get_arg(1))->get_decl());
seen.insert(to_app(val->get_arg(2))->get_decl());
#else
SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT);
SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT);
SASSERT(is_app(val->get_arg(0)));
SASSERT(m_bv_util.is_extract(val->get_arg(0)));
seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl());
#endif
if (!sgn && !sig && !exp)

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

@ -192,7 +192,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
app_ref sgn(m), s(m), e(m);
#ifdef Z3DEBUG
#ifdef Z3DEBUG_FPA2BV_NAMES
std::string p("fpa2bv");
std::string name = f->get_name().str();
@ -326,7 +326,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
expr_ref bv3(m);
bv3 = m.mk_fresh_const(
#ifdef Z3DEBUG
#ifdef Z3DEBUG_FPA2BV_NAMES
"fpa2bv_rm"
#else
nullptr
@ -465,7 +465,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
SASSERT(is_well_sorted(m, big_d_sig));
if (ebits > sbits)
throw default_exception("there is no floating point support for division for representations with non-standard bit representations");
throw default_exception("addition/subtract with ebits > sbits not supported");
expr_ref shifted_big(m), shifted_d_sig(m), sticky_raw(m), sticky(m);
@ -950,7 +950,7 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
if (ebits > sbits)
throw default_exception("there is no floating point support for division for representations with non-standard bit representations");
throw default_exception("division with ebits > sbits not supported");
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
@ -2561,9 +2561,7 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r
res_sig = sig;
res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
(void) sig_sz;
SASSERT(sig_sz == to_sbits + 4);
SASSERT(m_bv_util.get_bv_size(res_sig) == to_sbits + 4);
expr_ref exponent_overflow(m), exponent_underflow(m);
exponent_overflow = m.mk_false();
@ -2577,7 +2575,7 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r
lz_ext = m_bv_util.mk_zero_extend(to_ebits - from_ebits + 2, lz);
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
}
else if (from_ebits > (to_ebits + 2)) {
else if (from_ebits >= (to_ebits + 2)) {
unsigned ebits_diff = from_ebits - (to_ebits + 2);
// subtract lz for subnormal numbers.
@ -2617,9 +2615,6 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r
res_exp = m.mk_ite(ovf_cond, max_exp, res_exp);
res_exp = m.mk_ite(udf_cond, min_exp, res_exp);
}
else { // from_ebits == (to_ebits + 2)
res_exp = m_bv_util.mk_bv_sub(exp, lz);
}
SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits + 2);
SASSERT(is_well_sorted(m, res_exp));
@ -3839,7 +3834,7 @@ void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result)
}
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#ifdef Z3DEBUG
#ifdef Z3DEBUG_FPA2BV_NAMES
return;
// CMW: This works only for quantifier-free formulas.
if (m_util.is_fp(e)) {

22
src/ast/fpa_decl_plugin.cpp
View file

@ -207,7 +207,7 @@ sort * fpa_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
m_manager->raise_exception("minimum number of exponent bits is 2");
if (ebits > 63)
m_manager->raise_exception("maximum number of exponent bits is 63");
parameter p1(ebits), p2(sbits);
parameter ps[2] = { p1, p2 };
sort_size sz;
@ -929,16 +929,22 @@ bool fpa_decl_plugin::is_unique_value(app* e) const {
case OP_FPA_RM_TOWARD_NEGATIVE:
case OP_FPA_RM_TOWARD_ZERO:
return true;
case OP_FPA_PLUS_INF: /* No; +oo == fp(#b0 #b11 #b00) */
case OP_FPA_MINUS_INF: /* No; -oo == fp #b1 #b11 #b00) */
case OP_FPA_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */
case OP_FPA_MINUS_ZERO: /* No; -zero == fp #b1 #b00 #b000) */
case OP_FPA_PLUS_INF: /* No; +oo == (fp #b0 #b11 #b00) */
case OP_FPA_MINUS_INF: /* No; -oo == (fp #b1 #b11 #b00) */
case OP_FPA_PLUS_ZERO: /* No; +zero == (fp #b0 #b00 #b000) */
case OP_FPA_MINUS_ZERO: /* No; -zero == (fp #b1 #b00 #b000) */
case OP_FPA_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */
case OP_FPA_NUM: /* see NaN */
return false;
case OP_FPA_FP:
return false; /*No; generally not because of clashes with +oo, -oo, +zero, -zero, NaN */
// a refinement would require to return true only if there is no clash with these cases.
case OP_FPA_FP: {
if (m_manager->is_value(e->get_arg(0)) &&
m_manager->is_value(e->get_arg(1)) &&
m_manager->is_value(e->get_arg(2))) {
bv_util bu(*m_manager);
return !bu.is_allone(e->get_arg(1)) && !bu.is_zero(e->get_arg(1));
}
return false;
}
default:
return false;
}

13
src/smt/theory_fpa.cpp
View file

@ -38,7 +38,7 @@ namespace smt {
{
params_ref p;
p.set_bool("arith_lhs", true);
m_th_rw.updt_params(p);
m_th_rw.updt_params(p);
}
theory_fpa::~theory_fpa()
@ -284,6 +284,9 @@ namespace smt {
}
default: /* ignore */;
}
if (!ctx.relevancy())
relevant_eh(term);
}
return true;
@ -454,13 +457,9 @@ namespace smt {
expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) };
cc_args = m_bv_util.mk_concat(3, args);
c = m.mk_eq(wrapped, cc_args);
// NB code review: #5454 exposes a bug in fpa_solver that
// could be latent here as well. It needs also the equality
// n == bv_val_e to be asserted such that whenever something is assigned th
// bit-vector value cc_args it is equated with n
// I don't see another way this constraint would be enforced.
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
assert_cnstr(m.mk_eq(n, bv_val_e));
}
else {
expr_ref wu(m);
@ -627,7 +626,7 @@ namespace smt {
bv2fp.convert_min_max_specials(&mdl, &new_model, seen);
bv2fp.convert_uf2bvuf(&mdl, &new_model, seen);
for (func_decl* f : seen)
for (func_decl* f : seen)
mdl.unregister_decl(f);
for (unsigned i = 0; i < new_model.get_num_constants(); i++) {