From f4c8463619a2d5fdc7c827d3848b53c2b0f34c18 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Aug 2015 15:41:03 +0100 Subject: [PATCH] Bugfix for FP theory Fixes #207 --- src/smt/theory_fpa.cpp | 35 ++++++++++------------------------- 1 file changed, 10 insertions(+), 25 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 91e3883f6..c4407a011 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -581,22 +581,11 @@ namespace smt { expr_ref c(m); if (fu.is_float(xe) && fu.is_float(ye)) - { - TRACE("t_fpa_detail", tout << "xc=" << mk_ismt2_pp(xc, m) << std::endl; - tout << "yc=" << mk_ismt2_pp(yc, m) << std::endl;); - - expr *x_sgn, *x_sig, *x_exp; - m_converter.split_fp(xc, x_sgn, x_exp, x_sig); - expr *y_sgn, *y_sig, *y_exp; - m_converter.split_fp(yc, y_sgn, y_exp, y_sig); - - c = m.mk_eq(m_bv_util.mk_concat(m_bv_util.mk_concat(x_sgn, x_exp), x_sig), - m_bv_util.mk_concat(m_bv_util.mk_concat(y_sgn, y_exp), y_sig)); - } - else { - SASSERT(fu.is_rm(xe) && fu.is_rm(ye)); + m_converter.mk_eq(xc, yc, c); + else if (fu.is_rm(xe) && fu.is_rm(ye)) c = m.mk_eq(xc, yc); - } + else + UNREACHABLE(); m_th_rw(c); assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c)); @@ -631,18 +620,14 @@ namespace smt { expr_ref c(m); - if (fu.is_float(xe) && fu.is_float(ye)) - { - expr *x_sgn, *x_sig, *x_exp; - m_converter.split_fp(xc, x_sgn, x_exp, x_sig); - expr *y_sgn, *y_sig, *y_exp; - m_converter.split_fp(yc, y_sgn, y_exp, y_sig); - - c = m.mk_not(m.mk_eq(m_bv_util.mk_concat(m_bv_util.mk_concat(x_sgn, x_exp), x_sig), - m_bv_util.mk_concat(m_bv_util.mk_concat(y_sgn, y_exp), y_sig))); + if (fu.is_float(xe) && fu.is_float(ye)) { + m_converter.mk_eq(xc, yc, c); + c = m.mk_not(c); } - else + else if (fu.is_rm(xe) && fu.is_rm(ye)) c = m.mk_not(m.mk_eq(xc, yc)); + else + UNREACHABLE(); m_th_rw(c); assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));