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

bug fixes for unspecified FP results

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-16 16:57:20 +00:00
parent db6b9faabc
commit 7ec70c1686
2 changed files with 12 additions and 33 deletions

38
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -118,15 +118,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
return st;
}
br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) {
SASSERT(f->get_num_parameters() == 3);
SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int());
SASSERT(f->get_parameter(2).is_int());
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
unsigned width = f->get_parameter(2).get_int();
br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
bv_util bu(m());
if (m_hi_fp_unspecified)
// The "hardware interpretation" is 0.
@ -137,15 +129,7 @@ br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result)
return BR_DONE;
}
br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) {
SASSERT(f->get_num_parameters() == 3);
SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int());
SASSERT(f->get_parameter(2).is_int());
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
unsigned width = f->get_parameter(2).get_int();
br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
bv_util bu(m());
if (m_hi_fp_unspecified)
// The "hardware interpretation" is 0.
@ -156,13 +140,7 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result)
return BR_DONE;
}
br_status fpa_rewriter::mk_to_real_unspecified(func_decl * f, expr_ref & result) {
SASSERT(f->get_num_parameters() == 2);
SASSERT(f->get_parameter(0).is_int());
SASSERT(f->get_parameter(1).is_int());
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) {
if (m_hi_fp_unspecified)
// The "hardware interpretation" is 0.
result = m_util.au().mk_numeral(rational(0), false);
@ -799,9 +777,10 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
if (m_util.is_rm_numeral(arg1, rmv) &&
m_util.is_numeral(arg2, v)) {
const mpf & x = v.get();
if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) {
mk_to_ubv_unspecified(f, result);
mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_REWRITE_FULL;
}
@ -816,7 +795,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
if (r >= ll && r <= ul)
result = bu.mk_numeral(r, bv_sz);
else
mk_to_ubv_unspecified(f, result);
mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_DONE;
}
@ -832,9 +811,10 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
if (m_util.is_rm_numeral(arg1, rmv) &&
m_util.is_numeral(arg2, v)) {
const mpf & x = v.get();
if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
mk_to_sbv_unspecified(f, result);
mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_REWRITE_FULL;
}
@ -849,7 +829,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
if (r >= ll && r <= ul)
result = bu.mk_numeral(r, bv_sz);
else
mk_to_sbv_unspecified(f, result);
mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
return BR_DONE;
}

7
src/ast/rewriter/fpa_rewriter.h
View file

@ -86,10 +86,9 @@ public:
br_status mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result);
br_status mk_to_real(expr * arg, expr_ref & result);
br_status mk_to_ubv_unspecified(func_decl * f, expr_ref & result);
br_status mk_to_sbv_unspecified(func_decl * f, expr_ref & result);
br_status mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result);
br_status mk_to_real_unspecified(func_decl * f, expr_ref & result);
br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);
br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);
br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result);
};
#endif