mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-08-28 20:25:40 -07:00
parent 2fe0c05556 8feed01034
commit 0bc45ca250
1 changed files with 10 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/smt/theory_fpa.cpp
View file

@ -581,22 +581,11 @@ namespace smt {
expr_ref c(m); expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye)) if (fu.is_float(xe) && fu.is_float(ye))
{ m_converter.mk_eq(xc, yc, c);
TRACE("t_fpa_detail", tout << "xc=" << mk_ismt2_pp(xc, m) << std::endl; else if (fu.is_rm(xe) && fu.is_rm(ye))
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));
c = m.mk_eq(xc, yc); c = m.mk_eq(xc, yc);
} else
UNREACHABLE();
m_th_rw(c); m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c)); assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
@ -631,18 +620,14 @@ namespace smt {
expr_ref c(m); expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye)) if (fu.is_float(xe) && fu.is_float(ye)) {
{ m_converter.mk_eq(xc, yc, c);
expr *x_sgn, *x_sig, *x_exp; c = m.mk_not(c);
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)));
} }
else else if (fu.is_rm(xe) && fu.is_rm(ye))
c = m.mk_not(m.mk_eq(xc, yc)); c = m.mk_not(m.mk_eq(xc, yc));
else
UNREACHABLE();
m_th_rw(c); m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c)); assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));