initial commit of public abc

16 files changed, 143 insertions, 68 deletions

diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 2b28700c..6dc68cf8 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -21,6 +21,7 @@
 #ifndef __MSAT_H__
 #define __MSAT_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -29,22 +30,15 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef bool
-#undef bool
-#endif
-
-#ifndef __MVTYPES_H__
-typedef int  bool;
-#endif
-
 typedef struct Msat_Solver_t_      Msat_Solver_t;
 
 // the vector of intergers and of clauses
@@ -77,13 +71,13 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
 ////////////////////////////////////////////////////////////////////////
 
 /*=== satRead.c ============================================================*/
-extern bool             Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
+extern int              Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
 /*=== satSolver.c ===========================================================*/
 // adding vars, clauses, simplifying the database, and solving
-extern bool             Msat_SolverAddVar( Msat_Solver_t * p, int Level );
-extern bool             Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
-extern bool             Msat_SolverSimplifyDB( Msat_Solver_t * p );
-extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
+extern int              Msat_SolverAddVar( Msat_Solver_t * p, int Level );
+extern int              Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
+extern int              Msat_SolverSimplifyDB( Msat_Solver_t * p );
+extern int              Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
 // printing stats, assignments, and clauses
 extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
 extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
@@ -116,7 +110,7 @@ extern void             Msat_SolverRemoveLearned( Msat_Solver_t * p );
 extern void             Msat_SolverRemoveMarked( Msat_Solver_t * p );
 /*=== satSolverApi.c ===========================================================*/
 // allocation, cleaning, and freeing the solver
-extern Msat_Solver_t *  Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose );
+extern Msat_Solver_t *  Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, int fVerbose );
 extern void             Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc );
 extern void             Msat_SolverClean( Msat_Solver_t * p, int nVars );
 extern void             Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars );
@@ -161,9 +155,11 @@ extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double Weigh
 extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
 extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  
  
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index 1cd795bd..6ac27e2c 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -158,3 +161,5 @@ void Msat_SolverClaRescaleActivity( Msat_Solver_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index ca698866..a464f23a 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -52,7 +55,7 @@ struct Msat_Clause_t_
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, Msat_Clause_t ** pClause_out )
+int  Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, int  fLearned, Msat_Clause_t ** pClause_out )
 {
     int * pAssigns = Msat_SolverReadAssignsArray(p);
     Msat_ClauseVec_t ** pvWatched;
@@ -61,7 +64,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
     int nLits, i, j;
     int nBytes;
     Msat_Var_t Var;
-    bool Sign;
+    int  Sign;
 
     *pClause_out = NULL;
 
@@ -217,7 +220,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
   SeeAlso     []
 
 ***********************************************************************/
-void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched )
+void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, int  fRemoveWatched )
 {
     if ( fRemoveWatched )
     {
@@ -249,16 +252,16 @@ void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched
   SeeAlso     []
 
 ***********************************************************************/
-bool  Msat_ClauseReadLearned( Msat_Clause_t * pC )  {  return pC->fLearned; }
+int   Msat_ClauseReadLearned( Msat_Clause_t * pC )  {  return pC->fLearned; }
 int   Msat_ClauseReadSize( Msat_Clause_t * pC )     {  return pC->nSize;    }
 int * Msat_ClauseReadLits( Msat_Clause_t * pC )     {  return pC->pData;    }
-bool  Msat_ClauseReadMark( Msat_Clause_t * pC )     {  return pC->fMark;    }
+int   Msat_ClauseReadMark( Msat_Clause_t * pC )     {  return pC->fMark;    }
 int   Msat_ClauseReadNum( Msat_Clause_t * pC )      {  return pC->Num;      }
-bool  Msat_ClauseReadTypeA( Msat_Clause_t * pC )    {  return pC->fTypeA;    }
+int   Msat_ClauseReadTypeA( Msat_Clause_t * pC )    {  return pC->fTypeA;    }
 
-void  Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark )   {  pC->fMark = fMark;   }
+void  Msat_ClauseSetMark( Msat_Clause_t * pC, int  fMark )   {  pC->fMark = fMark;   }
 void  Msat_ClauseSetNum( Msat_Clause_t * pC, int Num )       {  pC->Num = Num;       }
-void  Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) {  pC->fTypeA = fTypeA; }
+void  Msat_ClauseSetTypeA( Msat_Clause_t * pC, int  fTypeA ) {  pC->fTypeA = fTypeA; }
 
 /**Function*************************************************************
 
@@ -272,10 +275,10 @@ void  Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) {  pC->fTypeA = fTy
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC )
+int  Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC )
 {
     Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p );
-    return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
+    return (int )(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
 }
 
 /**Function*************************************************************
@@ -326,7 +329,7 @@ void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out )
+int  Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out )
 {
     // make sure the false literal is pC->pData[1]
     Msat_Lit_t LitF = MSAT_LITNOT(Lit);
@@ -365,7 +368,7 @@ bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, M
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns )
+int  Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns )
 {
     Msat_Var_t Var;
     int i, j;
@@ -485,7 +488,7 @@ void Msat_ClausePrint( Msat_Clause_t * pC )
   SeeAlso     []
 
 ***********************************************************************/
-void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement )
+void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, int  fIncrement )
 {
     int i;
     for ( i = 0; i < (int)pC->nSize; i++ )
@@ -527,3 +530,5 @@ void Msat_ClausePrintSymbols( Msat_Clause_t * pC )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c
index f29de389..71895711 100644
--- a/src/sat/msat/msatClauseVec.c
+++ b/src/sat/msat/msatClauseVec.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -230,3 +233,5 @@ Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index b6759a0f..b4b5ff77 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -21,6 +21,7 @@
 #ifndef __MSAT_INT_H__
 #define __MSAT_INT_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -31,9 +32,13 @@
 #include <assert.h>
 #include <time.h>
 #include <math.h>
+
 #include "abc_global.h"
 #include "msat.h"
 
+ABC_NAMESPACE_HEADER_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
@@ -120,7 +125,7 @@ struct Msat_Solver_t_
 
     double              dRandSeed;   // For the internal random number generator (makes solver deterministic over different platforms). 
 
-    bool                fVerbose;    // the verbosity flag
+    int                 fVerbose;    // the verbosity flag
     double              dProgress;   // Set by 'search()'.
 
     // the variable cone and variable connectivity
@@ -197,10 +202,10 @@ extern void                Msat_SolverClausesIncrementL( Msat_Solver_t * p );
 extern void                Msat_SolverClausesDecrementL( Msat_Solver_t * p );
 extern void                Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit );
 extern void                Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC );
-extern bool                Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC );
+extern int                 Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC );
 extern double              Msat_SolverProgressEstimate( Msat_Solver_t * p );
 /*=== satSolverSearch.c ===========================================================*/
-extern bool                Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit );
+extern int                 Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit );
 extern Msat_Clause_t *     Msat_SolverPropagate( Msat_Solver_t * p );
 extern void                Msat_SolverCancelUntil( Msat_Solver_t * p, int Level );
 extern Msat_Type_t         Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars );
@@ -222,29 +227,29 @@ extern void                Msat_OrderVarAssigned( Msat_Order_t * p, int Var );
 extern void                Msat_OrderVarUnassigned( Msat_Order_t * p, int Var );
 extern void                Msat_OrderUpdate( Msat_Order_t * p, int Var );
 /*=== satClause.c ===========================================================*/
-extern bool                Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearnt, Msat_Clause_t ** pClause_out );
+extern int                 Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, int  fLearnt, Msat_Clause_t ** pClause_out );
 extern Msat_Clause_t *     Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits );
 extern Msat_Clause_t *     Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit );
-extern bool                Msat_ClauseReadLearned( Msat_Clause_t * pC );
+extern int                 Msat_ClauseReadLearned( Msat_Clause_t * pC );
 extern int                 Msat_ClauseReadSize( Msat_Clause_t * pC );
 extern int *               Msat_ClauseReadLits( Msat_Clause_t * pC );
-extern bool                Msat_ClauseReadMark( Msat_Clause_t * pC );
-extern void                Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark );
+extern int                 Msat_ClauseReadMark( Msat_Clause_t * pC );
+extern void                Msat_ClauseSetMark( Msat_Clause_t * pC, int  fMark );
 extern int                 Msat_ClauseReadNum( Msat_Clause_t * pC );
 extern void                Msat_ClauseSetNum( Msat_Clause_t * pC, int Num );
-extern bool                Msat_ClauseReadTypeA( Msat_Clause_t * pC );
-extern void                Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA );
-extern bool                Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC );
+extern int                 Msat_ClauseReadTypeA( Msat_Clause_t * pC );
+extern void                Msat_ClauseSetTypeA( Msat_Clause_t * pC, int  fTypeA );
+extern int                 Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC );
 extern float               Msat_ClauseReadActivity( Msat_Clause_t * pC );
 extern void                Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num );
-extern void                Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched );
-extern bool                Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out );
-extern bool                Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns );
+extern void                Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, int  fRemoveWatched );
+extern int                 Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out );
+extern int                 Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns );
 extern void                Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out );
 extern void                Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC );
 extern void                Msat_ClausePrint( Msat_Clause_t * pC );
 extern void                Msat_ClausePrintSymbols( Msat_Clause_t * pC );
-extern void                Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement );
+extern void                Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, int  fIncrement );
 extern unsigned            Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC );
 /*=== satSort.c ===========================================================*/
 extern void                Msat_SolverSortDB( Msat_Solver_t * p );
@@ -284,4 +289,8 @@ extern int                 Msat_MmStepReadMemUsage( Msat_MmStep_t * p );
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_HEADER_END
+
 #endif
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
index 439661f4..7e0dc0dd 100644
--- a/src/sat/msat/msatMem.c
+++ b/src/sat/msat/msatMem.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -31,7 +34,7 @@ struct Msat_MmFixed_t_
     int           nEntriesAlloc; // the total number of entries allocated
     int           nEntriesUsed;  // the number of entries in use
     int           nEntriesMax;   // the max number of entries in use
-    char *        pEntriesFree;  // the linked list of ABC_FREE entries
+    char *        pEntriesFree;  // the linked list of free entries
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -48,8 +51,8 @@ struct Msat_MmFlex_t_
 {
     // information about individual entries
     int           nEntriesUsed;  // the number of entries allocated
-    char *        pCurrent;      // the current pointer to ABC_FREE memory
-    char *        pEnd;          // the first entry outside the ABC_FREE memory
+    char *        pCurrent;      // the current pointer to free memory
+    char *        pEnd;          // the first entry outside the free memory
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -160,7 +163,7 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p )
     char * pTemp;
     int i;
 
-    // check if there are still ABC_FREE entries
+    // check if there are still free entries
     if ( p->nEntriesUsed == p->nEntriesAlloc )
     { // need to allocate more entries
         assert( p->pEntriesFree == NULL );
@@ -189,7 +192,7 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p )
     p->nEntriesUsed++;
     if ( p->nEntriesMax < p->nEntriesUsed )
         p->nEntriesMax = p->nEntriesUsed;
-    // return the first entry in the ABC_FREE entry list
+    // return the first entry in the free entry list
     pTemp = p->pEntriesFree;
     p->pEntriesFree = *((char **)pTemp);
     return pTemp;
@@ -210,7 +213,7 @@ void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry )
 {
     // decrement the counter of used entries
     p->nEntriesUsed--;
-    // add the entry to the linked list of ABC_FREE entries
+    // add the entry to the linked list of free entries
     *((char **)pEntry) = p->pEntriesFree;
     p->pEntriesFree = pEntry;
 }
@@ -244,7 +247,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
     }
     // set the last link
     *((char **)pTemp) = NULL;
-    // set the ABC_FREE entry list
+    // set the free entry list
     p->pEntriesFree  = p->pChunks[0];
     // set the correct statistics
     p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
@@ -346,7 +349,7 @@ void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose )
 char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes )
 {
     char * pTemp;
-    // check if there are still ABC_FREE entries
+    // check if there are still free entries
     if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
     { // need to allocate more entries
         if ( p->nChunks == p->nChunksAlloc )
@@ -527,3 +530,5 @@ int Msat_MmStepReadMemUsage( Msat_MmStep_t * p )
         nMemTotal += p->pMems[i]->nMemoryAlloc;
     return nMemTotal;
 }
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index 7d8484d5..2904607f 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -403,3 +406,5 @@ void Msat_HeapPercolateDown( Msat_Order_t * p, int i )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c
index 4db7ff7b..2be6b47b 100644
--- a/src/sat/msat/msatOrderJ.c
+++ b/src/sat/msat/msatOrderJ.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /* 
 The J-boundary (justification boundary) is defined as a set of unassigned 
 variables belonging to the cone of interest, such that for each of them,
@@ -470,3 +473,5 @@ void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c
index 0bcaf6b2..f025920b 100644
--- a/src/sat/msat/msatQueue.c
+++ b/src/sat/msat/msatQueue.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -155,3 +158,5 @@ void Msat_QueueClear( Msat_Queue_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c
index ba33278c..b2cae898 100644
--- a/src/sat/msat/msatRead.c
+++ b/src/sat/msat/msatRead.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -133,7 +136,7 @@ static void skipLine( char ** pIn )
 static int Msat_ReadInt( char ** pIn ) 
 {
     int     val = 0;
-    bool    neg = 0;
+    int     neg = 0;
 
     Msat_ReadWhitespace( pIn );
     if ( **pIn == '-' ) 
@@ -194,7 +197,7 @@ static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLi
   SeeAlso     []
 
 ***********************************************************************/
-static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) 
+static int  Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, int  fVerbose ) 
 {
     Msat_Solver_t * p = NULL; // Suppress "might be used uninitialized"
     Msat_IntVec_t * pLits = NULL; // Suppress "might be used uninitialized"
@@ -251,10 +254,10 @@ static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose )
+int  Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose )
 {
     char * pText;
-    bool Value;
+    int  Value;
     pText = Msat_FileRead( pFile );
     Value = Msat_ReadDimacs( pText, p, fVerbose );
     ABC_FREE( pText );
@@ -266,3 +269,5 @@ bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index 6a518212..622e94aa 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -47,7 +50,7 @@ int                Msat_SolverReadVarAllocNum( Msat_Solver_t * p )             {
 int                Msat_SolverReadDecisionLevel( Msat_Solver_t * p )           { return Msat_IntVecReadSize(p->vTrailLim); }
 int *              Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p )      { return p->pLevel;     }
 Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p )            { return p->pReasons;   }
-Msat_Lit_t          Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; }
+Msat_Type_t         Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return (Msat_Type_t)p->pAssigns[Var]; }
 Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p )                { return p->vLearned;   }
 Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p )           { return p->pvWatched;  }
 int *              Msat_SolverReadAssignsArray( Msat_Solver_t * p )            { return p->pAssigns;   }
@@ -151,7 +154,7 @@ Msat_IntVec_t *  Msat_SolverReadVarsUsed( Msat_Solver_t * p )
 Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     double dClaInc, double dClaDecay, 
     double dVarInc, double dVarDecay, 
-    bool fVerbose )
+    int  fVerbose )
 {
     Msat_Solver_t * p;
     int i;
@@ -498,3 +501,5 @@ void Msat_SolverSetupTruthTables( unsigned uTruths[][2] )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index 0462f11b..3312c23d 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -39,7 +42,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverAddVar( Msat_Solver_t * p, int Level )
+int  Msat_SolverAddVar( Msat_Solver_t * p, int Level )
 {
     if ( p->nVars == p->nVarsAlloc )
         Msat_SolverResize( p, 2 * p->nVarsAlloc );
@@ -59,10 +62,10 @@ bool Msat_SolverAddVar( Msat_Solver_t * p, int Level )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits )
+int  Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits )
 {
     Msat_Clause_t * pC; 
-    bool Value;
+    int  Value;
     Value = Msat_ClauseCreate( p, vLits, 0, &pC );
     if ( pC != NULL )
         Msat_ClauseVecPush( p->vClauses, pC );
@@ -132,7 +135,7 @@ void Msat_SolverPrintStats( Msat_Solver_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
+int  Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
 {
     Msat_SearchParams_t Params = { 0.95, 0.999 };
     double nConflictsLimit, nLearnedLimit;
@@ -208,3 +211,5 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c
index 05b7f6a9..38610b4d 100644
--- a/src/sat/msat/msatSolverIo.c
+++ b/src/sat/msat/msatSolverIo.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -175,3 +178,5 @@ char * Msat_TimeStamp()
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index 11a6540c..b3190e39 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/src/sat/msat/msatSolverSearch.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,7 +48,7 @@ static void            Msat_SolverReduceDB( Msat_Solver_t * p );
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit )
+int  Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit )
 {
     assert( Msat_QueueReadSize(p->pQueue) == 0 );
     if ( p->fVerbose )
@@ -167,7 +170,7 @@ Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC )
+int  Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC )
 {
     Msat_Var_t Var = MSAT_LIT2VAR(Lit);
 
@@ -276,7 +279,7 @@ Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverSimplifyDB( Msat_Solver_t * p )
+int  Msat_SolverSimplifyDB( Msat_Solver_t * p )
 {
     Msat_ClauseVec_t * vClauses;
     Msat_Clause_t ** pClauses;
@@ -627,3 +630,5 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatSort.c b/src/sat/msat/msatSort.c
index 3b89d102..a4b34030 100644
--- a/src/sat/msat/msatSort.c
+++ b/src/sat/msat/msatSort.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -171,3 +174,5 @@ void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
index 3716dbf7..7144b213 100644
--- a/src/sat/msat/msatVec.c
+++ b/src/sat/msat/msatVec.c
@@ -20,6 +20,9 @@
 
 #include "msatInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -493,3 +496,5 @@ int Msat_IntVecSortCompare2( int * pp1, int * pp2 )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+