Version abc90215

9 files changed, 90 insertions, 122 deletions

diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index c08e7e3a..ce686cef 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -19,29 +19,18 @@
 #ifndef __FRAIG_H__
 #define __FRAIG_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifndef SINT64
-#define SINT64
-
-#ifdef _WIN32
-typedef signed __int64     sint64;   // compatible with MS VS 6.0
-#else
-typedef long long          sint64;
-#endif
-
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -70,7 +59,7 @@ struct Fraig_ParamsStruct_t_
     int  fVerboseP;     // the verbosiness flag (for proof reporting)
     int  fInternal;     // is set to 1 for internal fraig calls
     int  nConfLimit;    // the limit on the number of conflicts
-    sint64 nInspLimit;  // the limit on the number of inspections
+    ABC_INT64_T nInspLimit;  // the limit on the number of inspections
 };
 
 struct Prove_ParamsStruct_t_
@@ -97,11 +86,11 @@ struct Prove_ParamsStruct_t_
     // last-gasp mitering
     int     nMiteringLimitLast;    // final mitering limit
     // global SAT solver limits
-    sint64  nTotalBacktrackLimit;  // global limit on the number of backtracks
-    sint64  nTotalInspectLimit;    // global limit on the number of clause inspects
+    ABC_INT64_T  nTotalBacktrackLimit;  // global limit on the number of backtracks
+    ABC_INT64_T  nTotalInspectLimit;    // global limit on the number of clause inspects
     // global resources applied
-    sint64  nTotalBacktracksMade;  // the total number of backtracks made
-    sint64  nTotalInspectsMade;    // the total number of inspects made
+    ABC_INT64_T  nTotalBacktracksMade;  // the total number of backtracks made
+    ABC_INT64_T  nTotalInspectsMade;    // the total number of inspects made
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -113,10 +102,10 @@ struct Prove_ParamsStruct_t_
 ////////////////////////////////////////////////////////////////////////
  
 // macros working with complemented attributes of the nodes
-#define Fraig_IsComplement(p)    (((int)((PORT_PTRUINT_T) (p) & 01)))
-#define Fraig_Regular(p)         ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) & ~01)) 
-#define Fraig_Not(p)             ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) ^ 01)) 
-#define Fraig_NotCond(p,c)       ((Fraig_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)))
+#define Fraig_IsComplement(p)    (((int)((ABC_PTRUINT_T) (p) & 01)))
+#define Fraig_Regular(p)         ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) & ~01)) 
+#define Fraig_Not(p)             ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ 01)) 
+#define Fraig_NotCond(p,c)       ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ (c)))
 
 // these are currently not used
 #define Fraig_Ref(p)              
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index e1e8d12c..7d99d146 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -391,7 +391,7 @@ void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats )
     vColumns = Fraig_FeedBackCoveringStart( p );
     // collect the number of 1s in each simulation vector
     nOnesTotal = 0;
-    pHits = ALLOC( int, vColumns->nSize );
+    pHits = ABC_ALLOC( int, vColumns->nSize );
     for ( i = 0; i < vColumns->nSize; i++ )
     {
         pSims = (unsigned *)vColumns->pArray[i];
@@ -412,7 +412,7 @@ void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats )
         Msat_IntVecPush( vPats, iPat );
     }
 
-    // free the set of columns
+    // ABC_FREE the set of columns
     for ( i = 0; i < vColumns->nSize; i++ )
         Fraig_MemFixedEntryRecycle( p->mmSims, (char *)vColumns->pArray[i] );
 
@@ -427,7 +427,7 @@ void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats )
         printf( "\n" );
     }
     Fraig_NodeVecFree( vColumns );
-    free( pHits );
+    ABC_FREE( pHits );
 }
 
 
@@ -736,7 +736,7 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
         // signatures remain without changes
     }
 
-    // replace the manager to free up some memory
+    // replace the manager to ABC_FREE up some memory
     Fraig_MemFixedStop( p->mmSims, 0 );
     p->mmSims = mmSimsNew;
 
@@ -783,7 +783,7 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
 int * Fraig_ManAllocCounterExample( Fraig_Man_t * p )
 {
     int * pModel;
-    pModel = ALLOC( int, p->vInputs->nSize );
+    pModel = ABC_ALLOC( int, p->vInputs->nSize );
     memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
     return pModel;
 }
@@ -896,7 +896,7 @@ printf( "\n" );
         assert( Fraig_ManSimulateBitNode( p, pNode, pModel ) );
         return pModel;
     }
-    FREE( pModel );
+    ABC_FREE( pModel );
     return NULL;
 }
 
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 0e8b1e31..3bea5e42 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -29,9 +29,9 @@
 #include <assert.h>
 #include <time.h>
 
+#include "abc_global.h"
 #include "fraig.h"
 #include "msat.h"
-#include "port_type.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -57,9 +57,9 @@
 #define FRAIG_MAX_PRIMES        1024   // the maximum number of primes used for hashing
 
 // this parameter determines when simulation info is extended
-// it will be extended when the free storage in the dynamic simulation
+// it will be extended when the ABC_FREE storage in the dynamic simulation
 // info is less or equal to this number of words (FRAIG_WORDS_STORE)
-// this is done because if the free storage for dynamic simulation info 
+// this is done because if the ABC_FREE storage for dynamic simulation info 
 // is not sufficient, computation becomes inefficient 
 #define FRAIG_WORDS_STORE           5   
 
@@ -86,35 +86,14 @@
 #define Fraig_NodeSetVarStr(p,i)     Fraig_BitStringSetBit(Fraig_Regular(p)->pSuppStr,i)
 #define Fraig_NodeHasVarStr(p,i)     Fraig_BitStringHasBit(Fraig_Regular(p)->pSuppStr,i)
 
-// copied from "util.h" for standaloneness
-#ifndef ALLOC
-#  define ALLOC(type, num)    \
-    ((type *) malloc(sizeof(type) * (num)))
-#endif 
-
-#ifndef REALLOC
-#  define REALLOC(type, obj, num)    \
-    (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num)))
-#endif 
-
-#ifndef FREE
-#  define FREE(obj)        \
-    ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
-#endif 
-
 // copied from "extra.h" for stand-aloneness
 #define Fraig_PrintTime(a,t)      printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
 
-#define Fraig_HashKey2(a,b,TSIZE) (((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b) * 12582917) % TSIZE)
+#define Fraig_HashKey2(a,b,TSIZE) (((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * 12582917) % TSIZE)
 //#define Fraig_HashKey2(a,b,TSIZE) (( ((unsigned)(a)->Num * 19) ^ ((unsigned)(b)->Num * 1999) ) % TSIZE)
 //#define Fraig_HashKey2(a,b,TSIZE) ( ((unsigned)((a)->Num + (b)->Num) * ((a)->Num + (b)->Num + 1) / 2) % TSIZE)
 // the other two hash functions give bad distribution of hash chain lengths (not clear why)
 
-#ifndef PRT
-#define PRT(a,t)        printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
-#endif 
-
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -152,7 +131,7 @@ struct Fraig_ManStruct_t_
     int                   fTryProve;     // tries to solve the final miter
     int                   fVerbose;      // the verbosiness flag
     int                   fVerboseP;     // the verbosiness flag
-    sint64                nInspLimit;    // the inspection limit
+    ABC_INT64_T                nInspLimit;    // the inspection limit
 
     int                   nTravIds;      // the traversal counter
     int                   nTravIds2;     // the traversal counter
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index cbeef4c6..b71262d8 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -204,7 +204,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
         pParams->nPatsRand = pParams->nPatsDyna = 128;
 
     // start the manager
-    p = ALLOC( Fraig_Man_t, 1 );
+    p = ABC_ALLOC( Fraig_Man_t, 1 );
     memset( p, 0, sizeof(Fraig_Man_t) );
 
     // set the default parameters
@@ -286,25 +286,25 @@ void Fraig_ManFree( Fraig_Man_t * p )
     if ( p->vProj )      Msat_IntVecFree( p->vProj );
     if ( p->vCones )     Fraig_NodeVecFree( p->vCones );
     if ( p->vPatsReal )  Msat_IntVecFree( p->vPatsReal );
-    if ( p->pModel )     free( p->pModel );
+    if ( p->pModel )     ABC_FREE( p->pModel );
 
     Fraig_MemFixedStop( p->mmNodes, 0 );
     Fraig_MemFixedStop( p->mmSims, 0 );
 
     if ( p->pSuppS )
     {
-        FREE( p->pSuppS[0] );
-        FREE( p->pSuppS );
+        ABC_FREE( p->pSuppS[0] );
+        ABC_FREE( p->pSuppS );
     }
     if ( p->pSuppF )
     {
-        FREE( p->pSuppF[0] );
-        FREE( p->pSuppF );
+        ABC_FREE( p->pSuppF[0] );
+        ABC_FREE( p->pSuppF );
     }
 
-    FREE( p->ppOutputNames );
-    FREE( p->ppInputNames );
-    FREE( p );
+    ABC_FREE( p->ppOutputNames );
+    ABC_FREE( p->ppInputNames );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -366,8 +366,8 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
     if ( p->time2 > 0 ) { Fraig_PrintTime( "time2", p->time2 ); }
     if ( p->time3 > 0 ) { Fraig_PrintTime( "time3", p->time3 ); }
     if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); }
-//    PRT( "Selection ", timeSelect );
-//    PRT( "Assignment", timeAssign );
+//    ABC_PRT( "Selection ", timeSelect );
+//    ABC_PRT( "Assignment", timeAssign );
     fflush( stdout );
 }
 
@@ -389,7 +389,7 @@ Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean )
     int i;
     assert( nSize > 0 && nWords > 0 );
     vInfo = Fraig_NodeVecAlloc( nSize );
-    pUnsigned = ALLOC( unsigned, nSize * nWords );
+    pUnsigned = ABC_ALLOC( unsigned, nSize * nWords );
     vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
     if ( fClean )
         memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c
index 500431c6..1cc99790 100644
--- a/src/sat/fraig/fraigMem.c
+++ b/src/sat/fraig/fraigMem.c
@@ -29,7 +29,7 @@ struct Fraig_MemFixed_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
@@ -61,7 +61,7 @@ Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize )
 {
     Fraig_MemFixed_t * p;
 
-    p = ALLOC( Fraig_MemFixed_t, 1 );
+    p = ABC_ALLOC( Fraig_MemFixed_t, 1 );
     memset( p, 0, sizeof(Fraig_MemFixed_t) );
 
     p->nEntrySize    = nEntrySize;
@@ -78,7 +78,7 @@ Fraig_MemFixed_t * Fraig_MemFixedStart( 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;
@@ -109,9 +109,9 @@ void Fraig_MemFixedStop( Fraig_MemFixed_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*************************************************************
@@ -130,16 +130,16 @@ char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_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;
@@ -159,7 +159,7 @@ char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_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;
@@ -180,7 +180,7 @@ void Fraig_MemFixedEntryRecycle( Fraig_MemFixed_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;
 }
@@ -203,7 +203,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_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];
@@ -214,7 +214,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_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;
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 53057fc3..66698600 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -109,7 +109,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
     }
     if ( p->fVerboseP ) 
     {
-//        PRT( "Final miter proof time", clock() - clk );
+//        ABC_PRT( "Final miter proof time", clock() - clk );
     }
 }
 
@@ -128,7 +128,7 @@ int Fraig_ManCheckMiter( Fraig_Man_t * p )
 {
     Fraig_Node_t * pNode;
     int i;
-    FREE( p->pModel );
+    ABC_FREE( p->pModel );
     for ( i = 0; i < p->vOutputs->nSize; i++ )
     {
         // get the output node (it can be complemented!)
@@ -352,7 +352,7 @@ clk = clock();
 p->timeTrav += clock() - clk;
 
 //    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
-//    PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", clock() - clk );
 
 if ( fVerbose )
     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
@@ -391,8 +391,8 @@ p->timeSat += clock() - clk;
 
 if ( fVerbose )
 {
-    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
+//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+//ABC_PRT( "time", clock() - clk );
 }
 
         // add the clause
@@ -409,8 +409,8 @@ PRT( "time", clock() - clk );
 
 if ( fVerbose )
 {
-    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
+//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+//ABC_PRT( "time", clock() - clk );
 }
 
         // record the counter example
@@ -468,8 +468,8 @@ p->timeSat += clock() - clk;
 
 if ( fVerbose )
 {
-    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
+//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+//ABC_PRT( "time", clock() - clk );
 }
 
         // add the clause
@@ -486,8 +486,8 @@ PRT( "time", clock() - clk );
 
 if ( fVerbose )
 {
-    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
+//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+//ABC_PRT( "time", clock() - clk );
 }
 
         // record the counter example
@@ -599,8 +599,8 @@ p->timeSat += clock() - clk;
 
 if ( fVerbose )
 {
-    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
+//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+//ABC_PRT( "time", clock() - clk );
 }
 
         // add the clause
@@ -618,8 +618,8 @@ PRT( "time", clock() - clk );
 
 if ( fVerbose )
 {
-    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
+//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+//ABC_PRT( "time", clock() - clk );
 }
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
@@ -690,8 +690,8 @@ p->timeSat += clock() - clk;
 
 if ( fVerbose )
 {
-    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
+//    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+//ABC_PRT( "time", clock() - clk );
 }
 
         // add the clause
@@ -709,8 +709,8 @@ PRT( "time", clock() - clk );
 
 if ( fVerbose )
 {
-    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
-PRT( "time", clock() - clk );
+//    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+//ABC_PRT( "time", clock() - clk );
 }
         // record the counter example
 //        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
@@ -907,7 +907,7 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t
         {
             // create the fanins of the supergate
             assert( pNode->fClauses == 0 );
-            // detecting a fanout-free cone (experiment only)
+            // detecting a fanout-ABC_FREE cone (experiment only)
 //            Fraig_DetectFanoutFreeCone( pMan, pNode );
 
             if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index b68bbe0e..55d92b4a 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -44,11 +44,11 @@ Fraig_HashTable_t * Fraig_HashTableCreate( int nSize )
 {
     Fraig_HashTable_t * p;
     // allocate the table
-    p = ALLOC( Fraig_HashTable_t, 1 );
+    p = ABC_ALLOC( Fraig_HashTable_t, 1 );
     memset( p, 0, sizeof(Fraig_HashTable_t) );
     // allocate and clean the bins
     p->nBins = Cudd_PrimeFraig(nSize);
-    p->pBins = ALLOC( Fraig_Node_t *, p->nBins );
+    p->pBins = ABC_ALLOC( Fraig_Node_t *, p->nBins );
     memset( p->pBins, 0, sizeof(Fraig_Node_t *) * p->nBins );
     return p;
 }
@@ -66,8 +66,8 @@ Fraig_HashTable_t * Fraig_HashTableCreate( int nSize )
 ***********************************************************************/
 void Fraig_HashTableFree( Fraig_HashTable_t * p )
 {
-    FREE( p->pBins );
-    FREE( p );
+    ABC_FREE( p->pBins );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -264,7 +264,7 @@ clk = clock();
     // get the new table size
     nBinsNew = Cudd_PrimeFraig(2 * p->nBins); 
     // allocate a new array
-    pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew );
+    pBinsNew = ABC_ALLOC( Fraig_Node_t *, nBinsNew );
     memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew );
     // rehash the entries from the old table
     Counter = 0;
@@ -278,9 +278,9 @@ clk = clock();
         }
     assert( Counter == p->nEntries );
 //    printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew );
-//    PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", clock() - clk );
     // replace the table and the parameters
-    free( p->pBins );
+    ABC_FREE( p->pBins );
     p->pBins = pBinsNew;
     p->nBins = nBinsNew;
 }
@@ -307,7 +307,7 @@ clk = clock();
     // get the new table size
     nBinsNew = Cudd_PrimeFraig(2 * p->nBins); 
     // allocate a new array
-    pBinsNew = ALLOC( Fraig_Node_t *, nBinsNew );
+    pBinsNew = ABC_ALLOC( Fraig_Node_t *, nBinsNew );
     memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * nBinsNew );
     // rehash the entries from the old table
     Counter = 0;
@@ -324,9 +324,9 @@ clk = clock();
         }
     assert( Counter == p->nEntries );
 //    printf( "Increasing the functional table size from %6d to %6d. ", p->nBins, nBinsNew );
-//    PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", clock() - clk );
     // replace the table and the parameters
-    free( p->pBins );
+    ABC_FREE( p->pBins );
     p->pBins = pBinsNew;
     p->nBins = nBinsNew;
 }
@@ -605,7 +605,7 @@ int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv )
     unsigned Key;
 
     // allocate a new array of bins
-    pBinsNew = ALLOC( Fraig_Node_t *, pT->nBins );
+    pBinsNew = ABC_ALLOC( Fraig_Node_t *, pT->nBins );
     memset( pBinsNew, 0, sizeof(Fraig_Node_t *) * pT->nBins );
 
     // rehash the entries in the table
@@ -645,7 +645,7 @@ int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv )
         }
     assert( Counter == pT->nEntries );
     // replace the table and the parameters
-    free( pT->pBins );
+    ABC_FREE( pT->pBins );
     pT->pBins = pBinsNew;
     return ReturnValue;
 }
diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c
index 342a7111..ea52d363 100644
--- a/src/sat/fraig/fraigUtil.c
+++ b/src/sat/fraig/fraigUtil.c
@@ -237,7 +237,7 @@ int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNe
   Description [This procedure collects the nodes reachable from
   the POs of the AIG and sets the type of fanout counter (none, one,
   or many) for each node. This procedure is useful to determine
-  fanout-free cones of AND-nodes, which is helpful for rebalancing
+  fanout-ABC_FREE cones of AND-nodes, which is helpful for rebalancing
   the AIG (see procedure Fraig_ManRebalance, or something like that).]
                
   SideEffects []
@@ -881,7 +881,7 @@ clk = clock();
             }
         }
     printf( "Number of candidate pairs = %d.  Proved = %d.\n", Counter, nProved );
-PRT( "Time", clock() - clk );
+//ABC_PRT( "Time", clock() - clk );
     return 0;
 }
 
diff --git a/src/sat/fraig/fraigVec.c b/src/sat/fraig/fraigVec.c
index ba3feecd..b47c6a2f 100644
--- a/src/sat/fraig/fraigVec.c
+++ b/src/sat/fraig/fraigVec.c
@@ -40,12 +40,12 @@
 Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap )
 {
     Fraig_NodeVec_t * p;
-    p = ALLOC( Fraig_NodeVec_t, 1 );
+    p = ABC_ALLOC( Fraig_NodeVec_t, 1 );
     if ( nCap > 0 && nCap < 8 )
         nCap = 8;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
     return p;
 }
 
@@ -62,8 +62,8 @@ Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap )
 ***********************************************************************/
 void Fraig_NodeVecFree( Fraig_NodeVec_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -80,10 +80,10 @@ void Fraig_NodeVecFree( Fraig_NodeVec_t * p )
 Fraig_NodeVec_t * Fraig_NodeVecDup( Fraig_NodeVec_t * pVec )
 {
     Fraig_NodeVec_t * p;
-    p = ALLOC( Fraig_NodeVec_t, 1 );
+    p = ABC_ALLOC( Fraig_NodeVec_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
     memcpy( p->pArray, pVec->pArray, sizeof(Fraig_Node_t *) * pVec->nSize );
     return p;
 }
@@ -135,7 +135,7 @@ void Fraig_NodeVecGrow( Fraig_NodeVec_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( Fraig_Node_t *, p->pArray, nCapMin ); 
+    p->pArray = ABC_REALLOC( Fraig_Node_t *, p->pArray, nCapMin ); 
     p->nCap   = nCapMin;
 }