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

Bugfix for FP theory

Browse source 
Fixes #207
This commit is contained in:
Christoph M. Wintersteiger 2015-08-28 15:41:03 +01:00
parent 81eecafa66
commit f4c8463619
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);
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));