mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into lackr

Browse source
This commit is contained in:
Mikolas Janota 2016-01-13 18:22:58 +00:00
commit a5ea17f1e3
3 changed files with 39 additions and 22 deletions
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(); ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm(); mpf_manager & mpfm = mk_c(c)->fpautil().fm();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); 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); scoped_mpf val(mpfm);
bool r = plugin->is_numeral(to_expr(t), val); bool r = plugin->is_numeral(to_expr(t), val);
if (!r || mpfm.is_nan(val)) { if (!r || mpfm.is_nan(val)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
*sgn = (mpfm.is_nan(val)) ? 0 : mpfm.sgn(val); *sgn = mpfm.sgn(val);
return r; return r;
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -943,17 +949,15 @@ extern "C" {
return ""; return "";
} }
scoped_mpf val(mpfm); scoped_mpf val(mpfm);
// app * a = to_app(e);
bool r = plugin->is_numeral(e, val); 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) SET_ERROR_CODE(Z3_INVALID_ARG)
return ""; return "";
} }
unsigned sbits = val.get().get_sbits(); unsigned sbits = val.get().get_sbits();
scoped_mpq q(mpqm); scoped_mpq q(mpqm);
scoped_mpz sn(mpzm); mpqm.set(q, mpfm.sig(val));
mpfm.sig_normalized(val, sn); if (!mpfm.is_denormal(val)) mpqm.add(q, mpfm.m_powers2(sbits - 1), q);
mpqm.set(q, sn);
mpqm.div(q, mpfm.m_powers2(sbits - 1), q); mpqm.div(q, mpfm.m_powers2(sbits - 1), q);
std::stringstream ss; std::stringstream ss;
mpqm.display_decimal(ss, q, sbits); mpqm.display_decimal(ss, q, sbits);
@ -981,10 +985,11 @@ extern "C" {
return 0; return 0;
} }
scoped_mpf val(mpfm); scoped_mpf val(mpfm);
// app * a = to_app(e);
bool r = plugin->is_numeral(e, val); bool r = plugin->is_numeral(e, val);
const mpz & z = mpfm.sig(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); SET_ERROR_CODE(Z3_INVALID_ARG);
*n = 0; *n = 0;
return 0; return 0;
@ -1012,13 +1017,14 @@ extern "C" {
return ""; return "";
} }
scoped_mpf val(mpfm); scoped_mpf val(mpfm);
// app * a = to_app(e);
bool r = plugin->is_numeral(e, val); 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); SET_ERROR_CODE(Z3_INVALID_ARG);
return ""; 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; std::stringstream ss;
ss << exp; ss << exp;
return mk_c(c)->mk_external_string(ss.str()); return mk_c(c)->mk_external_string(ss.str());
@ -1031,6 +1037,7 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m(); ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm(); mpf_manager & mpfm = mk_c(c)->fpautil().fm();
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
family_id fid = mk_c(c)->get_fpa_fid(); 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()); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
SASSERT(plugin != 0); SASSERT(plugin != 0);
@ -1044,14 +1051,15 @@ extern "C" {
return 0; return 0;
} }
scoped_mpf val(mpfm); scoped_mpf val(mpfm);
// app * a = to_app(e);
bool r = plugin->is_numeral(e, val); 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); SET_ERROR_CODE(Z3_INVALID_ARG);
*n = 0; *n = 0;
return 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; return 1;
Z3_CATCH_RETURN(0); 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 t a floating-point numeral
\param sgn sign \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))) 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 c logical context
\param t a floating-point numeral \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. enough to represent the real significand precisely.
def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST))) def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
@ -869,6 +870,8 @@ extern "C" {
\param c logical context \param c logical context
\param t a floating-point numeral \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))) 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); 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 t a floating-point numeral
\param n exponent \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))) 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); 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; } const mpf_exp_t & exp(mpf const & x) const { return x.exponent; }
mpf_exp_t exp_normalized(mpf const & x) { mpf_exp_t exp_normalized(mpf const & x) {
mpf t; if (is_zero(x))
set(t, x); return 0;
unpack(t, true); else {
mpf_exp_t r = t.exponent; mpf t;
del(t); set(t, x);
return r; unpack(t, true);
mpf_exp_t r = t.exponent;
del(t);
return r;
}
} }
bool is_nan(mpf const & x); bool is_nan(mpf const & x);