moved Minisat namespace into CVC4

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

5 files changed, 10 insertions, 2 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 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