From 5f8f0b128022790bc6e4402c4a5671404cd92891 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:49:21 +0000 Subject: [PATCH] Added bool rewriter case. --- src/ast/rewriter/bool_rewriter.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 6dec03307..0b8a51fb4 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -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; }