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

FPA min/max -+0.0 special cases changed to +0.0 instead of second argument.

Browse source 
Fixes #68
This commit is contained in:
Christoph M. Wintersteiger 2015-05-28 12:19:55 +01:00
parent 3d2ef8bb4a
commit 7619d609f9
2 changed files with 25 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1071,7 +1071,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
split_fp(x, x_sgn, x_exp, x_sig); split_fp(x, x_sgn, x_exp, x_sig);
split_fp(y, y_sgn, y_exp, y_sig); split_fp(y, y_sgn, y_exp, y_sig);
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);
mk_is_zero(x, x_is_zero); mk_is_zero(x, x_is_zero);
mk_is_zero(y, y_is_zero); mk_is_zero(y, y_is_zero);
m_simp.mk_and(x_is_zero, y_is_zero, both_zero); m_simp.mk_and(x_is_zero, y_is_zero, both_zero);
@ -1079,12 +1079,16 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
mk_is_nan(y, y_is_nan); mk_is_nan(y, y_is_nan);
mk_pzero(f, pzero); mk_pzero(f, pzero);
expr_ref sgn_diff(m);
sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn));
expr_ref lt(m); expr_ref lt(m);
mk_float_lt(f, num, args, lt); mk_float_lt(f, num, args, lt);
result = y; result = y;
mk_ite(lt, x, result, result); mk_ite(lt, x, result, result);
mk_ite(both_zero, y, result, result); mk_ite(both_zero, y, result, result);
mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
mk_ite(y_is_nan, x, result, result); mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result); mk_ite(x_is_nan, y, result, result);
@ -1109,12 +1113,16 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
mk_is_nan(y, y_is_nan); mk_is_nan(y, y_is_nan);
mk_pzero(f, pzero); mk_pzero(f, pzero);
expr_ref sgn_diff(m);
sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn));
expr_ref gt(m); expr_ref gt(m);
mk_float_gt(f, num, args, gt); mk_float_gt(f, num, args, gt);
result = y; result = y;
mk_ite(gt, x, result, result); mk_ite(gt, x, result, result);
mk_ite(both_zero, y, result, result); mk_ite(both_zero, y, result, result);
mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
mk_ite(y_is_nan, x, result, result); mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result); mk_ite(x_is_nan, y, result, result);

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

@ -243,7 +243,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
!m_util.au().is_numeral(args[2], r2)) !m_util.au().is_numeral(args[2], r2))
return BR_FAILED; return BR_FAILED;
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";); TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator()); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator());
result = m_util.mk_value(v); result = m_util.mk_value(v);
return BR_DONE; return BR_DONE;
@ -420,11 +420,15 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
arg2, arg2,
m().mk_ite(mk_eq_nan(arg2), m().mk_ite(mk_eq_nan(arg2),
arg1, arg1,
// min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2),
m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
m_util.mk_pzero(m().get_sort(arg1)),
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
arg2, arg2,
m().mk_ite(m_util.mk_lt(arg1, arg2), m().mk_ite(m_util.mk_lt(arg1, arg2),
arg1, arg1,
arg2)))); arg2)))));
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
@ -445,12 +449,16 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
result = m().mk_ite(mk_eq_nan(arg1), result = m().mk_ite(mk_eq_nan(arg1),
arg2, arg2,
m().mk_ite(mk_eq_nan(arg2), m().mk_ite(mk_eq_nan(arg2),
arg1, arg1,
// max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2),
m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
m_util.mk_pzero(m().get_sort(arg1)),
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
arg2, arg2,
m().mk_ite(m_util.mk_gt(arg1, arg2), m().mk_ite(m_util.mk_gt(arg1, arg2),
arg1, arg1,
arg2)))); arg2)))));
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
@ -583,6 +591,7 @@ br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) { if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false(); result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false();
return BR_DONE; return BR_DONE;
@ -593,6 +602,7 @@ br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) { if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false(); result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false();
return BR_DONE; return BR_DONE;
@ -603,6 +613,7 @@ br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm); scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) { if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false(); result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false();
return BR_DONE; return BR_DONE;