fixed build failure

7 files changed, 46 insertions, 73 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index fb7994699..805ed6cb7 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -188,9 +188,9 @@ libcvc4_la_SOURCES = \
 	theory/bv/bv_inequality_graph.cpp \
 	theory/bv/bitblast_strategies_template.h \
 	theory/bv/bitblaster_template.h \
-	theory/bv/lazy_bitblaster.h \
-	theory/bv/eager_bitblaster.h \
-	theory/bv/aig_bitblaster.h \
+	theory/bv/lazy_bitblaster.cpp \
+	theory/bv/eager_bitblaster.cpp \
+	theory/bv/aig_bitblaster.cpp \
 	theory/bv/bv_eager_solver.h \
 	theory/bv/bv_eager_solver.cpp \
 	theory/bv/slicer.h \
diff --git a/src/theory/bv/aig_bitblaster.h b/src/theory/bv/aig_bitblaster.cpp
index d1635f950..70d69a138 100644
--- a/src/theory/bv/aig_bitblaster.h
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file aig_bitblaster.h
+/*! \file aig_bitblaster.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
@@ -15,11 +15,6 @@
  **/
 
 #include "cvc4_private.h"
-
-#ifndef __CVC4__AIG__BITBLASTER_H
-#define __CVC4__AIG__BITBLASTER_H
-
-
 #include "bitblaster_template.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
@@ -112,6 +107,14 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
   return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b); 
 }
 
+} /* CVC4::theory::bv */
+} /* CVC4::theory */
+} /* CVC4 */
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
 
 Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
 
@@ -467,13 +470,6 @@ AigBitblaster::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_solveTime); 
 }
 
-
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-
 #else // CVC4_USE_ABC
 
 namespace CVC4 {
@@ -547,6 +543,13 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
   return NULL;
 }
 
+} /* CVC4::theory::bv */
+} /* CVC4::theory */
+} /* CVC4 */
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
 
 Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
 
@@ -647,12 +650,4 @@ AigBitblaster::Statistics::~Statistics() {}
 AigBitblaster::AigBitblaster() {
   Unreachable();
 }
-
-} // namespace bv
-} // namespace theory
-} // namespace CVC4
-
-
 #endif // CVC4_USE_ABC
-
-#endif // __CVC4__AIG__BITBLASTER_H
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 4b0465498..2b6037a12 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -27,6 +27,7 @@
 #include "bitblast_strategies_template.h"
 #include "prop/sat_solver.h"
 #include "theory/valuation.h"
+#include "theory/theory_registrar.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -263,6 +264,15 @@ public:
   void collectModelInfo(TheoryModel* m, bool fullModel);
 };
 
+class BitblastingRegistrar: public prop::Registrar {
+  EagerBitblaster* d_bitblaster; 
+public:
+  BitblastingRegistrar(EagerBitblaster* bb)
+    : d_bitblaster(bb)
+  {}
+  void preRegister(Node n);
+}; /* class Registrar */
+
 class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
   typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
   typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 166d43e35..4e822d3c0 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -16,8 +16,7 @@
 
 #include "theory/bv/bv_eager_solver.h"
 #include "theory/bv/bitblaster_template.h"
-#include "theory/bv/eager_bitblaster.h"
-#include "theory/bv/aig_bitblaster.h"
+#include "theory/bv/options.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index ebe017ee1..ad5ff15b6 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -17,9 +17,10 @@
 #include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/bv/lazy_bitblaster.h"
+#include "theory/bv/bitblaster_template.h"
 #include "theory/bv/bv_quick_check.h"
 #include "theory/bv/options.h"
+#include "theory/bv/abstraction.h"
 #include "theory/decision_attributes.h"
 #include "decision/options.h"
 
diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.cpp
index 91ef866bd..5b52fc241 100644
--- a/src/theory/bv/eager_bitblaster.h
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file eager_bitblaster.h
+/*! \file eager_bitblaster.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
@@ -11,39 +11,26 @@
  **
  ** \brief 
  **
- ** Bitblaster for the lazy bv solver. 
+ ** Bitblaster for the eager bv solver. 
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__EAGER__BITBLASTER_H
-#define __CVC4__EAGER__BITBLASTER_H
-
-
-#include "theory/theory_registrar.h"
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/options.h"
 #include "theory/theory_model.h"
+#include "theory/bv/theory_bv.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
 
 
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv; 
 
-class BitblastingRegistrar: public prop::Registrar {
-  EagerBitblaster* d_bitblaster; 
-public:
-  BitblastingRegistrar(EagerBitblaster* bb)
-    : d_bitblaster(bb)
-  {}
-  void preRegister(Node n) {
-    d_bitblaster->bbAtom(n); 
-  };
-
-};/* class Registrar */
+void BitblastingRegistrar::preRegister(Node n) {
+  d_bitblaster->bbAtom(n); 
+};
 
 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   : TBitblaster<Node>()
@@ -219,12 +206,3 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
 bool EagerBitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
-
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-
-
-#endif
diff --git a/src/theory/bv/lazy_bitblaster.h b/src/theory/bv/lazy_bitblaster.cpp
index e11254dbb..d3ab68a5a 100644
--- a/src/theory/bv/lazy_bitblaster.h
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file lazy_bitblaster.h
+/*! \file lazy_bitblaster.cpp
 ** \verbatim
 ** Original author: Liana Hadarean
 ** Major contributors: none
@@ -15,11 +15,6 @@
 **/
 
 #include "cvc4_private.h"
-
-#ifndef __CVC4__LAZY__BITBLASTER_H
-#define __CVC4__LAZY__BITBLASTER_H
-
-
 #include "bitblaster_template.h"
 #include "theory_bv_utils.h"
 #include "theory/rewriter.h"
@@ -31,9 +26,10 @@
 #include "theory/theory_model.h"
 #include "theory/bv/abstraction.h"
 
-namespace CVC4 {
-namespace theory {
-namespace bv {
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv; 
+
 
 TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify)
   : TBitblaster<Node>()
@@ -497,9 +493,3 @@ void TLazyBitblaster::clearSolver() {
     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
   d_satSolver->setNotify(notify);
 }
-
-} /*bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace*/
-
-#endif