This fixes a one definition rule violation for reduceDB_lt in Solver.cc in minisat...

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 0bf4edf6a8cb1bde36259639f34baf34e5a6aebe..fc5b29e891ac002285ff2aa49631f354ce50f5ab 100644 (file)
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -139,9 +139,5 @@ public:
   Statistics d_statistics;
 };
 
-}
-}
-
-
-
-
+} /* CVC4::prop namespace */
+} /* CVC4 namespace */

diff --git a/src/prop/bvminisat/core/Dimacs.h b/src/prop/bvminisat/core/Dimacs.h
index 64df4f635dfc658836a21e121e17e6629e235ea4..46451d4640e22d5f86ed34a0172de72acdb30bcd 100644 (file)
--- a/src/prop/bvminisat/core/Dimacs.h
+++ b/src/prop/bvminisat/core/Dimacs.h
@@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "utils/ParseUtils.h"
 #include "core/SolverTypes.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -84,6 +85,7 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
     parse_DIMACS_main(in, S); }
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/core/Main.cc b/src/prop/bvminisat/core/Main.cc
index 95cfe7bfedb911a86e4e78dd3c06ab22fabdbcaf..74cc9cde835c7e32098b36d3c8c7e70ea0ea342f 100644 (file)
--- a/src/prop/bvminisat/core/Main.cc
+++ b/src/prop/bvminisat/core/Main.cc
@@ -29,7 +29,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "core/Dimacs.h"
 #include "core/Solver.h"
 
-using namespace BVMinisat;
+
+namespace CVC4 {
+namespace BVMinisat {
 
 //=================================================================================================
 
@@ -63,6 +65,8 @@ static void SIGINT_exit(int signum) {
         printf("\n"); printf("*** INTERRUPTED ***\n"); }
     _exit(1); }
 
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 //=================================================================================================
 // Main:
@@ -70,6 +74,9 @@ static void SIGINT_exit(int signum) {
 
 int main(int argc, char** argv)
 {
+  using namespace CVC4;
+  using namespace CVC4::BVMinisat;
+
     try {
         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
         // printf("This is MiniSat 2.0 beta\n");

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 1267561fbd0c3bb4d73515933bc32a4c60c0c354..ca7228ee8453f01271d40de741a03b35612b6bc8 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -31,8 +31,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "theory/bv/options.h"
 #include "smt/options.h"
 #include "theory/interrupted.h"
-using namespace BVMinisat;
 
+namespace CVC4 {
 namespace BVMinisat {
 
 #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "
@@ -52,7 +52,6 @@ std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) {
   return out;
 }
 
-}
 
 //=================================================================================================
 // Options:
@@ -1207,3 +1206,6 @@ void Solver::garbageCollect()
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }
+
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */

diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 016a0c22558e68f87a112723a25fd11ce97c0136..214e425f9889b1cacffe5e032b5e7b7c91341e9f 100644 (file)
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -32,6 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <ext/hash_set>
 #include <vector>
 
+namespace CVC4 {
 namespace BVMinisat {
 
 /** Interface for minisat callbacks */
@@ -440,6 +441,8 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
+
 
 #endif

diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index 0400f956d8e78729adaac5dee38a7e78fd97bc53..aa0921b78aa8c8f4e6b491e53f83b955713f78a4 100644 (file)
--- a/src/prop/bvminisat/core/SolverTypes.h
+++ b/src/prop/bvminisat/core/SolverTypes.h
@@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Map.h"
 #include "prop/bvminisat/mtl/Alloc.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -417,6 +418,7 @@ inline void Clause::strengthen(Lit p)
 
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/mtl/Alg.h b/src/prop/bvminisat/mtl/Alg.h
index f3ecdecc5c6d8be8cd6e588db52944464b40bed1..e61dbb4159956767c042e09c22aa5d89e9c223ce 100644 (file)
--- a/src/prop/bvminisat/mtl/Alg.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -79,6 +80,7 @@ template<class T>
 static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/mtl/Alloc.h b/src/prop/bvminisat/mtl/Alloc.h
index f4303044fab999f479e8bdc522f016465b5173ec..4e58ab1592aa0f4bbbf53b6c106d55e2dde8fc0b 100644 (file)
--- a/src/prop/bvminisat/mtl/Alloc.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/XAlloc.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -126,6 +127,7 @@ RegionAllocator<T>::alloc(int size)
 
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/mtl/Heap.h b/src/prop/bvminisat/mtl/Heap.h
index d57824ba1ab7e87d5bdb4379886bf934664fa879..2d7ee01999c1a0e5812241c967ffee409162f3e9 100644 (file)
--- a/src/prop/bvminisat/mtl/Heap.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -143,6 +144,8 @@ class Heap {
 
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
+
 
 #endif

diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h
index 4e61d65824deda5b31a19a9021977cf57c7adb60..ee68a2155d61f7b527f4261168b5ee791b6e7d25 100644 (file)
--- a/src/prop/bvminisat/mtl/Map.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/IntTypes.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -189,6 +190,7 @@ class Map {
 };
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/mtl/Queue.h b/src/prop/bvminisat/mtl/Queue.h
index 83321ba95702b35cd000093c0629ac35e4e9d21e..c40f2322b2e67b66adb167fe26aa4c570375edf7 100644 (file)
--- a/src/prop/bvminisat/mtl/Queue.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -64,6 +65,7 @@ public:
 
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/mtl/Sort.h b/src/prop/bvminisat/mtl/Sort.h
index 9bab9a0df696fb88ccc06bedb1ad5f66954c0d92..f668aa8560c67cd327f1cdf03c451908a1923d60 100644 (file)
--- a/src/prop/bvminisat/mtl/Sort.h
+++ b/src/prop/bvminisat/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 BVMinisat {
 
 template<class T>
@@ -93,6 +94,7 @@ template <class T> void sort(vec<T>& v) {
 
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/mtl/Vec.h b/src/prop/bvminisat/mtl/Vec.h
index 8c568dfe9f7614269dc8552c5f4eeb83dfd4599f..8ee2a827f12d2d32906ead48b9fca9e54ec31a54 100644 (file)
--- a/src/prop/bvminisat/mtl/Vec.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/IntTypes.h"
 #include "prop/bvminisat/mtl/XAlloc.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -125,6 +126,7 @@ void vec<T>::clear(bool dealloc) {
         if (dealloc) free(data), data = NULL, cap = 0; } }
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/mtl/XAlloc.h b/src/prop/bvminisat/mtl/XAlloc.h
index 7b89d18031cc9e9180314f781c9af111349477bf..9e469a6fbde5ac69d79e601eecae578b82fc3bd3 100644 (file)
--- a/src/prop/bvminisat/mtl/XAlloc.h
+++ b/src/prop/bvminisat/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 BVMinisat {
 
 //=================================================================================================
@@ -40,6 +41,8 @@ static inline void* xrealloc(void *ptr, size_t size)
 }
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
+
 
 #endif

diff --git a/src/prop/bvminisat/simp/Main.cc b/src/prop/bvminisat/simp/Main.cc
index bfb655782b7a048175eb8098b8c94daf105afb62..96e318e5f8dd0232ac3a653c5de4bf7b8c1644f1 100644 (file)
--- a/src/prop/bvminisat/simp/Main.cc
+++ b/src/prop/bvminisat/simp/Main.cc
@@ -30,11 +30,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "core/Dimacs.h"
 #include "simp/SimpSolver.h"
 
-using namespace BVMinisat;
 
 //=================================================================================================
 
 
+namespace CVC4 {
+namespace BVMinisat {
+
 void printStats(Solver& solver)
 {
     double cpu_time = cpuTime();
@@ -65,11 +67,16 @@ static void SIGINT_exit(int signum) {
     _exit(1); }
 
 
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
+
 //=================================================================================================
 // Main:
 
 int main(int argc, char** argv)
 {
+  using namespace CVC4;
+  using namespace CVC4::BVMinisat;
     try {
         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
         // printf("This is MiniSat 2.0 beta\n");

diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index c651899856491afffeaf5f13e642bf5a101b6861..e7e48998524228e8fb16c4863849b1698f62765e 100644 (file)
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -23,7 +23,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "utils/System.h"
 #include "theory/bv/options.h"
 #include "smt/options.h"
-using namespace BVMinisat;
+
+namespace CVC4 {
+namespace BVMinisat {
 
 //=================================================================================================
 // Options:
@@ -749,3 +751,6 @@ void SimpSolver::garbageCollect()
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }
+
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */

diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 4ff17d3ab3fef43c796422f84f8af57b183035f7..707f62e342316da83e94eb9c47f2af1ec210af86 100644 (file)
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "util/statistics_registry.h"
 #include "context/context.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -218,6 +219,8 @@ inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){
     return solve_(do_simp, turn_off_simp); }
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
+
 
 #endif

diff --git a/src/prop/bvminisat/utils/Options.cc b/src/prop/bvminisat/utils/Options.cc
index a15220c4bb2816012d0bb870aab91721fd06a5c9..b2094d466dec9f83f6ded1c1250c737f7cb1ed68 100644 (file)
--- a/src/prop/bvminisat/utils/Options.cc
+++ b/src/prop/bvminisat/utils/Options.cc
@@ -21,9 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "utils/Options.h"
 #include "utils/ParseUtils.h"
 
-using namespace BVMinisat;
+namespace CVC4 {
+namespace BVMinisat {
 
-void Minisat::parseOptions(int& argc, char** argv, bool strict)
+void BVMinisat::parseOptions(int& argc, char** argv, bool strict)
 {
     int i, j;
     for (i = j = 1; i < argc; i++){
@@ -54,9 +55,9 @@ void Minisat::parseOptions(int& argc, char** argv, bool strict)
 }
 
 
-void Minisat::setUsageHelp      (const char* str){ Option::getUsageString() = str; }
-void Minisat::setHelpPrefixStr  (const char* str){ Option::getHelpPrefixString() = str; }
-void Minisat::printUsageAndExit (int argc, char** argv, bool verbose)
+void BVMinisat::setUsageHelp      (const char* str){ Option::getUsageString() = str; }
+void BVMinisat::setHelpPrefixStr  (const char* str){ Option::getHelpPrefixString() = str; }
+void BVMinisat::printUsageAndExit (int argc, char** argv, bool verbose)
 {
     const char* usage = Option::getUsageString();
     if (usage != NULL)
@@ -89,3 +90,6 @@ void Minisat::printUsageAndExit (int argc, char** argv, bool verbose)
     exit(0);
 }
 
+
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */

diff --git a/src/prop/bvminisat/utils/Options.h b/src/prop/bvminisat/utils/Options.h
index 2092a87e4b0d6282fceff651c0ff3ecc82df3e96..12321cba2ecc012ea0c84f20222f0a0dc7c22a12 100644 (file)
--- a/src/prop/bvminisat/utils/Options.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/utils/ParseUtils.h"
 
+namespace CVC4 {
 namespace BVMinisat {
 
 //==================================================================================================
@@ -381,6 +382,7 @@ class BoolOption : public Option
 };
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/utils/ParseUtils.h b/src/prop/bvminisat/utils/ParseUtils.h
index fc2ce9cbe15a26b32b287225146e219e450c4746..46f404c3eaf37a2a579b1923c23e46d0c230f7e1 100644 (file)
--- a/src/prop/bvminisat/utils/ParseUtils.h
+++ b/src/prop/bvminisat/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 BVMinisat {
 
 //-------------------------------------------------------------------------------------------------
@@ -118,6 +119,7 @@ static bool eagerMatch(B& in, const char* str) {
 
 
 //=================================================================================================
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 #endif

diff --git a/src/prop/bvminisat/utils/System.cc b/src/prop/bvminisat/utils/System.cc
index 9c2fcb083395dd53724ca894bf7885ddfc3a8560..dab33af3ee30132dd2e49d87663a964a772e302e 100644 (file)
--- a/src/prop/bvminisat/utils/System.cc
+++ b/src/prop/bvminisat/utils/System.cc
@@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdio.h>
 #include <stdlib.h>
 
-using namespace BVMinisat;
+namespace CVC4 {
+namespace BVMinisat {
 
 // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
 // one for reading the current virtual memory size.
@@ -67,14 +68,14 @@ static inline int memReadPeak(void)
     return peak_kb;
 }
 
-double Minisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
-double Minisat::memUsedPeak() { 
+double BVMinisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
+double BVMinisat::memUsedPeak() { 
     double peak = memReadPeak() / 1024;
     return peak == 0 ? memUsed() : peak; }
 
 #elif defined(__FreeBSD__)
 
-double Minisat::memUsed(void) {
+double BVMinisat::memUsed(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
     return (double)ru.ru_maxrss / 1024; }
@@ -84,12 +85,16 @@ double MiniSat::memUsedPeak(void) { return memUsed(); }
 #elif defined(__APPLE__)
 #include <malloc/malloc.h>
 
-double Minisat::memUsed(void) {
+double BVMinisat::memUsed(void) {
     malloc_statistics_t t;
     malloc_zone_statistics(NULL, &t);
     return (double)t.max_size_in_use / (1024*1024); }
 
 #else
-double Minisat::memUsed() { 
+double BVMinisat::memUsed() { 
     return 0; }
 #endif
+
+
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */

diff --git a/src/prop/bvminisat/utils/System.h b/src/prop/bvminisat/utils/System.h
index 4b4b73cb910a1901a4bc83224088b043e25358b4..a065ef91687e25525ddd038e0f654b2e60c5ece7 100644 (file)
--- a/src/prop/bvminisat/utils/System.h
+++ b/src/prop/bvminisat/utils/System.h
@@ -29,13 +29,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 //-------------------------------------------------------------------------------------------------
 
+namespace CVC4 {
 namespace BVMinisat {
 
 static inline double cpuTime(void); // CPU-time in seconds.
 extern double memUsed();            // Memory in mega bytes (returns 0 for unsupported architectures).
 extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for unsupported architectures).
 
-}
+} /* CVC4::BVMinisat namespace */
+} /* CVC4 namespace */
 
 //-------------------------------------------------------------------------------------------------
 // Implementation of inline functions:
@@ -43,14 +45,14 @@ extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for
 #if defined(_MSC_VER) || defined(__MINGW32__)
 #include <time.h>
 
-static inline double BVMinisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
+static inline double CVC4::BVMinisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
 
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
 
-static inline double BVMinisat::cpuTime(void) {
+static inline double CVC4::BVMinisat::cpuTime(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
     return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }

diff --git a/src/prop/minisat/core/Main.cc b/src/prop/minisat/core/Main.cc
index cb33d194e1e1ef6a41cd32950ae4bece27bd848d..64a2a1c507ae79b414d57428f6ab9bb5d482b21d 100644 (file)
--- a/src/prop/minisat/core/Main.cc
+++ b/src/prop/minisat/core/Main.cc
@@ -29,11 +29,11 @@ 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 CVC4::Minisat;
-
 //=================================================================================================
 
 
+namespace CVC4 {
+namespace Minisat {
 void printStats(Solver& solver)
 {
     double cpu_time = cpuTime();
@@ -63,6 +63,9 @@ static void SIGINT_exit(int signum) {
         printf("\n"); printf("*** INTERRUPTED ***\n"); }
     _exit(1); }
 
+} /* CVC4::Minisat namespace */
+} /* CVC4 namespace */
+
 
 //=================================================================================================
 // Main:
@@ -70,6 +73,8 @@ static void SIGINT_exit(int signum) {
 
 int main(int argc, char** argv)
 {
+  using namespace CVC4;
+  using namespace CVC4::Minisat;
     try {
         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
         // printf("This is MiniSat 2.0 beta\n");

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 2c94401fb79fe71f1b88d0e97d5a85ef9e2250ed..5dc618899137a382d5a323cb1113c81acce73d84 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -33,10 +33,11 @@ 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 CVC4::Minisat;
-using namespace CVC4;
 using namespace CVC4::prop;
 
+namespace CVC4 {
+namespace Minisat {
+
 //=================================================================================================
 // Options:
 
@@ -332,7 +333,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
           // as the final conflict.
           if(falseLiteralsCount == 1) {
             PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); )
-            PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
+            PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
             return ok = false;
           }
         } else {
@@ -372,7 +373,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
           if(! (ok = (confl == CRef_Undef)) ) {
             if(ca[confl].size() == 1) {
               PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); );
-              PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
+              PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
             } else {
               PROOF( ProofManager::getSatProof()->finalizeProof(confl); );
             }
@@ -1729,3 +1730,7 @@ inline bool Solver::withinBudget(uint64_t ammount) const {
     (propagation_budget < 0 || propagations < (uint64_t)propagation_budget);
   return within_budget;
 }
+
+
+} /* CVC4::Minisat namespace */
+} /* CVC4 namespace */

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

diff --git a/src/prop/minisat/simp/Main.cc b/src/prop/minisat/simp/Main.cc
index ff0f589cd10d8c8842c59b9197567b40e3a9f99d..675d0ed60a95d26099539696b5c1d3af0ae18e26 100644 (file)
--- a/src/prop/minisat/simp/Main.cc
+++ b/src/prop/minisat/simp/Main.cc
@@ -30,11 +30,12 @@ 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/simp/SimpSolver.h"
 
-using namespace Minisat;
-
 //=================================================================================================
 
 
+namespace CVC4 {
+namespace Minisat {
+
 void printStats(Solver& solver)
 {
     double cpu_time = cpuTime();
@@ -49,6 +50,8 @@ void printStats(Solver& solver)
 }
 
 
+
+
 static Solver* solver;
 // Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
 // for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
@@ -64,12 +67,16 @@ static void SIGINT_exit(int signum) {
         printf("\n"); printf("*** INTERRUPTED ***\n"); }
     _exit(1); }
 
+} /* CVC4::Minisat namespace */
+} /* CVC4 namespace */
 
 //=================================================================================================
 // Main:
 
 int main(int argc, char** argv)
 {
+  using namespace CVC4;
+  using namespace CVC4::Minisat;
     try {
         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
         // printf("This is MiniSat 2.0 beta\n");

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 370304d222a421ee2a5eb942607d2f7465957d79..0c50627267cf52bda3767fe55df882ee9591dd9e 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -235,7 +235,7 @@ inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bo
     assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
 
 //=================================================================================================
-}
-}
+} /* CVC4::Minisat namespace */
+} /* CVC4 namespace */
 
 #endif