diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 49f9abacdc2..3da45781f90 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()); @@ -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 de0b699466f..7876d2d79f3 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 @@ -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)) { diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 2dca61a3928..5062615f27b 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; } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 1543ac2c29a..d1f60eb973b 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; @@ -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++) {