From bd6d95fa2ca85c31137855af247b8d5e464be5b8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 6 Sep 2017 18:43:15 -0700 Subject: Renaming Glucose namespace to avoid collisions with external solvers. --- src/sat/glucose/AbcGlucose.cpp | 42 +++++++++++++++++++++--------------------- src/sat/glucose/Alg.h | 2 +- src/sat/glucose/Alloc.h | 2 +- src/sat/glucose/BoundedQueue.h | 2 +- src/sat/glucose/Dimacs.h | 2 +- src/sat/glucose/Glucose.cpp | 2 +- src/sat/glucose/Heap.h | 2 +- src/sat/glucose/Map.h | 2 +- src/sat/glucose/Options.cpp | 10 +++++----- src/sat/glucose/Options.h | 2 +- src/sat/glucose/ParseUtils.h | 2 +- src/sat/glucose/Queue.h | 2 +- src/sat/glucose/SimpSolver.cpp | 2 +- src/sat/glucose/SimpSolver.h | 2 +- src/sat/glucose/Solver.h | 2 +- src/sat/glucose/SolverTypes.h | 8 ++++---- src/sat/glucose/Sort.h | 2 +- src/sat/glucose/System.cpp | 12 ++++++------ src/sat/glucose/System.h | 6 +++--- src/sat/glucose/Vec.h | 2 +- src/sat/glucose/XAlloc.h | 2 +- 21 files changed, 55 insertions(+), 55 deletions(-) diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index b5c6b592..8825b763 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/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 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 lits; for (int i=0;isolveLimited(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************************************************************* diff --git a/src/sat/glucose/Alg.h b/src/sat/glucose/Alg.h index 401c9bd8..fd0d0b47 100644 --- a/src/sat/glucose/Alg.h +++ b/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: diff --git a/src/sat/glucose/Alloc.h b/src/sat/glucose/Alloc.h index 11b1350c..997a2516 100644 --- a/src/sat/glucose/Alloc.h +++ b/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: diff --git a/src/sat/glucose/BoundedQueue.h b/src/sat/glucose/BoundedQueue.h index dba9166d..6f510cda 100644 --- a/src/sat/glucose/BoundedQueue.h +++ b/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 bqueue { diff --git a/src/sat/glucose/Dimacs.h b/src/sat/glucose/Dimacs.h index aa98e9aa..00af09fc 100644 --- a/src/sat/glucose/Dimacs.h +++ b/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: diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index ac849584..7d8792ce 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/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: diff --git a/src/sat/glucose/Heap.h b/src/sat/glucose/Heap.h index d4c4cd86..14c113be 100644 --- a/src/sat/glucose/Heap.h +++ b/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. diff --git a/src/sat/glucose/Map.h b/src/sat/glucose/Map.h index 955996df..4fd2a89d 100644 --- a/src/sat/glucose/Map.h +++ b/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 diff --git a/src/sat/glucose/Options.cpp b/src/sat/glucose/Options.cpp index ba313dd3..c4729b04 100644 --- a/src/sat/glucose/Options.cpp +++ b/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) diff --git a/src/sat/glucose/Options.h b/src/sat/glucose/Options.h index bfe87197..08e9543e 100644 --- a/src/sat/glucose/Options.h +++ b/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: diff --git a/src/sat/glucose/ParseUtils.h b/src/sat/glucose/ParseUtils.h index 874931a4..adf0eff9 100644 --- a/src/sat/glucose/ParseUtils.h +++ b/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: diff --git a/src/sat/glucose/Queue.h b/src/sat/glucose/Queue.h index aa171179..b63558a6 100644 --- a/src/sat/glucose/Queue.h +++ b/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 { //================================================================================================= diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp index d7fe9658..1c3ee67b 100644 --- a/src/sat/glucose/SimpSolver.cpp +++ b/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: diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h index 816d10bc..3f02f13e 100644 --- a/src/sat/glucose/SimpSolver.h +++ b/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 { //================================================================================================= diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h index 491ca4c9..df110f67 100644 --- a/src/sat/glucose/Solver.h +++ b/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: diff --git a/src/sat/glucose/SolverTypes.h b/src/sat/glucose/SolverTypes.h index 21b9c2a8..78bc7d94 100644 --- a/src/sat/glucose/SolverTypes.h +++ b/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; diff --git a/src/sat/glucose/Sort.h b/src/sat/glucose/Sort.h index 899e01ab..34f816ce 100644 --- a/src/sat/glucose/Sort.h +++ b/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 struct LessThan_default { diff --git a/src/sat/glucose/System.cpp b/src/sat/glucose/System.cpp index d6c5a9fd..17f88088 100644 --- a/src/sat/glucose/System.cpp +++ b/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 #include -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 -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 diff --git a/src/sat/glucose/System.h b/src/sat/glucose/System.h index 9d94785e..d5011919 100644 --- a/src/sat/glucose/System.h +++ b/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 -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 #include #include -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; } diff --git a/src/sat/glucose/Vec.h b/src/sat/glucose/Vec.h index 79ce8cf7..8db84a03 100644 --- a/src/sat/glucose/Vec.h +++ b/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 diff --git a/src/sat/glucose/XAlloc.h b/src/sat/glucose/XAlloc.h index 6907e665..6724fb09 100644 --- a/src/sat/glucose/XAlloc.h +++ b/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 #include -namespace Glucose { +namespace Gluco { //================================================================================================= // Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing: -- cgit v1.2.3