mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Renaming for consistency mk_value -> mk_numeral

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-08 14:22:44 +00:00
parent c5b220cc12
commit c0bc2518b0
8 changed files with 73 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_ast.cpp
View file

@ -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;

4
src/api/api_numeral.cpp
View file

@ -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 {

4
src/api/z3_api.h
View file

@ -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,

22
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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));

8
src/ast/fpa_decl_plugin.cpp
View file

@ -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)) &&

36
src/ast/fpa_decl_plugin.h
View file

@ -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) {

62
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -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();
}

8
src/smt/theory_fpa.cpp
View file

@ -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;