This fixes a one definition rule violation for reduceDB_lt in Solver.cc in minisat and bvminisat. This also moves BVMinisat into CVC4. This also wrapped code in cpp files into the namespaces instead of having using namespace *.

5 files changed, 31 insertions, 16 deletions

diff --git a/src/prop/bvminisat/utils/Options.cc b/src/prop/bvminisat/utils/Options.cc
index a15220c4b..b2094d466 100644
--- 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 2092a87e4..12321cba2 100644
--- 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 fc2ce9cbe..46f404c3e 100644
--- 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 9c2fcb083..dab33af3e 100644
--- 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 4b4b73cb9..a065ef916 100644
--- 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; }