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

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 9d152a915..929cae346 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -29,6 +29,7 @@
 
 #include "expr/node.h"
 #include "prop/sat.h"
+#include "theory/registrar.h"
 
 #include <ext/hash_map>
 
@@ -70,6 +71,8 @@ private:
 
 protected:
 
+  theory::Registrar d_registrar;
+
   /** Top level nodes that we translated */
   std::vector<TNode> d_translationTrail;
 
@@ -177,7 +180,7 @@ public:
    * set of clauses and sends them to the given sat solver.
    * @param satSolver the sat solver to use
    */
-  CnfStream(SatInputInterface* satSolver);
+  CnfStream(SatInputInterface* satSolver, theory::Registrar r);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -252,7 +255,7 @@ public:
    * Constructs the stream to use the given sat solver.
    * @param satSolver the sat solver to use
    */
-  TseitinCnfStream(SatInputInterface* satSolver);
+  TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar reg);
 
 private: