From 4ceef091563ef0c5f760ee989d3a9c5cb34cd041 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 11 Sep 2017 15:03:02 +0100 Subject: [PATCH 01/15] Renamed FPA-internal functions now that they are exposed. --- src/api/api_ast.cpp | 20 +++---- src/ast/fpa/fpa2bv_converter.cpp | 16 +++--- src/ast/fpa/fpa2bv_rewriter.cpp | 20 +++---- src/ast/fpa_decl_plugin.cpp | 70 ++++++++++++------------ src/ast/fpa_decl_plugin.h | 91 +++++++++++++++---------------- src/ast/rewriter/fpa_rewriter.cpp | 46 ++++++++-------- src/smt/theory_fpa.cpp | 4 +- src/smt/theory_fpa.h | 5 +- 8 files changed, 135 insertions(+), 137 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 561bfa87b..cfea4098f 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1204,16 +1204,16 @@ extern "C" { case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV; case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL; case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV; - case OP_FPA_INTERNAL_MIN_I: return Z3_OP_FPA_MIN_I; - case OP_FPA_INTERNAL_MAX_I: return Z3_OP_FPA_MAX_I; - case OP_FPA_INTERNAL_BVWRAP: return Z3_OP_FPA_BVWRAP; - case OP_FPA_INTERNAL_BV2RM: return Z3_OP_FPA_BV2RM; - case OP_FPA_INTERNAL_MIN_UNSPECIFIED: return Z3_OP_FPA_MIN_UNSPECIFIED; - case OP_FPA_INTERNAL_MAX_UNSPECIFIED: return Z3_OP_FPA_MAX_UNSPECIFIED; - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: return Z3_OP_FPA_TO_UBV_UNSPECIFIED; - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return Z3_OP_FPA_TO_SBV_UNSPECIFIED; - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: return Z3_OP_FPA_TO_REAL_UNSPECIFIED; - case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED; + case OP_FPA_MIN_I: return Z3_OP_FPA_MIN_I; + case OP_FPA_MAX_I: return Z3_OP_FPA_MAX_I; + case OP_FPA_BVWRAP: return Z3_OP_FPA_BVWRAP; + case OP_FPA_BV2RM: return Z3_OP_FPA_BV2RM; + case OP_FPA_MIN_UNSPECIFIED: return Z3_OP_FPA_MIN_UNSPECIFIED; + case OP_FPA_MAX_UNSPECIFIED: return Z3_OP_FPA_MAX_UNSPECIFIED; + case OP_FPA_TO_UBV_UNSPECIFIED: return Z3_OP_FPA_TO_UBV_UNSPECIFIED; + case OP_FPA_TO_SBV_UNSPECIFIED: return Z3_OP_FPA_TO_SBV_UNSPECIFIED; + case OP_FPA_TO_REAL_UNSPECIFIED: return Z3_OP_FPA_TO_REAL_UNSPECIFIED; + case OP_FPA_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED; return Z3_OP_UNINTERPRETED; default: return Z3_OP_INTERNAL; diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 1a4698fa4..6f0c83df9 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1231,11 +1231,11 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref c(m), v(m); c = m.mk_and(both_are_zero, pn_or_np); - v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, x, y); + v = m.mk_app(m_util.get_family_id(), OP_FPA_MIN_UNSPECIFIED, x, y); // Note: This requires BR_REWRITE_FULL afterwards. expr_ref min_i(m); - min_i = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_I, x, y); + min_i = m.mk_app(m_util.get_family_id(), OP_FPA_MIN_I, x, y); m_simp.mk_ite(c, v, min_i, result); } @@ -1324,11 +1324,11 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref c(m), v(m); c = m.mk_and(both_are_zero, pn_or_np); - v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, x, y); + v = m.mk_app(m_util.get_family_id(), OP_FPA_MAX_UNSPECIFIED, x, y); // Note: This requires BR_REWRITE_FULL afterwards. expr_ref max_i(m); - max_i = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_I, x, y); + max_i = m.mk_app(m_util.get_family_id(), OP_FPA_MAX_I, x, y); m_simp.mk_ite(c, v, max_i, result); } @@ -3160,7 +3160,7 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * m_bv_util.mk_numeral(1, 1)))); else { app_ref unspec(m); - unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); + unspec = m_util.mk_to_ieee_bv_unspecified(ebits, sbits); mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv); } @@ -3402,7 +3402,7 @@ void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { expr_ref res(m); app_ref u(m); - u = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); + u = m_util.mk_to_ubv_unspecified(ebits, sbits, width); mk_to_sbv_unspecified(u->get_decl(), 0, 0, res); return res; } @@ -3431,7 +3431,7 @@ void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { expr_ref res(m); app_ref u(m); - u = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); + u = m_util.mk_to_sbv_unspecified(ebits, sbits, width); mk_to_sbv_unspecified(u->get_decl(), 0, 0, res); return res; } @@ -3454,7 +3454,7 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) { expr_ref res(m); app_ref u(m); - u = m_util.mk_internal_to_real_unspecified(ebits, sbits); + u = m_util.mk_to_real_unspecified(ebits, sbits); mk_to_real_unspecified(u->get_decl(), 0, 0, res); return res; } diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 0e3899c53..28ec35536 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -143,24 +143,24 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE; + case OP_FPA_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE; + case OP_FPA_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE; + case OP_FPA_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE; + case OP_FPA_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; - case OP_FPA_INTERNAL_MIN_UNSPECIFIED: - case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_min_max_unspecified(f, args[0], args[1]); return BR_DONE; - case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; + case OP_FPA_MIN_UNSPECIFIED: + case OP_FPA_MAX_UNSPECIFIED: result = m_conv.mk_min_max_unspecified(f, args[0], args[1]); return BR_DONE; + case OP_FPA_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; + case OP_FPA_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_BV2RM: + case OP_FPA_BVWRAP: + case OP_FPA_BV2RM: return BR_FAILED; default: diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index fc69c5f89..c50d6b985 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -361,10 +361,10 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters case OP_FPA_REM: name = "fp.rem"; break; case OP_FPA_MIN: name = "fp.min"; break; case OP_FPA_MAX: name = "fp.max"; break; - case OP_FPA_INTERNAL_MIN_I: name = "fp.min_i"; break; - case OP_FPA_INTERNAL_MAX_I: name = "fp.max_i"; break; - case OP_FPA_INTERNAL_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break; - case OP_FPA_INTERNAL_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break; + case OP_FPA_MIN_I: name = "fp.min_i"; break; + case OP_FPA_MAX_I: name = "fp.max_i"; break; + case OP_FPA_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break; + case OP_FPA_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break; default: UNREACHABLE(); break; @@ -676,10 +676,10 @@ func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k)); } -func_decl * fpa_decl_plugin::mk_internal_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 1) - m_manager->raise_exception("invalid number of arguments to internal_rm"); + m_manager->raise_exception("invalid number of arguments to bv2rm"); if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || domain[0]->get_parameter(0).get_int() != 3) m_manager->raise_exception("sort mismatch, expected argument of sort bitvector, size 3"); if (!is_rm_sort(range)) @@ -690,7 +690,7 @@ func_decl * fpa_decl_plugin::mk_internal_bv2rm(decl_kind k, unsigned num_paramet return m_manager->mk_func_decl(symbol("rm"), 1, &bv_srt, range, func_decl_info(m_family_id, k, num_parameters, parameters)); } -func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * fpa_decl_plugin::mk_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 1) m_manager->raise_exception("invalid number of arguments to bv_wrap"); @@ -711,7 +711,7 @@ func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_param } } -func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( +func_decl * fpa_decl_plugin::mk_to_ubv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) @@ -725,7 +725,7 @@ func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( 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)); } -func_decl * fpa_decl_plugin::mk_internal_to_sbv_unspecified( +func_decl * fpa_decl_plugin::mk_to_sbv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) @@ -739,7 +739,7 @@ func_decl * fpa_decl_plugin::mk_internal_to_sbv_unspecified( 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)); } -func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified( +func_decl * fpa_decl_plugin::mk_to_real_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) @@ -754,7 +754,7 @@ func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified( return m_manager->mk_func_decl(symbol("fp.to_real_unspecified"), 0, domain, m_real_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); } -func_decl * fpa_decl_plugin::mk_internal_to_ieee_bv_unspecified( +func_decl * fpa_decl_plugin::mk_to_ieee_bv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 0) @@ -835,25 +835,25 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_FPA_TO_IEEE_BV: return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_INTERNAL_BVWRAP: - return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_INTERNAL_BV2RM: - return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_BVWRAP: + return mk_bv_wrap(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_BV2RM: + return mk_bv2rm(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_INTERNAL_MIN_I: - case OP_FPA_INTERNAL_MAX_I: - case OP_FPA_INTERNAL_MIN_UNSPECIFIED: - case OP_FPA_INTERNAL_MAX_UNSPECIFIED: + case OP_FPA_MIN_I: + case OP_FPA_MAX_I: + case OP_FPA_MIN_UNSPECIFIED: + case OP_FPA_MAX_UNSPECIFIED: return mk_binary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: - return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: - return mk_internal_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - return mk_internal_to_real_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: - return mk_internal_to_ieee_bv_unspecified(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_TO_UBV_UNSPECIFIED: + return mk_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_TO_SBV_UNSPECIFIED: + return mk_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_TO_REAL_UNSPECIFIED: + return mk_to_real_unspecified(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_TO_IEEE_BV_UNSPECIFIED: + return mk_to_ieee_bv_unspecified(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -1054,28 +1054,28 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * fpa_util::mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { +app * fpa_util::mk_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, 3, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_TO_UBV_UNSPECIFIED, 3, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { +app * fpa_util::mk_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, 3, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_TO_SBV_UNSPECIFIED, 3, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) { +app * fpa_util::mk_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); + return m().mk_app(get_family_id(), OP_FPA_TO_IEEE_BV_UNSPECIFIED, 2, ps, 0, 0, range); } -app * fpa_util::mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits) { +app * fpa_util::mk_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, 2, ps, 0, 0, range); + return m().mk_app(get_family_id(), OP_FPA_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range); } bool fpa_util::contains_floats(ast * a) { diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 5d76345f6..c78194b63 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -86,18 +86,17 @@ enum fpa_op_kind { /* Extensions */ OP_FPA_TO_IEEE_BV, - /* Internal use only */ - OP_FPA_INTERNAL_BVWRAP, - OP_FPA_INTERNAL_BV2RM, + OP_FPA_BVWRAP, + OP_FPA_BV2RM, - OP_FPA_INTERNAL_MIN_I, - OP_FPA_INTERNAL_MAX_I, - OP_FPA_INTERNAL_MIN_UNSPECIFIED, - OP_FPA_INTERNAL_MAX_UNSPECIFIED, - OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, - OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, - OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, - OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, + OP_FPA_MIN_I, + OP_FPA_MAX_I, + OP_FPA_MIN_UNSPECIFIED, + OP_FPA_MAX_UNSPECIFIED, + OP_FPA_TO_UBV_UNSPECIFIED, + OP_FPA_TO_SBV_UNSPECIFIED, + OP_FPA_TO_IEEE_BV_UNSPECIFIED, + OP_FPA_TO_REAL_UNSPECIFIED, LAST_FLOAT_OP }; @@ -164,17 +163,17 @@ class fpa_decl_plugin : public decl_plugin { func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters, + func_decl * mk_bv2rm(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, + func_decl * mk_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, + func_decl * mk_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, + func_decl * mk_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, + func_decl * mk_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_to_ieee_bv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, + func_decl * mk_to_ieee_bv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); virtual void set_manager(ast_manager * m, family_id id); @@ -186,10 +185,10 @@ class fpa_decl_plugin : public decl_plugin { return false; switch (f->get_decl_kind()) { - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: + case OP_FPA_TO_UBV_UNSPECIFIED: + case OP_FPA_TO_SBV_UNSPECIFIED: + case OP_FPA_TO_REAL_UNSPECIFIED: + case OP_FPA_TO_IEEE_BV_UNSPECIFIED: return true; default: return false; @@ -373,35 +372,35 @@ public: app * mk_bv2rm(expr * bv3) { SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); - return m().mk_app(m_fid, OP_FPA_INTERNAL_BV2RM, 0, 0, 1, &bv3, mk_rm_sort()); + return m().mk_app(m_fid, OP_FPA_BV2RM, 0, 0, 1, &bv3, mk_rm_sort()); } - 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); + app * mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + app * mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); + app * mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); + app * mk_to_real_unspecified(unsigned ebits, unsigned sbits); - bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); } - bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; } - bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); } - bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; } + bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BVWRAP); } + bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; } + bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BV2RM); } + bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BV2RM; } - bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); } - bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); } - bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); } - bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); } - bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); } - bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); } - bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); } - bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); } + bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_I); } + bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_UNSPECIFIED); } + bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_I); } + bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_UNSPECIFIED); } + bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV_UNSPECIFIED); } + bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV_UNSPECIFIED); } + bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_IEEE_BV_UNSPECIFIED); } + bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_REAL_UNSPECIFIED); } - bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; } - bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; } - bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; } - bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; } - bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; } - bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; } - bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; } - bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; } + bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_I; } + bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_UNSPECIFIED; } + bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_I; } + bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_UNSPECIFIED; } + bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV_UNSPECIFIED; } + bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV_UNSPECIFIED; } + bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_IEEE_BV_UNSPECIFIED; } + bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_REAL_UNSPECIFIED; } bool contains_floats(ast * a); }; diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 41435818b..b31270ce8 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -94,19 +94,19 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break; case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; - case OP_FPA_INTERNAL_MIN_I:SASSERT(num_args == 2); st = mk_min_i(f, args[0], args[1], result); break; - case OP_FPA_INTERNAL_MAX_I: SASSERT(num_args == 2); st = mk_max_i(f, args[0], args[1], result); break; - case OP_FPA_INTERNAL_MIN_UNSPECIFIED: - case OP_FPA_INTERNAL_MAX_UNSPECIFIED: + case OP_FPA_MIN_I:SASSERT(num_args == 2); st = mk_min_i(f, args[0], args[1], result); break; + case OP_FPA_MAX_I: SASSERT(num_args == 2); st = mk_max_i(f, args[0], args[1], result); break; + case OP_FPA_MIN_UNSPECIFIED: + case OP_FPA_MAX_UNSPECIFIED: SASSERT(num_args == 2); st = BR_FAILED; break; - case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break; - case OP_FPA_INTERNAL_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break; + case OP_FPA_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break; + case OP_FPA_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break; - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: + case OP_FPA_TO_UBV_UNSPECIFIED: + case OP_FPA_TO_SBV_UNSPECIFIED: + case OP_FPA_TO_REAL_UNSPECIFIED: + case OP_FPA_TO_IEEE_BV_UNSPECIFIED: st = BR_FAILED; break; @@ -124,7 +124,7 @@ br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, un return BR_DONE; } else { - result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); + result = m_util.mk_to_ubv_unspecified(ebits, sbits, width); return BR_REWRITE1; } } @@ -137,7 +137,7 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, un return BR_DONE; } else { - result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); + result = m_util.mk_to_sbv_unspecified(ebits, sbits, width); return BR_REWRITE1; } } @@ -149,7 +149,7 @@ br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, e return BR_DONE; } else { - result = m_util.mk_internal_to_real_unspecified(ebits, sbits); + result = m_util.mk_to_real_unspecified(ebits, sbits); return BR_REWRITE1; } } @@ -432,7 +432,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { - result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); + result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); return BR_REWRITE1; } else { @@ -447,9 +447,9 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)), m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2)))); - v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); + v = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); - result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_I, arg1, arg2)); + result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_MIN_I, arg1, arg2)); return BR_REWRITE_FULL; } } @@ -458,7 +458,7 @@ br_status fpa_rewriter::mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_r scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) - result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); + result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); else result = m_util.mk_min(arg1, arg2); return BR_DONE; @@ -479,7 +479,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { - result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2); + result = m().mk_app(get_fid(), OP_FPA_MAX_UNSPECIFIED, arg1, arg2); return BR_REWRITE1; } else { @@ -494,9 +494,9 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)), m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2)))); - v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2); + v = m().mk_app(get_fid(), OP_FPA_MAX_UNSPECIFIED, arg1, arg2); - result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_I, arg1, arg2)); + result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_MAX_I, arg1, arg2)); return BR_REWRITE_FULL; } } @@ -505,7 +505,7 @@ br_status fpa_rewriter::mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_r scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) - result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); + result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); else result = m_util.mk_max(arg1, arg2); return BR_DONE; @@ -881,7 +881,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu result = bu.mk_concat(4, args); } else - result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + result = m_util.mk_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); return BR_REWRITE1; } @@ -902,7 +902,7 @@ 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)) { const mpf & x = v.get(); - result = m_util.mk_internal_to_real_unspecified(x.get_ebits(), x.get_sbits()); + result = m_util.mk_to_real_unspecified(x.get_ebits(), x.get_sbits()); } else { scoped_mpq r(m_fm.mpq_manager()); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index dfd295220..12c5fb0b1 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -237,7 +237,7 @@ namespace smt { if (m_fpa_util.is_fp(e)) { expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) }; - expr_ref tmp(m_bv_util.mk_concat(3, cargs), m); + expr_ref tmp(m_bv_util.mk_concat(3, cargs), m); m_th_rw(tmp); res = to_app(tmp); } @@ -255,7 +255,7 @@ namespace smt { } func_decl_ref wrap_fd(m); - wrap_fd = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &es, bv_srt); + wrap_fd = m.mk_func_decl(get_family_id(), OP_FPA_BVWRAP, 0, 0, 1, &es, bv_srt); res = m.mk_app(wrap_fd, e); } diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 5fcb8637c..7be82816e 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -82,7 +82,7 @@ namespace smt { m_th(*th) {} virtual ~fpa2bv_converter_wrapped() {} virtual void mk_const(func_decl * f, expr_ref & result); - virtual void mk_rm_const(func_decl * f, expr_ref & result); + virtual void mk_rm_const(func_decl * f, expr_ref & result); }; class fpa_value_proc : public model_value_proc { @@ -108,7 +108,7 @@ namespace smt { result.append(m_deps); } - virtual app * mk_value(model_generator & mg, ptr_vector & values); + virtual app * mk_value(model_generator & mg, ptr_vector & values); }; class fpa_rm_value_proc : public model_value_proc { @@ -179,7 +179,6 @@ namespace smt { expr_ref convert_atom(expr * e); expr_ref convert_term(expr * e); expr_ref convert_conversion_term(expr * e); - expr_ref convert_unwrap(expr * e); void add_trail(ast * a); From 31cfca0444d2df3f231e0a8b92e80a8fa531f7c1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 12 Sep 2017 19:43:45 +0100 Subject: [PATCH 02/15] Eliminated unspecified operators for fp.to_*bv, fp.to_real. Also fixes #1191. --- src/api/api_ast.cpp | 4 - src/api/z3_api.h | 16 --- src/ast/fpa/bv2fpa_converter.cpp | 26 ++++- src/ast/fpa/fpa2bv_converter.cpp | 183 +++++++++++++----------------- src/ast/fpa/fpa2bv_converter.h | 8 +- src/ast/fpa/fpa2bv_rewriter.cpp | 4 - src/ast/fpa_decl_plugin.cpp | 91 --------------- src/ast/fpa_decl_plugin.h | 44 +------ src/ast/rewriter/fpa_rewriter.cpp | 64 +---------- src/ast/rewriter/fpa_rewriter.h | 4 +- src/smt/theory_fpa.cpp | 11 +- 11 files changed, 118 insertions(+), 337 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index cfea4098f..491e08cf4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1210,10 +1210,6 @@ extern "C" { case OP_FPA_BV2RM: return Z3_OP_FPA_BV2RM; case OP_FPA_MIN_UNSPECIFIED: return Z3_OP_FPA_MIN_UNSPECIFIED; case OP_FPA_MAX_UNSPECIFIED: return Z3_OP_FPA_MAX_UNSPECIFIED; - case OP_FPA_TO_UBV_UNSPECIFIED: return Z3_OP_FPA_TO_UBV_UNSPECIFIED; - case OP_FPA_TO_SBV_UNSPECIFIED: return Z3_OP_FPA_TO_SBV_UNSPECIFIED; - case OP_FPA_TO_REAL_UNSPECIFIED: return Z3_OP_FPA_TO_REAL_UNSPECIFIED; - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED; return Z3_OP_UNINTERPRETED; default: return Z3_OP_INTERNAL; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 663a59fd9..bfc0b93a2 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1005,18 +1005,6 @@ typedef enum - Z3_OP_FPA_MAX_UNSPECIFIED: The same as Z3_OP_FPA_MAX, but the arguments are expected to be zeroes with different signs. - - Z3_OP_FPA_TO_UBV_UNSPECIFIED: A term representing the unspecified - results of Z3_OP_FPA_TO_UBV. - - - Z3_OP_FPA_TO_SBV_UNSPECIFIED: A term representing the unspecified - results of Z3_OP_FPA_TO_SBV. - - - Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED: A term representing the unspecified - results of Z3_OP_FPA_TO_IEEE_BV. - - - Z3_OP_FPA_TO_REAL_UNSPECIFIED: A term representing the unspecified - results of Z3_OP_FPA_TO_IEEE_BV. - - Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information. @@ -1310,10 +1298,6 @@ typedef enum { Z3_OP_FPA_BV2RM, Z3_OP_FPA_MIN_UNSPECIFIED, Z3_OP_FPA_MAX_UNSPECIFIED, - Z3_OP_FPA_TO_UBV_UNSPECIFIED, - Z3_OP_FPA_TO_SBV_UNSPECIFIED, - Z3_OP_FPA_TO_REAL_UNSPECIFIED, - Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED, Z3_OP_INTERNAL, diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 7e4f2f133..59f24779e 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -291,9 +291,11 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * app_ref bv_els(m); expr_ref ft_els(m); bv_els = (app*)bv_fi->get_else(); - ft_els = rebuild_floats(mc, rng, bv_els); - m_th_rw(ft_els); - result->set_else(ft_els); + if (bv_els != 0) { + ft_els = rebuild_floats(mc, rng, bv_els); + m_th_rw(ft_els); + result->set_else(ft_els); + } } return result; @@ -447,8 +449,22 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode } } else { - func_interp * fmv = convert_func_interp(mc, f, it->m_value); - if (fmv) target_model->register_decl(f, fmv); + if (it->get_key().get_family_id() == m_fpa_util.get_fid()) { + // it->m_value contains the model for the unspecified cases of it->m_key. + continue; + + // Upon request, add this 'recursive' definition? + func_interp * fmv = convert_func_interp(mc, f, it->m_value); + unsigned n = fmv->get_arity(); + expr_ref_vector args(m); + for (unsigned i = 0; i < n; i++) + args.push_back(m.mk_var(i, f->get_domain()[i])); + fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr())); + } + else { + func_interp * fmv = convert_func_interp(mc, f, it->m_value); + if (fmv) target_model->register_decl(f, fmv); + } } } } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6f0c83df9..da4052108 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2855,8 +2855,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); expr_ref unspec(m); - unspec = mk_to_real_unspecified(ebits, sbits); - + mk_to_real_unspecified(f, num, args, unspec); result = m.mk_ite(x_is_zero, zero, res); result = m.mk_ite(x_is_inf, unspec, result); result = m.mk_ite(x_is_nan, unspec, result); @@ -3141,11 +3140,12 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con 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); + expr_ref x(m), x_is_nan(m), x_flat(m); expr * sgn, * s, * e; x = args[0]; split_fp(x, sgn, e, s); mk_is_nan(x, x_is_nan); + join_fp(x, x_flat); sort * fp_srt = m.get_sort(x); unsigned ebits = m_util.get_ebits(fp_srt); @@ -3159,13 +3159,12 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * 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); - unspec = m_util.mk_to_ieee_bv_unspecified(ebits, sbits); - mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv); + expr * x_flatp = x_flat.get(); + mk_to_ieee_bv_unspecified(f, 1, &x_flatp, nanv); } expr_ref sgn_e_s(m); - sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); + join_fp(x, sgn_e_s); m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result); TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); @@ -3173,7 +3172,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * } void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - SASSERT(num == 0); + SASSERT(num == 1); + SASSERT(m_util.is_float(args[0])); unsigned ebits = f->get_parameter(0).get_int(); unsigned sbits = f->get_parameter(1).get_int(); @@ -3184,26 +3184,30 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex m_bv_util.mk_numeral(1, sbits-1)); } else { - func_decl * fd; - if (m_uf2bvuf.find(f, fd)) - result = m.mk_const(fd); - else { - fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range()); - m_uf2bvuf.insert(f, fd); + expr * n = args[0]; + expr_ref n_bv(m); + join_fp(n, n_bv); + + func_decl * f_bv; + if (!m_uf2bvuf.find(f, f_bv)) { + sort * domain[2] = { m.get_sort(n_bv) }; + f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range()); + m_uf2bvuf.insert(f, f_bv); m.inc_ref(f); - m.inc_ref(fd); - result = m.mk_const(fd); - - expr_ref exp_bv(m), exp_all_ones(m); - exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); - exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits)); - m_extra_assertions.push_back(exp_all_ones); - - expr_ref sig_bv(m), sig_is_non_zero(m); - sig_bv = m_bv_util.mk_extract(sbits-2, 0, result); - sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1))); - m_extra_assertions.push_back(sig_is_non_zero); + m.inc_ref(f_bv); } + + result = m.mk_app(f_bv, n_bv); + + expr_ref exp_bv(m), exp_all_ones(m); + exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); + exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits)); + m_extra_assertions.push_back(exp_all_ones); + + expr_ref sig_bv(m), sig_is_non_zero(m); + sig_bv = m_bv_util.mk_extract(sbits-2, 0, result); + sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1))); + m_extra_assertions.push_back(sig_is_non_zero); } TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); @@ -3238,15 +3242,13 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args mk_is_nzero(x, x_is_nzero); // NaN, Inf, or negative (except -0) -> unspecified - expr_ref c1(m), v1(m); - if (!is_signed) { + expr_ref c1(m), v1(m), unspec_v(m); + if (!is_signed) c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero))); - v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz); - } - else { + else c1 = m.mk_or(x_is_nan, x_is_inf); - v1 = mk_to_sbv_unspecified(ebits, sbits, bv_sz); - } + mk_to_bv_unspecified(f, num, args, unspec_v); + v1 = unspec_v; dbg_decouple("fpa2bv_to_bv_c1", c1); // +-Zero -> 0 @@ -3355,11 +3357,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args dbg_decouple("fpa2bv_to_bv_rnd", rnd); - expr_ref unspec(m); - unspec = is_signed ? mk_to_sbv_unspecified(ebits, sbits, bv_sz) : - mk_to_ubv_unspecified(ebits, sbits, bv_sz); - result = m.mk_ite(rnd_has_overflown, unspec, rnd); - result = m.mk_ite(c_in_limits, result, unspec); + result = m.mk_ite(rnd_has_overflown, unspec_v, rnd); + result = m.mk_ite(c_in_limits, result, unspec_v); result = m.mk_ite(c2, v2, result); result = m.mk_ite(c1, v1, result); @@ -3378,85 +3377,54 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg mk_to_bv(f, num, args, true, result); } -void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - SASSERT(num == 0); - unsigned width = m_bv_util.get_bv_size(f->get_range()); +void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(m_util.is_bv2rm(args[0])); + SASSERT(m_util.is_float(args[1])); if (m_hi_fp_unspecified) - result = m_bv_util.mk_numeral(0, width); + result = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(f->get_range())); else { - func_decl * fd; - if (!m_uf2bvuf.find(f, fd)) { - fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range()); - m_uf2bvuf.insert(f, fd); + expr * rm_bv = to_app(args[0])->get_arg(0); + expr * n = args[1]; + expr_ref n_bv(m); + join_fp(n, n_bv); + + func_decl * f_bv; + if (!m_uf2bvuf.find(f, f_bv)) { + sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) }; + f_bv = m.mk_fresh_func_decl(0, 2, domain, f->get_range()); + m_uf2bvuf.insert(f, f_bv); m.inc_ref(f); - m.inc_ref(fd); + m.inc_ref(f_bv); } - result = m.mk_const(fd); + result = m.mk_app(f_bv, rm_bv, n_bv); } - TRACE("fpa2bv_to_ubv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); + TRACE("fpa2bv_to_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); SASSERT(is_well_sorted(m, result)); } -expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { - expr_ref res(m); - app_ref u(m); - u = m_util.mk_to_ubv_unspecified(ebits, sbits, width); - mk_to_sbv_unspecified(u->get_decl(), 0, 0, res); - return res; -} - -void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - SASSERT(num == 0); - unsigned width = m_bv_util.get_bv_size(f->get_range()); - - if (m_hi_fp_unspecified) - result = m_bv_util.mk_numeral(0, width); - else { - func_decl * fd; - if (!m_uf2bvuf.find(f, fd)) { - fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range()); - m_uf2bvuf.insert(f, fd); - m.inc_ref(f); - m.inc_ref(fd); - } - result = m.mk_const(fd); - } - - TRACE("fpa2bv_to_sbv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); - SASSERT(is_well_sorted(m, result)); -} - -expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { - expr_ref res(m); - app_ref u(m); - u = m_util.mk_to_sbv_unspecified(ebits, sbits, width); - mk_to_sbv_unspecified(u->get_decl(), 0, 0, res); - return res; -} - void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + if (m_hi_fp_unspecified) result = m_arith_util.mk_numeral(rational(0), false); else { - func_decl * fd; - if (!m_uf2bvuf.find(f, fd)) { - fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range()); - m_uf2bvuf.insert(f, fd); - m.inc_ref(f); - m.inc_ref(fd); - } - result = m.mk_const(fd); - } -} + expr * n = args[0]; + expr_ref n_bv(m); + join_fp(n, n_bv); -expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) { - expr_ref res(m); - app_ref u(m); - u = m_util.mk_to_real_unspecified(ebits, sbits); - mk_to_real_unspecified(u->get_decl(), 0, 0, res); - return res; + func_decl * f_bv; + if (!m_uf2bvuf.find(f, f_bv)) { + sort * domain[2] = { m.get_sort(n_bv) }; + f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range()); + m_uf2bvuf.insert(f, f_bv); + m.inc_ref(f); + m.inc_ref(f_bv); + } + result = m.mk_app(f_bv, n_bv); + } } void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -3467,6 +3435,7 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e result = m_util.mk_fp(args[0], args[1], args[2]); TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;); } + void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const { SASSERT(m_util.is_fp(e)); SASSERT(to_app(e)->get_num_args() == 3); @@ -3485,6 +3454,14 @@ void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_r sig = e_sig; } +void fpa2bv_converter::join_fp(expr * e, expr_ref & res) { + SASSERT(m_util.is_fp(e)); + SASSERT(to_app(e)->get_num_args() == 3); + expr *sgn, *exp, *sig; + split_fp(e, sgn, exp, sig); + res = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, exp), sig); +} + void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split_fp(e, sgn, exp, sig); @@ -4051,7 +4028,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & // put the sticky bit into the significand. expr_ref ext_sticky(m); ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky); - expr * tmp[] = { sig, ext_sticky }; + expr * tmp[2] = { sig, ext_sticky }; sig = m_bv_util.mk_bv_or(2, tmp); SASSERT(is_well_sorted(m, sig)); SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 1e3e5d9b3..d54adac78 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -76,6 +76,7 @@ public: void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const; void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const; + void join_fp(expr * e, expr_ref & res); void mk_eq(expr * a, expr * b, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); @@ -138,9 +139,8 @@ public: void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -226,10 +226,6 @@ private: void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result); void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result); - - 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); }; #endif diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 28ec35536..07623ec48 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -143,13 +143,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; - case OP_FPA_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; - case OP_FPA_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; - case OP_FPA_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index c50d6b985..9bee51af7 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -711,65 +711,6 @@ func_decl * fpa_decl_plugin::mk_bv_wrap(decl_kind k, unsigned num_parameters, pa } } -func_decl * fpa_decl_plugin::mk_to_ubv_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_ubv_unspecified"); - 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, ¶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)); -} - -func_decl * fpa_decl_plugin::mk_to_sbv_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_sbv_unspecified"); - 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)); -} - -func_decl * fpa_decl_plugin::mk_to_real_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_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"); - - return m_manager->mk_func_decl(symbol("fp.to_real_unspecified"), 0, domain, m_real_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - -func_decl * fpa_decl_plugin::mk_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; expecting none"); - if (num_parameters != 2) - m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 2"); - if (!parameters[0].is_int() || !parameters[1].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting 2 integers"); - - 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("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - - func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (k) { @@ -846,14 +787,6 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_FPA_MAX_UNSPECIFIED: return mk_binary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_TO_UBV_UNSPECIFIED: - return mk_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_TO_SBV_UNSPECIFIED: - return mk_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_TO_REAL_UNSPECIFIED: - return mk_to_real_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: - return mk_to_ieee_bv_unspecified(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -1054,30 +987,6 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * fpa_util::mk_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_TO_UBV_UNSPECIFIED, 3, ps, 0, 0, range); -} - -app * fpa_util::mk_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_TO_SBV_UNSPECIFIED, 3, ps, 0, 0, range); -} - -app * fpa_util::mk_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_TO_IEEE_BV_UNSPECIFIED, 2, ps, 0, 0, range); -} - -app * fpa_util::mk_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_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range); -} - bool fpa_util::contains_floats(ast * a) { switch (a->get_kind()) { case AST_APP: { diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index c78194b63..79f44a13d 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -93,10 +93,6 @@ enum fpa_op_kind { OP_FPA_MAX_I, OP_FPA_MIN_UNSPECIFIED, OP_FPA_MAX_UNSPECIFIED, - OP_FPA_TO_UBV_UNSPECIFIED, - OP_FPA_TO_SBV_UNSPECIFIED, - OP_FPA_TO_IEEE_BV_UNSPECIFIED, - OP_FPA_TO_REAL_UNSPECIFIED, LAST_FLOAT_OP }; @@ -167,34 +163,12 @@ class fpa_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - func_decl * mk_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - func_decl * mk_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - func_decl * mk_to_ieee_bv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); void recycled_id(unsigned id); - virtual bool is_considered_uninterpreted(func_decl * f) { - if (f->get_family_id() != get_family_id()) - return false; - switch (f->get_decl_kind()) - { - case OP_FPA_TO_UBV_UNSPECIFIED: - case OP_FPA_TO_SBV_UNSPECIFIED: - case OP_FPA_TO_REAL_UNSPECIFIED: - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: - return true; - default: - return false; - } - return false; - } + virtual bool is_considered_uninterpreted(func_decl * f) { return false; } public: fpa_decl_plugin(); @@ -374,10 +348,6 @@ public: SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); return m().mk_app(m_fid, OP_FPA_BV2RM, 0, 0, 1, &bv3, mk_rm_sort()); } - app * mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); - app * mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); - app * mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); - app * mk_to_real_unspecified(unsigned ebits, unsigned sbits); bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BVWRAP); } bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; } @@ -388,19 +358,15 @@ public: bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_UNSPECIFIED); } bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_I); } bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_UNSPECIFIED); } - bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV_UNSPECIFIED); } - bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV_UNSPECIFIED); } - bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_IEEE_BV_UNSPECIFIED); } - bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_REAL_UNSPECIFIED); } + bool is_to_ubv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV); } + bool is_to_sbv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV); } bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_I; } bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MIN_UNSPECIFIED; } bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_I; } bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_MAX_UNSPECIFIED; } - bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV_UNSPECIFIED; } - bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV_UNSPECIFIED; } - bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_IEEE_BV_UNSPECIFIED; } - bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_REAL_UNSPECIFIED; } + bool is_to_ubv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV; } + bool is_to_sbv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV; } bool contains_floats(ast * a); }; diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index b31270ce8..644aff630 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -103,57 +103,12 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break; case OP_FPA_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break; - case OP_FPA_TO_UBV_UNSPECIFIED: - case OP_FPA_TO_SBV_UNSPECIFIED: - case OP_FPA_TO_REAL_UNSPECIFIED: - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: - st = BR_FAILED; - break; - default: NOT_IMPLEMENTED_YET(); } return st; } -br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) { - bv_util bu(m()); - if (m_hi_fp_unspecified) { - // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, width); - return BR_DONE; - } - else { - result = m_util.mk_to_ubv_unspecified(ebits, sbits, width); - return BR_REWRITE1; - } -} - -br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) { - bv_util bu(m()); - if (m_hi_fp_unspecified) { - // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, width); - return BR_DONE; - } - else { - result = m_util.mk_to_sbv_unspecified(ebits, sbits, width); - return BR_REWRITE1; - } -} - -br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) { - if (m_hi_fp_unspecified) { - // The "hardware interpretation" is 0. - result = m_util.au().mk_numeral(rational(0), false); - return BR_DONE; - } - else { - result = m_util.mk_to_real_unspecified(ebits, sbits); - return BR_REWRITE1; - } -} - br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); @@ -808,7 +763,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ const mpf & x = v.get(); if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) - return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); + return BR_FAILED; bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); @@ -822,9 +777,6 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ result = bu.mk_numeral(r, bv_sz); return BR_DONE; } - else - return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); - } return BR_FAILED; @@ -842,7 +794,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ const mpf & x = v.get(); if (m_fm.is_nan(v) || m_fm.is_inf(v)) - return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); + return BR_FAILED; bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); @@ -856,8 +808,6 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ result = bu.mk_numeral(r, bv_sz); return BR_DONE; } - else - return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); } return BR_FAILED; @@ -881,7 +831,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu result = bu.mk_concat(4, args); } else - result = m_util.mk_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + return BR_FAILED; return BR_REWRITE1; } @@ -900,16 +850,12 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { scoped_mpf v(m_fm); if (m_util.is_numeral(arg, v)) { - if (m_fm.is_nan(v) || m_fm.is_inf(v)) { - const mpf & x = v.get(); - result = m_util.mk_to_real_unspecified(x.get_ebits(), x.get_sbits()); - } - else { + if (!m_fm.is_nan(v) && !m_fm.is_inf(v)) { scoped_mpq r(m_fm.mpq_manager()); m_fm.to_rational(v, r); result = m_util.au().mk_numeral(r.get(), false); + return BR_DONE; } - return BR_DONE; } return BR_FAILED; diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 282cec4df..5d5b7e57d 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -88,9 +88,7 @@ public: br_status mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); - br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result); - br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result); - br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result); + br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr * n, expr_ref & result); br_status mk_bvwrap(expr * arg, expr_ref & result); }; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 12c5fb0b1..d337cc65d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -119,6 +119,7 @@ namespace smt { SASSERT(m_conversions.empty()); SASSERT(m_is_added_to_model.empty()); } + void theory_fpa::init(context * ctx) { smt::theory::init(ctx); m_is_initialized = true; @@ -890,14 +891,10 @@ namespace smt { if (f->get_family_id() == get_family_id()) { bool include = m_fpa_util.is_min_unspecified(f) || - m_fpa_util.is_max_unspecified(f) || - m_fpa_util.is_to_ubv_unspecified(f) || - m_fpa_util.is_to_sbv_unspecified(f) || - m_fpa_util.is_to_ieee_bv_unspecified(f) || - m_fpa_util.is_to_real_unspecified(f); + m_fpa_util.is_max_unspecified(f) ; if (include && !m_is_added_to_model.contains(f)) { - m_is_added_to_model.insert(f); - get_manager().inc_ref(f); + //m_is_added_to_model.insert(f); + //get_manager().inc_ref(f); return true; } return false; From de15932f4ca7e1419c205d2816f6f8e257e55286 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 13 Sep 2017 19:47:59 +0100 Subject: [PATCH 03/15] Fixed BV encoding of fp.to_{s,u}bv. --- src/ast/fpa/fpa2bv_converter.cpp | 137 +++++++++++++++---------------- 1 file changed, 66 insertions(+), 71 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index da4052108..190e86da3 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3140,12 +3140,11 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con 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), x_flat(m); + expr_ref x(m), x_is_nan(m); expr * sgn, * s, * e; x = args[0]; split_fp(x, sgn, e, s); mk_is_nan(x, x_is_nan); - join_fp(x, x_flat); sort * fp_srt = m.get_sort(x); unsigned ebits = m_util.get_ebits(fp_srt); @@ -3158,10 +3157,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * 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 { - expr * x_flatp = x_flat.get(); - mk_to_ieee_bv_unspecified(f, 1, &x_flatp, nanv); - } + else + mk_to_ieee_bv_unspecified(f, num, args, nanv); expr_ref sgn_e_s(m); join_fp(x, sgn_e_s); @@ -3174,8 +3171,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); SASSERT(m_util.is_float(args[0])); - unsigned ebits = f->get_parameter(0).get_int(); - unsigned sbits = f->get_parameter(1).get_int(); + unsigned ebits = f->get_domain()[0]->get_parameter(0).get_int(); + unsigned sbits = f->get_domain()[0]->get_parameter(1).get_int(); if (m_hi_fp_unspecified) { result = m_bv_util.mk_concat(m_bv_util.mk_concat( @@ -3251,7 +3248,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args v1 = unspec_v; dbg_decouple("fpa2bv_to_bv_c1", c1); - // +-Zero -> 0 + // +-0 -> 0 expr_ref c2(m), v2(m); c2 = x_is_zero; v2 = m_bv_util.mk_numeral(rational(0), bv_srt); @@ -3272,60 +3269,57 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args SASSERT(m_bv_util.get_bv_size(exp) == ebits); SASSERT(m_bv_util.get_bv_size(lz) == ebits); - unsigned sig_sz = m_bv_util.get_bv_size(sig); - SASSERT(sig_sz == sbits); + unsigned sig_sz = sbits; if (sig_sz < (bv_sz + 3)) - sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, bv_sz - sig_sz + 3)); + sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, bv_sz-sig_sz+3)); sig_sz = m_bv_util.get_bv_size(sig); SASSERT(sig_sz >= (bv_sz + 3)); - expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), bv0_e2(m), shift_abs(m), shift_le_0(m); - exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), - m_bv_util.mk_zero_extend(2, lz)); - e_m_lz_m_bv_sz = m_bv_util.mk_bv_sub(exp_m_lz, - m_bv_util.mk_numeral(bv_sz - 1, ebits + 2)); - shift = m_bv_util.mk_bv_neg(e_m_lz_m_bv_sz); - bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2); - shift_le_0 = m_bv_util.mk_sle(shift, bv0_e2); - shift_abs = m.mk_ite(shift_le_0, e_m_lz_m_bv_sz, shift); - SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2); - SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2); - dbg_decouple("fpa2bv_to_bv_shift", shift); - dbg_decouple("fpa2bv_to_bv_shift_abs", shift_abs); - // x is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long - // [1][ ... sig ... ][r][g][ ... s ...] - // [ ... ubv ... ][r][g][ ... s ... ] - shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs); - SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz); + expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), is_neg_shift(m), big_sig(m); + exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), + m_bv_util.mk_zero_extend(2, lz)); - expr_ref c_in_limits(m); - if (!is_signed) - c_in_limits = m_bv_util.mk_sle(bv0_e2, shift); - else { - expr_ref one_sle_shift(m), one_eq_shift(m), p2(m), sig_is_p2(m), shift1_and_sig_p2(m); - one_sle_shift = m_bv_util.mk_sle(m_bv_util.mk_numeral(1, ebits + 2), shift); - one_eq_shift = m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift); - p2 = m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sig_sz-1)); - sig_is_p2 = m.mk_eq(sig, p2); - shift1_and_sig_p2 = m.mk_and(one_eq_shift, sig_is_p2); - c_in_limits = m.mk_or(one_sle_shift, shift1_and_sig_p2); + // big_sig is +- [... bv_sz+2 bits ...].[r][g][ ... sbits-1 ... ] + big_sig = m_bv_util.mk_zero_extend(bv_sz+2, sig); + unsigned big_sig_sz = sig_sz+bv_sz+2; + SASSERT(m_bv_util.get_bv_size(big_sig) == big_sig_sz); + + is_neg_shift = m_bv_util.mk_sle(exp_m_lz, m_bv_util.mk_numeral(0, ebits+2)); + shift = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_neg(exp_m_lz), exp_m_lz); + if (ebits+2 < big_sig_sz) + shift = m_bv_util.mk_zero_extend(big_sig_sz-ebits-2, shift); + else if (ebits+2 > big_sig_sz) { + expr_ref upper(m); + upper = m_bv_util.mk_extract(big_sig_sz, ebits+2, shift); + shift = m_bv_util.mk_extract(ebits+1, 0, shift); + shift = m.mk_ite(m.mk_eq(upper, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(upper))), + shift, + m_bv_util.mk_numeral(big_sig_sz-1, ebits+2)); } - dbg_decouple("fpa2bv_to_bv_in_limits", c_in_limits); + dbg_decouple("fpa2bv_to_bv_shift_uncapped", shift); + SASSERT(m_bv_util.get_bv_size(shift) == m_bv_util.get_bv_size(big_sig)); + dbg_decouple("fpa2bv_to_bv_big_sig", big_sig); - expr_ref r_shifted_sig(m), l_shifted_sig(m); - r_shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs); - l_shifted_sig = m_bv_util.mk_bv_shl(sig, m_bv_util.mk_bv_sub( - m_bv_util.mk_numeral(m_bv_util.get_bv_size(sig), m_bv_util.get_bv_size(sig)), - shift_abs)); - dbg_decouple("fpa2bv_to_bv_r_shifted_sig", r_shifted_sig); - dbg_decouple("fpa2bv_to_bv_l_shifted_sig", l_shifted_sig); + expr_ref shift_limit(m); + shift_limit = m_bv_util.mk_numeral(bv_sz+2, m_bv_util.get_bv_size(shift)); + shift = m.mk_ite(m_bv_util.mk_ule(shift, shift_limit), shift, shift_limit); + dbg_decouple("fpa2bv_to_bv_shift_limit", shift_limit); + dbg_decouple("fpa2bv_to_bv_is_neg_shift", is_neg_shift); + dbg_decouple("fpa2bv_to_bv_shift", shift); - expr_ref last(m), round(m), sticky(m); - last = m_bv_util.mk_extract(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, r_shifted_sig); - round = m_bv_util.mk_extract(sig_sz - bv_sz - 1, sig_sz - bv_sz - 1, r_shifted_sig); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, l_shifted_sig.get()); + expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m); + big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift), + m_bv_util.mk_bv_shl(big_sig, shift)); + int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-bv_sz-3, big_sig_shifted); + SASSERT(m_bv_util.get_bv_size(int_part) == bv_sz+3); + last = m_bv_util.mk_extract(big_sig_sz-bv_sz-4, big_sig_sz-bv_sz-4, big_sig_shifted); + round = m_bv_util.mk_extract(big_sig_sz-bv_sz-5, big_sig_sz-bv_sz-5, big_sig_shifted); + stickies = m_bv_util.mk_extract(big_sig_sz-bv_sz-6, 0, big_sig_shifted); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies); + dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted); + dbg_decouple("fpa2bv_to_bv_int_part", int_part); dbg_decouple("fpa2bv_to_bv_last", last); dbg_decouple("fpa2bv_to_bv_round", round); dbg_decouple("fpa2bv_to_bv_sticky", sticky); @@ -3335,30 +3329,31 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1); dbg_decouple("fpa2bv_to_bv_rounding_decision", rounding_decision); - expr_ref unrounded_sig(m), pre_rounded(m), inc(m); - unrounded_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz, r_shifted_sig)); - inc = m_bv_util.mk_zero_extend(1, m_bv_util.mk_zero_extend(bv_sz - 1, rounding_decision)); - pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc); + expr_ref inc(m), pre_rounded(m); + inc = m_bv_util.mk_zero_extend(bv_sz+2, rounding_decision); + pre_rounded = m_bv_util.mk_bv_add(int_part, inc); dbg_decouple("fpa2bv_to_bv_inc", inc); dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded); - expr_ref rnd_overflow(m), rnd(m), rnd_has_overflown(m); - rnd_overflow = m_bv_util.mk_extract(bv_sz, bv_sz, pre_rounded); - rnd = m_bv_util.mk_extract(bv_sz - 1, 0, pre_rounded); - rnd_has_overflown = m.mk_eq(rnd_overflow, bv1); - dbg_decouple("fpa2bv_to_bv_rnd_has_overflown", rnd_has_overflown); - - if (is_signed) { - expr_ref sgn_eq_1(m), neg_rnd(m); - sgn_eq_1 = m.mk_eq(sgn, bv1); - neg_rnd = m_bv_util.mk_bv_neg(rnd); - m_simp.mk_ite(sgn_eq_1, neg_rnd, rnd, rnd); + expr_ref out_of_range(m); + if (!is_signed) { + expr_ref ul(m); + ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1))); + out_of_range = m_bv_util.mk_ule(ul, pre_rounded); } + else { + expr_ref ll(m), ul(m); + ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1))); + ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1)); + out_of_range = m.mk_not(m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul))); + } + dbg_decouple("fpa2bv_to_bv_out_of_range", out_of_range); - dbg_decouple("fpa2bv_to_bv_rnd", rnd); + expr_ref rounded(m); + rounded = m_bv_util.mk_extract(bv_sz-1, 0, pre_rounded); + dbg_decouple("fpa2bv_to_bv_rounded", rounded); - result = m.mk_ite(rnd_has_overflown, unspec_v, rnd); - result = m.mk_ite(c_in_limits, result, unspec_v); + result = m.mk_ite(out_of_range, unspec_v, rounded); result = m.mk_ite(c2, v2, result); result = m.mk_ite(c1, v1, result); From 2165c09defb5a989ba703e9ca05eaf8aa0a1e203 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 13 Sep 2017 19:50:51 +0100 Subject: [PATCH 04/15] Improved FPA models of partial theory functions --- src/ast/fpa/bv2fpa_converter.cpp | 52 +++++++++++++++++--------------- 1 file changed, 27 insertions(+), 25 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 59f24779e..d3eedbf54 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -120,9 +120,9 @@ expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr res = m_fpa_util.mk_value(fp_val); TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) << - " " << mk_ismt2_pp(exp, m) << - " " << mk_ismt2_pp(sig, m) << "] == " << - mk_ismt2_pp(res, m) << std::endl;); + " " << mk_ismt2_pp(exp, m) << + " " << mk_ismt2_pp(sig, m) << "] == " << + mk_ismt2_pp(res, m) << std::endl;); m_fpa_util.fm().del(fp_val); return res; @@ -263,7 +263,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * unsigned arity = bv_f->get_arity(); func_interp * bv_fi = mc->get_func_interp(bv_f); - if (bv_fi != 0) { + if (bv_fi) { fpa_rewriter rw(m); expr_ref ai(m); result = alloc(func_interp, m, arity); @@ -384,7 +384,7 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo expr * bvval = to_app(val)->get_arg(0); expr_ref fv(m); fv = convert_bv2rm(mc, to_app(bvval)); - TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;); + TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;); target_model->register_decl(var, fv); seen.insert(to_app(bvval)->get_decl()); } @@ -455,11 +455,14 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode // Upon request, add this 'recursive' definition? func_interp * fmv = convert_func_interp(mc, f, it->m_value); - unsigned n = fmv->get_arity(); - expr_ref_vector args(m); - for (unsigned i = 0; i < n; i++) - args.push_back(m.mk_var(i, f->get_domain()[i])); - fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr())); + if (fmv) { + unsigned n = fmv->get_arity(); + expr_ref_vector args(m); + for (unsigned i = 0; i < n; i++) + args.push_back(m.mk_var(i, f->get_domain()[i])); + fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr())); + target_model->register_decl(f, fmv); + } } else { func_interp * fmv = convert_func_interp(mc, f, it->m_value); @@ -554,21 +557,20 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) { void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) { TRACE("bv2fpa", tout << "BV Model: " << std::endl; - for (unsigned i = 0; i < mc->get_num_constants(); i++) - tout << mc->get_constant(i)->get_name() << " --> " << - mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl; - for (unsigned i = 0; i < mc->get_num_functions(); i++) { - func_decl * f = mc->get_function(i); - tout << f->get_name() << "(...) := " << std::endl; - func_interp * fi = mc->get_func_interp(f); - for (unsigned j = 0; j < fi->num_entries(); j++) { - func_entry const * fe = fi->get_entry(j); - for (unsigned k = 0; k < f->get_arity(); k++) { - tout << mk_ismt2_pp(fe->get_arg(k), m) << " "; + for (unsigned i = 0; i < mc->get_num_constants(); i++) + tout << mc->get_constant(i)->get_name() << " --> " << + mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl; + for (unsigned i = 0; i < mc->get_num_functions(); i++) { + func_decl * f = mc->get_function(i); + tout << f->get_name() << "(...) := " << std::endl; + func_interp * fi = mc->get_func_interp(f); + for (unsigned j = 0; j < fi->num_entries(); j++) { + func_entry const * fe = fi->get_entry(j); + for (unsigned k = 0; k < f->get_arity(); k++) + tout << mk_ismt2_pp(fe->get_arg(k), m) << " "; + tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl; } - tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl; - } - tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl; - }); + tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl; + }); } From 2bcbc5bb2fbe8711c790a05c5431301de2179f92 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 13 Sep 2017 20:15:11 +0100 Subject: [PATCH 05/15] Revert "[TravisCI] Temporarily disable the macOS build configuration." This reverts commit 9dc332ae9d4e1650af47daafe9821bbd8a2edf59. @wintersteiger is now satisfied that using TravisCI's macOS support is legal [1]. This fixes #1211 [1] https://github.com/Z3Prover/z3/issues/1211#issuecomment-328535885 --- .travis.yml | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/.travis.yml b/.travis.yml index 3764f8dac..50d63e593 100644 --- a/.travis.yml +++ b/.travis.yml @@ -60,17 +60,15 @@ env: - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug # macOS (a.k.a OSX) support -# FIXME: macOS support is temporarily disabled due to @wintersteiger 's concerns. -# See https://github.com/Z3Prover/z3/pull/1207#issuecomment-322200998 -# matrix: -# include: -# # For now just test a single configuration. macOS builds on TravisCI are -# # very slow so we should keep the number of configurations we test on this -# # OS to a minimum. -# - os: osx -# osx_image: xcode8.3 -# # Note: Apple Clang does not support OpenMP -# env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 +matrix: + include: + # For now just test a single configuration. macOS builds on TravisCI are + # very slow so we should keep the number of configurations we test on this + # OS to a minimum. + - os: osx + osx_image: xcode8.3 + # Note: Apple Clang does not support OpenMP + env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 script: # Use `travis_wait` when doing LTO builds because this configuration will # have long link times during which it will not show any output which From 8b6d7c0251722ba70b406759f935b7a8ea56fa37 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Sep 2017 17:34:51 +0100 Subject: [PATCH 06/15] Style, formatting --- src/ackermannization/ackr_model_converter.cpp | 61 ++++++++++--------- src/ackermannization/ackr_model_converter.h | 8 +-- 2 files changed, 35 insertions(+), 34 deletions(-) diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index 0697686eb..b48ab9af4 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -3,13 +3,13 @@ Copyright (c) 2015 Microsoft Corporation Module Name: -ackr_model_converter.cpp + ackr_model_converter.cpp Abstract: Author: -Mikolas Janota + Mikolas Janota Revision History: --*/ @@ -22,8 +22,8 @@ Revision History: class ackr_model_converter : public model_converter { public: ackr_model_converter(ast_manager & m, - const ackr_info_ref& info, - model_ref& abstr_model) + const ackr_info_ref& info, + model_ref& abstr_model) : m(m) , info(info) , abstr_model(abstr_model) @@ -31,7 +31,7 @@ public: { } ackr_model_converter(ast_manager & m, - const ackr_info_ref& info) + const ackr_info_ref& info) : m(m) , info(info) , fixed_model(false) @@ -51,8 +51,6 @@ public: virtual void operator()(model_ref & md) { operator()(md, 0); } - //void display(std::ostream & out); - virtual model_converter * translate(ast_translation & translator) { ackr_info_ref retv_info = info->translate(translator); if (fixed_model) { @@ -63,22 +61,23 @@ public: return alloc(ackr_model_converter, translator.to(), retv_info); } } + protected: - ast_manager& m; + ast_manager & m; const ackr_info_ref info; model_ref abstr_model; bool fixed_model; void convert(model * source, model * destination); void add_entry(model_evaluator & evaluator, - app* term, expr* value, - obj_map& interpretations); + app* term, expr* value, + obj_map& interpretations); void convert_constants(model * source, model * destination); }; void ackr_model_converter::convert(model * source, model * destination) { destination->copy_func_interps(*source); destination->copy_usort_interps(*source); - convert_constants(source,destination); + convert_constants(source, destination); } void ackr_model_converter::convert_constants(model * source, model * destination) { @@ -89,16 +88,17 @@ void ackr_model_converter::convert_constants(model * source, model * destination func_decl * const c = source->get_constant(i); app * const term = info->find_term(c); expr * value = source->get_const_interp(c); - if(!term) { + if (!term) { destination->register_decl(c, value); - } else { + } + else { add_entry(evaluator, term, value, interpretations); } } obj_map::iterator e = interpretations.end(); for (obj_map::iterator i = interpretations.begin(); - i!=e; ++i) { + i != e; ++i) { func_decl* const fd = i->m_key; func_interp* const fi = i->get_value(); fi->set_else(m.get_some_value(fd->get_range())); @@ -107,34 +107,35 @@ void ackr_model_converter::convert_constants(model * source, model * destination } void ackr_model_converter::add_entry(model_evaluator & evaluator, - app* term, expr* value, - obj_map& interpretations) { + app* term, expr* value, + obj_map& interpretations) { TRACE("ackr_model", tout << "add_entry" - << mk_ismt2_pp(term, m, 2) - << "->" - << mk_ismt2_pp(value, m, 2) << "\n"; + << mk_ismt2_pp(term, m, 2) + << "->" + << mk_ismt2_pp(value, m, 2) << "\n"; ); - func_interp* fi = 0; + func_interp * fi = 0; func_decl * const declaration = term->get_decl(); const unsigned sz = declaration->get_arity(); SASSERT(sz == term->get_num_args()); - if (!interpretations.find(declaration, fi)) { - fi = alloc(func_interp,m,sz); - interpretations.insert(declaration, fi); + if (!interpretations.find(declaration, fi)) { + fi = alloc(func_interp, m, sz); + interpretations.insert(declaration, fi); } expr_ref_vector args(m); for (unsigned gi = 0; gi < sz; ++gi) { - expr * const arg = term->get_arg(gi); - expr_ref aarg(m); - info->abstract(arg, aarg); - expr_ref arg_value(m); - evaluator(aarg,arg_value); - args.push_back(arg_value); + expr * const arg = term->get_arg(gi); + expr_ref aarg(m); + info->abstract(arg, aarg); + expr_ref arg_value(m); + evaluator(aarg, arg_value); + args.push_back(arg_value); } if (fi->get_entry(args.c_ptr()) == 0) { fi->insert_new_entry(args.c_ptr(), value); - } else { + } + else { TRACE("ackr_model", tout << "entry already present\n";); } } diff --git a/src/ackermannization/ackr_model_converter.h b/src/ackermannization/ackr_model_converter.h index cee7472aa..659b45926 100644 --- a/src/ackermannization/ackr_model_converter.h +++ b/src/ackermannization/ackr_model_converter.h @@ -3,13 +3,13 @@ Copyright (c) 2015 Microsoft Corporation Module Name: -ackr_model_converter.h + ackr_model_converter.h Abstract: Author: -Mikolas Janota + Mikolas Janota Revision History: --*/ @@ -19,7 +19,7 @@ Revision History: #include "tactic/model_converter.h" #include "ackermannization/ackr_info.h" -model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); -model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info); +model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info, model_ref & abstr_model); +model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info); #endif /* LACKR_MODEL_CONVERTER_H_ */ From 5d341814d8049102429618a3aa6beed4dea9cf18 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Sep 2017 17:46:17 +0100 Subject: [PATCH 07/15] Fixed bug in ackermannization model converter --- src/ackermannization/ackr_model_converter.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index b48ab9af4..a7c021913 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -84,6 +84,7 @@ void ackr_model_converter::convert_constants(model * source, model * destination TRACE("ackr_model", tout << "converting constants\n";); obj_map interpretations; model_evaluator evaluator(*source); + evaluator.set_model_completion(true); for (unsigned i = 0; i < source->get_num_constants(); i++) { func_decl * const c = source->get_constant(i); app * const term = info->find_term(c); @@ -133,6 +134,11 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator, args.push_back(arg_value); } if (fi->get_entry(args.c_ptr()) == 0) { + TRACE("ackr_model", + tout << mk_ismt2_pp(declaration, m) << " args: " << std::endl; + for (unsigned i = 0; i < args.size(); i++) + tout << mk_ismt2_pp(args.get(i), m) << std::endl; + tout << " -> " << mk_ismt2_pp(value, m) << "\n"; ); fi->insert_new_entry(args.c_ptr(), value); } else { From a479fa610acb201136f6c488cc604b2e460d552f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Sep 2017 20:29:07 +0100 Subject: [PATCH 08/15] Refactored treatment of unspecified FPA functions. --- src/ast/fpa/bv2fpa_converter.cpp | 7 +- src/ast/fpa/fpa2bv_converter.cpp | 10 +-- src/ast/fpa_decl_plugin.h | 3 +- src/ast/rewriter/fpa_rewriter.cpp | 144 ++++++++++++++++-------------- src/ast/rewriter/fpa_rewriter.h | 11 ++- 5 files changed, 95 insertions(+), 80 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index d3eedbf54..2aa4dc31a 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -451,16 +451,19 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode else { if (it->get_key().get_family_id() == m_fpa_util.get_fid()) { // it->m_value contains the model for the unspecified cases of it->m_key. - continue; - // Upon request, add this 'recursive' definition? func_interp * fmv = convert_func_interp(mc, f, it->m_value); if (fmv) { +#if 0 + // Upon request, add this 'recursive' definition? unsigned n = fmv->get_arity(); expr_ref_vector args(m); for (unsigned i = 0; i < n; i++) args.push_back(m.mk_var(i, f->get_domain()[i])); fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr())); +#else + fmv->set_else(0); +#endif target_model->register_decl(f, fmv); } } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 190e86da3..f0707a273 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2582,7 +2582,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); - if (m_bv_util.is_numeral(bv_rm) && m_util.au().is_numeral(x)) { + if (m_bv_util.is_numeral(bv_rm) && m_util.arith_util().is_numeral(x)) { rational tmp_rat; unsigned sz; m_bv_util.is_numeral(to_expr(bv_rm), tmp_rat, sz); SASSERT(tmp_rat.is_int32()); @@ -2600,7 +2600,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * rational q; bool is_int; - m_util.au().is_numeral(x, q, is_int); + m_util.arith_util().is_numeral(x, q, is_int); if (q.is_zero()) return mk_pzero(f, result); @@ -2617,12 +2617,12 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * result = m_util.mk_fp(sgn, exp, sig); } } - else if (m_util.au().is_numeral(x)) { + else if (m_util.arith_util().is_numeral(x)) { rational q; bool is_int; - m_util.au().is_numeral(x, q, is_int); + m_util.arith_util().is_numeral(x, q, is_int); - if (m_util.au().is_zero(x)) + if (m_util.arith_util().is_zero(x)) mk_pzero(f, result); else { expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 79f44a13d..b4730cc75 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -221,7 +221,8 @@ public: mpf_manager & fm() const { return m_plugin->fm(); } family_id get_fid() const { return m_fid; } family_id get_family_id() const { return m_fid; } - arith_util & au() { return m_a_util; } + arith_util & arith_util() { return m_a_util; } + bv_util & bv_util() { return m_bv_util; } fpa_decl_plugin & plugin() { return *m_plugin; } sort * mk_float_sort(unsigned ebits, unsigned sbits); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 644aff630..6c7190ebc 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -113,7 +113,6 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(1).is_int()); - bv_util bu(m()); scoped_mpf v(m_fm); mpf_rounding_mode rmv; rational r1, r2, r3; @@ -122,7 +121,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const unsigned sbits = f->get_parameter(1).get_int(); if (num_args == 1) { - if (bu.is_numeral(args[0], r1, bvs1)) { + if (m_util.bv_util().is_numeral(args[0], r1, bvs1)) { // BV -> float SASSERT(bvs1 == sbits + ebits); unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); @@ -163,7 +162,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const if (!m_util.is_rm_numeral(args[0], rmv)) return BR_FAILED; - if (m_util.au().is_numeral(args[1], r1)) { + if (m_util.arith_util().is_numeral(args[1], r1)) { // rm + real -> float TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;); scoped_mpf v(m_fm); @@ -181,10 +180,10 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const // TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else if (bu.is_numeral(args[1], r1, bvs1)) { + else if (m_util.bv_util().is_numeral(args[1], r1, bvs1)) { // rm + signed bv -> float TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;); - r1 = bu.norm(r1, bvs1, true); + r1 = m_util.bv_util().norm(r1, bvs1, true); TRACE("fp_rewriter", tout << "r1 norm: " << r1 << std::endl;); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); result = m_util.mk_value(v); @@ -193,12 +192,12 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const } else if (num_args == 3) { if (m_util.is_rm_numeral(args[0], rmv) && - m_util.au().is_real(args[1]) && - m_util.au().is_int(args[2])) { + m_util.arith_util().is_real(args[1]) && + m_util.arith_util().is_int(args[2])) { // rm + real + int -> float if (!m_util.is_rm_numeral(args[0], rmv) || - !m_util.au().is_numeral(args[1], r1) || - !m_util.au().is_numeral(args[2], r2)) + !m_util.arith_util().is_numeral(args[1], r1) || + !m_util.arith_util().is_numeral(args[2], r2)) return BR_FAILED; TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); @@ -207,12 +206,12 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const return BR_DONE; } else if (m_util.is_rm_numeral(args[0], rmv) && - m_util.au().is_int(args[1]) && - m_util.au().is_real(args[2])) { + m_util.arith_util().is_int(args[1]) && + m_util.arith_util().is_real(args[2])) { // rm + int + real -> float if (!m_util.is_rm_numeral(args[0], rmv) || - !m_util.au().is_numeral(args[1], r1) || - !m_util.au().is_numeral(args[2], r2)) + !m_util.arith_util().is_numeral(args[1], r1) || + !m_util.arith_util().is_numeral(args[2], r2)) return BR_FAILED; TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); @@ -220,9 +219,9 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const result = m_util.mk_value(v); return BR_DONE; } - else if (bu.is_numeral(args[0], r1, bvs1) && - bu.is_numeral(args[1], r2, bvs2) && - bu.is_numeral(args[2], r3, bvs3)) { + else if (m_util.bv_util().is_numeral(args[0], r1, bvs1) && + m_util.bv_util().is_numeral(args[1], r2, bvs2) && + m_util.bv_util().is_numeral(args[2], r3, bvs3)) { // 3 BV -> float SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator())); SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator())); @@ -245,7 +244,6 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(1).is_int()); - bv_util bu(m()); unsigned ebits = f->get_parameter(0).get_int(); unsigned sbits = f->get_parameter(1).get_int(); mpf_rounding_mode rmv; @@ -253,7 +251,7 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg unsigned bvs; if (m_util.is_rm_numeral(arg1, rmv) && - bu.is_numeral(arg2, r, bvs)) { + m_util.bv_util().is_numeral(arg2, r, bvs)) { scoped_mpf v(m_fm); m_fm.set(v, ebits, sbits, rmv, r.to_mpq()); result = m_util.mk_value(v); @@ -286,6 +284,7 @@ br_status fpa_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_fm), v3(m_fm); if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) { @@ -301,6 +300,7 @@ br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & br_status fpa_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_fm), v3(m_fm); if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) { @@ -310,7 +310,6 @@ br_status fpa_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & return BR_DONE; } } - return BR_FAILED; } @@ -348,6 +347,7 @@ br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { scoped_mpf t(m_fm); m_fm.rem(v1, v2, t); @@ -411,6 +411,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); @@ -418,6 +419,7 @@ br_status fpa_rewriter::mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_r result = m_util.mk_min(arg1, arg2); return BR_DONE; } + return BR_FAILED; } @@ -458,6 +460,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) result = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); @@ -465,11 +468,13 @@ br_status fpa_rewriter::mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_r result = m_util.mk_max(arg1, arg2); return BR_DONE; } + return BR_FAILED; } br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { mpf_rounding_mode rm; + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_fm), v3(m_fm), v4(m_fm); if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3) && m_util.is_numeral(arg4, v4)) { @@ -485,6 +490,7 @@ br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { mpf_rounding_mode rm; + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_fm); if (m_util.is_numeral(arg2, v2)) { @@ -500,6 +506,7 @@ br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result) { mpf_rounding_mode rm; + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_fm); if (m_util.is_numeral(arg2, v2)) { @@ -567,7 +574,6 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } - // TODO: more simplifications return BR_FAILED; } @@ -631,6 +637,7 @@ br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_nan(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -641,6 +648,7 @@ br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_inf(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -651,6 +659,7 @@ br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_normal(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -661,6 +670,7 @@ br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_denormal(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -671,6 +681,7 @@ br_status fpa_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_negative(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_neg(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -681,6 +692,7 @@ br_status fpa_rewriter::mk_is_negative(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_positive(expr * arg1, expr_ref & result) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_neg(v) || m_fm.is_nan(v)) ? m().mk_false() : m().mk_true(); return BR_DONE; @@ -693,6 +705,7 @@ br_status fpa_rewriter::mk_is_positive(expr * arg1, expr_ref & result) { // This the SMT = br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { // Note: == is the floats-equality, here we need normal equality. result = (m_fm.is_nan(v1) && m_fm.is_nan(v2)) ? m().mk_true() : @@ -706,10 +719,10 @@ br_status fpa_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) } br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) { - bv_util bu(m()); rational bv_val; unsigned sz = 0; - if (bu.is_numeral(arg, bv_val, sz)) { + + if (m_util.bv_util().is_numeral(arg, bv_val, sz)) { SASSERT(bv_val.is_uint64()); switch (bv_val.get_uint64()) { case BV_RM_TIES_TO_AWAY: result = m_util.mk_round_nearest_ties_to_away(); break; @@ -728,13 +741,12 @@ br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) { br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result) { unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); - bv_util bu(m()); rational rsgn, rexp, rsig; unsigned bvsz_sgn, bvsz_exp, bvsz_sig; - if (bu.is_numeral(sgn, rsgn, bvsz_sgn) && - bu.is_numeral(sig, rsig, bvsz_sig) && - bu.is_numeral(exp, rexp, bvsz_exp)) { + if (m_util.bv_util().is_numeral(sgn, rsgn, bvsz_sgn) && + m_util.bv_util().is_numeral(sig, rsig, bvsz_sig) && + m_util.bv_util().is_numeral(exp, rexp, bvsz_exp)) { SASSERT(mpzm.is_one(rexp.to_mpq().denominator())); SASSERT(mpzm.is_one(rsig.to_mpq().denominator())); scoped_mpf v(m_fm); @@ -751,38 +763,7 @@ br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & res return BR_FAILED; } -br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { - SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_int()); - int bv_sz = f->get_parameter(0).get_int(); - mpf_rounding_mode rmv; - scoped_mpf v(m_fm); - - if (m_util.is_rm_numeral(arg1, rmv) && - m_util.is_numeral(arg2, v)) { - const mpf & x = v.get(); - - if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) - return BR_FAILED; - - bv_util bu(m()); - scoped_mpq q(m_fm.mpq_manager()); - m_fm.to_sbv_mpq(rmv, v, q); - - rational r(q); - rational ul, ll; - ul = m_fm.m_powers2.m1(bv_sz); - ll = rational(0); - if (r >= ll && r <= ul) { - result = bu.mk_numeral(r, bv_sz); - return BR_DONE; - } - } - - return BR_FAILED; -} - -br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { +br_status fpa_rewriter::mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool is_signed, expr_ref & result) { SASSERT(f->get_num_parameters() == 1); SASSERT(f->get_parameter(0).is_int()); int bv_sz = f->get_parameter(0).get_int(); @@ -794,7 +775,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ const mpf & x = v.get(); if (m_fm.is_nan(v) || m_fm.is_inf(v)) - return BR_FAILED; + return mk_to_bv_unspecified(f, result); bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); @@ -802,17 +783,43 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ rational r(q); rational ul, ll; - ul = m_fm.m_powers2.m1(bv_sz - 1); - ll = - m_fm.m_powers2(bv_sz - 1); + if (!is_signed) { + ul = m_fm.m_powers2.m1(bv_sz); + ll = rational(0); + } + else { + ul = m_fm.m_powers2.m1(bv_sz - 1); + ll = -m_fm.m_powers2(bv_sz - 1); + } if (r >= ll && r <= ul) { result = bu.mk_numeral(r, bv_sz); return BR_DONE; } + else + return mk_to_bv_unspecified(f, result); } return BR_FAILED; } +br_status fpa_rewriter::mk_to_bv_unspecified(func_decl * f, expr_ref & result) { + if (m_hi_fp_unspecified) { + unsigned bv_sz = m_util.bv_util().get_bv_size(f->get_range()); + result = m_util.bv_util().mk_numeral(0, bv_sz); + return BR_DONE; + } + else + return BR_FAILED; +} + +br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { + return mk_to_bv(f, arg1, arg2, false, result); +} + +br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { + return mk_to_bv(f, arg1, arg2, true, result); +} + br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) { TRACE("fp_rewriter", tout << "to_ieee_bv of " << mk_ismt2_pp(arg, m()) << std::endl;); scoped_mpf v(m_fm); @@ -829,11 +836,8 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu bu.mk_numeral(0, x.get_sbits() - 2), bu.mk_numeral(1, 1) }; result = bu.mk_concat(4, args); + return BR_REWRITE1; } - else - return BR_FAILED; - - return BR_REWRITE1; } else { scoped_mpz rz(m_fm.mpq_manager()); @@ -851,9 +855,17 @@ 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)) { + if (m_hi_fp_unspecified) { + result = m_util.arith_util().mk_numeral(rational(0), false); + return BR_DONE; + } + else + return BR_FAILED; + } + else { scoped_mpq r(m_fm.mpq_manager()); m_fm.to_rational(v, r); - result = m_util.au().mk_numeral(r.get(), false); + result = m_util.arith_util().mk_numeral(r.get(), false); return BR_DONE; } } diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 5d5b7e57d..cfa1bea52 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -21,8 +21,9 @@ Notes: #include "ast/ast.h" #include "ast/rewriter/rewriter.h" -#include "util/params.h" #include "ast/fpa_decl_plugin.h" +#include "ast/expr_map.h" +#include "util/params.h" #include "util/mpf.h" class fpa_rewriter { @@ -33,6 +34,9 @@ class fpa_rewriter { app * mk_eq_nan(expr * arg); app * mk_neq_nan(expr * arg); + br_status mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool is_signed, expr_ref & result); + br_status mk_to_bv_unspecified(func_decl * f, expr_ref & result); + public: fpa_rewriter(ast_manager & m, params_ref const & p = params_ref()); ~fpa_rewriter(); @@ -73,14 +77,11 @@ public: br_status mk_is_negative(expr * arg1, expr_ref & result); br_status mk_is_positive(expr * arg1, expr_ref & result); - br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); - br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_bv2rm(expr * arg, expr_ref & result); br_status mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result); - br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result); @@ -88,8 +89,6 @@ public: br_status mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); - br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr * n, expr_ref & result); - br_status mk_bvwrap(expr * arg, expr_ref & result); }; From 2688fd55cf79d8dcb2a5a509cb68f60ac92ad759 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Sep 2017 20:29:54 +0100 Subject: [PATCH 09/15] Taught the model_evaluator to look for definitions of partial theory functions in the model upon evaluation failure. --- src/model/model_evaluator.cpp | 127 ++++++++++++++++++++-------------- 1 file changed, 76 insertions(+), 51 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 2b8f8abd6..32ed1e236 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -33,9 +33,11 @@ Revision History: #include "ast/ast_pp.h" #include "ast/ast_util.h" #include "model/model_smt2_pp.h" +#include "ast/rewriter/var_subst.h" struct evaluator_cfg : public default_rewriter_cfg { + ast_manager & m; model_core & m_model; bool_rewriter m_b_rw; arith_rewriter m_a_rw; @@ -53,6 +55,7 @@ struct evaluator_cfg : public default_rewriter_cfg { bool m_array_equalities; evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p): + m(m), m_model(md), m_b_rw(m), // We must allow customers to set parameters for arithmetic rewriter/evaluator. @@ -74,6 +77,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_ar_rw.set_expand_select_store(true); m_ar_rw.set_expand_select_ite(true); updt_params(p); + //add_unspecified_function_models(md); } void updt_params(params_ref const & _p) { @@ -85,10 +89,8 @@ struct evaluator_cfg : public default_rewriter_cfg { m_array_equalities = p.array_equalities(); } - ast_manager & m() const { return m_model.get_manager(); } - - bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) { - func_interp* fi = m_model.get_func_interp(f); + bool evaluate(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + func_interp * fi = m_model.get_func_interp(f); return (fi != 0) && eval_fi(fi, num, args, result); } @@ -101,9 +103,8 @@ struct evaluator_cfg : public default_rewriter_cfg { bool actuals_are_values = true; - for (unsigned i = 0; actuals_are_values && i < num; i++) { - actuals_are_values = m().is_value(args[i]); - } + for (unsigned i = 0; actuals_are_values && i < num; i++) + actuals_are_values = m.is_value(args[i]); if (!actuals_are_values) return false; // let get_macro handle it @@ -120,7 +121,7 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = 0; family_id fid = f->get_family_id(); - bool is_uninterp = fid != null_family_id && m().get_plugin(fid)->is_considered_uninterpreted(f); + bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f); if (num == 0 && (fid == null_family_id || is_uninterp)) { expr * val = m_model.get_const_interp(f); if (val != 0) { @@ -145,7 +146,7 @@ struct evaluator_cfg : public default_rewriter_cfg { if (k == OP_EQ) { // theory dispatch for = SASSERT(num == 2); - family_id s_fid = m().get_sort(args[0])->get_family_id(); + family_id s_fid = m.get_sort(args[0])->get_family_id(); if (s_fid == m_a_rw.get_fid()) st = m_a_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_bv_rw.get_fid()) @@ -178,16 +179,18 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_app_core(f, num, args, result); else if (fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_app_core(f, num, args, result); - else if (fid == m().get_label_family_id() && num == 1) { + else if (fid == m.get_label_family_id() && num == 1) { result = args[0]; st = BR_DONE; } else if (evaluate(f, num, args, result)) { TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; - for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; - tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";); + for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n"; + tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";); return BR_DONE; } + if (st == BR_FAILED && !m.is_builtin_family_id(fid)) + st = evaluate_partial_theory_func(f, num, args, result, result_pr); if (st == BR_DONE && is_app(result)) { app* a = to_app(result); if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) { @@ -200,14 +203,14 @@ struct evaluator_cfg : public default_rewriter_cfg { void expand_value(expr_ref& val) { vector stores; - expr_ref else_case(m()); + expr_ref else_case(m); bool _unused; if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) { - sort* srt = m().get_sort(val); + sort* srt = m.get_sort(val); val = m_ar.mk_const_array(srt, else_case); for (unsigned i = stores.size(); i > 0; ) { --i; - expr_ref_vector args(m()); + expr_ref_vector args(m); args.push_back(val); args.append(stores[i].size(), stores[i].c_ptr()); val = m_ar.mk_store(args.size(), args.c_ptr()); @@ -220,6 +223,7 @@ struct evaluator_cfg : public default_rewriter_cfg { #define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";); func_interp * fi = m_model.get_func_interp(f); + if (fi != 0) { TRACE_MACRO; if (fi->is_partial()) { @@ -228,31 +232,52 @@ struct evaluator_cfg : public default_rewriter_cfg { expr * val = m_model.get_some_value(s); fi->set_else(val); } - else { + else return false; - } } - def = fi->get_interp(); + def = fi->get_interp(); SASSERT(def != 0); return true; } if (m_model_completion && (f->get_family_id() == null_family_id || - m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) + m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) { TRACE_MACRO; sort * s = f->get_range(); expr * val = m_model.get_some_value(s); - func_interp * new_fi = alloc(func_interp, m(), f->get_arity()); + func_interp * new_fi = alloc(func_interp, m, f->get_arity()); new_fi->set_else(val); m_model.register_decl(f, new_fi); def = val; return true; } + return false; } + br_status evaluate_partial_theory_func(func_decl * f, + unsigned num, expr * const * args, + expr_ref & result, proof_ref & result_pr) { + SASSERT(f != 0); + SASSERT(!m.is_builtin_family_id(f->get_family_id())); + result = 0; + result_pr = 0; + + func_interp * fi = m_model.get_func_interp(f); + if (fi) { + if (fi->is_partial()) + fi->set_else(m.get_some_value(f->get_range())); + + var_subst vs(m, false); + vs(fi->get_interp(), num, args, result); + return BR_REWRITE_FULL; + } + + return BR_FAILED; + } + bool max_steps_exceeded(unsigned num_steps) const { cooperate("model evaluator"); @@ -266,7 +291,7 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status mk_array_eq(expr* a, expr* b, expr_ref& result) { if (a == b) { - result = m().mk_true(); + result = m.mk_true(); return BR_DONE; } if (!m_array_equalities) { @@ -275,19 +300,19 @@ struct evaluator_cfg : public default_rewriter_cfg { vector stores1, stores2; bool args_are_unique1, args_are_unique2; - expr_ref else1(m()), else2(m()); + expr_ref else1(m), else2(m); if (extract_array_func_interp(a, stores1, else1, args_are_unique1) && extract_array_func_interp(b, stores2, else2, args_are_unique2)) { - expr_ref_vector conj(m()), args1(m()), args2(m()); - if (m().are_equal(else1, else2)) { + expr_ref_vector conj(m), args1(m), args2(m); + if (m.are_equal(else1, else2)) { // no op } - else if (m().are_distinct(else1, else2) && !(m().get_sort(else1)->get_info()->get_num_elements().is_finite())) { - result = m().mk_false(); + else if (m.are_distinct(else1, else2) && !(m.get_sort(else1)->get_info()->get_num_elements().is_finite())) { + result = m.mk_false(); return BR_DONE; } else { - conj.push_back(m().mk_eq(else1, else2)); + conj.push_back(m.mk_eq(else1, else2)); } if (args_are_unique1 && args_are_unique2 && !stores1.empty()) { return mk_array_eq_core(stores1, else1, stores2, else2, conj, result); @@ -300,11 +325,11 @@ struct evaluator_cfg : public default_rewriter_cfg { for (unsigned i = 0; i < stores1.size(); ++i) { args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].c_ptr()); args2.resize(1); args2.append(stores1[i].size() - 1, stores1[i].c_ptr()); - expr_ref s1(m_ar.mk_select(args1.size(), args1.c_ptr()), m()); - expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m()); - conj.push_back(m().mk_eq(s1, s2)); + expr_ref s1(m_ar.mk_select(args1.size(), args1.c_ptr()), m); + expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m); + conj.push_back(m.mk_eq(s1, s2)); } - result = m().mk_and(conj.size(), conj.c_ptr()); + result = m.mk_and(conj.size(), conj.c_ptr()); return BR_REWRITE_FULL; } return BR_FAILED; @@ -362,15 +387,15 @@ struct evaluator_cfg : public default_rewriter_cfg { if (table1.find(stores2[i].c_ptr(), args)) { switch (compare(args[arity], val)) { case l_true: table1.remove(args); break; - case l_false: result = m().mk_false(); return BR_DONE; - default: conj.push_back(m().mk_eq(val, args[arity])); break; + case l_false: result = m.mk_false(); return BR_DONE; + default: conj.push_back(m.mk_eq(val, args[arity])); break; } } else { switch (compare(else1, val)) { case l_true: break; - case l_false: result = m().mk_false(); return BR_DONE; - default: conj.push_back(m().mk_eq(else1, val)); break; + case l_false: result = m.mk_false(); return BR_DONE; + default: conj.push_back(m.mk_eq(else1, val)); break; } } } @@ -378,8 +403,8 @@ struct evaluator_cfg : public default_rewriter_cfg { for (; it != end; ++it) { switch (compare((*it)[arity], else2)) { case l_true: break; - case l_false: result = m().mk_false(); return BR_DONE; - default: conj.push_back(m().mk_eq((*it)[arity], else2)); break; + case l_false: result = m.mk_false(); return BR_DONE; + default: conj.push_back(m.mk_eq((*it)[arity], else2)); break; } } result = mk_and(conj); @@ -387,8 +412,8 @@ struct evaluator_cfg : public default_rewriter_cfg { } lbool compare(expr* a, expr* b) { - if (m().are_equal(a, b)) return l_true; - if (m().are_distinct(a, b)) return l_false; + if (m.are_equal(a, b)) return l_true; + if (m.are_distinct(a, b)) return l_false; return l_undef; } @@ -396,8 +421,8 @@ struct evaluator_cfg : public default_rewriter_cfg { bool args_are_values(expr_ref_vector const& store, bool& are_unique) { bool are_values = true; for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) { - are_values = m().is_value(store[j]); - are_unique &= m().is_unique_value(store[j]); + are_values = m.is_value(store[j]); + are_unique &= m.is_unique_value(store[j]); } SASSERT(!are_unique || are_values); return are_values; @@ -408,10 +433,10 @@ struct evaluator_cfg : public default_rewriter_cfg { SASSERT(m_ar.is_array(a)); bool are_values = true; are_unique = true; - TRACE("model_evaluator", tout << mk_pp(a, m()) << "\n";); + TRACE("model_evaluator", tout << mk_pp(a, m) << "\n";); while (m_ar.is_store(a)) { - expr_ref_vector store(m()); + expr_ref_vector store(m); store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1); are_values &= args_are_values(store, are_unique); stores.push_back(store); @@ -424,7 +449,7 @@ struct evaluator_cfg : public default_rewriter_cfg { } if (!m_ar.is_as_array(a)) { - TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";); + TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m) << "\n";); return false; } @@ -434,13 +459,13 @@ struct evaluator_cfg : public default_rewriter_cfg { unsigned arity = f->get_arity(); unsigned base_sz = stores.size(); for (unsigned i = 0; i < sz; ++i) { - expr_ref_vector store(m()); + expr_ref_vector store(m); func_entry const* fe = g->get_entry(i); store.append(arity, fe->get_args()); store.push_back(fe->get_result()); for (unsigned j = 0; j < store.size(); ++j) { if (!is_ground(store[j].get())) { - TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";); + TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";); return false; } } @@ -448,18 +473,18 @@ struct evaluator_cfg : public default_rewriter_cfg { } else_case = g->get_else(); if (!else_case) { - TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n"; - /*model_smt2_pp(tout, m(), m_model, 0);*/ + TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n"; + /*model_smt2_pp(tout, m, m_model, 0);*/ ); return false; } if (!is_ground(else_case)) { - TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";); + TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m) << "\n" << else_case << "\n";); return false; } for (unsigned i = stores.size(); are_values && i > base_sz; ) { --i; - if (m().are_equal(else_case, stores[i].back())) { + if (m.are_equal(else_case, stores[i].back())) { for (unsigned j = i + 1; j < stores.size(); ++j) { stores[j-1].reset(); stores[j-1].append(stores[j]); @@ -469,7 +494,7 @@ struct evaluator_cfg : public default_rewriter_cfg { } are_values &= args_are_values(stores[i], are_unique); } - TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";); + TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m) << "\n";); return true; } From d82afcc48c9682765b9ca4a6bbe879a6a4369e9e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 15 Sep 2017 11:37:32 +0100 Subject: [PATCH 10/15] Whitespace --- src/tactic/fpa/fpa2bv_model_converter.cpp | 6 +++--- src/tactic/fpa/fpa2bv_model_converter.h | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 8ebb3375d..e82c06386 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -38,7 +38,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) { m_bv2fp->convert_rm_consts(mc, float_mdl, seen); m_bv2fp->convert_min_max_specials(mc, float_mdl, seen); m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen); - + // Keep all the non-float constants. unsigned sz = mc->get_num_constants(); for (unsigned i = 0; i < sz; i++) { @@ -46,7 +46,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) { if (!seen.contains(c)) float_mdl->register_decl(c, mc->get_const_interp(c)); } - + // And keep everything else sz = mc->get_num_functions(); for (unsigned i = 0; i < sz; i++) { @@ -57,7 +57,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) { float_mdl->register_decl(f, val); } } - + sz = mc->get_num_uninterpreted_sorts(); for (unsigned i = 0; i < sz; i++) { sort * s = mc->get_uninterpreted_sort(i); diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 465aaa1e4..989caaa58 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -26,7 +26,7 @@ Notes: class fpa2bv_model_converter : public model_converter { ast_manager & m; bv2fpa_converter * m_bv2fp; - + public: fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv): m(m), @@ -53,10 +53,10 @@ public: virtual model_converter * translate(ast_translation & translator); protected: - fpa2bv_model_converter(ast_manager & m) : + fpa2bv_model_converter(ast_manager & m) : m(m), m_bv2fp(0) {} - + void convert(model_core * mc, model * float_mdl); }; From ff42c44f37dae408ab9e73df650a9935ab156975 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 15 Sep 2017 11:48:25 +0100 Subject: [PATCH 11/15] Debug traces --- src/ast/fpa/bv2fpa_converter.cpp | 19 ------------------- src/tactic/fpa/fpa2bv_model_converter.cpp | 17 +++++++++++++++++ 2 files changed, 17 insertions(+), 19 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 2aa4dc31a..ae9f321d1 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -558,22 +558,3 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) { return res; } -void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) { - TRACE("bv2fpa", tout << "BV Model: " << std::endl; - for (unsigned i = 0; i < mc->get_num_constants(); i++) - tout << mc->get_constant(i)->get_name() << " --> " << - mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl; - for (unsigned i = 0; i < mc->get_num_functions(); i++) { - func_decl * f = mc->get_function(i); - tout << f->get_name() << "(...) := " << std::endl; - func_interp * fi = mc->get_func_interp(f); - for (unsigned j = 0; j < fi->num_entries(); j++) { - func_entry const * fe = fi->get_entry(j); - for (unsigned k = 0; k < f->get_arity(); k++) - tout << mk_ismt2_pp(fe->get_arg(k), m) << " "; - tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl; - } - tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl; - }); - -} diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index e82c06386..5e952eb6e 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -33,6 +33,23 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator } void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) { + TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl; + for (unsigned i = 0; i < mc->get_num_constants(); i++) + tout << mc->get_constant(i)->get_name() << " --> " << + mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl; + for (unsigned i = 0; i < mc->get_num_functions(); i++) { + func_decl * f = mc->get_function(i); + tout << f->get_name() << "(...) := " << std::endl; + func_interp * fi = mc->get_func_interp(f); + for (unsigned j = 0; j < fi->num_entries(); j++) { + func_entry const * fe = fi->get_entry(j); + for (unsigned k = 0; k < f->get_arity(); k++) + tout << mk_ismt2_pp(fe->get_arg(k), m) << " "; + tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl; + } + tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl; + }); + obj_hashtable seen; m_bv2fp->convert_consts(mc, float_mdl, seen); m_bv2fp->convert_rm_consts(mc, float_mdl, seen); From 15ccb34a8136e05f73b05ea7718b5219ef60dcf9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 15 Sep 2017 11:48:42 +0100 Subject: [PATCH 12/15] Removed unused function --- src/ast/fpa/bv2fpa_converter.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ast/fpa/bv2fpa_converter.h b/src/ast/fpa/bv2fpa_converter.h index 943f544ca..caf36c1fc 100644 --- a/src/ast/fpa/bv2fpa_converter.h +++ b/src/ast/fpa/bv2fpa_converter.h @@ -50,7 +50,6 @@ public: expr_ref convert_bv2rm(expr * eval_v); expr_ref convert_bv2rm(model_core * mc, app * val); - void convert(model_core * mc, model_core * float_mdl); void convert_consts(model_core * mc, model_core * target_model, obj_hashtable & seen); void convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable & seen); void convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable & seen); From 4267f304a4dfa1e06aac0232ce5fe09a043e34ae Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 15 Sep 2017 12:43:16 +0100 Subject: [PATCH 13/15] Fix for model completion (via cmd_context) --- src/cmd_context/cmd_context.cpp | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index c0e1c9f9c..0a61a5ce6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1665,6 +1665,16 @@ void cmd_context::complete_model() { } } + for (unsigned i = 0; i < md->get_num_functions(); i++) { + func_decl * f = md->get_function(i); + func_interp * fi = md->get_func_interp(f); + IF_VERBOSE(12, verbose_stream() << "(model.completion " << f->get_name() << ")\n"; ); + if (fi->is_partial()) { + sort * range = f->get_range(); + fi->set_else(m().get_some_value(range)); + } + } + for (auto kd : m_func_decls) { symbol const & k = kd.m_key; func_decls & v = kd.m_value; @@ -1948,13 +1958,13 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) { TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";); for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) { TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";); - m_owner.insert(c); + m_owner.insert(c); func_decl * r = m_dt_util.get_constructor_recognizer(c); m_owner.insert(r); TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";); for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) { TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";); - m_owner.insert(a); + m_owner.insert(a); } } if (m_owner.m_scopes.size() > 0) { From 05447d612a35af824212c696c3f899a11113093f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 15 Sep 2017 19:56:15 +0100 Subject: [PATCH 14/15] Bugfixes for fp.to_* operators --- src/ast/fpa/bv2fpa_converter.cpp | 19 ++++++++++++++++--- src/ast/fpa/fpa2bv_converter.cpp | 20 ++++++++++---------- src/ast/rewriter/fpa_rewriter.cpp | 4 +--- src/util/mpf.cpp | 8 ++++++++ 4 files changed, 35 insertions(+), 16 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index ae9f321d1..30d41bc53 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -285,7 +285,21 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * bv_fres = bv_fe->get_result(); ft_fres = rebuild_floats(mc, rng, to_app(bv_fres)); m_th_rw(ft_fres); - result->insert_new_entry(new_args.c_ptr(), ft_fres); + TRACE("bv2fpa", + for (unsigned i = 0; i < new_args.size(); i++) + tout << mk_ismt2_pp(bv_args[i], m) << " == " << + mk_ismt2_pp(new_args[i], m) << std::endl; + tout << mk_ismt2_pp(bv_fres, m) << " == " << mk_ismt2_pp(ft_fres, m) << std::endl;); + func_entry * fe = result->get_entry(new_args.c_ptr()); + if (fe == 0) + result->insert_new_entry(new_args.c_ptr(), ft_fres); + else { + // The BV model may have multiple equivalent entries using different + // representations of NaN. We can only keep one and we check that + // the results for all those entries are the same. + if (ft_fres != fe->get_result()) + throw default_exception("BUG: UF function entries disagree with each other"); + } } app_ref bv_els(m); @@ -462,6 +476,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode args.push_back(m.mk_var(i, f->get_domain()[i])); fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr())); #else + fmv->set_else(0); #endif target_model->register_decl(f, fmv); @@ -476,7 +491,6 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode } void bv2fpa_converter::display(std::ostream & out) { - out << "(fpa2bv-model-converter"; for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); it++) { @@ -510,7 +524,6 @@ void bv2fpa_converter::display(std::ostream & out) { out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << mk_ismt2_pp(it->m_value.second, m, indent) << ")"; } - out << ")"; } bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) { diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index f0707a273..5314bed07 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3312,11 +3312,11 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m); big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift), m_bv_util.mk_bv_shl(big_sig, shift)); - int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-bv_sz-3, big_sig_shifted); + int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted); SASSERT(m_bv_util.get_bv_size(int_part) == bv_sz+3); - last = m_bv_util.mk_extract(big_sig_sz-bv_sz-4, big_sig_sz-bv_sz-4, big_sig_shifted); - round = m_bv_util.mk_extract(big_sig_sz-bv_sz-5, big_sig_sz-bv_sz-5, big_sig_shifted); - stickies = m_bv_util.mk_extract(big_sig_sz-bv_sz-6, 0, big_sig_shifted); + last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted); + round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted); + stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted); sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies); dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted); dbg_decouple("fpa2bv_to_bv_int_part", int_part); @@ -3335,25 +3335,25 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args dbg_decouple("fpa2bv_to_bv_inc", inc); dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded); - expr_ref out_of_range(m); + expr_ref in_range(m); if (!is_signed) { expr_ref ul(m); - ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1))); - out_of_range = m_bv_util.mk_ule(ul, pre_rounded); + ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz)); + in_range = m_bv_util.mk_ule(pre_rounded, ul); } else { expr_ref ll(m), ul(m); ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1))); ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1)); - out_of_range = m.mk_not(m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul))); + in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul)); } - dbg_decouple("fpa2bv_to_bv_out_of_range", out_of_range); + dbg_decouple("fpa2bv_to_bv_in_range", in_range); expr_ref rounded(m); rounded = m_bv_util.mk_extract(bv_sz-1, 0, pre_rounded); dbg_decouple("fpa2bv_to_bv_rounded", rounded); - result = m.mk_ite(out_of_range, unspec_v, rounded); + result = m.mk_ite(m.mk_not(in_range), unspec_v, rounded); result = m.mk_ite(c2, v2, result); result = m.mk_ite(c1, v1, result); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 6c7190ebc..3e30faa6d 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -854,13 +854,11 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { scoped_mpf v(m_fm); if (m_util.is_numeral(arg, v)) { - if (!m_fm.is_nan(v) && !m_fm.is_inf(v)) { + if (m_fm.is_nan(v) || m_fm.is_inf(v)) { if (m_hi_fp_unspecified) { result = m_util.arith_util().mk_numeral(rational(0), false); return BR_DONE; } - else - return BR_FAILED; } else { scoped_mpq r(m_fm.mpq_manager()); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 7287b69cf..5e7233110 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1217,12 +1217,18 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o default: UNREACHABLE(); } if (inc) m_mpz_manager.inc(z); + TRACE("mpf_dbg_sbv", + tout << "SBV: (" << to_string(x) << ") == " << m_mpq_manager.to_string(z) << std::endl; + tout << "sign=" << t.sign() << " last=" << last << " round=" << round << + " sticky=" << sticky << " inc=" << inc << std::endl; ); } else m_mpz_manager.mul2k(z, (unsigned) e); m_mpq_manager.set(o, z); if (x.sign) m_mpq_manager.neg(o); + + TRACE("mpf_dbg", tout << "SBV = " << m_mpq_manager.to_string(o) << std::endl;); } void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) { @@ -1248,6 +1254,8 @@ void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) { m_mpz_manager.mul2k(o, sbits - 1); m_mpz_manager.add(o, sig(x), o); } + + TRACE("mpf_dbg", tout << "IEEE_BV = " << m_mpz_manager.to_string(o) << std::endl;); } void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig) { From 65697eb277c457a67ea8832027acc6715d751e7a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 15 Sep 2017 21:13:47 +0100 Subject: [PATCH 15/15] Portability fixes --- src/ast/fpa/fpa2bv_converter.cpp | 12 ++++---- src/ast/fpa_decl_plugin.h | 4 +-- src/ast/rewriter/fpa_rewriter.cpp | 48 +++++++++++++++---------------- 3 files changed, 32 insertions(+), 32 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 5314bed07..cd3b0ccca 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2582,7 +2582,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); - if (m_bv_util.is_numeral(bv_rm) && m_util.arith_util().is_numeral(x)) { + if (m_bv_util.is_numeral(bv_rm) && m_util.au().is_numeral(x)) { rational tmp_rat; unsigned sz; m_bv_util.is_numeral(to_expr(bv_rm), tmp_rat, sz); SASSERT(tmp_rat.is_int32()); @@ -2600,7 +2600,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * rational q; bool is_int; - m_util.arith_util().is_numeral(x, q, is_int); + m_util.au().is_numeral(x, q, is_int); if (q.is_zero()) return mk_pzero(f, result); @@ -2617,12 +2617,12 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * result = m_util.mk_fp(sgn, exp, sig); } } - else if (m_util.arith_util().is_numeral(x)) { + else if (m_util.au().is_numeral(x)) { rational q; bool is_int; - m_util.arith_util().is_numeral(x, q, is_int); + m_util.au().is_numeral(x, q, is_int); - if (m_util.arith_util().is_zero(x)) + if (m_util.au().is_zero(x)) mk_pzero(f, result); else { expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m); @@ -3317,7 +3317,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted); round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted); stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies.get()); dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted); dbg_decouple("fpa2bv_to_bv_int_part", int_part); dbg_decouple("fpa2bv_to_bv_last", last); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index b4730cc75..f59c8f92f 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -221,8 +221,8 @@ public: mpf_manager & fm() const { return m_plugin->fm(); } family_id get_fid() const { return m_fid; } family_id get_family_id() const { return m_fid; } - arith_util & arith_util() { return m_a_util; } - bv_util & bv_util() { return m_bv_util; } + arith_util & au() { return m_a_util; } + bv_util & bu() { return m_bv_util; } fpa_decl_plugin & plugin() { return *m_plugin; } sort * mk_float_sort(unsigned ebits, unsigned sbits); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 3e30faa6d..09307cbf2 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -121,7 +121,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const unsigned sbits = f->get_parameter(1).get_int(); if (num_args == 1) { - if (m_util.bv_util().is_numeral(args[0], r1, bvs1)) { + if (m_util.bu().is_numeral(args[0], r1, bvs1)) { // BV -> float SASSERT(bvs1 == sbits + ebits); unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); @@ -162,7 +162,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const if (!m_util.is_rm_numeral(args[0], rmv)) return BR_FAILED; - if (m_util.arith_util().is_numeral(args[1], r1)) { + if (m_util.au().is_numeral(args[1], r1)) { // rm + real -> float TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;); scoped_mpf v(m_fm); @@ -180,10 +180,10 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const // TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else if (m_util.bv_util().is_numeral(args[1], r1, bvs1)) { + else if (m_util.bu().is_numeral(args[1], r1, bvs1)) { // rm + signed bv -> float TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;); - r1 = m_util.bv_util().norm(r1, bvs1, true); + r1 = m_util.bu().norm(r1, bvs1, true); TRACE("fp_rewriter", tout << "r1 norm: " << r1 << std::endl;); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); result = m_util.mk_value(v); @@ -192,12 +192,12 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const } else if (num_args == 3) { if (m_util.is_rm_numeral(args[0], rmv) && - m_util.arith_util().is_real(args[1]) && - m_util.arith_util().is_int(args[2])) { + m_util.au().is_real(args[1]) && + m_util.au().is_int(args[2])) { // rm + real + int -> float if (!m_util.is_rm_numeral(args[0], rmv) || - !m_util.arith_util().is_numeral(args[1], r1) || - !m_util.arith_util().is_numeral(args[2], r2)) + !m_util.au().is_numeral(args[1], r1) || + !m_util.au().is_numeral(args[2], r2)) return BR_FAILED; TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); @@ -206,12 +206,12 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const return BR_DONE; } else if (m_util.is_rm_numeral(args[0], rmv) && - m_util.arith_util().is_int(args[1]) && - m_util.arith_util().is_real(args[2])) { + m_util.au().is_int(args[1]) && + m_util.au().is_real(args[2])) { // rm + int + real -> float if (!m_util.is_rm_numeral(args[0], rmv) || - !m_util.arith_util().is_numeral(args[1], r1) || - !m_util.arith_util().is_numeral(args[2], r2)) + !m_util.au().is_numeral(args[1], r1) || + !m_util.au().is_numeral(args[2], r2)) return BR_FAILED; TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); @@ -219,9 +219,9 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const result = m_util.mk_value(v); return BR_DONE; } - else if (m_util.bv_util().is_numeral(args[0], r1, bvs1) && - m_util.bv_util().is_numeral(args[1], r2, bvs2) && - m_util.bv_util().is_numeral(args[2], r3, bvs3)) { + else if (m_util.bu().is_numeral(args[0], r1, bvs1) && + m_util.bu().is_numeral(args[1], r2, bvs2) && + m_util.bu().is_numeral(args[2], r3, bvs3)) { // 3 BV -> float SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator())); SASSERT(m_fm.mpz_manager().is_one(r3.to_mpq().denominator())); @@ -251,7 +251,7 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg unsigned bvs; if (m_util.is_rm_numeral(arg1, rmv) && - m_util.bv_util().is_numeral(arg2, r, bvs)) { + m_util.bu().is_numeral(arg2, r, bvs)) { scoped_mpf v(m_fm); m_fm.set(v, ebits, sbits, rmv, r.to_mpq()); result = m_util.mk_value(v); @@ -722,7 +722,7 @@ br_status fpa_rewriter::mk_bv2rm(expr * arg, expr_ref & result) { rational bv_val; unsigned sz = 0; - if (m_util.bv_util().is_numeral(arg, bv_val, sz)) { + if (m_util.bu().is_numeral(arg, bv_val, sz)) { SASSERT(bv_val.is_uint64()); switch (bv_val.get_uint64()) { case BV_RM_TIES_TO_AWAY: result = m_util.mk_round_nearest_ties_to_away(); break; @@ -744,9 +744,9 @@ br_status fpa_rewriter::mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & res rational rsgn, rexp, rsig; unsigned bvsz_sgn, bvsz_exp, bvsz_sig; - if (m_util.bv_util().is_numeral(sgn, rsgn, bvsz_sgn) && - m_util.bv_util().is_numeral(sig, rsig, bvsz_sig) && - m_util.bv_util().is_numeral(exp, rexp, bvsz_exp)) { + if (m_util.bu().is_numeral(sgn, rsgn, bvsz_sgn) && + m_util.bu().is_numeral(sig, rsig, bvsz_sig) && + m_util.bu().is_numeral(exp, rexp, bvsz_exp)) { SASSERT(mpzm.is_one(rexp.to_mpq().denominator())); SASSERT(mpzm.is_one(rsig.to_mpq().denominator())); scoped_mpf v(m_fm); @@ -804,8 +804,8 @@ br_status fpa_rewriter::mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool i br_status fpa_rewriter::mk_to_bv_unspecified(func_decl * f, expr_ref & result) { if (m_hi_fp_unspecified) { - unsigned bv_sz = m_util.bv_util().get_bv_size(f->get_range()); - result = m_util.bv_util().mk_numeral(0, bv_sz); + unsigned bv_sz = m_util.bu().get_bv_size(f->get_range()); + result = m_util.bu().mk_numeral(0, bv_sz); return BR_DONE; } else @@ -856,14 +856,14 @@ 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)) { if (m_hi_fp_unspecified) { - result = m_util.arith_util().mk_numeral(rational(0), false); + result = m_util.au().mk_numeral(rational(0), false); return BR_DONE; } } else { scoped_mpq r(m_fm.mpq_manager()); m_fm.to_rational(v, r); - result = m_util.arith_util().mk_numeral(r.get(), false); + result = m_util.au().mk_numeral(r.get(), false); return BR_DONE; } }