From c0bc2518b007184ad18aa486f8e4f4e61d800fcc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 8 Jan 2015 14:22:44 +0000 Subject: [PATCH] Renaming for consistency mk_value -> mk_numeral Signed-off-by: Christoph M. Wintersteiger --- src/api/api_ast.cpp | 2 +- src/api/api_numeral.cpp | 4 +- src/api/z3_api.h | 4 +- src/ast/fpa/fpa2bv_converter.cpp | 22 +++++------ src/ast/fpa_decl_plugin.cpp | 8 ++-- src/ast/fpa_decl_plugin.h | 36 +++++++++--------- src/ast/rewriter/fpa_rewriter.cpp | 62 +++++++++++++++---------------- src/smt/theory_fpa.cpp | 8 ++-- 8 files changed, 73 insertions(+), 73 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index eed5f7553..b9c6230b7 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1127,7 +1127,7 @@ extern "C" { case OP_FPA_RM_TOWARD_POSITIVE: return Z3_OP_FPA_RM_TOWARD_POSITIVE; case OP_FPA_RM_TOWARD_NEGATIVE: return Z3_OP_FPA_RM_TOWARD_NEGATIVE; case OP_FPA_RM_TOWARD_ZERO: return Z3_OP_FPA_RM_TOWARD_ZERO; - case OP_FPA_VALUE: return Z3_OP_FPA_VALUE; + case OP_FPA_NUM: return Z3_OP_FPA_NUM; case OP_FPA_PLUS_INF: return Z3_OP_FPA_PLUS_INF; case OP_FPA_MINUS_INF: return Z3_OP_FPA_MINUS_INF; case OP_FPA_NAN: return Z3_OP_FPA_NAN; diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 89f01707e..7789f1157 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -149,7 +149,7 @@ extern "C" { return mk_c(c)->autil().is_numeral(e) || mk_c(c)->bvutil().is_numeral(e) || - mk_c(c)->fpa_util().is_value(e); + mk_c(c)->fpa_util().is_numeral(e); Z3_CATCH_RETURN(Z3_FALSE); } @@ -193,7 +193,7 @@ extern "C" { // floats are separated from all others to avoid huge rationals. fpa_util & fu = mk_c(c)->fpa_util(); scoped_mpf tmp(fu.fm()); - if (mk_c(c)->fpa_util().is_value(to_expr(a), tmp)) { + if (mk_c(c)->fpa_util().is_numeral(to_expr(a), tmp)) { return mk_c(c)->mk_external_string(fu.fm().to_string(tmp)); } else { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index c719354b6..a4ad8d90d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -887,7 +887,7 @@ typedef enum - Z3_OP_FPA_RM_TOWARD_ZERO: Floating-point rounding mode RTZ - - Z3_OP_FPA_VALUE: Floating-point value + - Z3_OP_FPA_NUM: Floating-point value - Z3_OP_FPA_PLUS_INF: Floating-point +oo @@ -1149,7 +1149,7 @@ typedef enum { Z3_OP_FPA_RM_TOWARD_NEGATIVE, Z3_OP_FPA_RM_TOWARD_ZERO, - Z3_OP_FPA_VALUE, + Z3_OP_FPA_NUM, Z3_OP_FPA_PLUS_INF, Z3_OP_FPA_MINUS_INF, Z3_OP_FPA_NAN, diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index dc1a255e8..4c570c1ba 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -80,7 +80,7 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { mk_triple(sgn, s, e, result); } -void fpa2bv_converter::mk_value(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 0); SASSERT(f->get_num_parameters() == 1); SASSERT(f->get_parameter(0).is_external()); @@ -2177,18 +2177,18 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator()); app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m); - a_nte = m_plugin->mk_value(nte); - a_nta = m_plugin->mk_value(nta); - a_tp = m_plugin->mk_value(tp); - a_tn = m_plugin->mk_value(tn); - a_tz = m_plugin->mk_value(tz); + a_nte = m_plugin->mk_numeral(nte); + a_nta = m_plugin->mk_numeral(nta); + a_tp = m_plugin->mk_numeral(tp); + a_tn = m_plugin->mk_numeral(tn); + a_tz = m_plugin->mk_numeral(tz); expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m); - mk_value(a_nte->get_decl(), 0, 0, bv_nte); - mk_value(a_nta->get_decl(), 0, 0, bv_nta); - mk_value(a_tp->get_decl(), 0, 0, bv_tp); - mk_value(a_tn->get_decl(), 0, 0, bv_tn); - mk_value(a_tz->get_decl(), 0, 0, bv_tz); + mk_numeral(a_nte->get_decl(), 0, 0, bv_nte); + mk_numeral(a_nta->get_decl(), 0, 0, bv_nta); + mk_numeral(a_tp->get_decl(), 0, 0, bv_tp); + mk_numeral(a_tn->get_decl(), 0, 0, bv_tn); + mk_numeral(a_tz->get_decl(), 0, 0, bv_tz); expr_ref c1(m), c2(m), c3(m), c4(m); c1 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 52a1a95f7..7d4a77d1c 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -72,7 +72,7 @@ func_decl * fpa_decl_plugin::mk_value_decl(mpf const & v) { parameter p(mk_id(v), true); SASSERT(p.is_external()); sort * s = mk_float_sort(v.get_ebits(), v.get_sbits()); - return m_manager->mk_const_decl(symbol("fpa"), s, func_decl_info(m_family_id, OP_FPA_VALUE, 1, &p)); + return m_manager->mk_const_decl(symbol("fpa"), s, func_decl_info(m_family_id, OP_FPA_NUM, 1, &p)); } app * fpa_decl_plugin::mk_value(mpf const & v) { @@ -80,7 +80,7 @@ app * fpa_decl_plugin::mk_value(mpf const & v) { } bool fpa_decl_plugin::is_value(expr * n, mpf & val) { - if (is_app_of(n, m_family_id, OP_FPA_VALUE)) { + if (is_app_of(n, m_family_id, OP_FPA_NUM)) { m_fm.set(val, m_values[to_app(n)->get_decl()->get_parameter(0).get_ext_id()]); return true; } @@ -860,7 +860,7 @@ bool fpa_decl_plugin::is_value(app * e) const { case OP_FPA_RM_TOWARD_POSITIVE: case OP_FPA_RM_TOWARD_NEGATIVE: case OP_FPA_RM_TOWARD_ZERO: - case OP_FPA_VALUE: + case OP_FPA_NUM: case OP_FPA_PLUS_INF: case OP_FPA_MINUS_INF: case OP_FPA_PLUS_ZERO: @@ -891,7 +891,7 @@ bool fpa_decl_plugin::is_unique_value(app* e) const { case OP_FPA_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */ case OP_FPA_MINUS_ZERO: /* No; -zero == fp #b1 #b00 #b000) */ case OP_FPA_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */ - case OP_FPA_VALUE: /* see NaN */ + case OP_FPA_NUM: /* see NaN */ return false; case OP_FPA_FP: return m_manager->is_unique_value(e->get_arg(0)) && diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 44f0e62c4..24481d348 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -41,7 +41,7 @@ enum fpa_op_kind { OP_FPA_RM_TOWARD_NEGATIVE, OP_FPA_RM_TOWARD_ZERO, - OP_FPA_VALUE, + OP_FPA_NUM, OP_FPA_PLUS_INF, OP_FPA_MINUS_INF, OP_FPA_NAN, @@ -189,12 +189,12 @@ public: virtual bool is_unique_value(app* e) const; mpf_manager & fm() { return m_fm; } - func_decl * mk_value_decl(mpf const & v); - app * mk_value(mpf const & v); - bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FPA_VALUE); } - bool is_value(expr * n, mpf & val); - bool is_rm_value(expr * n, mpf_rounding_mode & val); - bool is_rm_value(expr * n) { mpf_rounding_mode t; return is_rm_value(n, t); } + func_decl * mk_numeral_decl(mpf const & v); + app * mk_numeral(mpf const & v); + bool is_numeral(expr * n) { return is_app_of(n, m_family_id, OP_FPA_NUM); } + bool is_numeral(expr * n, mpf & val); + bool is_rm_numeral(expr * n, mpf_rounding_mode & val); + bool is_rm_numeral(expr * n) { mpf_rounding_mode t; return is_rm_numeral(n, t); } mpf const & get_value(unsigned id) const { SASSERT(m_value_table.contains(id)); @@ -244,23 +244,23 @@ public: app * mk_pinf(sort * s) { return mk_pinf(get_ebits(s), get_sbits(s)); } app * mk_ninf(sort * s) { return mk_ninf(get_ebits(s), get_sbits(s)); } - app * mk_value(mpf const & v) { return m_plugin->mk_value(v); } - bool is_value(expr * n) { return m_plugin->is_value(n); } - bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); } - bool is_rm_value(expr * n) { return m_plugin->is_rm_value(n); } - bool is_rm_value(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_value(n, v); } + app * mk_value(mpf const & v) { return m_plugin->mk_numeral(v); } + bool is_numeral(expr * n) { return m_plugin->is_numeral(n); } + bool is_numeral(expr * n, mpf & v) { return m_plugin->is_numeral(n, v); } + bool is_rm_numeral(expr * n) { return m_plugin->is_rm_numeral(n); } + bool is_rm_numeral(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_numeral(n, v); } app * mk_pzero(unsigned ebits, unsigned sbits); app * mk_nzero(unsigned ebits, unsigned sbits); app * mk_pzero(sort * s) { return mk_pzero(get_ebits(s), get_sbits(s)); } app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); } - bool is_nan(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nan(v); } - bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pinf(v); } - bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); } - bool is_zero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_zero(v); } - bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pzero(v); } - bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nzero(v); } + bool is_nan(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nan(v); } + bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pinf(v); } + bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_ninf(v); } + bool is_zero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_zero(v); } + bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); } + bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); } app * mk_fp(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FPA_FP, arg1, arg2, arg3); } app * mk_to_fp(sort * s, expr * bv_t) { diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index e7b8c7b34..915d25e50 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -81,7 +81,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const if (num_args == 2) { mpf_rounding_mode rm; - if (!m_util.is_rm_value(args[0], rm)) + if (!m_util.is_rm_numeral(args[0], rm)) return BR_FAILED; rational q; @@ -95,7 +95,7 @@ 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.is_value(args[1], q_mpf)) { + else if (m_util.is_numeral(args[1], q_mpf)) { TRACE("fp_rewriter", tout << "q: " << m_util.fm().to_string(q_mpf) << std::endl; ); scoped_mpf v(m_util.fm()); m_util.fm().set(v, ebits, sbits, rm, q_mpf); @@ -116,7 +116,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const m_util.au().is_real(args[1]) && m_util.au().is_int(args[2])) { mpf_rounding_mode rm; - if (!m_util.is_rm_value(args[0], rm)) + if (!m_util.is_rm_numeral(args[0], rm)) return BR_FAILED; rational q; @@ -169,9 +169,9 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, unsigned num_args, expr br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; - if (m_util.is_rm_value(arg1, rm)) { + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_util.fm()), v3(m_util.fm()); - if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) { + if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) { scoped_mpf t(m_util.fm()); m_util.fm().add(rm, v2, v3, t); result = m_util.mk_value(t); @@ -190,9 +190,9 @@ 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_value(arg1, rm)) { + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_util.fm()), v3(m_util.fm()); - if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) { + if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) { scoped_mpf t(m_util.fm()); m_util.fm().mul(rm, v2, v3, t); result = m_util.mk_value(t); @@ -205,9 +205,9 @@ 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_value(arg1, rm)) { + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_util.fm()), v3(m_util.fm()); - if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) { + if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3)) { scoped_mpf t(m_util.fm()); m_util.fm().div(rm, v2, v3, t); result = m_util.mk_value(t); @@ -241,7 +241,7 @@ br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) { } scoped_mpf v1(m_util.fm()); - if (m_util.is_value(arg1, v1)) { + if (m_util.is_numeral(arg1, v1)) { m_util.fm().neg(v1); result = m_util.mk_value(v1); return BR_DONE; @@ -253,7 +253,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_util.fm()), v2(m_util.fm()); - if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { scoped_mpf t(m_util.fm()); m_util.fm().rem(v1, v2, t); result = m_util.mk_value(t); @@ -316,9 +316,9 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { 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_value(arg1, rm)) { + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm()); - if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3) && m_util.is_value(arg4, v4)) { + if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3) && m_util.is_numeral(arg4, v4)) { scoped_mpf t(m_util.fm()); m_util.fm().fused_mul_add(rm, v2, v3, v4, t); result = m_util.mk_value(t); @@ -331,9 +331,9 @@ 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_value(arg1, rm)) { + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_util.fm()); - if (m_util.is_value(arg2, v2)) { + if (m_util.is_numeral(arg2, v2)) { scoped_mpf t(m_util.fm()); m_util.fm().sqrt(rm, v2, t); result = m_util.mk_value(t); @@ -346,9 +346,9 @@ br_status fpa_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) { mpf_rounding_mode rm; - if (m_util.is_rm_value(arg1, rm)) { + if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_util.fm()); - if (m_util.is_value(arg2, v2)) { + if (m_util.is_numeral(arg2, v2)) { scoped_mpf t(m_util.fm()); m_util.fm().round_to_integral(rm, v2, t); result = m_util.mk_value(t); @@ -362,7 +362,7 @@ br_status fpa_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) { // This the floating point theory == br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_util.fm()), v2(m_util.fm()); - if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { result = (m_util.fm().eq(v1, v2)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -407,7 +407,7 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { } scoped_mpf v1(m_util.fm()), v2(m_util.fm()); - if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { result = (m_util.fm().lt(v1, v2)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -427,7 +427,7 @@ br_status fpa_rewriter::mk_le(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } scoped_mpf v1(m_util.fm()), v2(m_util.fm()); - if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { result = (m_util.fm().le(v1, v2)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -442,7 +442,7 @@ br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_zero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -452,7 +452,7 @@ br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_nzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -462,7 +462,7 @@ br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_pzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -472,7 +472,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_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_nan(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -482,7 +482,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_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_inf(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -492,7 +492,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_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_normal(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -502,7 +502,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_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_denormal(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -512,7 +512,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_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_neg(v)) ? m().mk_true() : m().mk_false(); return BR_DONE; } @@ -522,7 +522,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_util.fm()); - if (m_util.is_value(arg1, v)) { + if (m_util.is_numeral(arg1, v)) { result = (m_util.fm().is_neg(v) || m_util.fm().is_nan(v)) ? m().mk_false() : m().mk_true(); return BR_DONE; } @@ -534,7 +534,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_util.fm()), v2(m_util.fm()); - if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { + 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() : (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1)!=m_fm.sgn(v2)) ? m().mk_false() : @@ -584,7 +584,7 @@ br_status fpa_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) { br_status fpa_rewriter::mk_to_real(expr * arg1, expr_ref & result) { scoped_mpf fv(m_util.fm()); - if (m_util.is_value(arg1, fv)) { + if (m_util.is_numeral(arg1, fv)) { if (m_fm.is_nan(fv) || m_fm.is_inf(fv)) { result = m_util.mk_internal_to_real_unspecified(); } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 487908173..158622428 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -647,11 +647,11 @@ namespace smt { wrapped = wrap(n); mpf_rounding_mode rm; scoped_mpf val(mpfm); - if (m_fpa_util.is_rm_value(n, rm)) { + if (m_fpa_util.is_rm_numeral(n, rm)) { c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3)); assert_cnstr(c); } - else if (m_fpa_util.is_value(n, val)) { + else if (m_fpa_util.is_numeral(n, val)) { unsigned sz = val.get().get_ebits() + val.get().get_sbits(); expr_ref bv_val_e(m); bv_val_e = convert(n); @@ -714,8 +714,8 @@ namespace smt { // If the owner is not internalized, it doesn't have an enode associated. SASSERT(ctx.e_internalized(owner)); - if (m_fpa_util.is_rm_value(owner) || - m_fpa_util.is_value(owner)) + if (m_fpa_util.is_rm_numeral(owner) || + m_fpa_util.is_numeral(owner)) return alloc(expr_wrapper_proc, owner); model_value_proc * res = 0;