mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Bugfixes for fp.min, fp.max.

Browse source 
Fixes the fix for #68
This commit is contained in:
Christoph M. Wintersteiger 2015-05-21 18:16:02 +01:00
parent 8c18bdcca9
commit eee076b9f8
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1072,7 +1072,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
result = y;
mk_ite(lt, x, result, result);
mk_ite(both_zero, pzero, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result);
@ -1102,7 +1102,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
result = y;
mk_ite(gt, x, result, result);
mk_ite(both_zero, pzero, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result);

8
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -412,7 +412,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
return BR_DONE;
}
if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
result = m_util.mk_pzero(m().get_sort(arg1));
result = arg2;
return BR_DONE;
}
@ -421,7 +421,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
m().mk_ite(mk_eq_nan(arg2),
arg1,
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
m_util.mk_pzero(m().get_sort(arg1)),
arg2,
m().mk_ite(m_util.mk_lt(arg1, arg2),
arg1,
arg2))));
@ -438,7 +438,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
return BR_DONE;
}
if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
result = m_util.mk_pzero(m().get_sort(arg1));
result = arg2;
return BR_DONE;
}
@ -447,7 +447,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
m().mk_ite(mk_eq_nan(arg2),
arg1,
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
m_util.mk_pzero(m().get_sort(arg1)),
arg2,
m().mk_ite(m_util.mk_gt(arg1, arg2),
arg1,
arg2))));