Version abc90215

13 files changed, 107 insertions, 107 deletions

diff --git a/src/aig/ivy/attr.h b/src/aig/ivy/attr.h
index 16cf0b84..ad342ce9 100644
--- a/src/aig/ivy/attr.h
+++ b/src/aig/ivy/attr.h
@@ -21,10 +21,6 @@
 #ifndef __ATTR_H__
 #define __ATTR_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,6 +31,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index 9832e061..2c915e5b 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -21,10 +21,6 @@
 #ifndef __IVY_H__
 #define __IVY_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -37,6 +33,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -121,7 +121,7 @@ struct Ivy_Man_t_
     // memory management
     Vec_Ptr_t *      vChunks;        // allocated memory pieces
     Vec_Ptr_t *      vPages;         // memory pages used by nodes
-    Ivy_Obj_t *      pListFree;      // the list of free nodes 
+    Ivy_Obj_t *      pListFree;      // the list of ABC_FREE nodes 
     // timing statistics
     int              time1;
     int              time2;
@@ -186,10 +186,10 @@ static inline int          Ivy_InfoHasBit( unsigned * p, int i )  { return (p[(i
 static inline void         Ivy_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                   }
 static inline void         Ivy_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                   }
 
-static inline Ivy_Obj_t *  Ivy_Regular( Ivy_Obj_t * p )           { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) & ~01); }
-static inline Ivy_Obj_t *  Ivy_Not( Ivy_Obj_t * p )               { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) ^  01); }
-static inline Ivy_Obj_t *  Ivy_NotCond( Ivy_Obj_t * p, int c )    { return (Ivy_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c)); }
-static inline int          Ivy_IsComplement( Ivy_Obj_t * p )      { return (int)((PORT_PTRUINT_T)(p) & 01);          }
+static inline Ivy_Obj_t *  Ivy_Regular( Ivy_Obj_t * p )           { return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
+static inline Ivy_Obj_t *  Ivy_Not( Ivy_Obj_t * p )               { return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) ^  01); }
+static inline Ivy_Obj_t *  Ivy_NotCond( Ivy_Obj_t * p, int c )    { return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
+static inline int          Ivy_IsComplement( Ivy_Obj_t * p )      { return (int)((ABC_PTRUINT_T)(p) & 01);          }
 
 static inline Ivy_Obj_t *  Ivy_ManConst0( Ivy_Man_t * p )         { return Ivy_Not(p->pConst1);                     }
 static inline Ivy_Obj_t *  Ivy_ManConst1( Ivy_Man_t * p )         { return p->pConst1;                              }
diff --git a/src/aig/ivy/ivyCut.c b/src/aig/ivy/ivyCut.c
index b0dd6db7..e3651645 100644
--- a/src/aig/ivy/ivyCut.c
+++ b/src/aig/ivy/ivyCut.c
@@ -980,7 +980,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p )
     }
     printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
         nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ivy/ivyCutTrav.c b/src/aig/ivy/ivyCutTrav.c
index ea57c9f5..a52bbcf9 100644
--- a/src/aig/ivy/ivyCutTrav.c
+++ b/src/aig/ivy/ivyCutTrav.c
@@ -457,7 +457,7 @@ void Ivy_ManTestCutsTravAll( Ivy_Man_t * p )
     }
     printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
         nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 
     Vec_PtrFree( vNodes );
     Vec_PtrFree( vFront );
diff --git a/src/aig/ivy/ivyFastMap.c b/src/aig/ivy/ivyFastMap.c
index 6ee177a4..0c0102c0 100644
--- a/src/aig/ivy/ivyFastMap.c
+++ b/src/aig/ivy/ivyFastMap.c
@@ -105,12 +105,12 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbo
     Ivy_Obj_t * pObj;
     int i, Delay, Area, clk, clkTotal = clock();
     // start the memory for supports
-    pMan = ALLOC( Ivy_SuppMan_t, 1 );
+    pMan = ABC_ALLOC( Ivy_SuppMan_t, 1 );
     memset( pMan, 0, sizeof(Ivy_SuppMan_t) );
     pMan->nLimit = nLimit;
     pMan->nObjs  = Ivy_ManObjIdMax(pAig) + 1;
     pMan->nSize  = sizeof(Ivy_Supp_t) + nLimit * sizeof(int);
-    pMan->pMem   = (char *)malloc( pMan->nObjs * pMan->nSize );
+    pMan->pMem   = (char *)ABC_ALLOC( char, pMan->nObjs * pMan->nSize );
     memset( pMan->pMem, 0, pMan->nObjs * pMan->nSize );
     pMan->vLuts  = Vec_VecAlloc( 100 );
     pAig->pData  = pMan;
@@ -191,8 +191,8 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig )
 {
     Ivy_SuppMan_t * p = pAig->pData;
     Vec_VecFree( p->vLuts );
-    free( p->pMem );
-    free( p );
+    ABC_FREE( p->pMem );
+    ABC_FREE( p );
     pAig->pData = NULL;
 }
 
@@ -210,7 +210,7 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig )
 void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr )
 {
     printf( "%s : Delay = %3d. Area = %6d. ", pStr, Delay, Area );
-    PRT( "Time", Time );
+    ABC_PRT( "Time", Time );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 7c5a139c..c0ec3021 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -50,9 +50,9 @@ struct Ivy_FraigMan_t_
 {
     // general info 
     Ivy_FraigParams_t * pParams;        // various parameters
-    // temporary backtrack limits because "sint64" cannot be defined in Ivy_FraigParams_t ...
-    sint64              nBTLimitGlobal; // global limit on the number of backtracks
-    sint64              nInsLimitGlobal;// global limit on the number of clause inspects
+    // temporary backtrack limits because "ABC_INT64_T" cannot be defined in Ivy_FraigParams_t ...
+    ABC_INT64_T              nBTLimitGlobal; // global limit on the number of backtracks
+    ABC_INT64_T              nInsLimitGlobal;// global limit on the number of clause inspects
     // AIG manager
     Ivy_Man_t *         pManAig;        // the starting AIG manager
     Ivy_Man_t *         pManFraig;      // the final AIG manager
@@ -126,11 +126,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
 };
 
 static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj )                            { return (Ivy_FraigSim_t *)pObj->pFanout;  }
@@ -141,7 +141,7 @@ static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj )
 static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj )                       { return pObj->pPrevFan0;  }
 static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj )                       { return pObj->pPrevFan1;  }
 static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj )                               { return pObj->pEquiv;     }
-static inline int         Ivy_ObjSatNum( Ivy_Obj_t * pObj )                              { return (int)(PORT_PTRUINT_T)pObj->pNextFan0;         }
+static inline int         Ivy_ObjSatNum( Ivy_Obj_t * pObj )                              { return (int)(ABC_PTRUINT_T)pObj->pNextFan0;         }
 static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj )                            { return (Vec_Ptr_t *)pObj->pNextFan1; }
 
 static inline void        Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim )       { pObj->pFanout = (Ivy_Obj_t *)pSim; }
@@ -152,7 +152,7 @@ static inline void        Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t *
 static inline void        Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
 static inline void        Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; }
 static inline void        Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode )         { pObj->pEquiv    = pNode; }
-static inline void        Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num )                  { pObj->pNextFan0 = (Ivy_Obj_t *)(PORT_PTRUINT_T)Num;     }
+static inline void        Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num )                  { pObj->pNextFan0 = (Ivy_Obj_t *)(ABC_PTRUINT_T)Num;     }
 static inline void        Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins )    { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; }
 
 static inline unsigned    Ivy_ObjRandomSim()                       { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
@@ -181,7 +181,7 @@ static inline unsigned    Ivy_ObjRandomSim()                       { return (ran
 
 static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
 static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
-static Ivy_Man_t *   Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects );
+static Ivy_Man_t *   Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, ABC_INT64_T nBTLimitGlobal, ABC_INT64_T nInsLimitGlobal, ABC_INT64_T * pnSatConfs, ABC_INT64_T * pnSatInspects );
 static void          Ivy_FraigPrint( Ivy_FraigMan_t * p );
 static void          Ivy_FraigStop( Ivy_FraigMan_t * p );
 static void          Ivy_FraigSimulate( Ivy_FraigMan_t * p );
@@ -199,8 +199,8 @@ static int *         Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
 
 static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
 
-static sint64 s_nBTLimitGlobal = 0;
-static sint64 s_nInsLimitGlobal = 0;
+static ABC_INT64_T s_nBTLimitGlobal = 0;
+static ABC_INT64_T s_nInsLimitGlobal = 0;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -253,7 +253,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
     Ivy_FraigParams_t Params, * pIvyParams = &Params; 
     Ivy_Man_t * pManAig, * pManTemp;
     int RetValue, nIter, clk;//, Counter;
-    sint64 nSatConfs = 0, nSatInspects = 0;
+    ABC_INT64_T nSatConfs = 0, nSatInspects = 0;
 
     // start the network and parameters
     pManAig = *ppManAig;
@@ -334,7 +334,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
         {
             clk = clock();
             pIvyParams->nBTLimitNode  = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
-            pIvyParams->nBTLimitMiter = (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
+            pIvyParams->nBTLimitMiter = 1 + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
             pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects );  Ivy_ManStop( pManTemp );
             RetValue = Ivy_FraigMiterStatus( pManAig );
             Ivy_FraigMiterPrint( pManAig, "Fraiging   ", clk, pParams->fVerbose );
@@ -387,7 +387,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
     // assign the model if it was proved by rewriting (const 1 miter)
     if ( RetValue == 0 && pManAig->pData == NULL )
     {
-        pManAig->pData = ALLOC( int, Ivy_ManPiNum(pManAig) );
+        pManAig->pData = ABC_ALLOC( int, Ivy_ManPiNum(pManAig) );
         memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
     }
     *ppManAig = pManAig;
@@ -405,7 +405,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects )
+Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, ABC_INT64_T nBTLimitGlobal, ABC_INT64_T nInsLimitGlobal, ABC_INT64_T * pnSatConfs, ABC_INT64_T * pnSatInspects )
 { 
     Ivy_FraigMan_t * p;
     Ivy_Man_t * pManAigNew;
@@ -504,7 +504,7 @@ clk = clock();
 p->timeTotal = clock() - clk;
 
 //printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
-//PRT( "Time", p->timeTotal );
+//ABC_PRT( "Time", p->timeTotal );
     Ivy_FraigStop( p );
     return pManAigNew;
 }
@@ -524,7 +524,7 @@ Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t *
 {
     Ivy_FraigMan_t * p;
     // allocat the fraiging manager
-    p = ALLOC( Ivy_FraigMan_t, 1 );
+    p = ABC_ALLOC( Ivy_FraigMan_t, 1 );
     memset( p, 0, sizeof(Ivy_FraigMan_t) );
     p->pParams   = pParams;
     p->pManAig   = pManAig;
@@ -555,16 +555,16 @@ Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParam
 //        pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
         assert( !pObj->pEquiv && !pObj->pFanout );
     // allocat the fraiging manager
-    p = ALLOC( Ivy_FraigMan_t, 1 );
+    p = ABC_ALLOC( Ivy_FraigMan_t, 1 );
     memset( p, 0, sizeof(Ivy_FraigMan_t) );
     p->pParams   = pParams;
     p->pManAig   = pManAig;
     p->pManFraig = Ivy_ManStartFrom( pManAig );
     // allocate simulation info
     p->nSimWords    = pParams->nSimWords;
-//    p->pSimWords    = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords ); 
+//    p->pSimWords    = ABC_ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords ); 
     EntrySize    = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords;
-    p->pSimWords = (char *)malloc( Ivy_ManObjNum(pManAig) * EntrySize ); 
+    p->pSimWords = (char *)ABC_ALLOC( char, Ivy_ManObjNum(pManAig) * EntrySize ); 
     memset( p->pSimWords, 0, EntrySize );
     k = 0;
     Ivy_ManForEachObj( pManAig, pObj, i )
@@ -592,8 +592,8 @@ Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParam
     assert( k == Ivy_ManObjNum(pManAig) );
     // allocate storage for sim pattern
     p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
-    p->pPatWords = ALLOC( unsigned, p->nPatWords ); 
-    p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
+    p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords ); 
+    p->pPatScores = ABC_ALLOC( int, 32 * p->nSimWords ); 
     p->vPiVars   = Vec_PtrAlloc( 100 );
     // set random number generator
     srand( 0xABCABC );
@@ -617,10 +617,10 @@ void Ivy_FraigStop( Ivy_FraigMan_t * p )
         Ivy_FraigPrint( p );
     if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
     if ( p->pSat ) sat_solver_delete( p->pSat );
-    FREE( p->pPatScores );
-    FREE( p->pPatWords );
-    FREE( p->pSimWords );
-    free( p );
+    ABC_FREE( p->pPatScores );
+    ABC_FREE( p->pPatWords );
+    ABC_FREE( p->pSimWords );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -646,15 +646,15 @@ void Ivy_FraigPrint( Ivy_FraigMan_t * p )
     printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
         Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
-    PRT( "AIG simulation  ", p->timeSim  );
-    PRT( "AIG traversal   ", p->timeTrav  );
-    PRT( "SAT solving     ", p->timeSat   );
-    PRT( "    Unsat       ", p->timeSatUnsat );
-    PRT( "    Sat         ", p->timeSatSat   );
-    PRT( "    Fail        ", p->timeSatFail  );
-    PRT( "Class refining  ", p->timeRef   );
-    PRT( "TOTAL RUNTIME   ", p->timeTotal );
-    if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
+    ABC_PRT( "AIG simulation  ", p->timeSim  );
+    ABC_PRT( "AIG traversal   ", p->timeTrav  );
+    ABC_PRT( "SAT solving     ", p->timeSat   );
+    ABC_PRT( "    Unsat       ", p->timeSatUnsat );
+    ABC_PRT( "    Sat         ", p->timeSatSat   );
+    ABC_PRT( "    Fail        ", p->timeSatFail  );
+    ABC_PRT( "Class refining  ", p->timeRef   );
+    ABC_PRT( "TOTAL RUNTIME   ", p->timeTotal );
+    if ( p->time1 ) { ABC_PRT( "time1           ", p->time1 ); }
 }
 
 
@@ -1172,7 +1172,7 @@ void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
     pConst1 = Ivy_ManConst1(p->pManAig);
     // allocate the table
     nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13;
-    pTable = ALLOC( Ivy_Obj_t *, nTableSize ); 
+    pTable = ABC_ALLOC( Ivy_Obj_t *, nTableSize ); 
     memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize );
     // collect nodes into the table
     Ivy_ManForEachObj( p->pManAig, pObj, i )
@@ -1218,8 +1218,8 @@ void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
         Ivy_ObjSetClassNodeRepr( pObj, NULL );
         Ivy_FraigAddClass( &p->lClasses, pObj );
     }
-    // free the table
-    free( pTable );
+    // ABC_FREE the table
+    ABC_FREE( pTable );
 }
 
 /**Function*************************************************************
@@ -1314,7 +1314,7 @@ void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
     // determine the best pattern
     BestPat = i * 32 + k;
     // fill in the counter-example data
-    pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+    pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
     Ivy_ManForEachPi( p->pManAig, pObj, i )
     {
         pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
@@ -1513,7 +1513,7 @@ int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
     int * pModel;
     Ivy_Obj_t * pObj;
     int i;
-    pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+    pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
     Ivy_ManForEachPi( p->pManFraig, pObj, i )
         pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
     return pModel;
@@ -1785,7 +1785,7 @@ void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbos
     if ( !fVerbose )
         return;
     printf( "Nodes = %7d.  Levels = %4d.  ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
-    PRT( pString, clock() - clk );
+    ABC_PRT( pString, clock() - clk );
 }
 
 /**Function*************************************************************
@@ -1871,7 +1871,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
     {
         if ( i && fVerbose )
         {
-            PRT( "Time", clock() -clk );
+            ABC_PRT( "Time", clock() -clk );
         }
         pObjNew = Ivy_ObjChild0Equiv(pObj);
         // check if the output is constant 1
@@ -1880,7 +1880,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
             if ( fVerbose )
                 printf( "Output %2d (out of %2d) is constant 1.  ", i, Ivy_ManPoNum(p->pManAig) );
             // assing constant 0 model
-            p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+            p->pManFraig->pData = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
             memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
             break;
         }
@@ -1897,7 +1897,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
             if ( fVerbose )
                 printf( "Output %2d (out of %2d) cannot be constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
             // assing constant 0 model
-            p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+            p->pManFraig->pData = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
             memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
             break;
         }
@@ -1934,7 +1934,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
     }
     if ( fVerbose )
     {
-        PRT( "Time", clock() -clk );
+        ABC_PRT( "Time", clock() -clk );
     }
 }
 
@@ -2127,7 +2127,7 @@ clk = clock();
     pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
@@ -2171,7 +2171,7 @@ clk = clock();
     pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
     pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
@@ -2203,12 +2203,12 @@ p->timeSatFail += clock() - clk;
     // check BDD proof
     {
         int RetVal;
-        PRT( "Sat", clock() - clk2 );
+        ABC_PRT( "Sat", clock() - clk2 );
         clk2 = clock();
         RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
 //        printf( "%d ", RetVal );
         assert( RetVal );
-        PRT( "Bdd", clock() - clk2 );
+        ABC_PRT( "Bdd", clock() - clk2 );
         printf( "\n" );
     }
 */
@@ -2259,7 +2259,7 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
 clk = clock();
     pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
-        (sint64)p->pParams->nBTLimitMiter, (sint64)0, 
+        (ABC_INT64_T)p->pParams->nBTLimitMiter, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
@@ -2395,7 +2395,7 @@ void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t
     assert( Ivy_ObjIsNode( pNode ) );
     // create storage for literals
     nLits = Vec_PtrSize(vSuper) + 1;
-    pLits = ALLOC( int, nLits );
+    pLits = ABC_ALLOC( int, nLits );
     // suppose AND-gate is A & B = C
     // add !A => !C   or   A + !C
     Vec_PtrForEachEntry( vSuper, pFanin, i )
@@ -2411,7 +2411,7 @@ void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t
     pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0);
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
     assert( RetValue );
-    free( pLits );
+    ABC_FREE( pLits );
 }
 
 /**Function*************************************************************
@@ -2663,7 +2663,7 @@ DdNode * Ivy_FraigNodesAreEquivBdd_int( DdManager * dd, DdNode * bFunc, Vec_Ptr_
     }
     // collect the permutation
     NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp));
-    pFuncs = ALLOC( DdNode *, NewSize );
+    pFuncs = ABC_ALLOC( DdNode *, NewSize );
     Vec_PtrForEachEntry( vFront, pObj, i )
     {
         if ( (int)pObj->Level != Level )
@@ -2693,9 +2693,9 @@ DdNode * Ivy_FraigNodesAreEquivBdd_int( DdManager * dd, DdNode * bFunc, Vec_Ptr_
     // deref
     for ( i = 0; i < dd->size; i++ )
         Cudd_RecursiveDeref( dd, pFuncs[i] );
-    free( pFuncs );
+    ABC_FREE( pFuncs );
 
-    free( vFront->pArray );
+    ABC_FREE( vFront->pArray );
     *vFront = *vTemp;
 
     vTemp->nCap = vTemp->nSize = 0;
diff --git a/src/aig/ivy/ivyHaig.c b/src/aig/ivy/ivyHaig.c
index 87021600..62624642 100644
--- a/src/aig/ivy/ivyHaig.c
+++ b/src/aig/ivy/ivyHaig.c
@@ -518,7 +518,7 @@ printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
         Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
             pObj->Init = pObj->Level, pObj->Level = 0;
     }
-    // free arrays
+    // ABC_FREE arrays
     Vec_IntFree( vNodes );
     Vec_IntFree( vLatches );
 }
diff --git a/src/aig/ivy/ivyMan.c b/src/aig/ivy/ivyMan.c
index 66c279cf..d09f6ffd 100644
--- a/src/aig/ivy/ivyMan.c
+++ b/src/aig/ivy/ivyMan.c
@@ -43,7 +43,7 @@ Ivy_Man_t * Ivy_ManStart()
 {
     Ivy_Man_t * p;
     // start the manager
-    p = ALLOC( Ivy_Man_t, 1 );
+    p = ABC_ALLOC( Ivy_Man_t, 1 );
     memset( p, 0, sizeof(Ivy_Man_t) );
     // perform initializations
     p->Ghost.Id   = -1;
@@ -63,7 +63,7 @@ Ivy_Man_t * Ivy_ManStart()
     p->nCreated = 1;
     // start the table
     p->nTableSize = 10007;
-    p->pTable = ALLOC( int, p->nTableSize );
+    p->pTable = ABC_ALLOC( int, p->nTableSize );
     memset( p->pTable, 0, sizeof(int) * p->nTableSize );
     return p;
 }
@@ -143,7 +143,7 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
     // update the counters of different objects
     pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p);
     pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p);
-    // free arrays
+    // ABC_FREE arrays
     Vec_IntFree( vNodes );
     Vec_IntFree( vLatches );
     // make sure structural hashing did not change anything
@@ -234,8 +234,8 @@ Ivy_Man_t * Ivy_ManFrames( Ivy_Man_t * pMan, int nLatches, int nFrames, int fIni
 ***********************************************************************/
 void Ivy_ManStop( Ivy_Man_t * p )
 {
-    if ( p->time1 ) { PRT( "Update lev  ", p->time1 ); }
-    if ( p->time2 ) { PRT( "Update levR ", p->time2 ); }
+    if ( p->time1 ) { ABC_PRT( "Update lev  ", p->time1 ); }
+    if ( p->time2 ) { ABC_PRT( "Update levR ", p->time2 ); }
 //    Ivy_TableProfile( p );
 //    if ( p->vFanouts )  Ivy_ManStopFanout( p );
     if ( p->vChunks )   Ivy_ManStopMemory( p );
@@ -244,8 +244,8 @@ void Ivy_ManStop( Ivy_Man_t * p )
     if ( p->vPos )      Vec_PtrFree( p->vPos );
     if ( p->vBufs )     Vec_PtrFree( p->vBufs );
     if ( p->vObjs )     Vec_PtrFree( p->vObjs );
-    free( p->pTable );
-    free( p );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -346,7 +346,7 @@ int Ivy_ManCleanupSeq( Ivy_Man_t * p )
         // delete buffer from the array of buffers
         if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
             Vec_PtrRemove( p->vBufs, pObj );
-        // free the node
+        // ABC_FREE the node
         Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
         Ivy_ManRecycleMemory( p, pObj );
     }
diff --git a/src/aig/ivy/ivyMem.c b/src/aig/ivy/ivyMem.c
index fd29e9ae..4ea6d891 100644
--- a/src/aig/ivy/ivyMem.c
+++ b/src/aig/ivy/ivyMem.c
@@ -65,7 +65,7 @@ void Ivy_ManStopMemory( Ivy_Man_t * p )
     void * pMemory;
     int i;
     Vec_PtrForEachEntry( p->vChunks, pMemory, i )
-        free( pMemory );
+        ABC_FREE( pMemory );
     Vec_PtrFree( p->vChunks );
     Vec_PtrFree( p->vPages );
     p->pListFree = NULL;
@@ -93,10 +93,10 @@ void Ivy_ManAddMemory( Ivy_Man_t * p )
 //    assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
     // allocate new memory page
     nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + EntrySizeMax;
-    pMemory = ALLOC( char, nBytes );
+    pMemory = ABC_ALLOC( char, nBytes );
     Vec_PtrPush( p->vChunks, pMemory );
     // align memory at the 32-byte boundary
-    pMemory = pMemory + EntrySizeMax - (((int)(PORT_PTRUINT_T)pMemory) & (EntrySizeMax-1));
+    pMemory = pMemory + EntrySizeMax - (((int)(ABC_PTRUINT_T)pMemory) & (EntrySizeMax-1));
     // remember the manager in the first entry
     Vec_PtrPush( p->vPages, pMemory );
     // break the memory down into nodes
diff --git a/src/aig/ivy/ivyObj.c b/src/aig/ivy/ivyObj.c
index 59dda19c..d7925fab 100644
--- a/src/aig/ivy/ivyObj.c
+++ b/src/aig/ivy/ivyObj.c
@@ -268,7 +268,7 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
     // clean and recycle the entry
     if ( fFreeTop )
     {
-        // free the node
+        // ABC_FREE the node
         Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
         Ivy_ManRecycleMemory( p, pObj );
     }
diff --git a/src/aig/ivy/ivyResyn.c b/src/aig/ivy/ivyResyn.c
index f42d7464..35ecb122 100644
--- a/src/aig/ivy/ivyResyn.c
+++ b/src/aig/ivy/ivyResyn.c
@@ -50,21 +50,21 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
 clk = clock();
     pMan = Ivy_ManBalance( pMan, fUpdateLevel );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
 clk = clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
     return pMan;
 }
@@ -91,49 +91,49 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
 clk = clock();
     pMan = Ivy_ManBalance( pMan, fUpdateLevel );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
 clk = clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
 clk = clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
 clk = clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
     return pMan;
 }
@@ -160,7 +160,7 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
 clk = clock();
     Ivy_ManRewritePre( pMan, 0, 0, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
@@ -168,21 +168,21 @@ clk = clock();
 //    pMan = Ivy_ManDup( pTemp = pMan );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 /*
 clk = clock();
     Ivy_ManRewritePre( pMan, 0, 0, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
     pMan = Ivy_ManBalance( pTemp = pMan, 0 );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 */
     return pMan;
diff --git a/src/aig/ivy/ivySeq.c b/src/aig/ivy/ivySeq.c
index f4585fa2..0971a548 100644
--- a/src/aig/ivy/ivySeq.c
+++ b/src/aig/ivy/ivySeq.c
@@ -1127,7 +1127,7 @@ void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs )
     }
     printf( "All = %6d. Minus = %6d. Triv = %6d.   Node = %6d. Satur = %6d.  ", 
         nCutsTotal, nCutsTotalM, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ivy/ivyTable.c b/src/aig/ivy/ivyTable.c
index 2ac0ae49..fdcc4bfb 100644
--- a/src/aig/ivy/ivyTable.c
+++ b/src/aig/ivy/ivyTable.c
@@ -210,7 +210,7 @@ clk = clock();
     nTableSizeOld = p->nTableSize;
     // get the new table
     p->nTableSize = Cudd_PrimeAig( 5 * Ivy_ManHashObjNum(p) ); 
-    p->pTable = ALLOC( int, p->nTableSize );
+    p->pTable = ABC_ALLOC( int, p->nTableSize );
     memset( p->pTable, 0, sizeof(int) * p->nTableSize );
     // rehash the entries from the old table
     Counter = 0;
@@ -227,9 +227,9 @@ clk = clock();
     nEntries = Ivy_ManHashObjNum(p);
 //    assert( Counter == nEntries );
 //    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
-//    PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", clock() - clk );
     // replace the table and the parameters
-    free( pTableOld );
+    ABC_FREE( pTableOld );
 }
 
 /**Function********************************************************************