Version abc90215

12 files changed, 108 insertions, 126 deletions

diff --git a/src/sat/msat/module.make b/src/sat/msat/module.make
index 0dadfbe1..33133963 100644
--- a/src/sat/msat/module.make
+++ b/src/sat/msat/module.make
@@ -2,7 +2,7 @@ SRC +=  src/sat/msat/msatActivity.c \
     src/sat/msat/msatClause.c \
     src/sat/msat/msatClauseVec.c \
     src/sat/msat/msatMem.c \
-    src/sat/msat/msatOrderJ.c \
+    src/sat/msat/msatOrderH.c \
     src/sat/msat/msatQueue.c \
     src/sat/msat/msatRead.c \
     src/sat/msat/msatSolverApi.c \
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 53353ba6..2b28700c 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -21,10 +21,6 @@
 #ifndef __MSAT_H__
 #define __MSAT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index 2ba8cd32..ca698866 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -152,7 +152,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
 //    nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned);
     nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned);
 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    pC = (Msat_Clause_t *)ALLOC( char, nBytes );
+    pC = (Msat_Clause_t *)ABC_ALLOC( char, nBytes );
 #else
     pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes );
 #endif
@@ -231,7 +231,7 @@ void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched
     }
 
 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    free( pC );
+    ABC_FREE( pC );
 #else
     Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc );
 #endif
diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c
index 04691cf2..f29de389 100644
--- a/src/sat/msat/msatClauseVec.c
+++ b/src/sat/msat/msatClauseVec.c
@@ -42,12 +42,12 @@
 Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap )
 {
     Msat_ClauseVec_t * p;
-    p = ALLOC( Msat_ClauseVec_t, 1 );
+    p = ABC_ALLOC( Msat_ClauseVec_t, 1 );
     if ( nCap > 0 && nCap < 16 )
         nCap = 16;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( Msat_Clause_t *, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( Msat_Clause_t *, p->nCap ) : NULL;
     return p;
 }
 
@@ -64,8 +64,8 @@ Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap )
 ***********************************************************************/
 void Msat_ClauseVecFree( Msat_ClauseVec_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -115,7 +115,7 @@ void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); 
+    p->pArray = ABC_REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); 
     p->nCap   = nCapMin;
 }
 
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 2ff0e695..b6759a0f 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -31,6 +31,7 @@
 #include <assert.h>
 #include <time.h>
 #include <math.h>
+#include "abc_global.h"
 #include "msat.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -41,25 +42,6 @@
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef _MSC_VER
-typedef __int64     int64;
-#else
-typedef long long   int64;
-#endif
-
-// outputs the runtime in seconds
-#define PRT(a,t) \
-    printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
-
-// memory management macros
-#define ALLOC(type, num)    \
-    ((type *) malloc(sizeof(type) * (num)))
-#define REALLOC(type, obj, num)    \
-    ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num))))
-#define FREE(obj)        \
-    ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
-
 // By default, custom memory management is used
 // which guarantees constant time allocation/deallocation 
 // for SAT clauses and other frequently modified objects.
@@ -92,12 +74,12 @@ typedef int                       Msat_Var_t;
 typedef struct Msat_SolverStats_t_ Msat_SolverStats_t;
 struct Msat_SolverStats_t_
 {
-    int64   nStarts;        // the number of restarts
-    int64   nDecisions;     // the number of decisions
-    int64   nPropagations;  // the number of implications
-    int64   nInspects;      // the number of times clauses are vising while watching them
-    int64   nConflicts;     // the number of conflicts
-    int64   nSuccesses;     // the number of sat assignments found
+    ABC_INT64_T   nStarts;        // the number of restarts
+    ABC_INT64_T   nDecisions;     // the number of decisions
+    ABC_INT64_T   nPropagations;  // the number of implications
+    ABC_INT64_T   nInspects;      // the number of times clauses are vising while watching them
+    ABC_INT64_T   nConflicts;     // the number of conflicts
+    ABC_INT64_T   nSuccesses;     // the number of sat assignments found
 };
 
 typedef struct Msat_SearchParams_t_ Msat_SearchParams_t;
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
index 30bf4a96..439661f4 100644
--- a/src/sat/msat/msatMem.c
+++ b/src/sat/msat/msatMem.c
@@ -31,7 +31,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 free entries
+    char *        pEntriesFree;  // the linked list of ABC_FREE entries
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -48,8 +48,8 @@ struct Msat_MmFlex_t_
 {
     // information about individual entries
     int           nEntriesUsed;  // the number of entries allocated
-    char *        pCurrent;      // the current pointer to free memory
-    char *        pEnd;          // the first entry outside the free memory
+    char *        pCurrent;      // the current pointer to ABC_FREE memory
+    char *        pEnd;          // the first entry outside the ABC_FREE memory
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -91,7 +91,7 @@ Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize )
 {
     Msat_MmFixed_t * p;
 
-    p = ALLOC( Msat_MmFixed_t, 1 );
+    p = ABC_ALLOC( Msat_MmFixed_t, 1 );
     memset( p, 0, sizeof(Msat_MmFixed_t) );
 
     p->nEntrySize    = nEntrySize;
@@ -108,7 +108,7 @@ Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize )
 
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
 
     p->nMemoryUsed   = 0;
     p->nMemoryAlloc  = 0;
@@ -139,9 +139,9 @@ void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose )
             p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
     }
     for ( i = 0; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    free( p->pChunks );
-    free( p );
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -160,16 +160,16 @@ char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p )
     char * pTemp;
     int i;
 
-    // check if there are still free entries
+    // check if there are still ABC_FREE entries
     if ( p->nEntriesUsed == p->nEntriesAlloc )
     { // need to allocate more entries
         assert( p->pEntriesFree == NULL );
         if ( p->nChunks == p->nChunksAlloc )
         {
             p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
         }
-        p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+        p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize );
         p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
         // transform these entries into a linked list
         pTemp = p->pEntriesFree;
@@ -189,7 +189,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 free entry list
+    // return the first entry in the ABC_FREE entry list
     pTemp = p->pEntriesFree;
     p->pEntriesFree = *((char **)pTemp);
     return pTemp;
@@ -210,7 +210,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 free entries
+    // add the entry to the linked list of ABC_FREE entries
     *((char **)pEntry) = p->pEntriesFree;
     p->pEntriesFree = pEntry;
 }
@@ -233,7 +233,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
 
     // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
+        ABC_FREE( p->pChunks[i] );
     p->nChunks = 1;
     // transform these entries into a linked list
     pTemp = p->pChunks[0];
@@ -244,7 +244,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
     }
     // set the last link
     *((char **)pTemp) = NULL;
-    // set the free entry list
+    // set the ABC_FREE entry list
     p->pEntriesFree  = p->pChunks[0];
     // set the correct statistics
     p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
@@ -286,7 +286,7 @@ Msat_MmFlex_t * Msat_MmFlexStart()
 {
     Msat_MmFlex_t * p;
 
-    p = ALLOC( Msat_MmFlex_t, 1 );
+    p = ABC_ALLOC( Msat_MmFlex_t, 1 );
     memset( p, 0, sizeof(Msat_MmFlex_t) );
 
     p->nEntriesUsed  = 0;
@@ -296,7 +296,7 @@ Msat_MmFlex_t * Msat_MmFlexStart()
     p->nChunkSize    = (1 << 12);
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
 
     p->nMemoryUsed   = 0;
     p->nMemoryAlloc  = 0;
@@ -327,9 +327,9 @@ void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose )
             p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
     }
     for ( i = 0; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    free( p->pChunks );
-    free( p );
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -346,13 +346,13 @@ 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 free entries
+    // check if there are still ABC_FREE entries
     if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
     { // need to allocate more entries
         if ( p->nChunks == p->nChunksAlloc )
         {
             p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
         }
         if ( nBytes > p->nChunkSize )
         {
@@ -360,7 +360,7 @@ char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes )
             // (ideally, this should never happen)
             p->nChunkSize = 2 * nBytes;
         }
-        p->pCurrent = ALLOC( char, p->nChunkSize );
+        p->pCurrent = ABC_ALLOC( char, p->nChunkSize );
         p->pEnd     = p->pCurrent + p->nChunkSize;
         p->nMemoryAlloc += p->nChunkSize;
         // add the chunk to the chunk storage
@@ -410,7 +410,7 @@ int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p )
   are employed internally. Calling this procedure with nSteps equal
   to 10 results in 10 hierarchically arranged internal memory managers, 
   which can allocate up to 4096 (1Kb) entries. Requests for larger 
-  entries are handed over to malloc() and then free()ed.]
+  entries are handed over to malloc() and then ABC_FREE()ed.]
                
   SideEffects []
 
@@ -421,15 +421,15 @@ Msat_MmStep_t * Msat_MmStepStart( int nSteps )
 {
     Msat_MmStep_t * p;
     int i, k;
-    p = ALLOC( Msat_MmStep_t, 1 );
+    p = ABC_ALLOC( Msat_MmStep_t, 1 );
     p->nMems = nSteps;
     // start the fixed memory managers
-    p->pMems = ALLOC( Msat_MmFixed_t *, p->nMems );
+    p->pMems = ABC_ALLOC( Msat_MmFixed_t *, p->nMems );
     for ( i = 0; i < p->nMems; i++ )
         p->pMems[i] = Msat_MmFixedStart( (8<<i) );
     // set up the mapping of the required memory size into the corresponding manager
     p->nMapSize = (4<<p->nMems);
-    p->pMap = ALLOC( Msat_MmFixed_t *, p->nMapSize+1 );
+    p->pMap = ABC_ALLOC( Msat_MmFixed_t *, p->nMapSize+1 );
     p->pMap[0] = NULL;
     for ( k = 1; k <= 4; k++ )
         p->pMap[k] = p->pMems[0];
@@ -457,9 +457,9 @@ void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose )
     int i;
     for ( i = 0; i < p->nMems; i++ )
         Msat_MmFixedStop( p->pMems[i], fVerbose );
-    free( p->pMems );
-    free( p->pMap );
-    free( p );
+    ABC_FREE( p->pMems );
+    ABC_FREE( p->pMap );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -480,7 +480,7 @@ char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes )
     if ( nBytes > p->nMapSize )
     {
 //        printf( "Allocating %d bytes.\n", nBytes );
-        return ALLOC( char, nBytes );
+        return ABC_ALLOC( char, nBytes );
     }
     return Msat_MmFixedEntryFetch( p->pMap[nBytes] );
 }
@@ -503,7 +503,7 @@ void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes )
         return;
     if ( nBytes > p->nMapSize )
     {
-        free( pEntry );
+        ABC_FREE( pEntry );
         return;
     }
     Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index 956e7fc6..7d8484d5 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -75,7 +75,7 @@ extern int timeSelect;
 Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat )
 {
     Msat_Order_t * p;
-    p = ALLOC( Msat_Order_t, 1 );
+    p = ABC_ALLOC( Msat_Order_t, 1 );
     memset( p, 0, sizeof(Msat_Order_t) );
     p->pSat   = pSat;
     p->vIndex = Msat_IntVecAlloc( 0 );
@@ -161,7 +161,7 @@ void Msat_OrderFree( Msat_Order_t * p )
 {
     Msat_IntVecFree( p->vHeap );
     Msat_IntVecFree( p->vIndex );
-    free( p );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c
index 5938e042..0bcaf6b2 100644
--- a/src/sat/msat/msatQueue.c
+++ b/src/sat/msat/msatQueue.c
@@ -50,10 +50,10 @@ struct Msat_Queue_t_
 Msat_Queue_t * Msat_QueueAlloc( int nVars )
 {
     Msat_Queue_t * p;
-    p = ALLOC( Msat_Queue_t, 1 );
+    p = ABC_ALLOC( Msat_Queue_t, 1 );
     memset( p, 0, sizeof(Msat_Queue_t) );
     p->nVars  = nVars;
-    p->pVars  = ALLOC( int, nVars );
+    p->pVars  = ABC_ALLOC( int, nVars );
     return p;
 }
 
@@ -70,8 +70,8 @@ Msat_Queue_t * Msat_QueueAlloc( int nVars )
 ***********************************************************************/
 void Msat_QueueFree( Msat_Queue_t * p )
 {
-    free( p->pVars );
-    free( p );
+    ABC_FREE( p->pVars );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c
index 20453fed..ba33278c 100644
--- a/src/sat/msat/msatRead.c
+++ b/src/sat/msat/msatRead.c
@@ -51,7 +51,7 @@ char * Msat_FileRead( FILE * pFile )
     // move the file current reading position to the beginning
     rewind( pFile ); 
     // load the contents of the file into memory
-    pBuffer = ALLOC( char, nFileSize + 3 );
+    pBuffer = ABC_ALLOC( char, nFileSize + 3 );
     fread( pBuffer, nFileSize, 1, pFile );
     // terminate the string with '\0'
     pBuffer[ nFileSize + 0] = '\n';
@@ -257,7 +257,7 @@ bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose )
     bool Value;
     pText = Msat_FileRead( pFile );
     Value = Msat_ReadDimacs( pText, p, fVerbose );
-    free( pText );
+    ABC_FREE( pText );
     return Value;
 }
 
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index ee3507a6..dece390c 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -159,7 +159,7 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
     assert(sizeof(float)     == sizeof(unsigned));
 
-    p = ALLOC( Msat_Solver_t, 1 );
+    p = ABC_ALLOC( Msat_Solver_t, 1 );
     memset( p, 0, sizeof(Msat_Solver_t) );
 
     p->nVarsAlloc = nVarsAlloc;
@@ -174,31 +174,31 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     p->dVarInc   = dVarInc;
     p->dVarDecay = dVarDecay;
 
-    p->pdActivity = ALLOC( double, p->nVarsAlloc );
-    p->pFactors   = ALLOC( float, p->nVarsAlloc );
+    p->pdActivity = ABC_ALLOC( double, p->nVarsAlloc );
+    p->pFactors   = ABC_ALLOC( float, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
     {
         p->pdActivity[i] = 0.0;
         p->pFactors[i]   = 1.0;
     }
 
-    p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
-    p->pModel    = ALLOC( int, p->nVarsAlloc ); 
+    p->pAssigns  = ABC_ALLOC( int, p->nVarsAlloc ); 
+    p->pModel    = ABC_ALLOC( int, p->nVarsAlloc ); 
     for ( i = 0; i < p->nVarsAlloc; i++ )
         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
 //    p->pOrder    = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
     p->pOrder    = Msat_OrderAlloc( p );
 
-    p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
+    p->pvWatched = ABC_ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
         p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
     p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
 
     p->vTrail    = Msat_IntVecAlloc( p->nVarsAlloc );
     p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
-    p->pReasons  = ALLOC( Msat_Clause_t *, p->nVarsAlloc );
+    p->pReasons  = ABC_ALLOC( Msat_Clause_t *, p->nVarsAlloc );
     memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
-    p->pLevel = ALLOC( int, p->nVarsAlloc );
+    p->pLevel = ABC_ALLOC( int, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
         p->pLevel[i] = -1;
     p->dRandSeed = 91648253;
@@ -215,7 +215,7 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
 
 
-    p->pSeen     = ALLOC( int, p->nVarsAlloc );
+    p->pSeen     = ABC_ALLOC( int, p->nVarsAlloc );
     memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
     p->nSeenId   = 1;
     p->vReason   = Msat_IntVecAlloc( p->nVarsAlloc );
@@ -243,38 +243,38 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
     nVarsAllocOld = p->nVarsAlloc;
     p->nVarsAlloc = nVarsAlloc;
 
-    p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
-    p->pFactors   = REALLOC( float, p->pFactors, p->nVarsAlloc );
+    p->pdActivity = ABC_REALLOC( double, p->pdActivity, p->nVarsAlloc );
+    p->pFactors   = ABC_REALLOC( float, p->pFactors, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
     {
         p->pdActivity[i] = 0.0;
         p->pFactors[i]   = 1.0;
     }
 
-    p->pAssigns  = REALLOC( int, p->pAssigns, p->nVarsAlloc );
-    p->pModel    = REALLOC( int, p->pModel, p->nVarsAlloc );
+    p->pAssigns  = ABC_REALLOC( int, p->pAssigns, p->nVarsAlloc );
+    p->pModel    = ABC_REALLOC( int, p->pModel, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
 
 //    Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
     Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
 
-    p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
+    p->pvWatched = ABC_REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
     for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
         p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
 
     Msat_QueueFree( p->pQueue );
     p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
 
-    p->pReasons  = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
-    p->pLevel    = REALLOC( int, p->pLevel, p->nVarsAlloc );
+    p->pReasons  = ABC_REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
+    p->pLevel    = ABC_REALLOC( int, p->pLevel, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
     {
         p->pReasons[i] = NULL;
         p->pLevel[i] = -1;
     }
 
-    p->pSeen     = REALLOC( int, p->pSeen, p->nVarsAlloc );
+    p->pSeen     = ABC_REALLOC( int, p->pSeen, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
         p->pSeen[i] = 0;
 
@@ -304,7 +304,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
 void Msat_SolverClean( Msat_Solver_t * p, int nVars )
 {
     int i;
-    // free the clauses
+    // ABC_FREE the clauses
     int nClauses;
     Msat_Clause_t ** pClauses;
 
@@ -326,7 +326,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars )
 //    Msat_ClauseVecFree( p->vLearned );
     Msat_ClauseVecClear( p->vLearned );
 
-//    FREE( p->pdActivity );
+//    ABC_FREE( p->pdActivity );
     for ( i = 0; i < p->nVars; i++ )
         p->pdActivity[i] = 0;
 
@@ -337,20 +337,20 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars )
     for ( i = 0; i < 2 * p->nVars; i++ )
 //        Msat_ClauseVecFree( p->pvWatched[i] );
         Msat_ClauseVecClear( p->pvWatched[i] );
-//    FREE( p->pvWatched );
+//    ABC_FREE( p->pvWatched );
 //    Msat_QueueFree( p->pQueue );
     Msat_QueueClear( p->pQueue );
 
-//    FREE( p->pAssigns );
+//    ABC_FREE( p->pAssigns );
     for ( i = 0; i < p->nVars; i++ )
         p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
 //    Msat_IntVecFree( p->vTrail );
     Msat_IntVecClear( p->vTrail );
 //    Msat_IntVecFree( p->vTrailLim );
     Msat_IntVecClear( p->vTrailLim );
-//    FREE( p->pReasons );
+//    ABC_FREE( p->pReasons );
     memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
-//    FREE( p->pLevel );
+//    ABC_FREE( p->pLevel );
     for ( i = 0; i < p->nVars; i++ )
         p->pLevel[i] = -1;
 //    Msat_IntVecFree( p->pModel );
@@ -358,7 +358,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars )
     p->dRandSeed = 91648253;
     p->dProgress = 0.0;
 
-//    FREE( p->pSeen );
+//    ABC_FREE( p->pSeen );
     memset( p->pSeen, 0, sizeof(int) * p->nVars );
     p->nSeenId = 1;
 //    Msat_IntVecFree( p->vReason );
@@ -366,7 +366,7 @@ void Msat_SolverClean( Msat_Solver_t * p, int nVars )
 //    Msat_IntVecFree( p->vTemp );
     Msat_IntVecClear( p->vTemp );
 //    printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
-//    FREE( p );
+//    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -384,7 +384,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
 {
     int i;
 
-    // free the clauses
+    // ABC_FREE the clauses
     int nClauses;
     Msat_Clause_t ** pClauses;
 //printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), 
@@ -402,21 +402,21 @@ void Msat_SolverFree( Msat_Solver_t * p )
         Msat_ClauseFree( p, pClauses[i], 0 );
     Msat_ClauseVecFree( p->vLearned );
 
-    FREE( p->pdActivity );
-    FREE( p->pFactors );
+    ABC_FREE( p->pdActivity );
+    ABC_FREE( p->pFactors );
     Msat_OrderFree( p->pOrder );
 
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
         Msat_ClauseVecFree( p->pvWatched[i] );
-    FREE( p->pvWatched );
+    ABC_FREE( p->pvWatched );
     Msat_QueueFree( p->pQueue );
 
-    FREE( p->pAssigns );
-    FREE( p->pModel );
+    ABC_FREE( p->pAssigns );
+    ABC_FREE( p->pModel );
     Msat_IntVecFree( p->vTrail );
     Msat_IntVecFree( p->vTrailLim );
-    FREE( p->pReasons );
-    FREE( p->pLevel );
+    ABC_FREE( p->pReasons );
+    ABC_FREE( p->pLevel );
 
     Msat_MmStepStop( p->pMem, 0 );
 
@@ -428,10 +428,10 @@ void Msat_SolverFree( Msat_Solver_t * p )
     Msat_IntVecFree( p->vConeVars );
     Msat_IntVecFree( p->vVarsUsed );
 
-    FREE( p->pSeen );
+    ABC_FREE( p->pSeen );
     Msat_IntVecFree( p->vReason );
     Msat_IntVecFree( p->vTemp );
-    FREE( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index e86ab511..0462f11b 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -139,7 +139,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
     Msat_Type_t Status;
     int timeStart = clock();
 
-//    p->pFreq = ALLOC( int, p->nVarsAlloc );
+//    p->pFreq = ABC_ALLOC( int, p->nVarsAlloc );
 //    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
  
     if ( vAssumps )
@@ -184,7 +184,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
     Msat_SolverCancelUntil( p, 0 );
     p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
 /*
-    PRT( "True solver runtime", clock() - timeStart );
+    ABC_PRT( "True solver runtime", clock() - timeStart );
     // print the statistics
     {
         int i, Counter = 0;
@@ -197,7 +197,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
         if ( Counter )
             printf( "\n" );
         printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
-        PRT( "Time", clock() - timeStart );
+        ABC_PRT( "Time", clock() - timeStart );
     }
 */
     return Status;
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
index 36ad55ba..3716dbf7 100644
--- a/src/sat/msat/msatVec.c
+++ b/src/sat/msat/msatVec.c
@@ -45,12 +45,12 @@ static int Msat_IntVecSortCompare2( int * pp1, int * pp2 );
 Msat_IntVec_t * Msat_IntVecAlloc( int nCap )
 {
     Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
+    p = ABC_ALLOC( Msat_IntVec_t, 1 );
     if ( nCap > 0 && nCap < 16 )
         nCap = 16;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL;
     return p;
 }
 
@@ -68,7 +68,7 @@ Msat_IntVec_t * Msat_IntVecAlloc( int nCap )
 Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize )
 {
     Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
+    p = ABC_ALLOC( Msat_IntVec_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
     p->pArray = pArray;
@@ -89,10 +89,10 @@ Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize )
 Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize )
 {
     Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
+    p = ABC_ALLOC( Msat_IntVec_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
-    p->pArray = ALLOC( int, nSize );
+    p->pArray = ABC_ALLOC( int, nSize );
     memcpy( p->pArray, pArray, sizeof(int) * nSize );
     return p;
 }
@@ -111,10 +111,10 @@ Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize )
 Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec )
 {
     Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
+    p = ABC_ALLOC( Msat_IntVec_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL;
     memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
     return p;
 }
@@ -133,7 +133,7 @@ Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec )
 Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec )
 {
     Msat_IntVec_t * p;
-    p = ALLOC( Msat_IntVec_t, 1 );
+    p = ABC_ALLOC( Msat_IntVec_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
     p->pArray = pVec->pArray;
@@ -156,8 +156,8 @@ Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec )
 ***********************************************************************/
 void Msat_IntVecFree( Msat_IntVec_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -297,7 +297,7 @@ void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( int, p->pArray, nCapMin ); 
+    p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); 
     p->nCap   = nCapMin;
 }