mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

Bugfix for denormal numeral exponents

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-07 12:38:12 +00:00
parent 758a6d98fb
commit 4e7077db70
1 changed files with 36 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

56
src/api/api_fpa.cpp
View file

@ -990,7 +990,7 @@ extern "C" {
scoped_mpq q(mpqm); scoped_mpq q(mpqm);
mpqm.set(q, mpfm.sig(val)); mpqm.set(q, mpfm.sig(val));
if (mpfm.is_inf(val)) mpqm.set(q, 0); if (mpfm.is_inf(val)) mpqm.set(q, 0);
app * a = mk_c(c)->bvutil().mk_numeral(q.get(), sbits); app * a = mk_c(c)->bvutil().mk_numeral(q.get(), sbits-1);
mk_c(c)->save_ast_trail(a); mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a)); RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -1083,12 +1083,18 @@ extern "C" {
return ""; return "";
} }
unsigned ebits = val.get().get_ebits(); unsigned ebits = val.get().get_ebits();
mpf_exp_t exp = mpfm.is_zero(val) ? 0 : mpf_exp_t exp;
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : if (biased) {
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : exp = mpfm.is_zero(val) ? 0 :
mpfm.bias_exp(ebits, mpfm.exp(val)); mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
if (mpfm.is_normal(val) && !biased) mpfm.bias_exp(ebits, mpfm.exp(val))
exp = mpfm.exp(val); }
else {
exp = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(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());
@ -1118,12 +1124,17 @@ extern "C" {
return 0; return 0;
} }
unsigned ebits = val.get().get_ebits(); unsigned ebits = val.get().get_ebits();
*n = mpfm.is_zero(val) ? 0 : if (biased) {
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : *n = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.bias_exp(ebits, mpfm.exp(val)); mpfm.bias_exp(ebits, mpfm.exp(val));
if (mpfm.is_normal(val) && !biased) }
*n = mpfm.exp(val); else {
*n = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
mpfm.exp(val);
}
return 1; return 1;
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -1150,13 +1161,18 @@ extern "C" {
RETURN_Z3(0); RETURN_Z3(0);
} }
unsigned ebits = val.get().get_ebits(); unsigned ebits = val.get().get_ebits();
mpf_exp_t exp = mpfm.is_zero(val) ? 0 : mpf_exp_t exp;
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) : if (biased) {
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : exp = mpfm.is_zero(val) ? 0 :
mpfm.bias_exp(ebits, mpfm.exp(val)); mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
if (mpfm.is_normal(val) && !biased) mpfm.bias_exp(ebits, mpfm.exp(val));
exp = mpfm.exp(val); }
else {
exp = mpfm.is_zero(val) ? 0 :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
mpfm.exp(val);
}
app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits); app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits);
mk_c(c)->save_ast_trail(a); mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a)); RETURN_Z3(of_expr(a));