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

disabled "hardware interpretation" of fp.min/fp.max because the unspecified, standard-compliant behaviour is cheap anyways.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-11 12:51:37 +00:00
parent b5279d1da8
commit 3e61ee2331
1 changed files with 50 additions and 58 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1155,38 +1155,34 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
expr_ref res(m);
// The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
// There is no "hardware interpretation" for fp.min.
if (m_hi_fp_unspecified)
// The hardware interpretation is -0.0.
mk_nzero(f, res);
else {
std::pair<app*, app*> decls(0, 0);
if (!m_specials.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_specials.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
std::pair<app*, app*> decls(0, 0);
if (!m_specials.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_specials.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
return res;
}
@ -1244,38 +1240,34 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
expr_ref res(m);
// The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
// There is no "hardware interpretation" for fp.max.
if (m_hi_fp_unspecified)
// The hardware interpretation is +0.0.
mk_pzero(f, res);
else {
std::pair<app*, app*> decls(0, 0);
if (!m_specials.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_specials.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
std::pair<app*, app*> decls(0, 0);
if (!m_specials.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_specials.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
return res;
}