From 9a9f8bbb341be84285d31956b030e7c89f3641a4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 8 Oct 2013 20:01:39 +0100 Subject: [PATCH] rewriter and value recognition bugfixes for floats Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 21 +++++++++++++++++++++ src/ast/rewriter/float_rewriter.cpp | 4 ++-- 2 files changed, 23 insertions(+), 2 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 4aab6ab32..128dd2ce7 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -85,6 +85,24 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) { m_fm.set(val, m_values[to_app(n)->get_decl()->get_parameter(0).get_ext_id()]); return true; } + else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_INF)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_ninf(ebits, sbits, val); + return true; + } + else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_INF)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_pinf(ebits, sbits, val); + return true; + } + else if (is_app_of(n, m_family_id, OP_FLOAT_NAN)) { + unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int(); + unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int(); + m_fm.mk_nan(ebits, sbits, val); + return true; + } return false; } @@ -523,6 +541,9 @@ bool float_decl_plugin::is_value(app * e) const { case OP_RM_TOWARD_NEGATIVE: case OP_RM_TOWARD_ZERO: case OP_FLOAT_VALUE: + case OP_FLOAT_PLUS_INF: + case OP_FLOAT_MINUS_INF: + case OP_FLOAT_NAN: return true; case OP_TO_FLOAT: return m_manager->is_value(e->get_arg(0)); diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 0a4c3fc4e..4f8c90301 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -354,7 +354,7 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_minus_inf(arg1)) { // -oo < arg2 --> not(arg2 = -oo) and not(arg2 = NaN) result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2)); - return BR_REWRITE2; + return BR_REWRITE3; } if (m_util.is_minus_inf(arg2)) { // arg1 < -oo --> false @@ -369,7 +369,7 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_plus_inf(arg2)) { // arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN) result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1)); - return BR_REWRITE2; + return BR_REWRITE3; } scoped_mpf v1(m_util.fm()), v2(m_util.fm());