mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

Bugfix for ITEs over FP rounding modes.

Browse source 
Fixes #751.
This commit is contained in:
Christoph M. Wintersteiger 2016-10-04 18:04:56 +01:00
parent 0bd06930ae
commit acdaeca826
2 changed files with 22 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -90,19 +90,28 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
}
void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
SASSERT(m_util.is_fp(t) && m_util.is_fp(f));
if (m_util.is_fp(t) && m_util.is_fp(f)) {
expr *t_sgn, *t_sig, *t_exp;
expr *f_sgn, *f_sig, *f_exp;
split_fp(t, t_sgn, t_exp, t_sig);
split_fp(f, f_sgn, f_exp, f_sig);
expr *t_sgn, *t_sig, *t_exp;
expr *f_sgn, *f_sig, *f_exp;
split_fp(t, t_sgn, t_exp, t_sig);
split_fp(f, f_sgn, f_exp, f_sig);
expr_ref sgn(m), s(m), e(m);
m_simp.mk_ite(c, t_sgn, f_sgn, sgn);
m_simp.mk_ite(c, t_sig, f_sig, s);
m_simp.mk_ite(c, t_exp, f_exp, e);
expr_ref sgn(m), s(m), e(m);
m_simp.mk_ite(c, t_sgn, f_sgn, sgn);
m_simp.mk_ite(c, t_sig, f_sig, s);
m_simp.mk_ite(c, t_exp, f_exp, e);
result = m_util.mk_fp(sgn, e, s);
result = m_util.mk_fp(sgn, e, s);
}
else if (m_util.is_rm(t) && m_util.is_rm(f))
{
SASSERT(m_util.is_bv2rm(t) && m_util.is_bv2rm(f));
TRACE("fpa2bv", tout << "ite rm: t=" << mk_ismt2_pp(t, m) << " f=" << mk_ismt2_pp(f, m) << std::endl; );
m_simp.mk_ite(c, to_app(t)->get_arg(0), to_app(f)->get_arg(0), result);
result = m_util.mk_bv2rm(result);
}
else
UNREACHABLE();
}
void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {

4
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -86,10 +86,10 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
return BR_DONE;
}
return BR_FAILED;
}
}
else if (m().is_ite(f)) {
SASSERT(num == 3);
if (m_conv.is_float(args[1])) {
if (m_conv.is_float(args[1]) || m_conv.is_rm(args[1])) {
m_conv.mk_ite(args[0], args[1], args[2], result);
return BR_DONE;
}