From 713126225b6e729d41ad6a246af58f79342b10dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 28 May 2015 12:19:55 +0100 Subject: [PATCH] FPA min/max -+0.0 special cases changed to +0.0 instead of second argument. --- src/ast/fpa/fpa2bv_converter.cpp | 12 ++++++++++-- src/ast/rewriter/fpa_rewriter.cpp | 19 +++++++++++++++---- 2 files changed, 25 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 2c32e7f1a..d2d2c6a3f 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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(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(y, y_is_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_pzero(f, pzero); + expr_ref sgn_diff(m); + sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn)); + expr_ref lt(m); mk_float_lt(f, num, args, lt); result = y; mk_ite(lt, x, 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(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_pzero(f, pzero); + expr_ref sgn_diff(m); + sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn)); + expr_ref gt(m); mk_float_gt(f, num, args, gt); result = y; 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(x_is_nan, y, result, result); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 37c42b494..738e8ec29 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -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)) 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()); result = m_util.mk_value(v); return BR_DONE; @@ -420,11 +420,15 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { arg2, m().mk_ite(mk_eq_nan(arg2), 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)), arg2, m().mk_ite(m_util.mk_lt(arg1, arg2), arg1, - arg2)))); + arg2))))); 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), 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)), arg2, m().mk_ite(m_util.mk_gt(arg1, arg2), arg1, - arg2)))); + arg2))))); 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) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false(); 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) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false(); 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) { scoped_mpf v(m_fm); + if (m_util.is_numeral(arg1, v)) { result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false(); return BR_DONE;