From 12c32663c67e48d4397759bb12c0c20f8e7bde1b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Sep 2021 11:44:39 +0000 Subject: [PATCH 1/9] Fix error messsages --- src/ast/fpa/fpa2bv_converter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index de0b69946..8f0820c13 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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); From e8d6d97ba378e4b80e4af4f7fc5296c02104d9a7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Sep 2021 11:45:17 +0000 Subject: [PATCH 2/9] Refine fpa_decl_plugin::is_unique_value --- src/ast/fpa_decl_plugin.cpp | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 2dca61a39..5062615f2 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -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; } From 515a2a771e270f8c84a2d1f3e8a3c3909d33e8cd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Sep 2021 11:45:49 +0000 Subject: [PATCH 3/9] Whitespace --- src/ast/fpa/bv2fpa_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 49f9abacd..00d75e364 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -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()); From f1acc4b78a8c80377c8f65a7a2758f8a59b1e5b5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Sep 2021 12:55:18 +0000 Subject: [PATCH 4/9] Make fpa2bv debug symbol names optional --- src/ast/fpa/bv2fpa_converter.cpp | 9 +++++---- src/ast/fpa/fpa2bv_converter.cpp | 6 +++--- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 00d75e364..3da45781f 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -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) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 8f0820c13..b35be66f6 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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 @@ -3839,7 +3839,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)) { From 8e69f76784a6fb6ef9418dfdf0d2c1aca11fb9b7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Sep 2021 13:27:32 +0000 Subject: [PATCH 5/9] Add additional equality in theory_fpa --- src/smt/theory_fpa.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 1543ac2c2..c36346de4 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -454,13 +454,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); From 00e8ea79621c5029d6773e3164ded601161c0898 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Sep 2021 15:46:58 +0000 Subject: [PATCH 6/9] Make terms that are internalized on the fly relevant --- src/smt/theory_fpa.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index c36346de4..d1f60eb97 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -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; @@ -623,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++) { From c24f438e51cc9af302e400d36e1f1b73a4bb0d9a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 15 Sep 2021 12:33:49 +0000 Subject: [PATCH 7/9] Fix for mk_to_fp_float; pertains to #4841 --- src/ast/fpa/fpa2bv_converter.cpp | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index b35be66f6..7876d2d79 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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)); From 738783a26c760d33a3ef18c31d0d4484f0c2f1f8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 15 Sep 2021 16:29:06 +0000 Subject: [PATCH 8/9] Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it. --- src/ast/fpa/fpa2bv_converter.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 7876d2d79..0d3f0e7c0 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -982,6 +982,8 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & // 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_a_sig_ext", a_sig_ext); + dbg_decouple("fpa2bv_div_b_sig_ext", b_sig_ext); dbg_decouple("fpa2bv_div_quotient", quotient); SASSERT(m_bv_util.get_bv_size(quotient) == (sbits + sbits + extra_bits)); @@ -989,6 +991,7 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & expr_ref sticky(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); + dbg_decouple("fpa2bv_div_sticky", sticky); SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4)); @@ -996,15 +999,21 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & mk_leading_zeros(res_sig, sbits + 4, res_sig_lz); dbg_decouple("fpa2bv_div_res_sig_lz", res_sig_lz); expr_ref res_sig_shift_amount(m); - res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); + res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(2, sbits + 4)); dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount); expr_ref shift_cond(m); shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); expr_ref res_sig_shifted(m), res_exp_shifted(m); res_sig_shifted = m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount); res_exp_shifted = m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits + 1, 0, res_sig_shift_amount)); + dbg_decouple("fpa2bv_div_res_sig", res_sig); + dbg_decouple("fpa2bv_div_res_exp", res_exp); + dbg_decouple("fpa2bv_div_res_sig_shifted", res_sig_shifted); + dbg_decouple("fpa2bv_div_res_exp_shifted", res_exp_shifted); 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); + dbg_decouple("fpa2bv_div_shift_cond", shift_cond); + round(s, rm, res_sgn, res_sig, res_exp, v8); From b471ebdf1cf17b4178c2b76033a8ba82315b0944 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 12 Oct 2021 12:44:16 +0000 Subject: [PATCH 9/9] Revert "Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it." This reverts commit f80fdb4ea3a762cfe95daa0321d9875cfa00c7ae. --- src/ast/fpa/fpa2bv_converter.cpp | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 0d3f0e7c0..7876d2d79 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -982,8 +982,6 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & // 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_a_sig_ext", a_sig_ext); - dbg_decouple("fpa2bv_div_b_sig_ext", b_sig_ext); dbg_decouple("fpa2bv_div_quotient", quotient); SASSERT(m_bv_util.get_bv_size(quotient) == (sbits + sbits + extra_bits)); @@ -991,7 +989,6 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & expr_ref sticky(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); - dbg_decouple("fpa2bv_div_sticky", sticky); SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4)); @@ -999,21 +996,15 @@ void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & mk_leading_zeros(res_sig, sbits + 4, res_sig_lz); dbg_decouple("fpa2bv_div_res_sig_lz", res_sig_lz); expr_ref res_sig_shift_amount(m); - res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(2, sbits + 4)); + res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount); expr_ref shift_cond(m); shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); expr_ref res_sig_shifted(m), res_exp_shifted(m); res_sig_shifted = m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount); res_exp_shifted = m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits + 1, 0, res_sig_shift_amount)); - dbg_decouple("fpa2bv_div_res_sig", res_sig); - dbg_decouple("fpa2bv_div_res_exp", res_exp); - dbg_decouple("fpa2bv_div_res_sig_shifted", res_sig_shifted); - dbg_decouple("fpa2bv_div_res_exp_shifted", res_exp_shifted); 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); - dbg_decouple("fpa2bv_div_shift_cond", shift_cond); - round(s, rm, res_sgn, res_sig, res_exp, v8);