summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/proof/proof_manager.h5
-rw-r--r--src/proof/sat_proof.cpp40
-rw-r--r--src/proof/sat_proof.h80
-rw-r--r--src/prop/minisat/core/Dimacs.h2
-rw-r--r--src/prop/minisat/core/Main.cc2
-rw-r--r--src/prop/minisat/core/Solver.cc2
-rw-r--r--src/prop/minisat/core/Solver.h2
-rw-r--r--src/prop/minisat/core/SolverTypes.h4
-rw-r--r--src/prop/minisat/mtl/Alg.h2
-rw-r--r--src/prop/minisat/mtl/Alloc.h2
-rw-r--r--src/prop/minisat/mtl/Heap.h2
-rw-r--r--src/prop/minisat/mtl/Map.h2
-rw-r--r--src/prop/minisat/mtl/Queue.h2
-rw-r--r--src/prop/minisat/mtl/Sort.h2
-rw-r--r--src/prop/minisat/mtl/Vec.h2
-rw-r--r--src/prop/minisat/mtl/XAlloc.h2
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc2
-rw-r--r--src/prop/minisat/simp/SimpSolver.h2
-rw-r--r--src/prop/minisat/utils/Options.h2
-rw-r--r--src/prop/minisat/utils/ParseUtils.h2
20 files changed, 97 insertions, 64 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index ee99b0159..4bab86745 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 <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 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 e54a03435..56316ca0b 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 46c2666c8..0df5eb123 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 */
+}
@@ -182,6 +184,7 @@ public:
+namespace CVC4 {
namespace Minisat{
//=================================================================================================
@@ -499,5 +502,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<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 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<T>::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 72563e6d3..17572713f 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 {
//=================================================================================================
@@ -190,5 +191,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<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 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<T>::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 <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 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<Lit>& 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 <zlib.h>
#include <unistd.h>
+namespace CVC4 {
namespace Minisat {
//-------------------------------------------------------------------------------------------------
@@ -119,5 +120,6 @@ static bool eagerMatch(B& in, const char* str) {
//=================================================================================================
}
+}
#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback