1 files changed, 0 insertions, 116 deletions
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index b1ff472ac..f8071d45d 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -24,122 +24,6 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) {
-  if(n.getKind() == kind::IFF) {
-    NodeManager* nodeManager = NodeManager::currentNM();
-    Node tt = nodeManager->mkConst(true);
-    Node ff = nodeManager->mkConst(false);
-
-    // rewrite simple cases of IFF
-    if(n[0] == tt) {
-      // IFF true x
-      return RewriteAgain(n[1]);
-    } else if(n[1] == tt) {
-      // IFF x true
-      return RewriteAgain(n[0]);
-    } else if(n[0] == ff) {
-      // IFF false x
-      return RewriteAgain(n[1].notNode());
-    } else if(n[1] == ff) {
-      // IFF x false
-      return RewriteAgain(n[0].notNode());
-    } else if(n[0] == n[1]) {
-      // IFF x x
-      return RewriteComplete(tt);
-    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
-      // IFF (NOT x) x
-      return RewriteComplete(ff);
-    } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
-      // IFF x (NOT x)
-      return RewriteComplete(ff);
-    }
-  } else if(n.getKind() == kind::ITE) {
-    // non-Boolean-valued ITEs should have been removed in place of
-    // a variable
-    Assert(n.getType().isBoolean());
-
-    NodeManager* nodeManager = NodeManager::currentNM();
-
-    // rewrite simple cases of ITE
-    if(n[0] == nodeManager->mkConst(true)) {
-      // ITE true x y
-      return RewriteAgain(n[1]);
-    } else if(n[0] == nodeManager->mkConst(false)) {
-      // ITE false x y
-      return RewriteAgain(n[2]);
-    } else if(n[1] == n[2]) {
-      // ITE c x x
-      return RewriteAgain(n[1]);
-    }
-  }
-
-  return RewriteComplete(n);
-}
-
-
-RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) {
-  if(n.getKind() == kind::IFF) {
-    NodeManager* nodeManager = NodeManager::currentNM();
-    Node tt = nodeManager->mkConst(true);
-    Node ff = nodeManager->mkConst(false);
-
-    // rewrite simple cases of IFF
-    if(n[0] == tt) {
-      // IFF true x
-      return RewriteComplete(n[1]);
-    } else if(n[1] == tt) {
-      // IFF x true
-      return RewriteComplete(n[0]);
-    } else if(n[0] == ff) {
-      // IFF false x
-      return RewriteAgain(n[1].notNode());
-    } else if(n[1] == ff) {
-      // IFF x false
-      return RewriteAgain(n[0].notNode());
-    } else if(n[0] == n[1]) {
-      // IFF x x
-      return RewriteComplete(tt);
-    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
-      // IFF (NOT x) x
-      return RewriteComplete(ff);
-    } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
-      // IFF x (NOT x)
-      return RewriteComplete(ff);
-    }
-
-    if(n[1] < n[0]) {
-      // normalize (IFF x y) ==> (IFF y x), if y < x
-      return RewriteComplete(n[1].iffNode(n[0]));
-    }
-  } else if(n.getKind() == kind::ITE) {
-    // non-Boolean-valued ITEs should have been removed in place of
-    // a variable
-    Assert(n.getType().isBoolean());
-
-    NodeManager* nodeManager = NodeManager::currentNM();
-
-    // rewrite simple cases of ITE
-    if(n[0] == nodeManager->mkConst(true)) {
-      // ITE true x y
-      return RewriteComplete(n[1]);
-    } else if(n[0] == nodeManager->mkConst(false)) {
-      // ITE false x y
-      return RewriteComplete(n[2]);
-    } else if(n[1] == n[2]) {
-      // ITE c x x
-      return RewriteComplete(n[1]);
-    }
-
-    if(n[0].getKind() == kind::NOT) {
-      // rewrite  (ITE (NOT c) x y)  to  (ITE c y x)
-      Node out = nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]);
-      return RewriteComplete(out);
-    }
-  }
-
-  return RewriteComplete(n);
-}
-
 Node TheoryBool::getValue(TNode n, TheoryEngine* engine) {
   NodeManager* nodeManager = NodeManager::currentNM();