mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

FPA: min/max special cases fixed.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-05-01 14:08:53 +01:00
parent 7ce88d4da9
commit 65af658fd7
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -242,13 +242,13 @@ br_status float_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
return BR_DONE; return BR_DONE;
} }
// expand as using ite's // expand as using ite's
result = m().mk_ite(mk_eq_nan(arg1), result = m().mk_ite(m().mk_or(mk_eq_nan(arg1), m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2))),
arg2, arg2,
m().mk_ite(mk_eq_nan(arg2), m().mk_ite(mk_eq_nan(arg2),
arg1, arg1,
m().mk_ite(m_util.mk_lt(arg1, arg2), m().mk_ite(m_util.mk_lt(arg1, arg2),
arg1, arg1,
arg2))); arg2)));
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
@ -262,7 +262,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
return BR_DONE; return BR_DONE;
} }
// expand as using ite's // expand as using ite's
result = m().mk_ite(mk_eq_nan(arg1), result = m().mk_ite(m().mk_or(mk_eq_nan(arg1), m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2))),
arg2, arg2,
m().mk_ite(mk_eq_nan(arg2), m().mk_ite(mk_eq_nan(arg2),
arg1, arg1,