From ca31b5f9de8575b9d6878c7ad7a674e48ae3c6df Mon Sep 17 00:00:00 2001 From: Finn Haedicke Date: Fri, 17 Apr 2015 10:46:07 +0200 Subject: [PATCH] moved Minisat namespace into CVC4 This avoids conflicts when CVC4 is linked to an application that also uses plain Minisat. --- src/proof/proof_manager.h | 5 +- src/proof/sat_proof.cpp | 40 +++++++-------- src/proof/sat_proof.h | 80 +++++++++++++++-------------- src/prop/minisat/core/Dimacs.h | 2 + src/prop/minisat/core/Main.cc | 2 +- src/prop/minisat/core/Solver.cc | 2 +- src/prop/minisat/core/Solver.h | 2 + src/prop/minisat/core/SolverTypes.h | 4 ++ src/prop/minisat/mtl/Alg.h | 2 + src/prop/minisat/mtl/Alloc.h | 2 + src/prop/minisat/mtl/Heap.h | 2 + src/prop/minisat/mtl/Map.h | 2 + src/prop/minisat/mtl/Queue.h | 2 + src/prop/minisat/mtl/Sort.h | 2 + src/prop/minisat/mtl/Vec.h | 2 + src/prop/minisat/mtl/XAlloc.h | 2 + src/prop/minisat/simp/SimpSolver.cc | 2 +- src/prop/minisat/simp/SimpSolver.h | 2 + src/prop/minisat/utils/Options.h | 2 + src/prop/minisat/utils/ParseUtils.h | 2 + 20 files changed, 97 insertions(+), 64 deletions(-) diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 43d6723fa..c35018b3e 100644 --- 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 3077f08ed..7867f1ddc 100644 --- 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 7c195c83d..a9793e784 100644 --- 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 IdToSatClause; typedef std::set < ClauseId > IdSet; -typedef std::vector < ::Minisat::Lit > LitVector; -typedef __gnu_cxx::hash_map IdToMinisatClause; +typedef std::vector < Minisat::Lit > LitVector; +typedef __gnu_cxx::hash_map 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 6bd19fb5b..e4728f6b6 100644 --- 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 de73b7327..cb33d194e 100644 --- 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 ea370ac08..5379c3088 100644 --- 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 ecebb086d..9243a2b35 100644 --- 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 bc60542e7..220114afa 100644 --- 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 6c3a18450..365b2d5aa 100644 --- 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& from, vec& to){ copy(from, to, true); //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h index 71f9f7281..e5b171bac 100644 --- 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::alloc(int size) //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index 5b9fb5822..c990f9a99 100644 --- 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 dda6c73d1..98996be60 100644 --- 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 2c818fcc9..ca2014429 100644 --- 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 644c39789..2c3454aa3 100644 --- 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 @@ -94,5 +95,6 @@ template void sort(vec& v) { //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index 5f85f6fcd..cb81ee580 100644 --- 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::clear(bool dealloc) { //================================================================================================= } +} #endif diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h index 1da176028..f1221f94f 100644 --- 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 #include +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 71e747f72..8408503e2 100644 --- 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 e1dfeb95e..370304d22 100644 --- 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& assumps, bool do_simp, bo //================================================================================================= } +} #endif diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h index b04799c4e..0577cbbd0 100644 --- 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 e9dc817c0..128205967 100644 --- 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 #include +namespace CVC4 { namespace Minisat { //------------------------------------------------------------------------------------------------- @@ -119,5 +120,6 @@ static bool eagerMatch(B& in, const char* str) { //================================================================================================= } +} #endif -- 2.30.2