Substantial Changes:

-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default.  This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.

- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.

- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.

- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.

- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.

Minor Changes:

- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.

- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.

-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.

- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)

2 files changed, 102 insertions, 20 deletions

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 9867ccd4e..1caa4b429 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -22,6 +22,10 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
+RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) {
+  return preRewrite(node);
+}
+
 /**
  * flattenNode looks for children of same kind, and if found merges
  * them into the parent.
@@ -88,6 +92,40 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
   }
 }
 
+// Equality parity returns
+// * 0 if no relation between a and b is found
+// * 1 if a == b
+// * 2 if a == not(b)
+// * 3 or b == not(a)
+inline int equalityParity(TNode a, TNode b){
+  if(a == b){
+    return 1;
+  }else if(a.getKind() == kind::NOT && a[0] == b){
+    return 2;
+  }else if(b.getKind() == kind::NOT && b[0] == a){
+    return 3;
+  }else{
+    return 0;
+  }
+}
+
+inline Node makeNegation(TNode n){
+  bool even = false;
+  while(n.getKind() == kind::NOT){
+    n = n[0];
+    even = !even;
+  }
+  if(even){
+    return n;
+  } else {
+    if(n.isConst()){
+      return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
+    }else{
+      return n.notNode();
+    }
+  }
+}
+
 RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
   NodeManager* nodeManager = NodeManager::currentNM();
   Node tt = nodeManager->mkConst(true);
@@ -132,7 +170,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
     if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff);
     if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
-    if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+    if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
     break;
   }
   case kind::IFF:
@@ -146,10 +184,10 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
       return RewriteResponse(REWRITE_AGAIN, n[0]);
     } else if(n[0] == ff) {
       // IFF false x
-      return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
     } else if(n[1] == ff) {
       // IFF x false
-      return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
     } else if(n[0] == n[1]) {
       // IFF x x
       return RewriteResponse(REWRITE_DONE, tt);
@@ -207,7 +245,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
           if(kappa.knownLessThanOrEqual(two)){
             return RewriteResponse(REWRITE_DONE, ff);
           }else{
-            Node neitherEquality = (n[0].notNode()).andNode(n[1].notNode());
+            Node neitherEquality = (makeNegation(n[0])).andNode(makeNegation(n[1]));
             return RewriteResponse(REWRITE_AGAIN, neitherEquality);
           }
         }
@@ -219,10 +257,10 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     // rewrite simple cases of XOR
     if(n[0] == tt) {
       // XOR true x
-      return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
     } else if(n[1] == tt) {
       // XCR x true
-      return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
     } else if(n[0] == ff) {
       // XOR false x
       return RewriteResponse(REWRITE_AGAIN, n[1]);
@@ -248,33 +286,79 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (n[0].isConst()) {
       if (n[0] == tt) {
         // ITE true x y
+
+        Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[1]);
       } else {
         Assert(n[0] == ff);
         // ITE false x y
+        Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[2]);
       }
     } else if (n[1].isConst()) {
       if (n[1] == tt && n[2] == ff) {
+        Debug("bool-ite") << "n[1] ==tt && n[2] == ff " << n << ": " << n[0] << std::endl;
         return RewriteResponse(REWRITE_AGAIN, n[0]);
       }
       else if (n[1] == ff && n[2] == tt) {
-        return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+        Debug("bool-ite") << "n[1] ==ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl;
+        return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
       }
+      // else if(n[1] == ff){
+      //   Node resp = (n[0].notNode()).andNode(n[2]);
+      //   return RewriteResponse(REWRITE_AGAIN, resp);
+      // }
     }
-    if (n[1] == n[2]) {
-      return RewriteResponse(REWRITE_AGAIN, n[1]);
+    // else if (n[2].isConst()) {
+    //   if(n[2] == ff){
+    //     Node resp = (n[0]).andNode(n[1]);
+    //     return RewriteResponse(REWRITE_AGAIN, resp);
+    //   }
+    // }
+
+    int parityTmp;
+    if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
+      Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].iffNode(n[1]);
+      Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
     // Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now
     // } else if (n[0].getKind() == kind::NOT) {
     //   return RewriteResponse(REWRITE_AGAIN, n[0][0].iteNode(n[2], n[1]));
-    } else if (n[0] == n[1]) {
-      return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(tt, n[2]));
-    } else if (n[0] == n[2]) {
-      return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], ff));
-    } else if (n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
-      return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(ff, n[2]));
-    } else if (n[2].getKind() == kind::NOT && n[2][0] == n[0]) {
-      return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], tt));
+    } else if(!n[1].isConst() && (parityTmp = equalityParity(n[0], n[1])) != 0){
+      // (parityTmp == 1) if n[0] == n[1]
+      // otherwise, n[0] == not(n[1]) or not(n[0]) == n[1]
+
+      // if n[1] is constant this can loop, this is possible in prewrite
+      Node resp = n[0].iteNode( (parityTmp == 1) ? tt : ff, n[2]);
+      Debug("bool-ite") << "equalityParity n[0], n[1] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    } else if(!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0){
+      // (parityTmp == 1) if n[0] == n[2]
+      // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2]
+      Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt);
+      Debug("bool-ite") << "equalityParity n[0], n[2] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    } else if(n[1].getKind() == kind::ITE &&
+              (parityTmp = equalityParity(n[0], n[1][0])) != 0){
+      // (parityTmp == 1) then n : (ite c (ite c x y) z)
+      // (parityTmp > 1)  then n : (ite c (ite (not c) x y) z) or
+      // n: (ite (not c) (ite c x y) z)
+      Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]);
+      Debug("bool-ite") << "equalityParity n[0], n[1][0] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    } else if(n[2].getKind() == kind::ITE &&
+              (parityTmp = equalityParity(n[0], n[2][0])) != 0){
+      // (parityTmp == 1) then n : (ite c x (ite c y z))
+      // (parityTmp > 1)  then n : (ite c x (ite (not c) y z)) or
+      // n: (ite (not c) x (ite c y z))
+      Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]);
+      Debug("bool-ite") << "equalityParity n[0], n[2][0] " << parityTmp
+                        << " " << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
     }
     break;
   }
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index 96bd2ae29..ac9469980 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -31,9 +31,7 @@ class TheoryBoolRewriter {
 public:
 
   static RewriteResponse preRewrite(TNode node);
-  static RewriteResponse postRewrite(TNode node) {
-    return preRewrite(node);
-  }
+  static RewriteResponse postRewrite(TNode node);
 
   static void init() {}
   static void shutdown() {}