mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Changed FP significand/exponent functions to return non-normalized results. Clarified function remarks. Relates to #383.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-13 16:32:32 +00:00
parent e0f873c732
commit 357ec9e7d1
3 changed files with 39 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/api/api_fpa.cpp
View file

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

9
src/api/z3_fpa.h
View file

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

16
src/util/mpf.h
View file

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