C++ comaptibility: add namespace support to Glucose

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 ==========================================================*/

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

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

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                              ///
 ////////////////////////////////////////////////////////////////////////

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    []

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<T>& from, vec<T>& to){ copy(from, to, true);
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

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<T>::alloc(int size)
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

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

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

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);
-}
+}
+
+ABC_NAMESPACE_IMPL_END

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

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 <misc/util/abc_namespaces.h>
+
 #endif

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

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

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

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

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

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

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

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

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

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 <class T> void sort(vec<T>& v) {
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

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 <stdio.h>
 #include <stdlib.h>
 
+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 <malloc/malloc.h>
 
+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
+

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 <time.h>
 
+ABC_NAMESPACE_CXX_HEADER_START
+
 static inline double Gluco::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
+
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
 
+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

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<T>::clear(bool dealloc) {
 //=================================================================================================
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #endif

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 <stdlib.h>
 #include <stdio.h>
 
+#include <misc/util/abc_namespaces.h>
+
+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