From 4ceef091563ef0c5f760ee989d3a9c5cb34cd041 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 11 Sep 2017 15:03:02 +0100 Subject: [PATCH] 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);