From 7bcfe6436938d8354f499522b3d013229931b009 Mon Sep 17 00:00:00 2001 From: Baruch Sterin Date: Thu, 23 Nov 2017 23:32:44 -0800 Subject: C++ comaptibility: add namespace support to Glucose --- src/base/abc/abc.h | 2 ++ src/misc/util/abc_namespaces.h | 6 ++++++ src/sat/glucose/AbcGlucose.cpp | 7 ++----- src/sat/glucose/AbcGlucose.h | 4 ++-- src/sat/glucose/AbcGlucoseCmd.cpp | 11 ++++++++--- src/sat/glucose/Alg.h | 4 ++++ src/sat/glucose/Alloc.h | 4 ++++ src/sat/glucose/BoundedQueue.h | 4 ++++ src/sat/glucose/Dimacs.h | 4 ++++ src/sat/glucose/Glucose.cpp | 6 +++++- src/sat/glucose/Heap.h | 4 ++++ src/sat/glucose/IntTypes.h | 2 ++ src/sat/glucose/Map.h | 4 ++++ src/sat/glucose/Options.cpp | 3 +++ src/sat/glucose/Options.h | 4 ++++ src/sat/glucose/ParseUtils.h | 4 ++++ src/sat/glucose/Queue.h | 4 ++++ src/sat/glucose/SimpSolver.cpp | 4 +++- src/sat/glucose/SimpSolver.h | 3 +++ src/sat/glucose/Solver.h | 3 +++ src/sat/glucose/SolverTypes.h | 5 ++++- src/sat/glucose/Sort.h | 3 +++ src/sat/glucose/System.cpp | 19 +++++++++++++++++++ src/sat/glucose/System.h | 13 +++++++++++++ src/sat/glucose/Vec.h | 4 ++++ src/sat/glucose/XAlloc.h | 6 ++++++ 26 files changed, 124 insertions(+), 13 deletions(-) diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 2489c140..8ac5040d 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -1043,6 +1043,8 @@ extern ABC_DLL void Abc_NtkPrintCiLevels( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkReverseTopoOrder( Abc_Ntk_t * pNtk ); extern ABC_DLL int Abc_NtkIsTopo( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkTransferPhases( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk ); +extern ABC_DLL Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp ); + /*=== abcVerify.c ==========================================================*/ diff --git a/src/misc/util/abc_namespaces.h b/src/misc/util/abc_namespaces.h index 76826f75..9588e1b8 100644 --- a/src/misc/util/abc_namespaces.h +++ b/src/misc/util/abc_namespaces.h @@ -30,6 +30,8 @@ # ifdef ABC_NAMESPACE # define ABC_NAMESPACE_HEADER_START namespace ABC_NAMESPACE { # define ABC_NAMESPACE_HEADER_END } +# define ABC_NAMESPACE_CXX_HEADER_START ABC_NAMESPACE_HEADER_START +# define ABC_NAMESPACE_CXX_HEADER_END ABC_NAMESPACE_HEADER_END # define ABC_NAMESPACE_IMPL_START namespace ABC_NAMESPACE { # define ABC_NAMESPACE_IMPL_END } # define ABC_NAMESPACE_PREFIX ABC_NAMESPACE:: @@ -37,6 +39,8 @@ # else # define ABC_NAMESPACE_HEADER_START extern "C" { # define ABC_NAMESPACE_HEADER_END } +# define ABC_NAMESPACE_CXX_HEADER_START +# define ABC_NAMESPACE_CXX_HEADER_END # define ABC_NAMESPACE_IMPL_START # define ABC_NAMESPACE_IMPL_END # define ABC_NAMESPACE_PREFIX @@ -45,6 +49,8 @@ #else # define ABC_NAMESPACE_HEADER_START # define ABC_NAMESPACE_HEADER_END +# define ABC_NAMESPACE_CXX_HEADER_START +# define ABC_NAMESPACE_CXX_HEADER_END # define ABC_NAMESPACE_IMPL_START # define ABC_NAMESPACE_IMPL_END # define ABC_NAMESPACE_PREFIX diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 6069065b..247bc89a 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -26,15 +26,14 @@ #include "sat/glucose/AbcGlucose.h" +#include "base/abc/abc.h" #include "aig/gia/gia.h" #include "sat/cnf/cnf.h" #include "misc/extra/extra.h" -using namespace Gluco; - ABC_NAMESPACE_IMPL_START -extern "C" { +using namespace Gluco; //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1367,6 +1366,4 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -} - ABC_NAMESPACE_IMPL_END diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index 1bf29aed..4489adc7 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -31,13 +31,13 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -ABC_NAMESPACE_HEADER_START - #define GLUCOSE_UNSAT -1 #define GLUCOSE_SAT 1 #define GLUCOSE_UNDEC 0 +ABC_NAMESPACE_HEADER_START + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/glucose/AbcGlucoseCmd.cpp b/src/sat/glucose/AbcGlucoseCmd.cpp index 404685cf..591f7761 100644 --- a/src/sat/glucose/AbcGlucoseCmd.cpp +++ b/src/sat/glucose/AbcGlucoseCmd.cpp @@ -23,6 +23,14 @@ #include "sat/glucose/AbcGlucose.h" + +ABC_NAMESPACE_HEADER_START + +void Glucose_Init(Abc_Frame_t *pAbc); +void Glucose_End( Abc_Frame_t * pAbc ); + +ABC_NAMESPACE_HEADER_END + ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// @@ -46,7 +54,6 @@ static int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ); SeeAlso [] ***********************************************************************/ -extern "C" { void Glucose_Init(Abc_Frame_t *pAbc) { @@ -57,8 +64,6 @@ void Glucose_End( Abc_Frame_t * pAbc ) { } -} - /**Function************************************************************* Synopsis [] diff --git a/src/sat/glucose/Alg.h b/src/sat/glucose/Alg.h index fd0d0b47..2d9f4122 100644 --- a/src/sat/glucose/Alg.h +++ b/src/sat/glucose/Alg.h @@ -23,6 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "sat/glucose/Vec.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -81,4 +83,6 @@ static inline void append(const vec& from, vec& to){ copy(from, to, true); //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/Alloc.h b/src/sat/glucose/Alloc.h index 5dfad58a..e56b5441 100644 --- a/src/sat/glucose/Alloc.h +++ b/src/sat/glucose/Alloc.h @@ -24,6 +24,8 @@ 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" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -129,4 +131,6 @@ RegionAllocator::alloc(int size) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/BoundedQueue.h b/src/sat/glucose/BoundedQueue.h index 6f510cda..00ba072f 100644 --- a/src/sat/glucose/BoundedQueue.h +++ b/src/sat/glucose/BoundedQueue.h @@ -25,6 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "sat/glucose/Vec.h" +ABC_NAMESPACE_CXX_HEADER_START + //================================================================================================= namespace Gluco { @@ -107,4 +109,6 @@ public: } //================================================================================================= +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/Dimacs.h b/src/sat/glucose/Dimacs.h index 00af09fc..bea6eaf9 100644 --- a/src/sat/glucose/Dimacs.h +++ b/src/sat/glucose/Dimacs.h @@ -26,6 +26,8 @@ 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" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -86,4 +88,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index bfe90361..3ca372a8 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -34,6 +34,8 @@ 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" +ABC_NAMESPACE_IMPL_START + using namespace Gluco; //================================================================================================= @@ -1490,4 +1492,6 @@ void Solver::reset() add_tmp.clear(false); assumptionPositions.clear(false); initialPositions.clear(false); -} \ No newline at end of file +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/glucose/Heap.h b/src/sat/glucose/Heap.h index 14c113be..820d9362 100644 --- a/src/sat/glucose/Heap.h +++ b/src/sat/glucose/Heap.h @@ -23,6 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "sat/glucose/Vec.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -147,4 +149,6 @@ class Heap { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/IntTypes.h b/src/sat/glucose/IntTypes.h index de2bdea7..3f75862b 100644 --- a/src/sat/glucose/IntTypes.h +++ b/src/sat/glucose/IntTypes.h @@ -44,4 +44,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #endif //================================================================================================= +#include + #endif diff --git a/src/sat/glucose/Map.h b/src/sat/glucose/Map.h index 4fd2a89d..bc08317f 100644 --- a/src/sat/glucose/Map.h +++ b/src/sat/glucose/Map.h @@ -23,6 +23,8 @@ 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" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -190,4 +192,6 @@ class Map { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/Options.cpp b/src/sat/glucose/Options.cpp index d9521c52..a310809e 100644 --- a/src/sat/glucose/Options.cpp +++ b/src/sat/glucose/Options.cpp @@ -21,6 +21,8 @@ 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" +ABC_NAMESPACE_IMPL_START + using namespace Gluco; void Gluco::parseOptions(int& argc, char** argv, bool strict) @@ -90,3 +92,4 @@ void Gluco::printUsageAndExit (int argc, char** argv, bool verbose) exit(0); } +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/glucose/Options.h b/src/sat/glucose/Options.h index 598d66d6..bc55b2f3 100644 --- a/src/sat/glucose/Options.h +++ b/src/sat/glucose/Options.h @@ -31,6 +31,8 @@ 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" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================== @@ -385,4 +387,6 @@ class BoolOption : public Option //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/ParseUtils.h b/src/sat/glucose/ParseUtils.h index adf0eff9..a3f25a62 100644 --- a/src/sat/glucose/ParseUtils.h +++ b/src/sat/glucose/ParseUtils.h @@ -27,6 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "misc/zlib/zlib.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //------------------------------------------------------------------------------------------------- @@ -148,4 +150,6 @@ static bool eagerMatch(B& in, const char* str) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/Queue.h b/src/sat/glucose/Queue.h index b63558a6..f1043d22 100644 --- a/src/sat/glucose/Queue.h +++ b/src/sat/glucose/Queue.h @@ -23,6 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "sat/glucose/Vec.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -66,4 +68,6 @@ public: //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp index f46ae03e..f4436d43 100644 --- a/src/sat/glucose/SimpSolver.cpp +++ b/src/sat/glucose/SimpSolver.cpp @@ -22,6 +22,8 @@ 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" +ABC_NAMESPACE_IMPL_START + using namespace Gluco; //================================================================================================= @@ -771,4 +773,4 @@ void SimpSolver::reset() remove_satisfied = false; } - +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h index 6c9272a2..8cfb171c 100644 --- a/src/sat/glucose/SimpSolver.h +++ b/src/sat/glucose/SimpSolver.h @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "sat/glucose/Queue.h" #include "sat/glucose/Solver.h" +ABC_NAMESPACE_CXX_HEADER_START namespace Gluco { @@ -201,4 +202,6 @@ inline void SimpSolver::addVar(Var v) { while (v >= nVars()) newVar(); } //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h index 43053062..df72660a 100644 --- a/src/sat/glucose/Solver.h +++ b/src/sat/glucose/Solver.h @@ -37,6 +37,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "sat/glucose/BoundedQueue.h" #include "sat/glucose/Constants.h" +ABC_NAMESPACE_CXX_HEADER_START namespace Gluco { @@ -488,4 +489,6 @@ inline void Solver::printInitialClause(CRef cr) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/SolverTypes.h b/src/sat/glucose/SolverTypes.h index 2f0796c9..4f2670a7 100644 --- a/src/sat/glucose/SolverTypes.h +++ b/src/sat/glucose/SolverTypes.h @@ -38,6 +38,8 @@ 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" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -430,5 +432,6 @@ inline void Clause::strengthen(Lit p) //================================================================================================= } - +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/Sort.h b/src/sat/glucose/Sort.h index 34f816ce..cecfc654 100644 --- a/src/sat/glucose/Sort.h +++ b/src/sat/glucose/Sort.h @@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //================================================================================================= // Some sorting algorithms for vec's +ABC_NAMESPACE_CXX_HEADER_START namespace Gluco { @@ -95,4 +96,6 @@ template void sort(vec& v) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/System.cpp b/src/sat/glucose/System.cpp index 17f88088..8fc5ce26 100644 --- a/src/sat/glucose/System.cpp +++ b/src/sat/glucose/System.cpp @@ -25,6 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include +ABC_NAMESPACE_IMPL_START + using namespace Gluco; // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and @@ -72,24 +74,41 @@ double Gluco::memUsedPeak() { double peak = memReadPeak() / 1024; return peak == 0 ? memUsed() : peak; } +ABC_NAMESPACE_IMPL_END + #elif defined(__FreeBSD__) +ABC_NAMESPACE_IMPL_START + double Gluco::memUsed(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_maxrss / 1024; } double MiniSat::memUsedPeak(void) { return memUsed(); } +ABC_NAMESPACE_IMPL_END #elif defined(__APPLE__) + #include +ABC_NAMESPACE_IMPL_START + double Gluco::memUsed(void) { malloc_statistics_t t; malloc_zone_statistics(NULL, &t); return (double)t.max_size_in_use / (1024*1024); } +ABC_NAMESPACE_IMPL_END + #else + +ABC_NAMESPACE_IMPL_START + double Gluco::memUsed() { return 0; } + +ABC_NAMESPACE_IMPL_END + #endif + diff --git a/src/sat/glucose/System.h b/src/sat/glucose/System.h index a7f8c93d..5529af95 100644 --- a/src/sat/glucose/System.h +++ b/src/sat/glucose/System.h @@ -27,6 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "sat/glucose/IntTypes.h" +ABC_NAMESPACE_CXX_HEADER_START + //------------------------------------------------------------------------------------------------- namespace Gluco { @@ -37,24 +39,35 @@ extern double memUsedPeak(); // Peak-memory in mega bytes (returns 0 for } +ABC_NAMESPACE_CXX_HEADER_END + //------------------------------------------------------------------------------------------------- // Implementation of inline functions: #if defined(_MSC_VER) || defined(__MINGW32__) #include +ABC_NAMESPACE_CXX_HEADER_START + static inline double Gluco::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; } +ABC_NAMESPACE_CXX_HEADER_END + + #else #include #include #include +ABC_NAMESPACE_CXX_HEADER_START + 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; } +ABC_NAMESPACE_CXX_HEADER_END + #endif #endif diff --git a/src/sat/glucose/Vec.h b/src/sat/glucose/Vec.h index f44c65f0..da87af35 100644 --- a/src/sat/glucose/Vec.h +++ b/src/sat/glucose/Vec.h @@ -27,6 +27,8 @@ 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" +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -127,4 +129,6 @@ void vec::clear(bool dealloc) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/glucose/XAlloc.h b/src/sat/glucose/XAlloc.h index 6724fb09..233f834e 100644 --- a/src/sat/glucose/XAlloc.h +++ b/src/sat/glucose/XAlloc.h @@ -25,6 +25,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include +#include + +ABC_NAMESPACE_CXX_HEADER_START + namespace Gluco { //================================================================================================= @@ -44,4 +48,6 @@ static inline void* xrealloc(void *ptr, size_t size) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif -- cgit v1.2.3