From 357ec9e7d1ccc7ae79d2ed2ffc711857401e7744 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 13 Jan 2016 16:32:32 +0000 Subject: [PATCH] Changed FP significand/exponent functions to return non-normalized results. Clarified function remarks. Relates to #383. --- src/api/api_fpa.cpp | 36 ++++++++++++++++++++++-------------- src/api/z3_fpa.h | 9 +++++++-- src/util/mpf.h | 16 ++++++++++------ 3 files changed, 39 insertions(+), 22 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index eaffdd226..33c1448e7 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -912,13 +912,19 @@ extern "C" { ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); + family_id fid = mk_c(c)->get_fpa_fid(); + expr * e = to_expr(t); + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } scoped_mpf val(mpfm); bool r = plugin->is_numeral(to_expr(t), val); if (!r || mpfm.is_nan(val)) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - *sgn = (mpfm.is_nan(val)) ? 0 : mpfm.sgn(val); + *sgn = mpfm.sgn(val); return r; Z3_CATCH_RETURN(0); } @@ -943,17 +949,15 @@ extern "C" { return ""; } scoped_mpf val(mpfm); -// app * a = to_app(e); bool r = plugin->is_numeral(e, val); - if (!r || !mpfm.is_regular(val)) { + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { SET_ERROR_CODE(Z3_INVALID_ARG) return ""; } unsigned sbits = val.get().get_sbits(); scoped_mpq q(mpqm); - scoped_mpz sn(mpzm); - mpfm.sig_normalized(val, sn); - mpqm.set(q, sn); + mpqm.set(q, mpfm.sig(val)); + if (!mpfm.is_denormal(val)) mpqm.add(q, mpfm.m_powers2(sbits - 1), q); mpqm.div(q, mpfm.m_powers2(sbits - 1), q); std::stringstream ss; mpqm.display_decimal(ss, q, sbits); @@ -981,10 +985,11 @@ extern "C" { return 0; } scoped_mpf val(mpfm); -// app * a = to_app(e); bool r = plugin->is_numeral(e, val); const mpz & z = mpfm.sig(val); - if (!r || mpfm.is_regular(val)|| !mpzm.is_uint64(z)) { + if (!r || + !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val)) || + !mpzm.is_uint64(z)) { SET_ERROR_CODE(Z3_INVALID_ARG); *n = 0; return 0; @@ -1012,13 +1017,14 @@ extern "C" { return ""; } scoped_mpf val(mpfm); -// app * a = to_app(e); bool r = plugin->is_numeral(e, val); - if (!r || !mpfm.is_regular(val)) { + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } - mpf_exp_t exp = mpfm.exp_normalized(val); + mpf_exp_t exp = mpfm.is_zero(val) ? 0 : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : + mpfm.exp(val); std::stringstream ss; ss << exp; return mk_c(c)->mk_external_string(ss.str()); @@ -1031,6 +1037,7 @@ extern "C" { RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0); @@ -1044,14 +1051,15 @@ extern "C" { return 0; } scoped_mpf val(mpfm); -// app * a = to_app(e); bool r = plugin->is_numeral(e, val); - if (!r || !mpfm.is_regular(val)) { + if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { SET_ERROR_CODE(Z3_INVALID_ARG); *n = 0; return 0; } - *n = mpfm.exp(val); + *n = mpfm.is_zero(val) ? 0 : + mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : + mpfm.exp(val); return 1; Z3_CATCH_RETURN(0); } diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index b43e19860..510fa0473 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -829,7 +829,8 @@ extern "C" { \param t a floating-point numeral \param sgn sign - Remarks: sets \c sgn to 0 if the literal is NaN or positive and to 1 otherwise. + Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for + NaN, which is an invalid argument. def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT))) */ @@ -841,7 +842,7 @@ extern "C" { \param c logical context \param t a floating-point numeral - Remarks: The significand s is always 0 < s < 2.0; the resulting string is long + Remarks: The significand s is always 0.0 <= s < 2.0; the resulting string is long enough to represent the real significand precisely. def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST))) @@ -869,6 +870,8 @@ extern "C" { \param c logical context \param t a floating-point numeral + Remarks: This function extracts the exponent in `t`, without normalization. + def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST))) */ Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t); @@ -880,6 +883,8 @@ extern "C" { \param t a floating-point numeral \param n exponent + Remarks: This function extracts the exponent in `t`, without normalization. + def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64))) */ Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n); diff --git a/src/util/mpf.h b/src/util/mpf.h index 80d3f4b47..101491e3b 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -155,12 +155,16 @@ public: } const mpf_exp_t & exp(mpf const & x) const { return x.exponent; } mpf_exp_t exp_normalized(mpf const & x) { - mpf t; - set(t, x); - unpack(t, true); - mpf_exp_t r = t.exponent; - del(t); - return r; + if (is_zero(x)) + return 0; + else { + mpf t; + set(t, x); + unpack(t, true); + mpf_exp_t r = t.exponent; + del(t); + return r; + } } bool is_nan(mpf const & x);