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

Resolved rebase conflicts

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-21 16:00:56 +01:00
parent 8926b3311d
commit 0a11e8f3c0
1 changed files with 56 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

94
src/api/api_fpa.cpp
View file

@ -913,8 +913,9 @@ extern "C" {
CHECK_VALID_AST(t, 0); CHECK_VALID_AST(t, 0);
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());
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(fid);
fpa_util & fu = mk_c(c)->fpautil();
expr * e = to_expr(t); expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
@ -941,30 +942,27 @@ extern "C" {
mpf_manager & mpfm = mk_c(c)->fpautil().fm(); mpf_manager & mpfm = mk_c(c)->fpautil().fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); unsynch_mpq_manager & mpqm = mpfm.mpq_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(fid);
fpa_util & fu = mk_c(c)->fpautil(); fpa_util & fu = mk_c(c)->fpautil();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
expr * e = to_expr(t); expr * e = to_expr(t);
if (!is_app(e) || if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) {
is_app_of(e, fid, OP_FPA_NAN)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
if (is_app_of(e, fid, OP_FPA_PLUS_INF)) { scoped_mpf val(mpfm);
expr * r = ctx->bvutil().mk_numeral(0, 1); bool r = plugin->is_numeral(to_expr(t), val);
ctx->save_ast_trail(r); if (!r || mpfm.is_nan(val)) {
RETURN_Z3(of_expr(r));
}
if (is_app_of(e, fid, OP_FPA_MINUS_INF)) {
expr * r = ctx->bvutil().mk_numeral(1, 1);
ctx->save_ast_trail(r);
RETURN_Z3(of_expr(r));
}
if (!fu.is_fp(e)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); return 0;
} }
app * a = to_app(e); app * a;
RETURN_Z3(of_expr(a->get_arg(0))); if (mpfm.is_pos(val))
a = ctx->bvutil().mk_numeral(0, 1);
else
a = ctx->bvutil().mk_numeral(1, 1);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -978,22 +976,31 @@ extern "C" {
mpf_manager & mpfm = mk_c(c)->fpautil().fm(); mpf_manager & mpfm = mk_c(c)->fpautil().fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); unsynch_mpq_manager & mpqm = mpfm.mpq_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(fid);
fpa_util & fu = mk_c(c)->fpautil(); fpa_util & fu = mk_c(c)->fpautil();
expr * e = to_expr(t); expr * e = to_expr(t);
if (!is_app(e) || if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) {
is_app_of(e, fid, OP_FPA_NAN) ||
is_app_of(e, fid, OP_FPA_PLUS_INF) ||
is_app_of(e, fid, OP_FPA_MINUS_INF)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
if (!fu.is_fp(e)) { scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
api::context * ctx = mk_c(c); unsigned ebits = val.get().get_ebits();
app * a = to_app(e); mpf_exp_t q = mpfm.exp(val);
RETURN_Z3(of_expr(a->get_arg(1))); mpf_exp_t q_biassed = mpfm.bias_exp(ebits, q);
app * a;
if (mpfm.is_inf(val))
a = mk_c(c)->bvutil().mk_numeral(-1, ebits);
else if (mpfm.is_zero(val) || mpfm.is_denormal(val))
a = mk_c(c)->bvutil().mk_numeral(0, ebits);
else
a = mk_c(c)->bvutil().mk_numeral(q_biassed, ebits);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -1007,22 +1014,27 @@ extern "C" {
mpf_manager & mpfm = mk_c(c)->fpautil().fm(); mpf_manager & mpfm = mk_c(c)->fpautil().fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); unsynch_mpq_manager & mpqm = mpfm.mpq_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(fid);
SASSERT(plugin != 0);
fpa_util & fu = mk_c(c)->fpautil(); fpa_util & fu = mk_c(c)->fpautil();
expr * e = to_expr(t); expr * e = to_expr(t);
if (!is_app(e) || if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) {
is_app_of(e, fid, OP_FPA_NAN) ||
is_app_of(e, fid, OP_FPA_PLUS_INF) ||
is_app_of(e, fid, OP_FPA_MINUS_INF)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
if (!fu.is_fp(e)) { scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
api::context * ctx = mk_c(c); unsigned sbits = val.get().get_sbits();
app * a = to_app(e); scoped_mpq q(mpqm);
RETURN_Z3(of_expr(a->get_arg(2))); mpqm.set(q, mpfm.sig(val));
if (mpfm.is_inf(val)) mpqm.set(q, 0);
app * a = mk_c(c)->bvutil().mk_numeral(q.get(), sbits);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -1038,6 +1050,7 @@ extern "C" {
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(fid); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
SASSERT(plugin != 0); SASSERT(plugin != 0);
fpa_util & fu = mk_c(c)->fpautil();
expr * e = to_expr(t); expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
@ -1045,8 +1058,8 @@ extern "C" {
} }
scoped_mpf val(mpfm); scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val); bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(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();
@ -1071,6 +1084,7 @@ extern "C" {
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(fid); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
SASSERT(plugin != 0); SASSERT(plugin != 0);
fpa_util & fu = mk_c(c)->fpautil();
expr * e = to_expr(t); expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
@ -1081,7 +1095,7 @@ extern "C" {
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 || if (!r ||
!(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val)) || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val)) ||
!mpzm.is_uint64(z)) { !mpzm.is_uint64(z)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
*n = 0; *n = 0;
@ -1101,6 +1115,7 @@ extern "C" {
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);
fpa_util & fu = mk_c(c)->fpautil();
expr * e = to_expr(t); expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
@ -1108,12 +1123,13 @@ extern "C" {
} }
scoped_mpf val(mpfm); scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val); bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return ""; return "";
} }
mpf_exp_t exp = mpfm.is_zero(val) ? 0 : mpf_exp_t exp = mpfm.is_zero(val) ? 0 :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) :
mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) :
mpfm.exp(val); mpfm.exp(val);
std::stringstream ss; std::stringstream ss;
ss << exp; ss << exp;
@ -1130,6 +1146,7 @@ extern "C" {
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);
fpa_util & fu = mk_c(c)->fpautil();
expr * e = to_expr(t); expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
@ -1138,13 +1155,14 @@ extern "C" {
} }
scoped_mpf val(mpfm); scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val); bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val))) { if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
*n = 0; *n = 0;
return 0; return 0;
} }
*n = mpfm.is_zero(val) ? 0 : *n = mpfm.is_zero(val) ? 0 :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) : mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) :
mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) :
mpfm.exp(val); mpfm.exp(val);
return 1; return 1;
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);