From 99d7a47f82fed5ceaeaa396dd5ed812c817ab576 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Mar 2016 21:45:54 +0000 Subject: [PATCH] Bugfixes for unspecified results from fp.to_* (models are still incomplete). Relates to #507 --- src/ast/fpa/fpa2bv_converter.cpp | 89 +++++++++++++++-------- src/ast/fpa/fpa2bv_converter.h | 8 +- src/ast/fpa_decl_plugin.cpp | 67 +++++++++-------- src/ast/fpa_decl_plugin.h | 8 +- src/ast/rewriter/fpa_rewriter.cpp | 88 +++++++++++++--------- src/ast/rewriter/fpa_rewriter.h | 2 +- src/tactic/fpa/fpa2bv_model_converter.cpp | 32 ++++++++ src/tactic/fpa/fpa2bv_model_converter.h | 9 +++ 8 files changed, 196 insertions(+), 107 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 7cd470312..20d04ebe6 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2647,8 +2647,8 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); result = m.mk_ite(x_is_zero, zero, res); - result = m.mk_ite(x_is_inf, mk_to_real_unspecified(), result); - result = m.mk_ite(x_is_nan, mk_to_real_unspecified(), result); + result = m.mk_ite(x_is_inf, mk_to_real_unspecified(ebits, sbits), result); + result = m.mk_ite(x_is_nan, mk_to_real_unspecified(ebits, sbits), result); SASSERT(is_well_sorted(m, result)); } @@ -2925,13 +2925,6 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con mk_ite(c1, v1, v2, result); } -expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned width) { - if (m_hi_fp_unspecified) - return expr_ref(m_bv_util.mk_numeral(0, width), m); - else - return expr_ref(m_util.mk_internal_to_ieee_bv_unspecified(width), m); -} - void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); expr_ref x(m), x_is_nan(m); @@ -2941,17 +2934,31 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * mk_is_nan(x, x_is_nan); sort * fp_srt = m.get_sort(x); + unsigned ebits = m_util.get_ebits(fp_srt); unsigned sbits = m_util.get_sbits(fp_srt); - expr_ref sig_unspec(s, m); - if (sbits > 2) - sig_unspec = m_bv_util.mk_concat( - mk_to_ieee_bv_unspecified(sbits - 2), - m_bv_util.mk_numeral(1, 1)); - else - sig_unspec = m_bv_util.mk_numeral(1, 1); + expr_ref nanv(m); + if (m_hi_fp_unspecified) + // The "hardware interpretation" is 01...10...01. + nanv = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), + m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), + m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2), + m_bv_util.mk_numeral(1, 1)))); + else { + app_ref unspec(m), mask(m); + unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); + m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), + m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), + m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits-2), + m_bv_util.mk_numeral(1, 1)))); + expr * args[2] = { unspec, mask }; + nanv = m_bv_util.mk_bv_or(2, args); + } - result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), m.mk_ite(x_is_nan, sig_unspec, s)); + result = m.mk_ite(x_is_nan, nanv, m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s)); + + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) { @@ -2987,7 +2994,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero))); else c1 = m.mk_or(x_is_nan, x_is_inf); - v1 = mk_to_ubv_unspecified(bv_sz); + v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz); dbg_decouple("fpa2bv_to_bv_c1", c1); // +-Zero -> 0 @@ -3086,8 +3093,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args dbg_decouple("fpa2bv_to_bv_rnd", rnd); - result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(bv_sz), rnd); - result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(bv_sz)); + result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(ebits, sbits, bv_sz), rnd); + result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(ebits, sbits, bv_sz)); result = m.mk_ite(c2, v2, result); result = m.mk_ite(c1, v1, result); @@ -3106,25 +3113,43 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg mk_to_bv(f, num, args, true, result); } -expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned width) { +expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { + expr_ref result(m); if (m_hi_fp_unspecified) - return expr_ref(m_bv_util.mk_numeral(0, width), m); - else - return expr_ref(m_util.mk_internal_to_ubv_unspecified(width), m); + result = m_bv_util.mk_numeral(0, width); + else { + app_ref unspec(m); + unspec = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); + m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + result = unspec; + } + return result; } -expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned width) { +expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { + expr_ref result(m); if (m_hi_fp_unspecified) - return expr_ref(m_bv_util.mk_numeral(0, width), m); - else - return expr_ref(m_util.mk_internal_to_sbv_unspecified(width), m); + result = m_bv_util.mk_numeral(0, width); + else { + app_ref unspec(m); + unspec = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); + m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + result = unspec; + } + return result; } -expr_ref fpa2bv_converter::mk_to_real_unspecified() { +expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) { + expr_ref result(m); if (m_hi_fp_unspecified) - return expr_ref(m_arith_util.mk_numeral(rational(0), false), m); - else - return expr_ref(m_util.mk_internal_to_real_unspecified(), m); + result = m_arith_util.mk_numeral(rational(0), false); + else { + app_ref unspec(m); + unspec = m_util.mk_internal_to_real_unspecified(ebits, sbits); + m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + result = unspec; + } + return result; } void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) { diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 7724d7673..2414b2110 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -41,6 +41,7 @@ protected: obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; + obj_hashtable m_unspecified_ufs; obj_map > m_specials; @@ -134,10 +135,9 @@ public: void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); - expr_ref mk_to_ubv_unspecified(unsigned width); - expr_ref mk_to_sbv_unspecified(unsigned width); - expr_ref mk_to_ieee_bv_unspecified(unsigned width); - expr_ref mk_to_real_unspecified(); + expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits); void reset(void); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 168d33829..511d36e67 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -728,12 +728,12 @@ func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( unsigned arity, sort * const * domain, sort * range) { if (arity != 0) m_manager->raise_exception("invalid number of arguments to fp.to_ubv_unspecified"); - if (num_parameters != 1) - m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 1"); - if (!parameters[0].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting an integer"); + if (num_parameters != 3) + m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 3"); + if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int()) + m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting 3 integers"); - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ¶meters[2]); return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } @@ -742,11 +742,12 @@ func_decl * fpa_decl_plugin::mk_internal_to_sbv_unspecified( unsigned arity, sort * const * domain, sort * range) { if (arity != 0) m_manager->raise_exception("invalid number of arguments to fp.to_sbv_unspecified"); - if (num_parameters != 1) - m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 1"); - if (!parameters[0].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting an integer"); - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); + if (num_parameters != 3) + m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 3"); + if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int()) + m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting 3 integers"); + + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ¶meters[2]); return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } @@ -755,6 +756,10 @@ func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified( unsigned arity, sort * const * domain, sort * range) { if (arity != 0) m_manager->raise_exception("invalid number of arguments to fp.to_real_unspecified"); + if (num_parameters != 2) + m_manager->raise_exception("invalid number of parameters to fp.to_real_unspecified; expecting 2"); + if (!parameters[0].is_int() || !parameters[1].is_int()) + m_manager->raise_exception("invalid parameters type provided to fp.to_real_unspecified; expecting 2 integers"); if (!is_sort_of(range, m_arith_fid, REAL_SORT)) m_manager->raise_exception("sort mismatch, expected range of Real sort"); @@ -765,16 +770,15 @@ func_decl * fpa_decl_plugin::mk_internal_to_ieee_bv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) - m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv_unspecified"); - if (num_parameters != 1) - m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 1"); - if (!parameters[0].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting an integer"); - if (!is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); + m_manager->raise_exception("invalid number of arguments to to_ieee_bv_unspecified; expecting none"); + if (num_parameters != 2) + m_manager->raise_exception("invalid number of parameters to to_ieee_bv_unspecified; expecting 2"); + if (!parameters[0].is_int() || !parameters[1].is_int()) + m_manager->raise_exception("invalid parameters type provided to to_ieee_bv_unspecified; expecting 2 integers"); - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); - return m_manager->mk_func_decl(symbol("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); + parameter width_p[1] = { parameter(parameters[0].get_int() + parameters[1].get_int()) }; + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, width_p); + return m_manager->mk_func_decl(symbol("to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } @@ -1063,25 +1067,26 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) { - parameter ps[] = { parameter(width) }; +app * fpa_util::mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { + parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) }; sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 3, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) { - parameter ps[] = { parameter(width) }; +app * fpa_util::mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { + parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) }; sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 3, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned width) { - parameter ps[] = { parameter(width) }; - sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 1, ps, 0, 0, range); +app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) { + parameter ps[] = { parameter(ebits), parameter(sbits) }; + sort * range = m_bv_util.mk_sort(ebits+sbits); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 2, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_real_unspecified() { +app * fpa_util::mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits) { + parameter ps[] = { parameter(ebits), parameter(sbits) }; sort * range = m_a_util.mk_real(); - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range); } diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 51f6ecf75..84eb5168b 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -346,10 +346,10 @@ public: app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); } - app * mk_internal_to_ubv_unspecified(unsigned width); - app * mk_internal_to_sbv_unspecified(unsigned width); - app * mk_internal_to_ieee_bv_unspecified(unsigned width); - app * mk_internal_to_real_unspecified(); + app * mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + app * mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); + app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits); bool is_wrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); } bool is_unwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVUNWRAP); } diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 5d9175259..b5d8f6754 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -106,7 +106,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break; + SASSERT(num_args == 0); st = mk_to_real_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_ieee_bv_unspecified(f, result); break; @@ -122,61 +122,55 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con } br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_num_parameters() == 3); SASSERT(f->get_parameter(0).is_int()); - unsigned bv_sz = f->get_parameter(0).get_int(); + SASSERT(f->get_parameter(1).is_int()); + SASSERT(f->get_parameter(2).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + unsigned width = f->get_parameter(2).get_int(); bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, bv_sz); + result = bu.mk_numeral(0, ebits+sbits); else - result = m_util.mk_internal_to_ubv_unspecified(bv_sz); + result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); return BR_DONE; } br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_num_parameters() == 3); SASSERT(f->get_parameter(0).is_int()); - unsigned bv_sz = f->get_parameter(0).get_int(); + SASSERT(f->get_parameter(1).is_int()); + SASSERT(f->get_parameter(2).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + unsigned width = f->get_parameter(2).get_int(); bv_util bu(m()); if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, bv_sz); + result = bu.mk_numeral(0, ebits+sbits); else - result = m_util.mk_internal_to_sbv_unspecified(bv_sz); + result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); return BR_DONE; } -br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) { - bv_util bu(m()); - unsigned bv_sz = bu.get_bv_size(f->get_range()); +br_status fpa_rewriter::mk_to_real_unspecified(func_decl * f, expr_ref & result) { + SASSERT(f->get_num_parameters() == 2); + SASSERT(f->get_parameter(0).is_int()); + SASSERT(f->get_parameter(1).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); - if (m_hi_fp_unspecified) - // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, bv_sz); - else { - unsigned sbits = m_util.get_sbits(f->get_domain()[0]); - - if (sbits > 2) - result = bu.mk_concat(m_util.mk_internal_to_ieee_bv_unspecified(sbits - 2), - bu.mk_numeral(1, 1)); - else - result = bu.mk_numeral(1, 1); - } - - return BR_DONE; -} - -br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) { if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. result = m_util.au().mk_numeral(rational(0), false); else - result = m_util.mk_internal_to_real_unspecified(); + result = m_util.mk_internal_to_real_unspecified(ebits, sbits); return BR_DONE; } @@ -865,20 +859,43 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ return BR_FAILED; } +br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) { + SASSERT(f->get_num_parameters() == 2); + SASSERT(f->get_parameter(0).is_int()); + SASSERT(f->get_parameter(1).is_int()); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + + bv_util bu(m()); + + if (m_hi_fp_unspecified) + // The "hardware interpretation" is 01...10...01. + result = bu.mk_concat(bu.mk_numeral(0, 1), + bu.mk_concat(bu.mk_numeral(-1, ebits), + bu.mk_concat(bu.mk_numeral(0, sbits - 2), + bu.mk_numeral(1, 1)))); + else + result = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); + + return BR_DONE; +} + br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) { scoped_mpf v(m_fm); if (m_util.is_numeral(arg, v)) { + bv_util bu(m()); + const mpf & x = v.get(); if (m_fm.is_nan(v)) { - mk_to_ieee_bv_unspecified(f, result); - return BR_REWRITE_FULL; + result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + return BR_REWRITE1; } else { - bv_util bu(m()); scoped_mpz rz(m_fm.mpq_manager()); m_fm.to_ieee_bv_mpz(v, rz); - result = bu.mk_numeral(rational(rz), v.get().get_ebits() + v.get().get_sbits()); + + result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits()); return BR_DONE; } } @@ -891,7 +908,8 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { if (m_util.is_numeral(arg, v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v)) { - result = m_util.mk_internal_to_real_unspecified(); + const mpf & x = v.get(); + result = m_util.mk_internal_to_real_unspecified(x.get_ebits(), x.get_sbits()); } else { scoped_mpq r(m_fm.mpq_manager()); diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 0889bba72..b71b12120 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -89,7 +89,7 @@ public: br_status mk_to_ubv_unspecified(func_decl * f, expr_ref & result); br_status mk_to_sbv_unspecified(func_decl * f, expr_ref & result); br_status mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result); - br_status mk_to_real_unspecified(expr_ref & result); + br_status mk_to_real_unspecified(func_decl * f, expr_ref & result); }; #endif diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index a41b92b2d..61f6c8549 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -54,6 +54,14 @@ void fpa2bv_model_converter::display(std::ostream & out) { out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << mk_ismt2_pp(it->m_value.second, m, indent) << ")"; } + for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); + it != m_unspecified_ufs.end(); + it++) + { + const symbol & n = (*it)->get_name(); + unsigned indent = n.size() + 4; + out << n << " "; + } out << ")" << std::endl; } @@ -99,6 +107,14 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator translator.to().inc_ref(v1); translator.to().inc_ref(v2); } + for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); + it != m_unspecified_ufs.end(); + it++) + { + func_decl * k = translator(*it); + res->m_unspecified_ufs.insert(k); + translator.to().inc_ref(k); + } return res; } @@ -367,6 +383,22 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { float_mdl->register_decl(f, flt_fi); } + // fp.to_*_unspecified UFs. + for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); + it != m_unspecified_ufs.end(); + it++) + { + func_decl * f = *it; + + if (bv_mdl->has_interpretation(f)) { + func_interp * val = bv_mdl->get_func_interp(f)->copy(); + TRACE("fpa2bv_mc", tout << "Keeping interpretation for " << mk_ismt2_pp(f, m) << std::endl;); + float_mdl->register_decl(f, val); + } + else + TRACE("fpa2bv_mc", tout << "No interpretation for " << mk_ismt2_pp(f, m) << std::endl;); + } + // Keep all the non-float constants. unsigned sz = bv_mdl->get_num_constants(); for (unsigned i = 0; i < sz; i++) diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 854543f24..589d3c201 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -28,6 +28,7 @@ class fpa2bv_model_converter : public model_converter { obj_map m_rm_const2bv; obj_map m_uf2bvuf; obj_map > m_specials; + obj_hashtable m_unspecified_ufs; public: fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) { @@ -63,6 +64,13 @@ public: m.inc_ref(it->m_value.first); m.inc_ref(it->m_value.second); } + for (obj_hashtable::iterator it = conv.m_unspecified_ufs.begin(); + it != conv.m_unspecified_ufs.end(); + it++) + { + m_unspecified_ufs.insert(*it); + m.inc_ref(*it); + } } virtual ~fpa2bv_model_converter() { @@ -76,6 +84,7 @@ public: m.dec_ref(it->m_value.first); m.dec_ref(it->m_value.second); } + dec_ref_collection_values(m, m_unspecified_ufs); } virtual void operator()(model_ref & md, unsigned goal_idx) {