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, 2 insertions, 10 deletions

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"); }
 };