Merge pull request #74 from finnhaedicke/namespace_minisat

moved Minisat namespace into CVC4

17 files changed, 33 insertions, 3 deletions

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