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, 17 deletions

diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index cce5ac6b8..baa1493b6 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -28,25 +28,10 @@ namespace theory {
 namespace builtin {
 
 class TheoryBuiltin : public Theory {
-  /** rewrite a DISTINCT expr */
-  static Node blastDistinct(TNode in);
-
 public:
-  TheoryBuiltin(int id, context::Context* c, OutputChannel& out) :
-    Theory(id, c, out) {
-  }
-
-  ~TheoryBuiltin() { }
-
-  void preRegisterTerm(TNode n) { Unreachable(); }
-  void registerTerm(TNode n) { Unreachable(); }
-  void check(Effort e) { Unreachable(); }
-  void propagate(Effort e) { Unreachable(); }
-  void explain(TNode n, Effort e) { Unreachable(); }
-  void presolve() { Unreachable(); }
+  TheoryBuiltin(context::Context* c, OutputChannel& out) :
+    Theory(THEORY_BUILTIN, c, out) {}
   Node getValue(TNode n, TheoryEngine* engine);
-  void shutdown() { }
-  RewriteResponse preRewrite(TNode n, bool topLevel);
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */