1 files changed, 343 insertions, 221 deletions

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index c53610efa..b13cb82b3 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -25,10 +25,30 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) {
-  return preRewrite(node);
+void TheoryBoolRewriter::registerRewrites(Rewriter* rewriter)
+{
+  rewriter->registerPreRewrite(kind::CONST_BOOLEAN, identityRewrite);
+  rewriter->registerPostRewrite(kind::CONST_BOOLEAN, identityRewrite);
+  rewriter->registerPreRewrite(kind::NOT, rewriteNot);
+  rewriter->registerPostRewrite(kind::NOT, rewriteNot);
+  rewriter->registerPreRewrite(kind::OR, rewriteOr);
+  rewriter->registerPostRewrite(kind::OR, rewriteOr);
+  rewriter->registerPreRewrite(kind::AND, rewriteAnd);
+  rewriter->registerPostRewrite(kind::AND, rewriteAnd);
+  rewriter->registerPreRewrite(kind::IMPLIES, rewriteImplies);
+  rewriter->registerPostRewrite(kind::IMPLIES, rewriteImplies);
+  rewriter->registerPreRewrite(kind::XOR, rewriteXor);
+  rewriter->registerPostRewrite(kind::XOR, rewriteXor);
+  rewriter->registerPreRewrite(kind::ITE, rewriteIte);
+  rewriter->registerPostRewrite(kind::ITE, rewriteIte);
+  rewriter->registerPreRewriteEqual(THEORY_BOOL, rewriteEqual);
+  rewriter->registerPostRewriteEqual(THEORY_BOOL, rewriteEqual);
 }
 
+RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { Unreachable(); }
+
+RewriteResponse TheoryBoolRewriter::postRewrite(TNode n) { Unreachable(); }
+
 /**
  * flattenNode looks for children of same kind, and if found merges
  * them into the parent.
@@ -134,243 +154,345 @@ inline Node makeNegation(TNode n){
   }
 }
 
-RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
-  NodeManager* nodeManager = NodeManager::currentNM();
-  Node tt = nodeManager->mkConst(true);
-  Node ff = nodeManager->mkConst(false);
-
-  switch(n.getKind()) {
-  case kind::NOT: {
-    if (n[0] == tt) return RewriteResponse(REWRITE_DONE, ff);
-    if (n[0] == ff) return RewriteResponse(REWRITE_DONE, tt);
-    if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]);
-    break;
-  }
-  case kind::OR: {
-    bool done = true;
-    TNode::iterator i = n.begin(), iend = n.end();
-    for(; i != iend; ++i) {
-      if (*i == tt) return RewriteResponse(REWRITE_DONE, tt);
-      if (*i == ff) done = false;
-      if ((*i).getKind() == kind::OR) done = false;
-    }
-    if (!done) {
-      return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff);
-    }
-    break;
-  }
-  case kind::AND: {
-    bool done = true;
-    TNode::iterator i = n.begin(), iend = n.end();
-    for(; i != iend; ++i) {
-      if (*i == ff) return RewriteResponse(REWRITE_DONE, ff);
-      if (*i == tt) done = false;
-      if ((*i).getKind() == kind::AND) done = false;
+RewriteResponse TheoryBoolRewriter::rewriteNot(RewriteEnvironment* re, TNode n)
+{
+  NodeManager* nm = re->getNodeManager();
+  Node tt = nm->mkConst(true);
+  Node ff = nm->mkConst(false);
+
+  if (n[0] == tt) return RewriteResponse(REWRITE_DONE, ff);
+  if (n[0] == ff) return RewriteResponse(REWRITE_DONE, tt);
+  if (n[0].getKind() == kind::NOT)
+    return RewriteResponse(REWRITE_AGAIN, n[0][0]);
+
+  return RewriteResponse(REWRITE_DONE, n);
+}
+
+RewriteResponse TheoryBoolRewriter::rewriteOr(RewriteEnvironment* re, TNode n)
+{
+  NodeManager* nm = re->getNodeManager();
+  Node tt = nm->mkConst(true);
+  Node ff = nm->mkConst(false);
+
+  bool done = true;
+  TNode::iterator i = n.begin(), iend = n.end();
+  for (; i != iend; ++i)
+  {
+    if (*i == tt) return RewriteResponse(REWRITE_DONE, tt);
+    if (*i == ff) done = false;
+    if ((*i).getKind() == kind::OR) done = false;
+  }
+  if (!done)
+  {
+    return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff);
+  }
+
+  return RewriteResponse(REWRITE_DONE, n);
+}
+
+RewriteResponse TheoryBoolRewriter::rewriteAnd(RewriteEnvironment* re, TNode n)
+{
+  NodeManager* nm = re->getNodeManager();
+  Node tt = nm->mkConst(true);
+  Node ff = nm->mkConst(false);
+
+  bool done = true;
+  TNode::iterator i = n.begin(), iend = n.end();
+  for (; i != iend; ++i)
+  {
+    if (*i == ff) return RewriteResponse(REWRITE_DONE, ff);
+    if (*i == tt) done = false;
+    if ((*i).getKind() == kind::AND) done = false;
+  }
+  if (!done)
+  {
+    RewriteResponse ret =
+        flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt);
+    Debug("bool-flatten") << n << ": " << ret.node << std::endl;
+    return ret;
+  }
+
+  return RewriteResponse(REWRITE_DONE, n);
+}
+
+RewriteResponse TheoryBoolRewriter::rewriteImplies(RewriteEnvironment* re,
+                                                   TNode n)
+{
+  NodeManager* nm = re->getNodeManager();
+  Node tt = nm->mkConst(true);
+  Node ff = nm->mkConst(false);
+
+  if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
+  if (n[0] == tt && n[1] == ff) return RewriteResponse(REWRITE_DONE, ff);
+  if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
+  if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
+  return RewriteResponse(REWRITE_DONE, n);
+}
+
+RewriteResponse TheoryBoolRewriter::rewriteEqual(RewriteEnvironment* re,
+                                                 TNode n)
+{
+  NodeManager* nm = re->getNodeManager();
+  Node tt = nm->mkConst(true);
+  Node ff = nm->mkConst(false);
+
+  // rewrite simple cases of IFF
+  if (n[0] == tt)
+  {
+    // IFF true x
+    return RewriteResponse(REWRITE_AGAIN, n[1]);
+  }
+  else if (n[1] == tt)
+  {
+    // IFF x true
+    return RewriteResponse(REWRITE_AGAIN, n[0]);
+  }
+  else if (n[0] == ff)
+  {
+    // IFF false x
+    return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
+  }
+  else if (n[1] == ff)
+  {
+    // IFF x false
+    return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
+  }
+  else if (n[0] == n[1])
+  {
+    // IFF x x
+    return RewriteResponse(REWRITE_DONE, tt);
+  }
+  else if (n[0].getKind() == kind::NOT && n[0][0] == n[1])
+  {
+    // IFF (NOT x) x
+    return RewriteResponse(REWRITE_DONE, ff);
+  }
+  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)
+  {
+    // a : (= i x)
+    // i : (= j k)
+    // x : (= y z)
+
+    // assume wlog k, z are constants and j is the same symbol as y
+    // (iff (= j k) (= j z))
+    // if k = z
+    //  then (iff (= j k) (= j k)) => true
+    // else
+    //  (iff (= j k) (= j z)) <=> b
+    //  b : (and (not (= j k)) (not (= j z)))
+    //  (= j k) (= j z) | a b
+    //  f       f       | t t
+    //  f       t       | f f
+    //  t       f       | f f
+    //  t       t       | * f
+    // * j cannot equal both k and z in a theory model
+    TNode t, c;
+    if (n[0][0].isConst())
+    {
+      c = n[0][0];
+      t = n[0][1];
     }
-    if (!done) {
-      RewriteResponse ret = flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt);
-      Debug("bool-flatten") << n << ": " << ret.node << std::endl;
-      return ret;
+    else if (n[0][1].isConst())
+    {
+      c = n[0][1];
+      t = n[0][0];
     }
-    break;
-  }
-  case kind::IMPLIES: {
-    if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
-    if (n[0] == tt && n[1] == ff) return RewriteResponse(REWRITE_DONE, ff);
-    if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
-    if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
-    break;
-  }
-  case kind::EQUAL: {
-    // rewrite simple cases of IFF
-    if(n[0] == tt) {
-      // IFF true x
-      return RewriteResponse(REWRITE_AGAIN, n[1]);
-    } else if(n[1] == tt) {
-      // IFF x true
-      return RewriteResponse(REWRITE_AGAIN, n[0]);
-    } else if(n[0] == ff) {
-      // IFF false x
-      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
-    } else if(n[1] == ff) {
-      // IFF x false
-      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
-    } else if(n[0] == n[1]) {
-      // IFF x x
-      return RewriteResponse(REWRITE_DONE, tt);
-    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
-      // IFF (NOT x) x
-      return RewriteResponse(REWRITE_DONE, ff);
-    } 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) {
-      // a : (= i x)
-      // i : (= j k)
-      // x : (= y z)
-
-      // assume wlog k, z are constants and j is the same symbol as y
-      // (iff (= j k) (= j z))
-      // if k = z
-      //  then (iff (= j k) (= j k)) => true
-      // else
-      //  (iff (= j k) (= j z)) <=> b
-      //  b : (and (not (= j k)) (not (= j z)))
-      //  (= j k) (= j z) | a b
-      //  f       f       | t t
-      //  f       t       | f f
-      //  t       f       | f f
-      //  t       t       | * f
-      // * j cannot equal both k and z in a theory model
-      TNode t,c;
-      if (n[0][0].isConst()) {
-        c = n[0][0];
-        t = n[0][1];
+    bool matchesForm = false;
+    bool constantsEqual = false;
+    if (!c.isNull())
+    {
+      if (n[1][0] == t && n[1][1].isConst())
+      {
+        matchesForm = true;
+        constantsEqual = (n[1][1] == c);
       }
-      else if (n[0][1].isConst()) {
-        c = n[0][1];
-        t = n[0][0];
+      else if (n[1][1] == t && n[1][0].isConst())
+      {
+        matchesForm = true;
+        constantsEqual = (n[1][0] == c);
       }
-      bool matchesForm = false;
-      bool constantsEqual = false;
-      if (!c.isNull()) {
-        if (n[1][0] == t && n[1][1].isConst()) {
-          matchesForm = true;
-          constantsEqual = (n[1][1] == c);
-        }
-        else if (n[1][1] == t && n[1][0].isConst()) {
-          matchesForm = true;
-          constantsEqual = (n[1][0] == c);
-        }
+    }
+    if (matchesForm)
+    {
+      if (constantsEqual)
+      {
+        return RewriteResponse(REWRITE_DONE, tt);
       }
-      if(matchesForm){
-        if(constantsEqual){
-          return RewriteResponse(REWRITE_DONE, tt);
-        }else{
-          Cardinality kappa = t.getType().getCardinality();
-          Cardinality two(2l);
-          if(kappa.knownLessThanOrEqual(two)){
-            return RewriteResponse(REWRITE_DONE, ff);
-          }else{
-            Node neitherEquality = (makeNegation(n[0])).andNode(makeNegation(n[1]));
-            return RewriteResponse(REWRITE_AGAIN, neitherEquality);
-          }
+      else
+      {
+        Cardinality kappa = t.getType().getCardinality();
+        Cardinality two(2l);
+        if (kappa.knownLessThanOrEqual(two))
+        {
+          return RewriteResponse(REWRITE_DONE, ff);
+        }
+        else
+        {
+          Node neitherEquality =
+              (makeNegation(n[0])).andNode(makeNegation(n[1]));
+          return RewriteResponse(REWRITE_AGAIN, neitherEquality);
         }
       }
     }
-    break;
-  }
-  case kind::XOR: {
-    // rewrite simple cases of XOR
-    if(n[0] == tt) {
-      // XOR true x
-      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
-    } else if(n[1] == tt) {
-      // XOR x true
-      return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
-    } else if(n[0] == ff) {
-      // XOR false x
+  }
+
+  return RewriteResponse(REWRITE_DONE, n);
+}
+
+RewriteResponse TheoryBoolRewriter::rewriteXor(RewriteEnvironment* re, TNode n)
+{
+  NodeManager* nm = re->getNodeManager();
+  Node tt = nm->mkConst(true);
+  Node ff = nm->mkConst(false);
+
+  // rewrite simple cases of XOR
+  if (n[0] == tt)
+  {
+    // XOR true x
+    return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
+  }
+  else if (n[1] == tt)
+  {
+    // XOR x true
+    return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
+  }
+  else if (n[0] == ff)
+  {
+    // XOR false x
+    return RewriteResponse(REWRITE_AGAIN, n[1]);
+  }
+  else if (n[1] == ff)
+  {
+    // XOR x false
+    return RewriteResponse(REWRITE_AGAIN, n[0]);
+  }
+  else if (n[0] == n[1])
+  {
+    // XOR x x
+    return RewriteResponse(REWRITE_DONE, ff);
+  }
+  else if (n[0].getKind() == kind::NOT && n[0][0] == n[1])
+  {
+    // XOR (NOT x) x
+    return RewriteResponse(REWRITE_DONE, tt);
+  }
+  else if (n[1].getKind() == kind::NOT && n[1][0] == n[0])
+  {
+    // XOR x (NOT x)
+    return RewriteResponse(REWRITE_DONE, tt);
+  }
+  return RewriteResponse(REWRITE_DONE, n);
+}
+
+RewriteResponse TheoryBoolRewriter::rewriteIte(RewriteEnvironment* re, TNode n)
+{
+  NodeManager* nm = re->getNodeManager();
+  Node tt = nm->mkConst(true);
+  Node ff = nm->mkConst(false);
+
+  // non-Boolean-valued ITEs should have been removed in place of
+  // a variable
+  // rewrite simple cases of ITE
+  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 if(n[1] == ff) {
-      // XOR x false
+    }
+    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[0] == n[1]) {
-      // XOR x x
-      return RewriteResponse(REWRITE_DONE, ff);
-    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
-      // XOR (NOT x) x
-      return RewriteResponse(REWRITE_DONE, tt);
-    } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
-      // XOR x (NOT x)
-      return RewriteResponse(REWRITE_DONE, tt);
     }
-    break;
-  }
-  case kind::ITE: {
-    // non-Boolean-valued ITEs should have been removed in place of
-    // a variable
-    // rewrite simple cases of ITE
-    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) {
-        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);
-      // }
+    else if (n[1] == ff && n[2] == tt)
+    {
+      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[2].isConst()) {
-    //   if(n[2] == ff){
-    //     Node resp = (n[0]).andNode(n[1]);
-    //     return RewriteResponse(REWRITE_AGAIN, resp);
-    //   }
+    // else if(n[1] ==ff){
+    //   Node resp = (n[0].notNode()).andNode(n[2]);
+    //   return RewriteResponse(REWRITE_AGAIN, resp);
     // }
+  }
+  // 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].eqNode(n[1]);
-      Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp
-                        << " " << n << ": " << resp << std::endl;
-      return RewriteResponse(REWRITE_AGAIN, resp);
+  int parityTmp;
+  if ((parityTmp = equalityParity(n[1], n[2])) != 0)
+  {
+    Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(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[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;
   }
-  default:
-    return RewriteResponse(REWRITE_DONE, n);
+  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);
   }
   return RewriteResponse(REWRITE_DONE, n);
 }