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.

6 files changed, 118 insertions, 128 deletions

diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index c8a9b4dbd..0263ae017 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libbooleans.la
 libbooleans_la_SOURCES = \
 	theory_bool.h \
 	theory_bool.cpp \
-	theory_bool_type_rules.h
+	theory_bool_type_rules.h \
+	theory_bool_rewriter.h \
+	theory_bool_rewriter.cpp	
 
 EXTRA_DIST = kinds
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index ac6b05881..25ca1cfe3 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -4,7 +4,13 @@
 # src/theory/builtin/kinds.
 #
 
-theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h"
+theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h"
+
+properties finite  
+
+rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
+
+sort BOOLEAN_TYPE "Boolean type"
 
 constant CONST_BOOLEAN \
     bool \
@@ -19,3 +25,5 @@ operator IMPLIES 2 "logical implication"
 operator OR 2: "logical or"
 operator XOR 2 "exclusive or"
 operator ITE 3 "if-then-else"
+
+endtheory
\ No newline at end of file
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();
 
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index fa826539c..5d91842d7 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -30,8 +30,8 @@ namespace booleans {
 
 class TheoryBool : public Theory {
 public:
-  TheoryBool(int id, context::Context* c, OutputChannel& out) :
-    Theory(id, c, out) {
+  TheoryBool(context::Context* c, OutputChannel& out) :
+    Theory(THEORY_BOOL, c, out) {
   }
 
   void preRegisterTerm(TNode n) {
@@ -42,17 +42,9 @@ public:
     Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl;
     Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
   }
-  void check(Effort e) { Unimplemented(); }
-  void propagate(Effort e) { Unimplemented(); }
-  void explain(TNode n, Effort e) { Unimplemented(); }
-
-  void presolve(){ Unimplemented(); }
 
   Node getValue(TNode n, TheoryEngine* engine);
 
-  RewriteResponse preRewrite(TNode n, bool topLevel);
-  RewriteResponse postRewrite(TNode n, bool topLevel);
-
   std::string identify() const { return std::string("TheoryBool"); }
 };
 
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
new file mode 100644
index 000000000..a62bc6fa0
--- /dev/null
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -0,0 +1,72 @@
+#include <algorithm>
+#include "theory/booleans/theory_bool_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+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::IFF: {
+    // 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, n[1].notNode());
+    } else if(n[1] == ff) {
+      // IFF x false
+      return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+    } 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);
+    }
+    break;
+  }
+  case kind::ITE: {
+    // non-Boolean-valued ITEs should have been removed in place of
+    // a variable
+    Assert(n.getType().isBoolean());
+    // rewrite simple cases of ITE
+    if(n[0] == tt) {
+      // ITE true x y
+      return RewriteResponse(REWRITE_AGAIN, n[1]);
+    } else if(n[0] == ff) {
+      // ITE false x y
+      return RewriteResponse(REWRITE_AGAIN, n[2]);
+    } else if(n[1] == n[2]) {
+      // ITE c x x
+      return RewriteResponse(REWRITE_AGAIN, n[1]);
+    }
+    break;
+  }
+  default:
+    return RewriteResponse(REWRITE_DONE, n);
+  }
+  return RewriteResponse(REWRITE_DONE, n);
+}
+
+}
+}
+}
+
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
new file mode 100644
index 000000000..62eed9e2b
--- /dev/null
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -0,0 +1,32 @@
+/*
+ * theory_bool_rewriter.h
+ *
+ *  Created on: Dec 21, 2010
+ *      Author: dejan
+ */
+
+#pragma once
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+class TheoryBoolRewriter {
+
+public:
+
+  static RewriteResponse preRewrite(TNode node);
+  static RewriteResponse postRewrite(TNode node) {
+    return preRewrite(node);
+  }
+
+  static void init() {}
+  static void shutdown() {}
+
+};
+
+}
+}
+}