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

1 files changed, 31 insertions, 0 deletions

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 */