moved Minisat namespace into CVC4

This avoids conflicts when CVC4 is linked to an application that
also uses plain Minisat.

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 43d6723fa377faf5cc8600992d3cc43cb23ee345..c35018b3ed55cfae626948e45a1bd0ea96deeb24 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -27,13 +27,14 @@
 #include "theory/logic_info.h"
 #include "theory/substitutions.h"
 
+
+namespace CVC4 {
+
 // forward declarations
 namespace Minisat {
   class Solver;
 }/* Minisat namespace */
 
-namespace CVC4 {
-
 namespace prop {
   class CnfStream;
 }/* CVC4::prop namespace */

diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 3077f08ed993b620395dc5452798383267b60a13..7867f1ddcff4fcf979c22e94417a6648efad195f 100644 (file)
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -21,7 +21,7 @@
 #include "prop/minisat/minisat.h"
 
 using namespace std;
-using namespace Minisat;
+using namespace CVC4::Minisat;
 using namespace CVC4::prop;
 namespace CVC4 {
 
@@ -259,7 +259,7 @@ bool SatProof::checkResolution(ClauseId id) {
 
 /// helper methods
 
-ClauseId SatProof::getClauseId(::Minisat::CRef ref) {
+ClauseId SatProof::getClauseId(Minisat::CRef ref) {
   if(d_clauseId.find(ref) == d_clauseId.end()) {
     Debug("proof:sat") << "Missing clause \n";
   }
@@ -268,7 +268,7 @@ ClauseId SatProof::getClauseId(::Minisat::CRef ref) {
 }
 
 
-ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
+ClauseId SatProof::getClauseId(Minisat::Lit lit) {
   Assert(d_unitId.find(toInt(lit)) != d_unitId.end());
   return d_unitId[toInt(lit)];
 }
@@ -298,11 +298,11 @@ bool SatProof::isUnit(ClauseId id) {
   return d_idUnit.find(id) != d_idUnit.end();
 }
 
-bool SatProof::isUnit(::Minisat::Lit lit) {
+bool SatProof::isUnit(Minisat::Lit lit) {
   return d_unitId.find(toInt(lit)) != d_unitId.end();
 }
 
-ClauseId SatProof::getUnitId(::Minisat::Lit lit) {
+ClauseId SatProof::getUnitId(Minisat::Lit lit) {
   Assert(isUnit(lit));
   return d_unitId[toInt(lit)];
 }
@@ -363,7 +363,7 @@ void SatProof::printRes(ResChain* res) {
 
 /// registration methods
 
-ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) {
+ClauseId SatProof::registerClause(Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) {
   Debug("cores") << "registerClause " << proof_id << std::endl;
   Assert(clause != CRef_Undef);
   ClauseIdMap::iterator it = d_clauseId.find(clause);
@@ -385,7 +385,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint6
   return d_clauseId[clause];
 }
 
-ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) {
+ClauseId SatProof::registerUnitClause(Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) {
   Debug("cores") << "registerUnitClause " << kind << " " << proof_id << std::endl;
   UnitIdMap::iterator it = d_unitId.find(toInt(lit));
   if (it == d_unitId.end()) {
@@ -407,7 +407,7 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint6
   return d_unitId[toInt(lit)];
 }
 
-void SatProof::removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) {
+void SatProof::removedDfs(Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) {
   // if we already added the literal return
   if (seen.count(lit)) {
     return;
@@ -483,13 +483,13 @@ void SatProof::registerResolution(ClauseId id, ResChain* res) {
 
 /// recording resolutions
 
-void SatProof::startResChain(::Minisat::CRef start) {
+void SatProof::startResChain(Minisat::CRef start) {
   ClauseId id = getClauseId(start);
   ResChain* res = new ResChain(id);
   d_resStack.push_back(res);
 }
 
-void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) {
+void SatProof::addResolutionStep(Minisat::Lit lit, Minisat::CRef clause, bool sign) {
   ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
   ResChain* res = d_resStack.back();
   res->addStep(lit, id, sign);
@@ -504,7 +504,7 @@ void SatProof::endResChain(CRef clause) {
 }
 
 
-void SatProof::endResChain(::Minisat::Lit lit) {
+void SatProof::endResChain(Minisat::Lit lit) {
   Assert(d_resStack.size() > 0);
   ClauseId id = registerUnitClause(lit, LEARNT, uint64_t(-1));
   ResChain* res = d_resStack.back();
@@ -512,7 +512,7 @@ void SatProof::endResChain(::Minisat::Lit lit) {
   d_resStack.pop_back();
 }
 
-void SatProof::storeLitRedundant(::Minisat::Lit lit) {
+void SatProof::storeLitRedundant(Minisat::Lit lit) {
   Assert(d_resStack.size() > 0);
   ResChain* res = d_resStack.back();
   res->addRedundantLit(lit);
@@ -520,18 +520,18 @@ void SatProof::storeLitRedundant(::Minisat::Lit lit) {
 
 /// constructing resolutions
 
-void SatProof::resolveOutUnit(::Minisat::Lit lit) {
+void SatProof::resolveOutUnit(Minisat::Lit lit) {
   ClauseId id = resolveUnit(~lit);
   ResChain* res = d_resStack.back();
   res->addStep(lit, id, !sign(lit));
 }
 
-void SatProof::storeUnitResolution(::Minisat::Lit lit) {
+void SatProof::storeUnitResolution(Minisat::Lit lit) {
   Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
   resolveUnit(lit);
 }
 
-ClauseId SatProof::resolveUnit(::Minisat::Lit lit) {
+ClauseId SatProof::resolveUnit(Minisat::Lit lit) {
   // first check if we already have a resolution for lit
   if(isUnit(lit)) {
     ClauseId id = getClauseId(lit);
@@ -566,7 +566,7 @@ void SatProof::toStream(std::ostream& out) {
   Unimplemented("native proof printing not supported yet");
 }
 
-void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) {
+void SatProof::storeUnitConflict(Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) {
   Debug("cores") << "STORE UNIT CONFLICT" << std::endl;
   Assert(!d_storedUnitConflict);
   d_unitConflictId = registerUnitClause(conflict_lit, kind, proof_id);
@@ -574,11 +574,11 @@ void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, u
   Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId << "\n";
 }
 
-void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
+void SatProof::finalizeProof(Minisat::CRef conflict_ref) {
   Assert(d_resStack.size() == 0);
-  Assert(conflict_ref != ::Minisat::CRef_Undef);
+  Assert(conflict_ref != Minisat::CRef_Undef);
   ClauseId conflict_id;
-  if (conflict_ref == ::Minisat::CRef_Lazy) {
+  if (conflict_ref == Minisat::CRef_Lazy) {
     Assert(d_storedUnitConflict);
     conflict_id = d_unitConflictId;
 
@@ -616,7 +616,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
 
 /// CRef manager
 
-void SatProof::updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref) {
+void SatProof::updateCRef(Minisat::CRef oldref, Minisat::CRef newref) {
   if (d_clauseId.find(oldref) == d_clauseId.end()) {
     return;
   }

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 7c195c83ddc8d7a936368d6b530fc64eb043d034..a9793e784b7a42aa2cf402d1bddc6bcbc19bf02e 100644 (file)
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -29,10 +29,12 @@
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
 
+namespace CVC4 {
 namespace Minisat {
   class Solver;
   typedef uint32_t CRef;
 }/* Minisat namespace */
+}
 
 #include "prop/minisat/core/SolverTypes.h"
 #include "util/proof.h"
@@ -46,14 +48,14 @@ namespace CVC4 {
 /**
  * Helper debugging functions
  */
-void printDebug(::Minisat::Lit l);
-void printDebug(::Minisat::Clause& c);
+void printDebug(Minisat::Lit l);
+void printDebug(Minisat::Clause& c);
 
 struct ResStep {
-  ::Minisat::Lit lit;
+  Minisat::Lit lit;
   ClauseId id;
   bool sign;
-  ResStep(::Minisat::Lit l, ClauseId i, bool s) :
+  ResStep(Minisat::Lit l, ClauseId i, bool s) :
     lit(l),
     id(i),
     sign(s)
@@ -61,7 +63,7 @@ struct ResStep {
 };/* struct ResStep */
 
 typedef std::vector< ResStep > ResSteps;
-typedef std::set < ::Minisat::Lit> LitSet;
+typedef std::set < Minisat::Lit> LitSet;
 
 class ResChain {
 private:
@@ -70,9 +72,9 @@ private:
   LitSet*        d_redundantLits;
 public:
   ResChain(ClauseId start);
-  void addStep(::Minisat::Lit, ClauseId, bool);
+  void addStep(Minisat::Lit, ClauseId, bool);
   bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); }
-  void addRedundantLit(::Minisat::Lit lit);
+  void addRedundantLit(Minisat::Lit lit);
   ~ResChain();
   // accessor methods
   ClauseId  getStart()     { return d_start; }
@@ -80,9 +82,9 @@ public:
   LitSet*   getRedundant() { return d_redundantLits; }
 };/* class ResChain */
 
-typedef std::hash_map < ClauseId, ::Minisat::CRef > IdCRefMap;
-typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap;
-typedef std::hash_map < ClauseId, ::Minisat::Lit>   IdUnitMap;
+typedef std::hash_map < ClauseId, Minisat::CRef > IdCRefMap;
+typedef std::hash_map < Minisat::CRef, ClauseId > ClauseIdMap;
+typedef std::hash_map < ClauseId, Minisat::Lit>   IdUnitMap;
 typedef std::hash_map < int, ClauseId>            UnitIdMap; //FIXME
 typedef std::hash_map < ClauseId, ResChain*>      IdResMap;
 typedef std::hash_set < ClauseId >                IdHashSet;
@@ -90,8 +92,8 @@ typedef std::hash_map < ClauseId, uint64_t >      IdProofRuleMap;
 typedef std::vector   < ResChain* >               ResStack;
 typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;
 typedef std::set < ClauseId >                     IdSet;
-typedef std::vector < ::Minisat::Lit >              LitVector;
-typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause;
+typedef std::vector < Minisat::Lit >              LitVector;
+typedef __gnu_cxx::hash_map<ClauseId, Minisat::Clause& > IdToMinisatClause;
 
 class SatProof;
 
@@ -100,7 +102,7 @@ private:
   SatProof* d_proof;
 public:
   ProofProxy(SatProof* pf);
-  void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
+  void updateCRef(Minisat::CRef oldref, Minisat::CRef newref);
 };/* class ProofProxy */
 
 
@@ -108,7 +110,7 @@ class CnfProof;
 
 class SatProof {
 protected:
-  ::Minisat::Solver*    d_solver;
+  Minisat::Solver*    d_solver;
   // clauses
   IdCRefMap           d_idClause;
   ClauseIdMap         d_clauseId;
@@ -138,7 +140,7 @@ protected:
   ClauseId d_unitConflictId;
   bool d_storedUnitConflict;
 public:
-  SatProof(::Minisat::Solver* solver, bool checkRes = false);
+  SatProof(Minisat::Solver* solver, bool checkRes = false);
   virtual ~SatProof();
 protected:
   void print(ClauseId id);
@@ -149,17 +151,17 @@ protected:
   bool isTheoryConflict(ClauseId id);
   bool isLemmaClause(ClauseId id);
   bool isUnit(ClauseId id);
-  bool isUnit(::Minisat::Lit lit);
+  bool isUnit(Minisat::Lit lit);
   bool hasResolution(ClauseId id);
   void createLitSet(ClauseId id, LitSet& set);
   void registerResolution(ClauseId id, ResChain* res);
 
-  ClauseId      getClauseId(::Minisat::CRef clause);
-  ClauseId      getClauseId(::Minisat::Lit lit);
-  ::Minisat::CRef getClauseRef(ClauseId id);
-  ::Minisat::Lit  getUnit(ClauseId id);
-  ClauseId      getUnitId(::Minisat::Lit lit);
-  ::Minisat::Clause& getClause(::Minisat::CRef ref);
+  ClauseId      getClauseId(Minisat::CRef clause);
+  ClauseId      getClauseId(Minisat::Lit lit);
+  Minisat::CRef getClauseRef(ClauseId id);
+  Minisat::Lit  getUnit(ClauseId id);
+  ClauseId      getUnitId(Minisat::Lit lit);
+  Minisat::Clause& getClause(Minisat::CRef ref);
   virtual void toStream(std::ostream& out);
 
   bool checkResolution(ClauseId id);
@@ -170,7 +172,7 @@ protected:
    *
    * @return
    */
-  ClauseId resolveUnit(::Minisat::Lit lit);
+  ClauseId resolveUnit(Minisat::Lit lit);
   /**
    * Does a depth first search on removed literals and adds the literals
    * to be removed in the proper order to the stack.
@@ -179,27 +181,27 @@ protected:
    * @param removedSet the previously computed set of redundant literals
    * @param removeStack the stack of literals in reverse order of resolution
    */
-  void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
+  void removedDfs(Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
   void removeRedundantFromRes(ResChain* res, ClauseId id);
 public:
-  void startResChain(::Minisat::CRef start);
-  void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign);
+  void startResChain(Minisat::CRef start);
+  void addResolutionStep(Minisat::Lit lit, Minisat::CRef clause, bool sign);
   /**
    * Pops the current resolution of the stack and stores it
    * in the resolution map. Also registers the 'clause' parameter
    * @param clause the clause the resolution is proving
    */
-  void endResChain(::Minisat::CRef clause);
-  void endResChain(::Minisat::Lit lit);
+  void endResChain(Minisat::CRef clause);
+  void endResChain(Minisat::Lit lit);
   /**
    * Stores in the current derivation the redundant literals that were
    * eliminated from the conflict clause during conflict clause minimization.
    * @param lit the eliminated literal
    */
-  void storeLitRedundant(::Minisat::Lit lit);
+  void storeLitRedundant(Minisat::Lit lit);
 
   /// update the CRef Id maps when Minisat does memory reallocation x
-  void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref);
+  void updateCRef(Minisat::CRef old_ref, Minisat::CRef new_ref);
   void finishUpdateCRef();
 
   /**
@@ -207,33 +209,33 @@ public:
    *
    * @param conflict
    */
-  void finalizeProof(::Minisat::CRef conflict);
+  void finalizeProof(Minisat::CRef conflict);
 
   /// clause registration methods
-  ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id);
-  ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
+  ClauseId registerClause(const Minisat::CRef clause, ClauseKind kind, uint64_t proof_id);
+  ClauseId registerUnitClause(const Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
 
-  void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
+  void storeUnitConflict(Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
 
   /**
    * Marks the deleted clauses as deleted. Note we may still use them in the final
    * resolution.
    * @param clause
    */
-  void markDeleted(::Minisat::CRef clause);
+  void markDeleted(Minisat::CRef clause);
   bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); }
   /**
    * Constructs the resolution of ~q and resolves it with the current
    * resolution thus eliminating q from the current clause
    * @param q the literal to be resolved out
    */
-  void     resolveOutUnit(::Minisat::Lit q);
+  void     resolveOutUnit(Minisat::Lit q);
   /**
    * Constructs the resolution of the literal lit. Called when a clause
    * containing lit becomes satisfied and is removed.
    * @param lit
    */
-  void     storeUnitResolution(::Minisat::Lit lit);
+  void     storeUnitResolution(Minisat::Lit lit);
 
   ProofProxy* getProxy() {return d_proxy; }
 
@@ -248,7 +250,7 @@ protected:
   IdHashSet          d_seenTheoryConflicts;
   IdHashSet          d_seenLemmas;
 
-  inline std::string varName(::Minisat::Lit lit);
+  inline std::string varName(Minisat::Lit lit);
   inline std::string clauseName(ClauseId id);
 
   void collectClauses(ClauseId id);
@@ -261,7 +263,7 @@ class LFSCSatProof : public SatProof {
 private:
   void printResolution(ClauseId id, std::ostream& out, std::ostream& paren);
 public:
-  LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false)
+  LFSCSatProof(Minisat::Solver* solver, bool checkRes = false)
     : SatProof(solver, checkRes)
   {}
   virtual void printResolutions(std::ostream& out, std::ostream& paren);

diff --git a/src/prop/minisat/core/Dimacs.h b/src/prop/minisat/core/Dimacs.h
index 6bd19fb5b5551338df52ac747fe729fa95925318..e4728f6b6c9b65291950cc981d0e0095006679e9 100644 (file)
--- a/src/prop/minisat/core/Dimacs.h
+++ b/src/prop/minisat/core/Dimacs.h
@@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/utils/ParseUtils.h"
 #include "prop/minisat/core/SolverTypes.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -85,5 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/core/Main.cc b/src/prop/minisat/core/Main.cc
index de73b7327b227a497bc368f1b705fff99dd114f7..cb33d194e1e1ef6a41cd32950ae4bece27bd848d 100644 (file)
--- a/src/prop/minisat/core/Main.cc
+++ b/src/prop/minisat/core/Main.cc
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/core/Dimacs.h"
 #include "prop/minisat/core/Solver.h"
 
-using namespace Minisat;
+using namespace CVC4::Minisat;
 
 //=================================================================================================
 

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ea370ac0819ebe1eadb3197ba6612f8eda43e3df..5379c3088ce38c68121abb51940a836ebe5f4f75 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -33,7 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
 
-using namespace Minisat;
+using namespace CVC4::Minisat;
 using namespace CVC4;
 using namespace CVC4::prop;
 

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index ecebb086dde43516fed12428250ec81d7cbfaef6..9243a2b356207908d84b158790348215240ed1f1 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -44,6 +44,7 @@ namespace CVC4 {
   }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -557,5 +558,6 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 
 //=================================================================================================
 }/* Minisat namespace */
+}
 
 #endif

diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index bc60542e78969a4f3153c1df36503fbc486643e8..220114afa1cdf78d9493234f378135d81f59b6a9 100644 (file)
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -31,6 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Map.h"
 #include "prop/minisat/mtl/Alloc.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -169,6 +170,7 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
 
 
 } /* Minisat */
+}
 
 
 
@@ -181,6 +183,7 @@ public:
 
 
 
+namespace CVC4 {
 namespace Minisat{
 
 //=================================================================================================
@@ -498,5 +501,6 @@ inline void Clause::strengthen(Lit p)
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index 6c3a184508b438ac4087a1f8af0c47573f331b9b..365b2d5aa1d652cea4d9273b2536dbecb23b8eac 100644 (file)
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "prop/minisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -80,5 +81,6 @@ static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true);
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
index 71f9f72818e5e20aa63820fa7aa80d3c0140029b..e5b171bacaae9e20f3f1810dcbb445bf7291b436 100644 (file)
--- a/src/prop/minisat/mtl/Alloc.h
+++ b/src/prop/minisat/mtl/Alloc.h
@@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/XAlloc.h"
 #include "prop/minisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -127,5 +128,6 @@ RegionAllocator<T>::alloc(int size)
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index 5b9fb582288a1a1c1733fd8c3fabfbf21593ce9e..c990f9a99cb1fc75ca529dd6c20c0e80fae75b84 100644 (file)
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "prop/minisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -144,5 +145,6 @@ class Heap {
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index dda6c73d13c8482a2964f7be1b5594ca4750374f..98996be6067329b76d489cbd2c7308a198b7a355 100644 (file)
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/IntTypes.h"
 #include "prop/minisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -189,5 +190,6 @@ class Map {
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index 2c818fcc9fd568999a44d6421f06e154cb4c3335..ca2014429ca45145dbd50394623ccfa05d30db56 100644 (file)
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "prop/minisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -65,5 +66,6 @@ public:
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index 644c39789f05bb46d2b893c0b3270208eae4679a..2c3454aa38b5c39ba8a6d78d110884ccc1f0d114 100644 (file)
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 // Some sorting algorithms for vec's
 
 
+namespace CVC4 {
 namespace Minisat {
 
 template<class T>
@@ -94,5 +95,6 @@ template <class T> void sort(vec<T>& v) {
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index 5f85f6fcddc081d424a1e27c0893eda27d60b8ab..cb81ee5803b9e8f3c29f90cddf6b017585dac100 100644 (file)
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/IntTypes.h"
 #include "prop/minisat/mtl/XAlloc.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -126,5 +127,6 @@ void vec<T>::clear(bool dealloc) {
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h
index 1da176028d3458cae0fed04d905f545a1e7f45f7..f1221f94f6df041b8b6552430eee68c3c412796f 100644 (file)
--- a/src/prop/minisat/mtl/XAlloc.h
+++ b/src/prop/minisat/mtl/XAlloc.h
@@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <errno.h>
 #include <stdlib.h>
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -41,5 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size)
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 71e747f72c4cf78057c6719562c660082ea81517..8408503e27e9031d77c975d59852b1a8f9eb493e 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -23,8 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/utils/System.h"
 #include "prop/options.h"
 #include "proof/proof.h"
-using namespace Minisat;
 using namespace CVC4;
+using namespace CVC4::Minisat;
 
 //=================================================================================================
 // Options:

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index e1dfeb95ef525a3ee6e99a729b0c69aa324c14e6..370304d222a421ee2a5eb942607d2f7465957d79 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -33,6 +33,7 @@ namespace prop {
 }
 }
 
+namespace CVC4 {
 namespace Minisat {
 
 //=================================================================================================
@@ -235,5 +236,6 @@ inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bo
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h
index b04799c4e7e4497871fb0b10d7a945a59473774f..0577cbbd0b890d28a0aec366a0caa13107370b5e 100644 (file)
--- a/src/prop/minisat/utils/Options.h
+++ b/src/prop/minisat/utils/Options.h
@@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Vec.h"
 #include "prop/minisat/utils/ParseUtils.h"
 
+namespace CVC4 {
 namespace Minisat {
 
 //==================================================================================================
@@ -382,5 +383,6 @@ class BoolOption : public Option
 
 //=================================================================================================
 }
+}
 
 #endif

diff --git a/src/prop/minisat/utils/ParseUtils.h b/src/prop/minisat/utils/ParseUtils.h
index e9dc817c0b8b2635e7a0e9ce1d48f4be2abe809d..1282059670b50cec32482ded95bd659441161315 100644 (file)
--- a/src/prop/minisat/utils/ParseUtils.h
+++ b/src/prop/minisat/utils/ParseUtils.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 //#include <zlib.h>
 #include <unistd.h>
 
+namespace CVC4 {
 namespace Minisat {
 
 //-------------------------------------------------------------------------------------------------
@@ -119,5 +120,6 @@ static bool eagerMatch(B& in, const char* str) {
 
 //=================================================================================================
 }
+}
 
 #endif