Merging the satliteral-before-prereg branch into trunk. Theory preregistration is now called during the conversion to cnf. This fixes bug 257.

4 files changed, 37 insertions, 4 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index a9ff5376d..b72502eca 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -19,6 +19,7 @@ libtheory_la_SOURCES = \
 	shared_term_manager.cpp \
 	shared_data.h \
 	shared_data.cpp \
+	registrar.h \
 	rewriter.h \
 	rewriter_attributes.h \
 	rewriter.cpp \
diff --git a/src/theory/registrar.h b/src/theory/registrar.h
new file mode 100644
index 000000000..ce3a301d7
--- /dev/null
+++ b/src/theory/registrar.h
@@ -0,0 +1,31 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_REGISTRAR_H
+#define __CVC4__THEORY_REGISTRAR_H
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+class Registrar {
+private:
+  TheoryEngine* d_theoryEngine;
+
+public:
+  Registrar() : d_theoryEngine(NULL){ }
+
+  Registrar(TheoryEngine* te) : d_theoryEngine(te){ }
+
+  void preRegister(Node n){
+    if(d_theoryEngine != NULL){
+      d_theoryEngine->preRegister(n);
+    }
+  }
+
+};/* class Registrar */
+
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY_REGISTRAR_H */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d1040e6fc..aa70a9bda 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -162,13 +162,15 @@ struct preprocess_stack_element {
 };
 
 Node TheoryEngine::preprocess(TNode node) {
-
   // Remove ITEs and rewrite the node
   Node preprocessed = Rewriter::rewrite(removeITEs(node));
+  return preprocessed;
+}
 
+void TheoryEngine::preRegister(TNode preprocessed) {
   // If we are pre-registered already we are done
   if (preprocessed.getAttribute(PreRegistered())) {
-    return preprocessed;
+    return;
   }
 
   // Do a topological sort of the subexpressions and preregister them
@@ -223,8 +225,6 @@ Node TheoryEngine::preprocess(TNode node) {
       }
     }
   }
-
-  return preprocessed;
 }
 
 /**
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index be2e6e271..2e12d3a16 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -247,6 +247,7 @@ public:
    * @param n the node to preprocess
    */
   Node preprocess(TNode n);
+  void preRegister(TNode preprocessed);
 
   /**
    * Assert the formula to the appropriate theory.