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<T>& from, vec<T>& 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<T>::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 <misc/util/abc_namespaces.h>
+
 #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 <class T> void sort(vec<T>& 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 <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
+
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 <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
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<T>::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 <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