From 7b8c765e84987ae90226f9f7244492318fa85817 Mon Sep 17 00:00:00 2001 From: lianah Date: Sat, 21 Jun 2014 17:45:31 -0400 Subject: [PATCH] fixed build failure --- src/Makefile.am | 6 +-- .../{aig_bitblaster.h => aig_bitblaster.cpp} | 37 ++++++++--------- src/theory/bv/bitblaster_template.h | 10 +++++ src/theory/bv/bv_eager_solver.cpp | 3 +- src/theory/bv/bv_subtheory_bitblast.cpp | 3 +- ...ager_bitblaster.h => eager_bitblaster.cpp} | 40 +++++-------------- ...{lazy_bitblaster.h => lazy_bitblaster.cpp} | 20 +++------- test/unit/theory/theory_bv_white.h | 2 +- 8 files changed, 47 insertions(+), 74 deletions(-) rename src/theory/bv/{aig_bitblaster.h => aig_bitblaster.cpp} (98%) rename src/theory/bv/{eager_bitblaster.h => eager_bitblaster.cpp} (91%) rename src/theory/bv/{lazy_bitblaster.h => lazy_bitblaster.cpp} (98%) 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 similarity index 98% rename from src/theory/bv/aig_bitblaster.h rename to 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* 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* 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 { typedef std::hash_map TNodeAigMap; typedef std::hash_map 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 similarity index 91% rename from src/theory/bv/eager_bitblaster.h rename to 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() @@ -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 similarity index 98% rename from src/theory/bv/lazy_bitblaster.h rename to 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() @@ -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 diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index dd65fc8e4..64dd680ae 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -22,7 +22,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/bv/theory_bv.h" -#include "theory/bv/eager_bitblaster.h" +#include "theory/bv/bitblaster_template.h" #include "expr/node.h" #include "expr/node_manager.h" #include "context/context.h" -- 2.30.2