From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 14 Mar 2013 00:37:57 +0000 (-0400)
Subject: Added a rewrite for iff:
X-Git-Tag: cvc5-1.0.0~7394
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c03a972a85d565f10953ee58ec809f1751063f8e;p=cvc5.git

Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.
---

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 567a8dd70..2fa2e095a 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -118,6 +118,24 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
       // IFF x (NOT x)
       return RewriteResponse(REWRITE_DONE, ff);
+    } else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) {
+      TNode t,c;
+      if (n[0][0].isConst()) {
+        c = n[0][0];
+        t = n[0][1];
+      }
+      else if (n[0][1].isConst()) {
+        c = n[0][1];
+        t = n[0][0];
+      }
+      if (!c.isNull()) {
+        if (n[1][0] == t && n[1][1].isConst()) {
+          return RewriteResponse(REWRITE_DONE, n[1][1] == c ? tt : ff);
+        }
+        else if (n[1][1] == t && n[1][0].isConst()) {
+          return RewriteResponse(REWRITE_DONE, n[1][0] == c ? tt : ff);
+        }
+      }
     }
     break;
   }