mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Added bool rewriter case.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-12 14:49:21 +00:00
parent 5cf2caa7e9
commit 5f8f0b1280
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/ast/rewriter/bool_rewriter.cpp
View file

@ -708,6 +708,19 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
result = m().mk_eq(lhs, rhs);
return BR_DONE;
}
expr *la, *lb, *ra, *rb;
// fold (iff (iff a b) (iff (not a) b)) to false
if (m().is_iff(lhs, la, lb) && m().is_iff(rhs, ra, rb)) {
expr *n;
if ((la == ra && ((m().is_not(rb, n) && n == lb) ||
(m().is_not(lb, n) && n == rb))) ||
(lb == rb && ((m().is_not(ra, n) && n == la) ||
(m().is_not(la, n) && n == ra)))) {
result = m().mk_false();
return BR_DONE;
}
}
}
return BR_FAILED;
}