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 *.

22 files changed, 99 insertions, 39 deletions

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 0bf4edf6a..fc5b29e89 100644
--- 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 64df4f635..46451d464 100644
--- 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 95cfe7bfe..74cc9cde8 100644
--- 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 1267561fb..ca7228ee8 100644
--- 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 016a0c225..214e425f9 100644
--- 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 0400f956d..aa0921b78 100644
--- 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 f3ecdecc5..e61dbb415 100644
--- 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 f4303044f..4e58ab159 100644
--- 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 d57824ba1..2d7ee0199 100644
--- 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 4e61d6582..ee68a2155 100644
--- 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 83321ba95..c40f2322b 100644
--- 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 9bab9a0df..f668aa856 100644
--- 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 8c568dfe9..8ee2a827f 100644
--- 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 7b89d1803..9e469a6fb 100644
--- 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 bfb655782..96e318e5f 100644
--- 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 c65189985..e7e489985 100644
--- 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 4ff17d3ab..707f62e34 100644
--- 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 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; }