Renaming Glucose namespace to avoid collisions with external solvers.

src/sat/glucose/AbcGlucose.cpp

@@ -29,7 +29,7 @@
 #include "aig/gia/gia.h"
 #include "sat/cnf/cnf.h"
 
-using namespace Glucose;
+using namespace Gluco;
 
 ABC_NAMESPACE_IMPL_START
 
@@ -54,19 +54,19 @@ extern "C" {
   SeeAlso     []
 
 ***********************************************************************/
-Glucose::Solver * glucose_solver_start()
+Gluco::Solver * glucose_solver_start()
 {
     Solver * S = new Solver;
     S->setIncrementalMode();
     return S;
 }
 
-void glucose_solver_stop(Glucose::Solver* S)
+void glucose_solver_stop(Gluco::Solver* S)
 {
     delete S;
 }
 
-int glucose_solver_addclause(Glucose::Solver* S, int * plits, int nlits)
+int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits)
 {
     vec<Lit> lits;
     for ( int i = 0; i < nlits; i++,plits++)
@@ -81,14 +81,14 @@ int glucose_solver_addclause(Glucose::Solver* S, int * plits, int nlits)
     return S->addClause(lits); // returns 0 if the problem is UNSAT
 }
 
-void glucose_solver_setcallback(Glucose::Solver* S, void * pman, int(*pfunc)(void*, int, int*))
+void glucose_solver_setcallback(Gluco::Solver* S, void * pman, int(*pfunc)(void*, int, int*))
 {
     S->pCnfMan = pman;
     S->pCnfFunc = pfunc;
     S->nCallConfl = 1000;
 }
 
-int glucose_solver_solve(Glucose::Solver* S, int * plits, int nlits)
+int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits)
 {
     vec<Lit> lits;
     for (int i=0;i<nlits;i++,plits++)
@@ -97,22 +97,22 @@ int glucose_solver_solve(Glucose::Solver* S, int * plits, int nlits)
         p.x = *plits;
         lits.push(p);
     }
-    Glucose::lbool res = S->solveLimited(lits);
+    Gluco::lbool res = S->solveLimited(lits);
     return (res == l_True ? 1 : res == l_False ? -1 : 0);
 }
 
-int glucose_solver_addvar(Glucose::Solver* S)
+int glucose_solver_addvar(Gluco::Solver* S)
 {
     S->newVar();
     return S->nVars() - 1;
 }
 
-int glucose_solver_read_cex_varvalue(Glucose::Solver* S, int ivar)
+int glucose_solver_read_cex_varvalue(Gluco::Solver* S, int ivar)
 {
     return S->model[ivar] == l_True;
 }
 
-void glucose_solver_setstop(Glucose::Solver* S, int * pstop)
+void glucose_solver_setstop(Gluco::Solver* S, int * pstop)
 {
     S->pstop = pstop;
 }
@@ -155,54 +155,54 @@ bmcg_sat_solver * bmcg_sat_solver_start()
 }
 void bmcg_sat_solver_stop(bmcg_sat_solver* s)
 {
-    glucose_solver_stop((Glucose::Solver*)s);
+    glucose_solver_stop((Gluco::Solver*)s);
 }
 
 int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits)
 {
-    return glucose_solver_addclause((Glucose::Solver*)s,plits,nlits);
+    return glucose_solver_addclause((Gluco::Solver*)s,plits,nlits);
 }
 
 void bmcg_sat_solver_setcallback(bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*))
 {
-    glucose_solver_setcallback((Glucose::Solver*)s,pman,pfunc);
+    glucose_solver_setcallback((Gluco::Solver*)s,pman,pfunc);
 }
 
 int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits)
 {
-    return glucose_solver_solve((Glucose::Solver*)s,plits,nlits);
+    return glucose_solver_solve((Gluco::Solver*)s,plits,nlits);
 }
 
 int bmcg_sat_solver_addvar(bmcg_sat_solver* s)
 {
-    return glucose_solver_addvar((Glucose::Solver*)s);
+    return glucose_solver_addvar((Gluco::Solver*)s);
 }
 
 int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
 {
-    return glucose_solver_read_cex_varvalue((Glucose::Solver*)s, ivar);
+    return glucose_solver_read_cex_varvalue((Gluco::Solver*)s, ivar);
 }
 
 void bmcg_sat_solver_setstop(bmcg_sat_solver* s, int * pstop)
 {
-    glucose_solver_setstop((Glucose::Solver*)s, pstop);
+    glucose_solver_setstop((Gluco::Solver*)s, pstop);
 }
 
 int bmcg_sat_solver_varnum(bmcg_sat_solver* s)
 {
-    return ((Glucose::Solver*)s)->nVars();
+    return ((Gluco::Solver*)s)->nVars();
 }
 int bmcg_sat_solver_clausenum(bmcg_sat_solver* s)
 {
-    return ((Glucose::Solver*)s)->nClauses();
+    return ((Gluco::Solver*)s)->nClauses();
 }
 int bmcg_sat_solver_learntnum(bmcg_sat_solver* s)
 {
-    return ((Glucose::Solver*)s)->nLearnts();
+    return ((Gluco::Solver*)s)->nLearnts();
 }
 int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s)
 {
-    return ((Glucose::Solver*)s)->conflicts;
+    return ((Gluco::Solver*)s)->conflicts;
 }
 
 /**Function*************************************************************

src/sat/glucose/Alg.h

@@ -23,7 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "sat/glucose/Vec.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // Useful functions on vector-like types:

src/sat/glucose/Alloc.h

@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/XAlloc.h"
 #include "sat/glucose/Vec.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // Simple Region-based memory allocator:

src/sat/glucose/BoundedQueue.h

@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 //=================================================================================================
 
-namespace Glucose {
+namespace Gluco {
 
 template <class T>
 class bqueue {

src/sat/glucose/Dimacs.h

@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/ParseUtils.h"
 #include "sat/glucose/SolverTypes.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // DIMACS Parser:

src/sat/glucose/Glucose.cpp

@@ -34,7 +34,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/Constants.h"
 #include "sat/glucose/System.h"
 
-using namespace Glucose;
+using namespace Gluco;
 
 //=================================================================================================
 // Options:

src/sat/glucose/Heap.h

@@ -23,7 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "sat/glucose/Vec.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // A heap implementation with support for decrease/increase key.

src/sat/glucose/Map.h

@@ -23,7 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/IntTypes.h"
 #include "sat/glucose/Vec.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // Default hash/equals functions

src/sat/glucose/Options.cpp

@@ -21,9 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/Options.h"
 #include "sat/glucose/ParseUtils.h"
 
-using namespace Glucose;
+using namespace Gluco;
 
-void Glucose::parseOptions(int& argc, char** argv, bool strict)
+void Gluco::parseOptions(int& argc, char** argv, bool strict)
 {
     int i, j;
     for (i = j = 1; i < argc; i++){
@@ -54,9 +54,9 @@ void Glucose::parseOptions(int& argc, char** argv, bool strict)
 }
 
 
-void Glucose::setUsageHelp      (const char* str){ Option::getUsageString() = str; }
-void Glucose::setHelpPrefixStr  (const char* str){ Option::getHelpPrefixString() = str; }
-void Glucose::printUsageAndExit (int argc, char** argv, bool verbose)
+void Gluco::setUsageHelp      (const char* str){ Option::getUsageString() = str; }
+void Gluco::setHelpPrefixStr  (const char* str){ Option::getHelpPrefixString() = str; }
+void Gluco::printUsageAndExit (int argc, char** argv, bool verbose)
 {
     const char* usage = Option::getUsageString();
     if (usage != NULL)

src/sat/glucose/Options.h

@@ -31,7 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/Vec.h"
 #include "sat/glucose/ParseUtils.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //==================================================================================================
 // Top-level option parse/help functions:

src/sat/glucose/ParseUtils.h

@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "misc/zlib/zlib.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //-------------------------------------------------------------------------------------------------
 // A simple buffered character stream class:

src/sat/glucose/Queue.h

@@ -23,7 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "sat/glucose/Vec.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 

src/sat/glucose/SimpSolver.cpp

@@ -22,7 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/SimpSolver.h"
 #include "sat/glucose/System.h"
 
-using namespace Glucose;
+using namespace Gluco;
 
 //=================================================================================================
 // Options:

src/sat/glucose/SimpSolver.h

@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/Solver.h"
 
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 

src/sat/glucose/Solver.h

@@ -38,7 +38,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/Constants.h"
 
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // Solver -- the main class:

src/sat/glucose/SolverTypes.h

@@ -38,7 +38,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/Map.h"
 #include "sat/glucose/Alloc.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // Variables, literals, lifted booleans, clauses:
@@ -88,9 +88,9 @@ const Lit lit_Error = { -1 };  // }
 //       does enough constant propagation to produce sensible code, and this appears to be somewhat
 //       fragile unfortunately.
 
-#define l_True  (Glucose::lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
-#define l_False (Glucose::lbool((uint8_t)1))
-#define l_Undef (Glucose::lbool((uint8_t)2))
+#define l_True  (Gluco::lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
+#define l_False (Gluco::lbool((uint8_t)1))
+#define l_Undef (Gluco::lbool((uint8_t)2))
 
 class lbool {
     uint8_t value;

src/sat/glucose/Sort.h

@@ -27,7 +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 Glucose {
+namespace Gluco {
 
 template<class T>
 struct LessThan_default {

src/sat/glucose/System.cpp

@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdio.h>
 #include <stdlib.h>
 
-using namespace Glucose;
+using namespace Gluco;
 
 // 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 +67,14 @@ static inline int memReadPeak(void)
     return peak_kb;
 }
 
-double Glucose::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
-double Glucose::memUsedPeak() { 
+double Gluco::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
+double Gluco::memUsedPeak() { 
     double peak = memReadPeak() / 1024;
     return peak == 0 ? memUsed() : peak; }
 
 #elif defined(__FreeBSD__)
 
-double Glucose::memUsed(void) {
+double Gluco::memUsed(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
     return (double)ru.ru_maxrss / 1024; }
@@ -84,12 +84,12 @@ double MiniSat::memUsedPeak(void) { return memUsed(); }
 #elif defined(__APPLE__)
 #include <malloc/malloc.h>
 
-double Glucose::memUsed(void) {
+double Gluco::memUsed(void) {
     malloc_statistics_t t;
     malloc_zone_statistics(NULL, &t);
     return (double)t.max_size_in_use / (1024*1024); }
 
 #else
-double Glucose::memUsed() { 
+double Gluco::memUsed() { 
     return 0; }
 #endif

src/sat/glucose/System.h

@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 //-------------------------------------------------------------------------------------------------
 
-namespace Glucose {
+namespace Gluco {
 
 static inline double cpuTime(void); // CPU-time in seconds.
 extern double memUsed();            // Memory in mega bytes (returns 0 for unsupported architectures).
@@ -43,14 +43,14 @@ extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for
 #if defined(_MSC_VER) || defined(__MINGW32__)
 #include <time.h>
 
-static inline double Glucose::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
+static inline double Gluco::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
 
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
 
-static inline double Glucose::cpuTime(void) {
+static inline double Gluco::cpuTime(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
     return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }

src/sat/glucose/Vec.h

@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose/IntTypes.h"
 #include "sat/glucose/XAlloc.h"
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // Automatically resizable arrays

src/sat/glucose/XAlloc.h

@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdlib.h>
 #include <stdio.h>
 
-namespace Glucose {
+namespace Gluco {
 
 //=================================================================================================
 // Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing: