Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

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();