Version abc90215

42 files changed, 582 insertions, 627 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index d7a3e98c..f81479b3 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -29,10 +29,6 @@
 #ifndef __EXTRA_H__
 #define __EXTRA_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
 #endif
@@ -46,14 +42,12 @@ extern "C" {
 #include <string.h>
 #include <assert.h>
 #include <time.h>
+#include "abc_global.h"
 #include "st.h"
 #include "cuddInt.h"
-#include "port_type.h"
 
-// catch memory leaks in Visual Studio
-#ifdef _DEBUG
-#define _CRTDBG_MAP_ALLOC
-#include <crtdbg.h>
+#ifdef __cplusplus
+extern "C" {
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -76,25 +70,9 @@ extern "C" {
 /* Macro declarations                                                        */
 /*---------------------------------------------------------------------------*/
 
-#ifdef WIN32
-#define ABC_DLLEXPORT __declspec(dllexport)
-#define ABC_DLLIMPORT __declspec(dllimport)
-#else  /* defined(WIN32) */
-#define ABC_DLLIMPORT
-#endif /* defined(WIN32) */
-
-#ifndef ABC_DLL
-#define ABC_DLL ABC_DLLIMPORT
-#endif
-
 typedef unsigned char      uint8;
 typedef unsigned short     uint16;
 typedef unsigned int       uint32;
-#ifdef WIN32
-typedef unsigned __int64   uint64;
-#else
-typedef unsigned long long uint64;
-#endif
 
 /* constants of the manager */
 #define     b0     Cudd_Not((dd)->one)
@@ -106,34 +84,21 @@ typedef unsigned long long uint64;
 
 // hash key macros
 #define hashKey1(a,TSIZE) \
-((PORT_PTRUINT_T)(a) % TSIZE)
+((ABC_PTRUINT_T)(a) % TSIZE)
 
 #define hashKey2(a,b,TSIZE) \
-(((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b) * DD_P1) % TSIZE)
+(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)
 
 #define hashKey3(a,b,c,TSIZE) \
-(((((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b)) * DD_P1 + (PORT_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
+(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
 
 #define hashKey4(a,b,c,d,TSIZE) \
-((((((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b)) * DD_P1 + (PORT_PTRUINT_T)(c)) * DD_P2 + \
-   (PORT_PTRUINT_T)(d)) * DD_P3) % TSIZE)
+((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
+   (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)
 
 #define hashKey5(a,b,c,d,e,TSIZE) \
-(((((((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b)) * DD_P1 + (PORT_PTRUINT_T)(c)) * DD_P2 + \
-   (PORT_PTRUINT_T)(d)) * DD_P3 + (PORT_PTRUINT_T)(e)) * DD_P1) % TSIZE)
-
-#ifndef PRT
-#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
-#define PRTn(a,t)  printf("%s = ", (a)); printf("%6.2f sec  ", (float)(t)/(float)(CLOCKS_PER_SEC))
-#endif
-
-#ifndef PRTP
-#define PRTP(a,t,T)  printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
-#endif
-
-#ifndef PRB
-#define PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
-#endif
+(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
+   (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)
 
 /*===========================================================================*/
 /*     Various Utilities                                                     */
@@ -229,6 +194,10 @@ extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
 extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
 extern DdNode *     Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
 
+#ifndef ABC_PRB
+#define ABC_PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
+#endif
+
 /*=== extraBddKmap.c ================================================================*/
 
 /* displays the Karnaugh Map of a function */
@@ -617,33 +586,6 @@ extern unsigned    Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux
 
 /*=== extraUtilUtil.c ================================================================*/
 
-#ifndef ABS
-#define ABS(a)            ((a) < 0 ? -(a) : (a))
-#endif
-
-#ifndef MAX
-#define MAX(a,b)        ((a) > (b) ? (a) : (b))
-#endif
-
-#ifndef MIN
-#define MIN(a,b)        ((a) < (b) ? (a) : (b))
-#endif
-
-#ifndef ALLOC
-#define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
-#endif
-
-#ifndef FREE
-#define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
-#endif
-
-#ifndef REALLOC
-#define REALLOC(type, obj, num)    \
-        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-         ((type *) malloc(sizeof(type) * (num))))
-#endif
-
-
 extern long          Extra_CpuTime();
 extern double        Extra_CpuTimeDouble();
 extern int           Extra_GetSoftDataLimit();
diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c
index 11612ef4..ebafb3a8 100644
--- a/src/misc/extra/extraBddAuto.c
+++ b/src/misc/extra/extraBddAuto.c
@@ -159,7 +159,7 @@ DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
     int i, lev;
 
     // get the support
-    pSupport = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
+    pSupport = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
     Extra_SupportArray( dd, bFunc, pSupport );
     nSupp = 0;
     for ( i = 0; i < dd->size; i++ )
@@ -171,14 +171,14 @@ DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
     {
         printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" );
         fflush( stdout );
-        free( pSupport );
+        ABC_FREE( pSupport );
         return NULL;
     }
 
     // create the permutation arrays
-    pPermute     = ALLOC( int, dd->size );
-    pPermuteBack = ALLOC( int, dd->size );
-    pCompose     = ALLOC( DdNode *, dd->size );
+    pPermute     = ABC_ALLOC( int, dd->size );
+    pPermuteBack = ABC_ALLOC( int, dd->size );
+    pCompose     = ABC_ALLOC( DdNode *, dd->size );
     for ( i = 0; i < dd->size; i++ )
     {
         pPermute[i]     = i;
@@ -225,10 +225,10 @@ DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
 
     for ( i = 0; i < dd->size; i++ )
         Cudd_RecursiveDeref( dd, pCompose[i] );
-    free( pPermute );
-    free( pPermuteBack );
-    free( pCompose );
-    free( pSupport );
+    ABC_FREE( pPermute );
+    ABC_FREE( pPermuteBack );
+    ABC_FREE( pCompose );
+    ABC_FREE( pSupport );
 
     Cudd_Deref( bSpace );
     return bSpace;
@@ -500,11 +500,11 @@ DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * z
     DdNode * zExor, * zTemp;
 
     // get the set of non-canonical variables
-    pVarsNonCan = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
+    pVarsNonCan = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
     Extra_SupportArray( dd, bFuncRed, pVarsNonCan );
 
     // allocate storage for the EXOR sets
-    pzRes = ALLOC( DdNode *, dd->size );
+    pzRes = ABC_ALLOC( DdNode *, dd->size );
     memset( pzRes, 0, sizeof(DdNode *) * dd->size );
 
     // go through all the equations
@@ -536,7 +536,7 @@ DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * z
     }
     Cudd_RecursiveDerefZdd( dd, zEquRem );
 
-    free( pVarsNonCan );
+    ABC_FREE( pVarsNonCan );
     return pzRes;
 }
 
@@ -575,7 +575,7 @@ DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
     // both bFunc and bCore are not constants
 
     // the operation is commutative - normalize the problem
-    if ( (unsigned)(PORT_PTRUINT_T)bF > (unsigned)(PORT_PTRUINT_T)bG )
+    if ( (unsigned)(ABC_PTRUINT_T)bF > (unsigned)(ABC_PTRUINT_T)bG )
         return extraBddSpaceFromFunction(dd, bG, bF);
 
 
diff --git a/src/misc/extra/extraBddCas.c b/src/misc/extra/extraBddCas.c
index 29382bfb..ccf7397d 100644
--- a/src/misc/extra/extraBddCas.c
+++ b/src/misc/extra/extraBddCas.c
@@ -226,7 +226,7 @@ Extra_bddEncodingNonStrict(
 //    s_EncSearchTime += clock() - clk;
 
     // allocate the temporary storage for the columns
-    s_pbTemp = (DdNode **) malloc( nColumns * sizeof(DdNode *) );
+    s_pbTemp = (DdNode **)ABC_ALLOC( char, nColumns * sizeof(DdNode *) );
 
 //    clk = clock();
     bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars );   Cudd_Ref( bResult );
@@ -236,7 +236,7 @@ Extra_bddEncodingNonStrict(
     Cudd_RecursiveDeref( dd, bEncoded );
 //    Cudd_RecursiveDeref( dd, aEncoded );
 
-    free( s_pbTemp );
+    ABC_FREE( s_pbTemp );
 
     *pSimple = s_nVarsBest;
     Cudd_Deref( bResult );
@@ -306,7 +306,7 @@ st_table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLe
         st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) 
         {
             Cudd_RecursiveDeref( dd, p->bSum );
-            free( p );
+            ABC_FREE( p );
         }
         st_free_table( Visited );
     }
@@ -394,7 +394,7 @@ int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode *
         st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) 
         {
             Cudd_RecursiveDeref( dd, p->bSum );
-            free( p );
+            ABC_FREE( p );
         }
         st_free_table( Visited );
     }
@@ -1123,7 +1123,7 @@ void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st_table * Visited )
     assert( !Cudd_IsComplement(aFunc) );
 
     // create the new traversal entry
-    p = (traventry *) malloc( sizeof(traventry) );
+    p = (traventry *) ABC_ALLOC( char, sizeof(traventry) );
     // set the initial sum of edges to zero BDD
     p->bSum = b0;   Cudd_Ref( b0 );
     // set the starting number of incoming edges
diff --git a/src/misc/extra/extraBddImage.c b/src/misc/extra/extraBddImage.c
index 23c1c682..11d60a40 100644
--- a/src/misc/extra/extraBddImage.c
+++ b/src/misc/extra/extraBddImage.c
@@ -170,7 +170,7 @@ Extra_ImageTree_t * Extra_bddImageStart(
     pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
     
     // create the tree
-    pTree = ALLOC( Extra_ImageTree_t, 1 );
+    pTree = ABC_ALLOC( Extra_ImageTree_t, 1 );
     memset( pTree, 0, sizeof(Extra_ImageTree_t) );
     pTree->pCare = pNodes[nParts];
     pTree->fVerbose = fVerbose;
@@ -181,7 +181,7 @@ Extra_ImageTree_t * Extra_bddImageStart(
     // make sure the variables are gone
     for ( v = 0; v < dd->size; v++ )
         assert( pVars[v] == NULL );
-    FREE( pVars );
+    ABC_FREE( pVars );
 
     // merge the topmost nodes
     while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
@@ -189,7 +189,7 @@ Extra_ImageTree_t * Extra_bddImageStart(
     // make sure the nodes are gone
     for ( v = 0; v < nParts + 1; v++ )
         assert( pNodes[v] == NULL );
-    FREE( pNodes );
+    ABC_FREE( pNodes );
 
 //    if ( fVerbose )
 //        Extra_bddImagePrintTree( pTree );
@@ -199,7 +199,7 @@ Extra_ImageTree_t * Extra_bddImageStart(
 
     // clean the partitions
     Extra_DeleteParts_rec( pTree->pRoot );
-    FREE( pParts );
+    ABC_FREE( pParts );
     return pTree;
 }
 
@@ -229,9 +229,9 @@ DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare )
         if ( bRem != b1 )
         {
 printf( "Original care set support: " );
-PRB( dd, pTree->bCareSupp );
+ABC_PRB( dd, pTree->bCareSupp );
 printf( "Current care set support: " );
-PRB( dd, bSupp );
+ABC_PRB( dd, bSupp );
             Cudd_RecursiveDeref( dd, bSupp );
             Cudd_RecursiveDeref( dd, bRem );
             printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
@@ -272,7 +272,7 @@ void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree )
     if ( pTree->bCareSupp )
         Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
     Extra_bddImageTreeDelete_rec( pTree->pRoot );
-    FREE( pTree );
+    ABC_FREE( pTree );
 }
 
 /**Function*************************************************************
@@ -317,11 +317,11 @@ Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
     int i;
 
     // start the partitions
-    pParts = ALLOC( Extra_ImagePart_t *, nParts + 1 );
+    pParts = ABC_ALLOC( Extra_ImagePart_t *, nParts + 1 );
     // create structures for each variable
     for ( i = 0; i < nParts; i++ )
     {
-        pParts[i] = ALLOC( Extra_ImagePart_t, 1 );
+        pParts[i] = ABC_ALLOC( Extra_ImagePart_t, 1 );
         pParts[i]->bFunc  = pbParts[i];                           Cudd_Ref( pParts[i]->bFunc );
         pParts[i]->bSupp  = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
         pParts[i]->nSupp  = Extra_bddSuppSize( dd, pParts[i]->bSupp );
@@ -329,7 +329,7 @@ Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
         pParts[i]->iPart  = i;
     }
     // add the care set as the last partition
-    pParts[nParts] = ALLOC( Extra_ImagePart_t, 1 );
+    pParts[nParts] = ABC_ALLOC( Extra_ImagePart_t, 1 );
     pParts[nParts]->bFunc = bCare;                                     Cudd_Ref( pParts[nParts]->bFunc );
     pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
     pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp );
@@ -359,11 +359,11 @@ Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
     int nVarsTotal, iVar, p, Counter;
 
     // put all the functions into one array
-    pbFuncs = ALLOC( DdNode *, nParts );
+    pbFuncs = ABC_ALLOC( DdNode *, nParts );
     for ( p = 0; p < nParts; p++ )
         pbFuncs[p] = pParts[p]->bSupp;
     bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts );  Cudd_Ref( bSupp );
-    FREE( pbFuncs );
+    ABC_FREE( pbFuncs );
 
     // remove the NS vars
     bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );        Cudd_Ref( bCubeNs );
@@ -375,13 +375,13 @@ Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
     nVarsTotal = Extra_bddSuppSize( dd, bSupp );
 
     // start the variables
-    pVars = ALLOC( Extra_ImageVar_t *, dd->size );
+    pVars = ABC_ALLOC( Extra_ImageVar_t *, dd->size );
     memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size );
     // create structures for each variable
     for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
     {
         iVar = bSuppTemp->index;
-        pVars[iVar] = ALLOC( Extra_ImageVar_t, 1 );
+        pVars[iVar] = ABC_ALLOC( Extra_ImageVar_t, 1 );
         pVars[iVar]->iNum = iVar;
         // collect all the parts this var belongs to
         Counter = 0;
@@ -428,11 +428,11 @@ Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
     Extra_ImagePart_t * pPart;    // the partition (temporary)
 */
     // start the partitions
-    pNodes = ALLOC( Extra_ImageNode_t *, nParts );
+    pNodes = ABC_ALLOC( Extra_ImageNode_t *, nParts );
     // create structures for each leaf nodes
     for ( i = 0; i < nParts; i++ )
     {
-        pNodes[i] = ALLOC( Extra_ImageNode_t, 1 );
+        pNodes[i] = ABC_ALLOC( Extra_ImageNode_t, 1 );
         memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) );
         pNodes[i]->dd    = dd;
         pNodes[i]->pPart = pParts[i];
@@ -459,7 +459,7 @@ Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
         }
         // remove these  variables
         Cudd_RecursiveDeref( dd, pVars[v]->bParts );
-        FREE( pVars[v] );
+        ABC_FREE( pVars[v] );
     }
 
     // assign the leaf node images
@@ -494,9 +494,9 @@ Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
     for ( i = 0; i < nParts; i++ )
     {
         pNode = pNodes[i];
-PRB( dd, pNode->bCube );
-PRB( dd, pNode->pPart->bFunc );
-PRB( dd, pNode->pPart->bSupp );
+ABC_PRB( dd, pNode->bCube );
+ABC_PRB( dd, pNode->pPart->bFunc );
+ABC_PRB( dd, pNode->pPart->bSupp );
 printf( "\n" );
     }
 */
@@ -525,7 +525,7 @@ void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode )
     pPart = pNode->pPart;
     Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
     Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
-    FREE( pNode->pPart );
+    ABC_FREE( pNode->pPart );
 }
 
 /**Function*************************************************************
@@ -550,7 +550,7 @@ void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode )
     if ( pNode->bImage )
         Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
     assert( pNode->pPart == NULL );
-    FREE( pNode );
+    ABC_FREE( pNode );
 }
 
 /**Function*************************************************************
@@ -663,11 +663,11 @@ int Extra_BuildTreeNode( DdManager * dd,
                 Cudd_RecursiveDeref( dd, bTemp );
                 // clean this var
                 Cudd_RecursiveDeref( dd, pVars[v]->bParts );
-                FREE( pVars[v] );
+                ABC_FREE( pVars[v] );
             }
         // clean the best var
         Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
-        FREE( pVars[iVarBest] );
+        ABC_FREE( pVars[iVarBest] );
 
         // combines two nodes
         pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
@@ -783,7 +783,7 @@ Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
     Extra_ImagePart_t * pPart;
 
     // create a new partition
-    pPart = ALLOC( Extra_ImagePart_t, 1 );
+    pPart = ABC_ALLOC( Extra_ImagePart_t, 1 );
     memset( pPart, 0, sizeof(Extra_ImagePart_t) );
     // create the function
     pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
@@ -796,12 +796,12 @@ Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
     pPart->nNodes = Cudd_DagSize( pPart->bFunc );
     pPart->iPart = -1;
 /*
-PRB( dd, pNode1->pPart->bSupp );
-PRB( dd, pNode2->pPart->bSupp );
-PRB( dd, pPart->bSupp );
+ABC_PRB( dd, pNode1->pPart->bSupp );
+ABC_PRB( dd, pNode2->pPart->bSupp );
+ABC_PRB( dd, pPart->bSupp );
 */
     // create a new node
-    pNode = ALLOC( Extra_ImageNode_t, 1 );
+    pNode = ABC_ALLOC( Extra_ImageNode_t, 1 );
     memset( pNode, 0, sizeof(Extra_ImageNode_t) );
     pNode->dd     = dd;
     pNode->pPart  = pPart;
@@ -1013,7 +1013,7 @@ void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
         printf( "<%d> ", pNode->pPart->iPart );
         if ( Cube != NULL )
         {
-            PRB( pNode->dd, Cube );
+            ABC_PRB( pNode->dd, Cube );
         }
         else
             printf( "\n" );
@@ -1023,7 +1023,7 @@ void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
     printf( "<*> " );
     if ( Cube != NULL )
     {
-        PRB( pNode->dd, Cube );
+        ABC_PRB( pNode->dd, Cube );
     }
     else
         printf( "\n" );
@@ -1069,7 +1069,7 @@ Extra_ImageTree2_t * Extra_bddImageStart2(
     DdNode * bCubeAll, * bCubeNot, * bTemp;
     int i;
 
-    pTree = ALLOC( Extra_ImageTree2_t, 1 );
+    pTree = ABC_ALLOC( Extra_ImageTree2_t, 1 );
     pTree->dd = dd;
     pTree->bImage = NULL;
 
@@ -1130,7 +1130,7 @@ void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree )
         Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
     if ( pTree->bImage )
         Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
-    FREE( pTree );
+    ABC_FREE( pTree );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 8b8bdd81..e17d1744 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -112,7 +112,7 @@ DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestina
 
     nMin = ddMin(ddSource->size, ddDestination->size);
     nMax = ddMax(ddSource->size, ddDestination->size);
-    pPermute = ALLOC( int, nMax );
+    pPermute = ABC_ALLOC( int, nMax );
     // set up the variable permutation
     for ( i = 0; i < nMin; i++ )
         pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i];
@@ -122,7 +122,7 @@ DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestina
             pPermute[ ddSource->invperm[i] ] = -1;
     }
     bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute );
-    FREE( pPermute );
+    ABC_FREE( pPermute );
     return bRes;
 }
 
@@ -145,7 +145,7 @@ DdNode * Extra_bddRemapUp(
     DdNode * bSupp, * bTemp, * bRes;
     int Counter;
 
-    pPermute = ALLOC( int, dd->size );
+    pPermute = ABC_ALLOC( int, dd->size );
 
     // get support
     bSupp = Cudd_Support( dd, bF );    Cudd_Ref( bSupp );
@@ -164,7 +164,7 @@ DdNode * Extra_bddRemapUp(
 
     // return
     Cudd_Deref( bRes );
-    free( pPermute );
+    ABC_FREE( pPermute );
     return bRes;
 }
 
@@ -584,7 +584,7 @@ DdNode *  Extra_bddFindOneCube( DdManager * dd, DdNode * bF )
     int v;
 
     // get the vector of variables in the cube
-    s_Temp = ALLOC( char, dd->size );
+    s_Temp = ABC_ALLOC( char, dd->size );
     Cudd_bddPickOneCube( dd, bF, s_Temp );
 
     // start the cube
@@ -603,7 +603,7 @@ DdNode *  Extra_bddFindOneCube( DdManager * dd, DdNode * bF )
             Cudd_RecursiveDeref( dd, bTemp );
         }
     Cudd_Deref(bCube);
-    free( s_Temp );
+    ABC_FREE( s_Temp );
     return bCube;
 }
 
@@ -745,7 +745,7 @@ DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
 
     /* Allocate and initialize support array for ddSupportStep. */
     size = ddMax( dd->size, dd->sizeZ );
-    support = ALLOC( int, size );
+    support = ABC_ALLOC( int, size );
     if ( support == NULL )
     {
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -793,7 +793,7 @@ DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
     }
     while ( dd->reordered == 1 );
 
-    FREE( support );
+    ABC_FREE( support );
     if ( res != NULL )
         cuddDeref( res );
     return ( res );
diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c
index 666814f6..e42130d4 100644
--- a/src/misc/extra/extraBddSymm.c
+++ b/src/misc/extra/extraBddSymm.c
@@ -207,12 +207,12 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
     Extra_SymmInfo_t * p;
 
     // allocate and clean the storage for symmetry info
-    p = ALLOC( Extra_SymmInfo_t, 1 );
+    p = ABC_ALLOC( Extra_SymmInfo_t, 1 );
     memset( p, 0, sizeof(Extra_SymmInfo_t) );
     p->nVars     = nVars;
-    p->pVars     = ALLOC( int, nVars );  
-    p->pSymms    = ALLOC( char *, nVars );  
-    p->pSymms[0] = ALLOC( char  , nVars * nVars );
+    p->pVars     = ABC_ALLOC( int, nVars );  
+    p->pSymms    = ABC_ALLOC( char *, nVars );  
+    p->pSymms[0] = ABC_ALLOC( char  , nVars * nVars );
     memset( p->pSymms[0], 0, nVars * nVars * sizeof(char) );
 
     for ( i = 1; i < nVars; i++ )
@@ -234,10 +234,10 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
 ******************************************************************************/
 void Extra_SymmPairsDissolve( Extra_SymmInfo_t * p )
 {
-    free( p->pVars );
-    free( p->pSymms[0] );
-    free( p->pSymms    );
-    free( p );
+    ABC_FREE( p->pVars );
+    ABC_FREE( p->pSymms[0] );
+    ABC_FREE( p->pSymms    );
+    ABC_FREE( p );
 } /* end of Extra_SymmPairsDissolve */
 
 /**Function********************************************************************
@@ -298,7 +298,7 @@ Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs
     p = Extra_SymmPairsAllocate( nSuppSize );
 
     // allocate the storage for the temporary map
-    pMapVars2Nums = ALLOC( int, dd->size );
+    pMapVars2Nums = ABC_ALLOC( int, dd->size );
     memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
 
     // assign the variables
@@ -337,7 +337,7 @@ Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs
     } // for each cube 
     Cudd_RecursiveDerefZdd( dd, zSet );
 
-    FREE( pMapVars2Nums );
+    ABC_FREE( pMapVars2Nums );
     return p;
 
 } /* end of Extra_SymmPairsCreateFromZdd */
diff --git a/src/misc/extra/extraBddUnate.c b/src/misc/extra/extraBddUnate.c
index 92396c38..715731bd 100644
--- a/src/misc/extra/extraBddUnate.c
+++ b/src/misc/extra/extraBddUnate.c
@@ -153,10 +153,10 @@ Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars )
 {
     Extra_UnateInfo_t * p;
     // allocate and clean the storage for unateness info
-    p = ALLOC( Extra_UnateInfo_t, 1 );
+    p = ABC_ALLOC( Extra_UnateInfo_t, 1 );
     memset( p, 0, sizeof(Extra_UnateInfo_t) );
     p->nVars     = nVars;
-    p->pVars     = ALLOC( Extra_UnateVar_t, nVars );  
+    p->pVars     = ABC_ALLOC( Extra_UnateVar_t, nVars );  
     memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) );
     return p;
 } /* end of Extra_UnateInfoAllocate */
@@ -174,8 +174,8 @@ Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars )
 ******************************************************************************/
 void Extra_UnateInfoDissolve( Extra_UnateInfo_t * p )
 {
-    free( p->pVars );
-    free( p );
+    ABC_FREE( p->pVars );
+    ABC_FREE( p );
 } /* end of Extra_UnateInfoDissolve */
 
 /**Function********************************************************************
@@ -193,7 +193,7 @@ void Extra_UnateInfoPrint( Extra_UnateInfo_t * p )
 {
     char * pBuffer;
     int i;
-    pBuffer = ALLOC( char, p->nVarsMax+1 );
+    pBuffer = ABC_ALLOC( char, p->nVarsMax+1 );
     memset( pBuffer, ' ', p->nVarsMax );
     pBuffer[p->nVarsMax] = 0;
     for ( i = 0; i < p->nVars; i++ )
@@ -204,7 +204,7 @@ void Extra_UnateInfoPrint( Extra_UnateInfo_t * p )
         else
             pBuffer[ p->pVars[i].iVar ] = '.';
     printf( "%s\n", pBuffer );
-    free( pBuffer );
+    ABC_FREE( pBuffer );
 } /* end of Extra_UnateInfoPrint */
 
 
@@ -234,7 +234,7 @@ Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPair
     p = Extra_UnateInfoAllocate( nSuppSize );
 
     // allocate the storage for the temporary map
-    pMapVars2Nums = ALLOC( int, dd->size );
+    pMapVars2Nums = ABC_ALLOC( int, dd->size );
     memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
 
     // assign the variables
@@ -269,7 +269,7 @@ Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPair
 
     } // for each cube 
     Cudd_RecursiveDerefZdd( dd, zSet );
-    FREE( pMapVars2Nums );
+    ABC_FREE( pMapVars2Nums );
     return p;
 
 } /* end of Extra_UnateInfoCreateFromZdd */
diff --git a/src/misc/extra/extraUtilBitMatrix.c b/src/misc/extra/extraUtilBitMatrix.c
index b860a538..dd63e05c 100644
--- a/src/misc/extra/extraUtilBitMatrix.c
+++ b/src/misc/extra/extraUtilBitMatrix.c
@@ -79,14 +79,14 @@ Extra_BitMat_t * Extra_BitMatrixStart( int nSize )
 {
     Extra_BitMat_t * p;
     int i;
-    p = ALLOC( Extra_BitMat_t, 1 );
+    p = ABC_ALLOC( Extra_BitMat_t, 1 );
     memset( p, 0, sizeof(Extra_BitMat_t) );
     p->nSize     = nSize;
     p->nBitShift = (sizeof(unsigned) == 4) ?  5:  6;
     p->uMask     = (sizeof(unsigned) == 4) ? 31: 63;
     p->nWords    = nSize / (8 * sizeof(unsigned)) + ((nSize % (8 * sizeof(unsigned))) > 0);
-    p->ppData    = ALLOC( unsigned *, nSize );
-    p->ppData[0] = ALLOC( unsigned, nSize * p->nWords );
+    p->ppData    = ABC_ALLOC( unsigned *, nSize );
+    p->ppData[0] = ABC_ALLOC( unsigned, nSize * p->nWords );
     memset( p->ppData[0], 0, sizeof(unsigned) * nSize * p->nWords );
     for ( i = 1; i < nSize; i++ )
         p->ppData[i] = p->ppData[i-1] + p->nWords;
@@ -122,9 +122,9 @@ void Extra_BitMatrixClean( Extra_BitMat_t * p )
 ***********************************************************************/
 void Extra_BitMatrixStop( Extra_BitMat_t * p )
 {
-    FREE( p->ppData[0] );
-    FREE( p->ppData );
-    FREE( p );
+    ABC_FREE( p->ppData[0] );
+    ABC_FREE( p->ppData );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index 44dff1e0..96cf8601 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -98,7 +98,7 @@ char * Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2,
             }
         }
     }
-    FREE( pFileGen );
+    ABC_FREE( pFileGen );
     if ( pFile )
     {
         fclose( pFile );
@@ -238,7 +238,7 @@ char * Extra_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';
@@ -482,9 +482,9 @@ char * Extra_StringAppend( char * pStrGiven, char * pStrAdd )
     char * pTemp;
     if ( pStrGiven )
     {
-        pTemp = ALLOC( char, strlen(pStrGiven) + strlen(pStrAdd) + 2 );
+        pTemp = ABC_ALLOC( char, strlen(pStrGiven) + strlen(pStrAdd) + 2 );
         sprintf( pTemp, "%s%s", pStrGiven, pStrAdd );
-        free( pStrGiven );
+        ABC_FREE( pStrGiven );
     }
     else
         pTemp = Extra_UtilStrsav( pStrAdd );
diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c
index e672afbb..626d58b5 100644
--- a/src/misc/extra/extraUtilMemory.c
+++ b/src/misc/extra/extraUtilMemory.c
@@ -35,7 +35,7 @@ struct Extra_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
@@ -52,8 +52,8 @@ struct Extra_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
@@ -120,7 +120,7 @@ Extra_MmFixed_t * Extra_MmFixedStart( int nEntrySize )
 {
     Extra_MmFixed_t * p;
 
-    p = ALLOC( Extra_MmFixed_t, 1 );
+    p = ABC_ALLOC( Extra_MmFixed_t, 1 );
     memset( p, 0, sizeof(Extra_MmFixed_t) );
 
     p->nEntrySize    = nEntrySize;
@@ -137,7 +137,7 @@ Extra_MmFixed_t * Extra_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;
@@ -180,9 +180,9 @@ void Extra_MmFixedStop( Extra_MmFixed_t * p )
     if ( p == NULL )
         return;
     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*************************************************************
@@ -201,16 +201,16 @@ char * Extra_MmFixedEntryFetch( Extra_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;
@@ -230,7 +230,7 @@ char * Extra_MmFixedEntryFetch( Extra_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;
@@ -251,7 +251,7 @@ void Extra_MmFixedEntryRecycle( Extra_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;
 }
@@ -274,7 +274,7 @@ void Extra_MmFixedRestart( Extra_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];
@@ -285,7 +285,7 @@ void Extra_MmFixedRestart( Extra_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;
@@ -342,7 +342,7 @@ Extra_MmFlex_t * Extra_MmFlexStart()
 { 
     Extra_MmFlex_t * p;
 //printf( "allocing flex\n" );
-    p = ALLOC( Extra_MmFlex_t, 1 );
+    p = ABC_ALLOC( Extra_MmFlex_t, 1 );
     memset( p, 0, sizeof(Extra_MmFlex_t) );
 
     p->nEntriesUsed  = 0;
@@ -352,7 +352,7 @@ Extra_MmFlex_t * Extra_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;
@@ -396,9 +396,9 @@ void Extra_MmFlexStop( Extra_MmFlex_t * p )
         return;
 //printf( "deleting flex\n" );
     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*************************************************************
@@ -415,13 +415,13 @@ void Extra_MmFlexStop( Extra_MmFlex_t * p )
 char * Extra_MmFlexEntryFetch( Extra_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 )
         {
@@ -429,7 +429,7 @@ char * Extra_MmFlexEntryFetch( Extra_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
@@ -479,7 +479,7 @@ int Extra_MmFlexReadMemUsage( Extra_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 []
 
@@ -490,16 +490,16 @@ Extra_MmStep_t * Extra_MmStepStart( int nSteps )
 {
     Extra_MmStep_t * p;
     int i, k;
-    p = ALLOC( Extra_MmStep_t, 1 );
+    p = ABC_ALLOC( Extra_MmStep_t, 1 );
     memset( p, 0, sizeof(Extra_MmStep_t) );
     p->nMems = nSteps;
     // start the fixed memory managers
-    p->pMems = ALLOC( Extra_MmFixed_t *, p->nMems );
+    p->pMems = ABC_ALLOC( Extra_MmFixed_t *, p->nMems );
     for ( i = 0; i < p->nMems; i++ )
         p->pMems[i] = Extra_MmFixedStart( (8<<i) );
     // set up the mapping of the required memory size into the corresponding manager
     p->nMapSize = (4<<p->nMems);
-    p->pMap = ALLOC( Extra_MmFixed_t *, p->nMapSize+1 );
+    p->pMap = ABC_ALLOC( Extra_MmFixed_t *, p->nMapSize+1 );
     p->pMap[0] = NULL;
     for ( k = 1; k <= 4; k++ )
         p->pMap[k] = p->pMems[0];
@@ -530,12 +530,12 @@ void Extra_MmStepStop( Extra_MmStep_t * p )
     if ( p->pLargeChunks ) 
     {
       for ( i = 0; i < p->nLargeChunks; i++ )
-          free( p->pLargeChunks[i] );
-      free( p->pLargeChunks );
+          ABC_FREE( p->pLargeChunks[i] );
+      ABC_FREE( p->pLargeChunks );
     }
-    free( p->pMems );
-    free( p->pMap );
-    free( p );
+    ABC_FREE( p->pMems );
+    ABC_FREE( p->pMap );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -556,15 +556,15 @@ char * Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes )
     if ( nBytes > p->nMapSize )
     {
 //        printf( "Allocating %d bytes.\n", nBytes );
-//        return ALLOC( char, nBytes );
+//        return ABC_ALLOC( char, nBytes );
         if ( p->nLargeChunks == p->nLargeChunksAlloc )
         {
             if ( p->nLargeChunksAlloc == 0 )
                 p->nLargeChunksAlloc = 32;
             p->nLargeChunksAlloc *= 2;
-            p->pLargeChunks = REALLOC( void *, p->pLargeChunks, p->nLargeChunksAlloc );
+            p->pLargeChunks = ABC_REALLOC( void *, p->pLargeChunks, p->nLargeChunksAlloc );
         }
-        p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes );
+        p->pLargeChunks[ p->nLargeChunks++ ] = ABC_ALLOC( char, nBytes );
         return p->pLargeChunks[ p->nLargeChunks - 1 ];
     }
     return Extra_MmFixedEntryFetch( p->pMap[nBytes] );
@@ -588,7 +588,7 @@ void Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes )
         return;
     if ( nBytes > p->nMapSize )
     {
-//        free( pEntry );
+//        ABC_FREE( pEntry );
         return;
     }
     Extra_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 48fca0ba..293b23e7 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -265,8 +265,8 @@ int Extra_Factorial( int n )
 
   Description [The number of permutations in the array is n!. The number of
   entries in each permutation is n. Therefore, the resulting array is a 
-  two-dimentional array of the size: n! x n. To free the resulting array,
-  call free() on the pointer returned by this procedure.]
+  two-dimentional array of the size: n! x n. To ABC_FREE the resulting array,
+  call ABC_FREE() on the pointer returned by this procedure.]
 
   SideEffects []
 
@@ -397,8 +397,8 @@ unsigned Extra_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReve
 
     assert( nVars < 6 );
     nMints  = (1 << nVars);
-    pMints  = ALLOC( int, nMints );
-    pMintsP = ALLOC( int, nMints );
+    pMints  = ABC_ALLOC( int, nMints );
+    pMintsP = ABC_ALLOC( int, nMints );
     for ( i = 0; i < nMints; i++ )
         pMints[i] = i;
 
@@ -418,8 +418,8 @@ unsigned Extra_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReve
                 Result |= (1 << pMintsP[m]);
     }
 
-    free( pMints );
-    free( pMintsP );
+    ABC_FREE( pMints );
+    ABC_FREE( pMintsP );
 
     return Result;
 }
@@ -546,7 +546,7 @@ unsigned Extra_TruthCanonP( unsigned uTruth, int nVars )
     }
     else if ( nVarsOld != nVars )
     {
-        free( pPerms );
+        ABC_FREE( pPerms );
         nPerms = Extra_Factorial( nVars );   
         pPerms = Extra_Permutations( nVars );
         nVarsOld = nVars;
@@ -589,7 +589,7 @@ unsigned Extra_TruthCanonNP( unsigned uTruth, int nVars )
     }
     else if ( nVarsOld != nVars )
     {
-        free( pPerms );
+        ABC_FREE( pPerms );
         nPerms = Extra_Factorial( nVars );   
         pPerms = Extra_Permutations( nVars );
         nVarsOld = nVars;
@@ -637,7 +637,7 @@ unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
     }
     else if ( nVarsOld != nVars )
     {
-        free( pPerms );
+        ABC_FREE( pPerms );
         nPerms = Extra_Factorial( nVars );   
         pPerms = Extra_Permutations( nVars );
         nVarsOld = nVars;
@@ -687,10 +687,10 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
     int i, k;
 
     nFuncs  = (1 << 16);
-    uCanons = ALLOC( unsigned short, nFuncs );
-    uPhases = ALLOC( char, nFuncs );
-    uPerms  = ALLOC( char, nFuncs );
-    uMap    = ALLOC( unsigned char, nFuncs );
+    uCanons = ABC_ALLOC( unsigned short, nFuncs );
+    uPhases = ABC_ALLOC( char, nFuncs );
+    uPerms  = ABC_ALLOC( char, nFuncs );
+    uMap    = ABC_ALLOC( unsigned char, nFuncs );
     memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
     memset( uPhases, 0, sizeof(char) * nFuncs );
     memset( uPerms,  0, sizeof(char) * nFuncs );
@@ -751,23 +751,23 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
     }
     uPhases[(1<<16)-1] = 16;
     assert( nClasses == 222 );
-    free( pPerms4 );
+    ABC_FREE( pPerms4 );
     if ( puCanons ) 
         *puCanons = uCanons;
     else
-        free( uCanons );
+        ABC_FREE( uCanons );
     if ( puPhases ) 
         *puPhases = uPhases;
     else
-        free( uPhases );
+        ABC_FREE( uPhases );
     if ( puPerms ) 
         *puPerms = uPerms;
     else
-        free( uPerms );
+        ABC_FREE( uPerms );
     if ( puMap ) 
         *puMap = uMap;
     else
-        free( uMap );
+        ABC_FREE( uMap );
 }
 
 /**Function*************************************************************
@@ -790,9 +790,9 @@ void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounte
     int nFuncs, nClasses, i;
 
     nFuncs  = (1 << 8);
-    uCanons = ALLOC( unsigned, nFuncs );
+    uCanons = ABC_ALLOC( unsigned, nFuncs );
     memset( uCanons, 0, sizeof(unsigned) * nFuncs );
-    pCounters = ALLOC( char, nFuncs );
+    pCounters = ABC_ALLOC( char, nFuncs );
     memset( pCounters, 0, sizeof(char) * nFuncs );
     uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) );
     nClasses = 0;
@@ -826,15 +826,15 @@ void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounte
     if ( puCanons ) 
         *puCanons = uCanons;
     else
-        free( uCanons );
+        ABC_FREE( uCanons );
     if ( puPhases ) 
         *puPhases = uPhases;
     else
-        free( uPhases );
+        ABC_FREE( uPhases );
     if ( ppCounters ) 
         *ppCounters = pCounters;
     else
-        free( pCounters );
+        ABC_FREE( pCounters );
 //    printf( "The number of 3N-classes = %d.\n", nClasses );
 }
 
@@ -857,9 +857,9 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
     int nFuncs, nClasses, i;
 
     nFuncs  = (1 << 16);
-    uCanons = ALLOC( unsigned short, nFuncs );
+    uCanons = ABC_ALLOC( unsigned short, nFuncs );
     memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
-    pCounters = ALLOC( char, nFuncs );
+    pCounters = ABC_ALLOC( char, nFuncs );
     memset( pCounters, 0, sizeof(char) * nFuncs );
     uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) );
     nClasses = 0;
@@ -892,15 +892,15 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
     if ( puCanons ) 
         *puCanons = uCanons;
     else
-        free( uCanons );
+        ABC_FREE( uCanons );
     if ( puPhases ) 
         *puPhases = uPhases;
     else
-        free( uPhases );
+        ABC_FREE( uPhases );
     if ( ppCounters ) 
         *ppCounters = pCounters;
     else
-        free( pCounters );
+        ABC_FREE( pCounters );
 //    printf( "The number of 4N-classes = %d.\n", nClasses );
 }
 
@@ -921,7 +921,7 @@ void ** Extra_ArrayAlloc( int nCols, int nRows, int Size )
     char * pBuffer;
     int i;
     assert( nCols > 0 && nRows > 0 && Size > 0 );
-    pBuffer = ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
+    pBuffer = ABC_ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
     pRes = (void **)pBuffer;
     pRes[0] = pBuffer + nCols * sizeof(void *);
     for ( i = 1; i < nCols; i++ )
diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c
index 6b6d5132..5e3b0f06 100644
--- a/src/misc/extra/extraUtilProgress.c
+++ b/src/misc/extra/extraUtilProgress.c
@@ -62,7 +62,7 @@ ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal )
     extern void * Abc_FrameGetGlobalFrame();
 
     if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
-    p = ALLOC( ProgressBar, 1 );
+    p = ABC_ALLOC( ProgressBar, 1 );
     memset( p, 0, sizeof(ProgressBar) );
     p->pFile       = pFile;
     p->nItemsTotal = nItemsTotal;
@@ -118,7 +118,7 @@ void Extra_ProgressBarStop( ProgressBar * p )
 {
     if ( p == NULL ) return;
     Extra_ProgressBarClean( p );
-    FREE( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c
index b6a53fbc..46179e50 100644
--- a/src/misc/extra/extraUtilReader.c
+++ b/src/misc/extra/extraUtilReader.c
@@ -96,7 +96,7 @@ Extra_FileReader_t * Extra_FileReaderAlloc( char * pFileName,
         return NULL;
     }
     // start the file reader    
-    p = ALLOC( Extra_FileReader_t, 1 );
+    p = ABC_ALLOC( Extra_FileReader_t, 1 );
     memset( p, 0, sizeof(Extra_FileReader_t) );
     p->pFileName   = pFileName;
     p->pFile       = pFile;
@@ -113,7 +113,7 @@ Extra_FileReader_t * Extra_FileReaderAlloc( char * pFileName,
     p->nFileSize = ftell( pFile );  
     rewind( pFile ); 
     // allocate the buffer
-    p->pBuffer = ALLOC( char, EXTRA_BUFFER_SIZE+1 );
+    p->pBuffer = ABC_ALLOC( char, EXTRA_BUFFER_SIZE+1 );
     p->nBufferSize = EXTRA_BUFFER_SIZE;
     p->pBufferCur  = p->pBuffer;
     // determine how many chars to read
@@ -146,10 +146,10 @@ void Extra_FileReaderFree( Extra_FileReader_t * p )
 {
     if ( p->pFile )
         fclose( p->pFile );
-    FREE( p->pBuffer );
+    ABC_FREE( p->pBuffer );
     Vec_PtrFree( p->vTokens );
     Vec_IntFree( p->vLines );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index 7165a0cd..3f0dd365 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -169,7 +169,7 @@ char * Extra_UtilStrsav( char *s )
        return s;
     }
     else {
-       return strcpy(ALLOC(char, strlen(s)+1), s);
+       return strcpy(ABC_ALLOC(char, strlen(s)+1), s);
     }
 }
 
@@ -199,7 +199,7 @@ char * Extra_UtilTildeExpand( char *fname )
 
     home     = getenv("HOME");
     length   = n_tildes * strlen(home) + strlen(fname);
-    expanded = ALLOC(char, length + 1);
+    expanded = ABC_ALLOC(char, length + 1);
 
     j = 0;
     for (i = 0; i < (int)strlen(fname); i++){
@@ -279,22 +279,22 @@ char * Extra_UtilFileSearch(char *file, char *path, char *mode)
     if (strcmp(path, ".") == 0) {
         buffer = Extra_UtilStrsav(file);
     } else {
-        buffer = ALLOC(char, strlen(path) + strlen(file) + 4);
+        buffer = ABC_ALLOC(char, strlen(path) + strlen(file) + 4);
         (void) sprintf(buffer, "%s/%s", path, file);
     }
     filename = Extra_UtilTildeExpand(buffer);
-    FREE(buffer);
+    ABC_FREE(buffer);
 
     /* see if we can access it */
     if (Extra_UtilCheckFile(filename, mode)) {
-        FREE(save_path);
+        ABC_FREE(save_path);
         return filename;
     }
-    FREE(filename);
+    ABC_FREE(filename);
     path = ++cp;
     } while (! quit); 
 
-    FREE(save_path);
+    ABC_FREE(save_path);
     return 0;
 }
 
@@ -390,7 +390,7 @@ double Extra_CpuTimeDouble()
 ***********************************************************************/
 void Extra_MemTest()
 {
-    malloc( 1002 );
+    ABC_ALLOC( char, 1002 );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/hash/hash.h b/src/misc/hash/hash.h
index 90e72868..dad4db18 100644
--- a/src/misc/hash/hash.h
+++ b/src/misc/hash/hash.h
@@ -21,13 +21,14 @@
 #ifndef __HASH_H__
 #define __HASH_H__
 
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef _WIN32
-#define inline __inline // compatible with MS VS 6.0
-#endif
+#include "abc_global.h"
 
 #include "hashInt.h"
 #include "hashFlt.h"
@@ -45,16 +46,12 @@
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifndef ABS
-#define ABS(a)            ((a) < 0 ? -(a) : (a))
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 int Hash_DefaultHashFunc(int key, int nBins) {
-  return ABS( ( (key+11)*(key)*7+3 ) % nBins );
+  return ABC_ABS( ( (key+11)*(key)*7+3 ) % nBins );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/hash/hashFlt.h b/src/misc/hash/hashFlt.h
index da20ee28..43b9dd7f 100644
--- a/src/misc/hash/hashFlt.h
+++ b/src/misc/hash/hashFlt.h
@@ -86,11 +86,11 @@ static inline Hash_Flt_t * Hash_FltAlloc( int nBins )
   Hash_Flt_t * p;
   int i;
   assert(nBins > 0);
-  p = ALLOC( Hash_Flt_t, 1);
+  p = ABC_ALLOC( Hash_Flt_t, 1);
   p->nBins = nBins;
   p->fHash = Hash_DefaultHashFunc;
   p->nSize  = 0;
-  p->pArray = ALLOC( Hash_Flt_Entry_t *, nBins );
+  p->pArray = ABC_ALLOC( Hash_Flt_Entry_t *, nBins );
   for(i=0; i<nBins; i++)
     p->pArray[i] = NULL;
 
@@ -164,7 +164,7 @@ static inline void Hash_FltWriteEntry( Hash_Flt_t *p, int key, float data )
   // this key does not currently exist
   // create a new entry and add to bin
   p->nSize++;
-  (*pLast) = pEntry = ALLOC( Hash_Flt_Entry_t, 1 );
+  (*pLast) = pEntry = ABC_ALLOC( Hash_Flt_Entry_t, 1 );
   pEntry->pNext = NULL;
   pEntry->key = key;
   pEntry->data = data;
@@ -206,7 +206,7 @@ static inline float Hash_FltEntry( Hash_Flt_t *p, int key, int fCreate )
   if (fCreate) {
     // create a new entry and add to bin
     p->nSize++;
-    (*pLast) = pEntry = ALLOC( Hash_Flt_Entry_t, 1 );
+    (*pLast) = pEntry = ABC_ALLOC( Hash_Flt_Entry_t, 1 );
     pEntry->pNext = NULL;
     pEntry->key = key;
     pEntry->data = 0.0;
@@ -249,7 +249,7 @@ static inline float* Hash_FltEntryPtr( Hash_Flt_t *p, int key )
   // this key does not currently exist
   // create a new entry and add to bin
   p->nSize++;
-  (*pLast) = pEntry = ALLOC( Hash_Flt_Entry_t, 1 );
+  (*pLast) = pEntry = ABC_ALLOC( Hash_Flt_Entry_t, 1 );
   pEntry->pNext = NULL;
   pEntry->key = key;
   pEntry->data = 0.0;
@@ -283,7 +283,7 @@ static inline void Hash_FltRemove( Hash_Flt_t *p, int key )
     if (pEntry->key == key) {
       p->nSize--;
       *pLast = pEntry->pNext;
-      FREE( pEntry );
+      ABC_FREE( pEntry );
       return;
     }
     pLast = &(pEntry->pNext);
@@ -309,18 +309,18 @@ static inline void Hash_FltFree( Hash_Flt_t *p ) {
   int bin;
   Hash_Flt_Entry_t *pEntry;
 
-  // free bins
+  // ABC_FREE bins
   for(bin = 0; bin < p->nBins; bin++) {
     pEntry = p->pArray[bin];
     while(pEntry) {
       pEntry = pEntry->pNext;
-      FREE( pEntry );
+      ABC_FREE( pEntry );
     }
   }
  
-  // free hash
-  FREE( p->pArray );
-  FREE( p );
+  // ABC_FREE hash
+  ABC_FREE( p->pArray );
+  ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/hash/hashInt.h b/src/misc/hash/hashInt.h
index b7ec8a8c..7993e562 100644
--- a/src/misc/hash/hashInt.h
+++ b/src/misc/hash/hashInt.h
@@ -86,11 +86,11 @@ static inline Hash_Int_t * Hash_IntAlloc( int nBins )
   Hash_Int_t * p;
   int i;
   assert(nBins > 0);
-  p = ALLOC( Hash_Int_t, 1);
+  p = ABC_ALLOC( Hash_Int_t, 1);
   p->nBins = nBins;
   p->fHash = Hash_DefaultHashFunc;
   p->nSize  = 0;
-  p->pArray = ALLOC( Hash_Int_Entry_t *, nBins+1 );
+  p->pArray = ABC_ALLOC( Hash_Int_Entry_t *, nBins+1 );
   for(i=0; i<nBins; i++)
     p->pArray[i] = NULL;
 
@@ -164,7 +164,7 @@ static inline void Hash_IntWriteEntry( Hash_Int_t *p, int key, int data )
   // this key does not currently exist
   // create a new entry and add to bin
   p->nSize++;
-  (*pLast) = pEntry = ALLOC( Hash_Int_Entry_t, 1 );
+  (*pLast) = pEntry = ABC_ALLOC( Hash_Int_Entry_t, 1 );
   pEntry->pNext = NULL;
   pEntry->key = key;
   pEntry->data = data;
@@ -206,7 +206,7 @@ static inline int Hash_IntEntry( Hash_Int_t *p, int key, int fCreate )
   if (fCreate) {
     // create a new entry and add to bin
     p->nSize++;
-    (*pLast) = pEntry = ALLOC( Hash_Int_Entry_t, 1 );
+    (*pLast) = pEntry = ABC_ALLOC( Hash_Int_Entry_t, 1 );
     pEntry->pNext = NULL;
     pEntry->key = key;
     pEntry->data = 0;
@@ -249,7 +249,7 @@ static inline int* Hash_IntEntryPtr( Hash_Int_t *p, int key )
   // this key does not currently exist
   // create a new entry and add to bin
   p->nSize++;
-  (*pLast) = pEntry = ALLOC( Hash_Int_Entry_t, 1 );
+  (*pLast) = pEntry = ABC_ALLOC( Hash_Int_Entry_t, 1 );
   pEntry->pNext = NULL;
   pEntry->key = key;
   pEntry->data = 0;
@@ -272,19 +272,19 @@ static inline void Hash_IntFree( Hash_Int_t *p ) {
   int bin;
   Hash_Int_Entry_t *pEntry, *pTemp;
 
-  // free bins
+  // ABC_FREE bins
   for(bin = 0; bin < p->nBins; bin++) {
     pEntry = p->pArray[bin];
     while(pEntry) {
       pTemp = pEntry;
       pEntry = pEntry->pNext;
-      FREE( pTemp );
+      ABC_FREE( pTemp );
     }
   }
 
-  // free hash
-  FREE( p->pArray );
-  FREE( p );
+  // ABC_FREE hash
+  ABC_FREE( p->pArray );
+  ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/hash/hashPtr.h b/src/misc/hash/hashPtr.h
index 15398a8a..224e5c84 100644
--- a/src/misc/hash/hashPtr.h
+++ b/src/misc/hash/hashPtr.h
@@ -86,11 +86,11 @@ static inline Hash_Ptr_t * Hash_PtrAlloc( int nBins )
   Hash_Ptr_t * p;
   int i;
   assert(nBins > 0);
-  p = ALLOC( Hash_Ptr_t, 1);
+  p = ABC_ALLOC( Hash_Ptr_t, 1);
   p->nBins = nBins;
   p->fHash = Hash_DefaultHashFunc;
   p->nSize  = 0;
-  p->pArray = ALLOC( Hash_Ptr_Entry_t *, nBins );
+  p->pArray = ABC_ALLOC( Hash_Ptr_Entry_t *, nBins );
   for(i=0; i<nBins; i++)
     p->pArray[i] = NULL;
 
@@ -164,7 +164,7 @@ static inline void Hash_PtrWriteEntry( Hash_Ptr_t *p, int key, void * data )
   // this key does not currently exist
   // create a new entry and add to bin
   p->nSize++;
-  (*pLast) = pEntry = ALLOC( Hash_Ptr_Entry_t, 1 );
+  (*pLast) = pEntry = ABC_ALLOC( Hash_Ptr_Entry_t, 1 );
   pEntry->pNext = NULL;
   pEntry->key = key;
   pEntry->data = data;
@@ -206,7 +206,7 @@ static inline void * Hash_PtrEntry( Hash_Ptr_t *p, int key, int fCreate )
   if (fCreate) {
     // create a new entry and add to bin
     p->nSize++;
-    (*pLast) = pEntry = ALLOC( Hash_Ptr_Entry_t, 1 );
+    (*pLast) = pEntry = ABC_ALLOC( Hash_Ptr_Entry_t, 1 );
     pEntry->pNext = NULL;
     pEntry->key = key;
     pEntry->data = NULL;
@@ -249,7 +249,7 @@ static inline void** Hash_PtrEntryPtr( Hash_Ptr_t *p, int key )
   // this key does not currently exist
   // create a new entry and add to bin
   p->nSize++;
-  (*pLast) = pEntry = ALLOC( Hash_Ptr_Entry_t, 1 );
+  (*pLast) = pEntry = ABC_ALLOC( Hash_Ptr_Entry_t, 1 );
   pEntry->pNext = NULL;
   pEntry->key = key;
   pEntry->data = NULL;
@@ -310,18 +310,18 @@ static inline void Hash_PtrFree( Hash_Ptr_t *p ) {
   int bin;
   Hash_Ptr_Entry_t *pEntry;
 
-  // free bins
+  // ABC_FREE bins
   for(bin = 0; bin < p->nBins; bin++) {
     pEntry = p->pArray[bin];
     while(pEntry) {
       pEntry = pEntry->pNext;
-      FREE( pEntry );
+      ABC_FREE( pEntry );
     }
   }
  
-  // free hash
-  FREE( p->pArray );
-  FREE( p );
+  // ABC_FREE hash
+  ABC_FREE( p->pArray );
+  ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/mvc/mvc.h b/src/misc/mvc/mvc.h
index 70834e0a..4cc765b2 100644
--- a/src/misc/mvc/mvc.h
+++ b/src/misc/mvc/mvc.h
@@ -561,8 +561,8 @@ struct MvcManagerStruct
 // macros which work with memory
 // MEM_ALLOC: allocate the given number (Size) of items of type (Type)
 // MEM_FREE:  deallocate the pointer (Pointer) to the given number (Size) of items of type (Type)
-#define MEM_ALLOC( Manager, Type, Size )          ((Type *)malloc( (Size) * sizeof(Type) ))
-#define MEM_FREE( Manager, Type, Size, Pointer )  if ( Pointer ) { free(Pointer); Pointer = NULL; }
+#define MEM_ALLOC( Manager, Type, Size )          ((Type *)ABC_ALLOC( char, (Size) * sizeof(Type) ))
+#define MEM_FREE( Manager, Type, Size, Pointer )  if ( Pointer ) { ABC_FREE(Pointer); Pointer = NULL; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/misc/mvc/mvcContain.c b/src/misc/mvc/mvcContain.c
index a9eae06e..950a80a2 100644
--- a/src/misc/mvc/mvcContain.c
+++ b/src/misc/mvc/mvcContain.c
@@ -4,7 +4,7 @@
 
   PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
 
-  Synopsis    [Making the cover single-cube containment free.]
+  Synopsis    [Making the cover single-cube containment ABC_FREE.]
 
   Author      [MVSIS Group]
   
diff --git a/src/misc/mvc/mvcCover.c b/src/misc/mvc/mvcCover.c
index d8584446..bad76170 100644
--- a/src/misc/mvc/mvcCover.c
+++ b/src/misc/mvc/mvcCover.c
@@ -44,7 +44,7 @@ Mvc_Cover_t * Mvc_CoverAlloc( Mvc_Manager_t * pMem, int nBits )
 
     nBitsInUnsigned  = 8 * sizeof(Mvc_CubeWord_t);
 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    p                = (Mvc_Cover_t *)malloc( sizeof(Mvc_Cover_t) );
+    p                = (Mvc_Cover_t *)ABC_ALLOC( char, sizeof(Mvc_Cover_t) );
 #else
     p                = (Mvc_Cover_t *)Extra_MmFixedEntryFetch( pMem->pManC );
 #endif
@@ -77,7 +77,7 @@ Mvc_Cover_t * Mvc_CoverClone( Mvc_Cover_t * p )
 {
     Mvc_Cover_t * pCover;
 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    pCover                = (Mvc_Cover_t *)malloc( sizeof(Mvc_Cover_t) );
+    pCover                = (Mvc_Cover_t *)ABC_ALLOC( char, sizeof(Mvc_Cover_t) );
 #else
     pCover                = (Mvc_Cover_t *)Extra_MmFixedEntryFetch( p->pMem->pManC );
 #endif
@@ -144,7 +144,7 @@ void Mvc_CoverFree( Mvc_Cover_t * p )
     MEM_FREE( p->pMem, int,          p->nBits,       p->pLits  );
 
 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    free( p );
+    ABC_FREE( p );
 #else
     Extra_MmFixedEntryRecycle( p->pMem->pManC, (char *)p );
 #endif
diff --git a/src/misc/mvc/mvcCube.c b/src/misc/mvc/mvcCube.c
index e157879f..9ccdb427 100644
--- a/src/misc/mvc/mvcCube.c
+++ b/src/misc/mvc/mvcCube.c
@@ -45,9 +45,9 @@ Mvc_Cube_t * Mvc_CubeAlloc( Mvc_Cover_t * pCover )
     // allocate the cube
 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
     if ( pCover->nWords == 0 )
-        pCube = (Mvc_Cube_t *)malloc( sizeof(Mvc_Cube_t) );
+        pCube = (Mvc_Cube_t *)ABC_ALLOC( char, sizeof(Mvc_Cube_t) );
     else
-        pCube = (Mvc_Cube_t *)malloc( sizeof(Mvc_Cube_t) + sizeof(Mvc_CubeWord_t) * (pCover->nWords - 1) );
+        pCube = (Mvc_Cube_t *)ABC_ALLOC( char,  sizeof(Mvc_Cube_t) + sizeof(Mvc_CubeWord_t) * (pCover->nWords - 1) );
 #else
     switch( pCover->nWords )
     {
@@ -63,7 +63,7 @@ Mvc_Cube_t * Mvc_CubeAlloc( Mvc_Cover_t * pCover )
         pCube = (Mvc_Cube_t *)Extra_MmFixedEntryFetch( pCover->pMem->pMan4 );
         break;
     default:
-        pCube = (Mvc_Cube_t *)malloc( sizeof(Mvc_Cube_t) + sizeof(Mvc_CubeWord_t) * (pCover->nWords - 1) );
+        pCube = (Mvc_Cube_t *)ABC_ALLOC( char, sizeof(Mvc_Cube_t) + sizeof(Mvc_CubeWord_t) * (pCover->nWords - 1) );
         break;
     }
 #endif
@@ -119,7 +119,7 @@ void Mvc_CubeFree( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
 
     // deallocate the cube
 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-    free( pCube );
+    ABC_FREE( pCube );
 #else
     switch( pCover->nWords )
     {
@@ -135,7 +135,7 @@ void Mvc_CubeFree( Mvc_Cover_t * pCover, Mvc_Cube_t * pCube )
         Extra_MmFixedEntryRecycle( pCover->pMem->pMan4, (char *)pCube );
         break;
     default:
-        free( pCube );
+        ABC_FREE( pCube );
         break;
     }
 #endif
diff --git a/src/misc/mvc/mvcDivisor.c b/src/misc/mvc/mvcDivisor.c
index ecdea75b..1ce556a5 100644
--- a/src/misc/mvc/mvcDivisor.c
+++ b/src/misc/mvc/mvcDivisor.c
@@ -76,7 +76,7 @@ void Mvc_CoverDivisorZeroKernel( Mvc_Cover_t * pCover )
 //    iLit = Mvc_CoverBestLiteral( pCover, NULL );
     if ( iLit == -1 )
         return;
-    // derive the cube-free quotient
+    // derive the cube-ABC_FREE quotient
     Mvc_CoverDivideByLiteralQuo( pCover, iLit ); // the same cover
     Mvc_CoverMakeCubeFree( pCover );             // the same cover
     // call recursively
diff --git a/src/misc/mvc/mvcMan.c b/src/misc/mvc/mvcMan.c
index 7b4ef2af..168410a4 100644
--- a/src/misc/mvc/mvcMan.c
+++ b/src/misc/mvc/mvcMan.c
@@ -41,7 +41,7 @@
 Mvc_Manager_t * Mvc_ManagerStart()
 {
     Mvc_Manager_t * p;
-    p = ALLOC( Mvc_Manager_t, 1 );
+    p = ABC_ALLOC( Mvc_Manager_t, 1 );
     memset( p, 0, sizeof(Mvc_Manager_t) );
     p->pMan1 = Extra_MmFixedStart( sizeof(Mvc_Cube_t)                              );
     p->pMan2 = Extra_MmFixedStart( sizeof(Mvc_Cube_t) +     sizeof(Mvc_CubeWord_t) );
@@ -67,7 +67,7 @@ void Mvc_ManagerFree( Mvc_Manager_t * p )
     Extra_MmFixedStop( p->pMan2 );
     Extra_MmFixedStop( p->pMan4 );
     Extra_MmFixedStop( p->pManC );
-    free( p );
+    ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/mvc/mvcUtils.c b/src/misc/mvc/mvcUtils.c
index 4b13b23d..bb4b1191 100644
--- a/src/misc/mvc/mvcUtils.c
+++ b/src/misc/mvc/mvcUtils.c
@@ -329,7 +329,7 @@ int Mvc_CoverGetCubeSize( Mvc_Cube_t * pCube )
   entries as there are different pairs of cubes in the cover: n(n-1)/2.
   Fills out the array pDiffs with the following info: For each cube
   pair, included in the array is the number of literals in both cubes
-  after they are made cube free.]
+  after they are made cube ABC_FREE.]
                
   SideEffects []
 
@@ -671,7 +671,7 @@ Mvc_Cover_t ** Mvc_CoverCofactors( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int
     // start the covers for cofactors
     iValueFirst = Vm_VarMapReadValuesFirst(pData->pVm, iVar);
     nValues = Vm_VarMapReadValues(pData->pVm, iVar);
-    ppCofs = ALLOC( Mvc_Cover_t *, nValues + 1 );
+    ppCofs = ABC_ALLOC( Mvc_Cover_t *, nValues + 1 );
     for ( i = 0; i <= nValues; i++ )
         ppCofs[i] = Mvc_CoverClone( pCover );
 
diff --git a/src/misc/nm/nm.h b/src/misc/nm/nm.h
index c6344bbf..6f46c291 100644
--- a/src/misc/nm/nm.h
+++ b/src/misc/nm/nm.h
@@ -21,10 +21,6 @@
 #ifndef __NM_H__
 #define __NM_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 /*
     This manager is designed to store ID-to-name and name-to-ID mapping
     for Boolean networks and And-Inverter Graphs.
@@ -54,6 +50,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/nm/nmApi.c b/src/misc/nm/nmApi.c
index 576882a7..7f7cbb97 100644
--- a/src/misc/nm/nmApi.c
+++ b/src/misc/nm/nmApi.c
@@ -43,15 +43,15 @@ Nm_Man_t * Nm_ManCreate( int nSize )
 {
     Nm_Man_t * p;
     // allocate the table
-    p = ALLOC( Nm_Man_t, 1 );
+    p = ABC_ALLOC( Nm_Man_t, 1 );
     memset( p, 0, sizeof(Nm_Man_t) );
     // set the parameters
     p->nSizeFactor   = 2; // determined the limit on the grow of data before the table resizes
     p->nGrowthFactor = 3; // determined how much the table grows after resizing
     // allocate and clean the bins
     p->nBins = Cudd_PrimeNm(nSize);
-    p->pBinsI2N = ALLOC( Nm_Entry_t *, p->nBins );
-    p->pBinsN2I = ALLOC( Nm_Entry_t *, p->nBins );
+    p->pBinsI2N = ABC_ALLOC( Nm_Entry_t *, p->nBins );
+    p->pBinsN2I = ABC_ALLOC( Nm_Entry_t *, p->nBins );
     memset( p->pBinsI2N, 0, sizeof(Nm_Entry_t *) * p->nBins );
     memset( p->pBinsN2I, 0, sizeof(Nm_Entry_t *) * p->nBins );
     // start the memory manager
@@ -73,9 +73,9 @@ Nm_Man_t * Nm_ManCreate( int nSize )
 void Nm_ManFree( Nm_Man_t * p )
 {
     Extra_MmFlexStop( p->pMem );
-    FREE( p->pBinsI2N );
-    FREE( p->pBinsN2I );
-    FREE( p );
+    ABC_FREE( p->pBinsI2N );
+    ABC_FREE( p->pBinsN2I );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/nm/nmInt.h b/src/misc/nm/nmInt.h
index 028316e1..03948f22 100644
--- a/src/misc/nm/nmInt.h
+++ b/src/misc/nm/nmInt.h
@@ -21,10 +21,6 @@
 #ifndef __NM_INT_H__
 #define __NM_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -37,6 +33,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/nm/nmTable.c b/src/misc/nm/nmTable.c
index e50388ba..a147b16c 100644
--- a/src/misc/nm/nmTable.c
+++ b/src/misc/nm/nmTable.c
@@ -259,8 +259,8 @@ clk = clock();
     // get the new table size
     nBinsNew = Cudd_PrimeCopy( p->nGrowthFactor * p->nBins ); 
     // allocate a new array
-    pBinsNewI2N = ALLOC( Nm_Entry_t *, nBinsNew );
-    pBinsNewN2I = ALLOC( Nm_Entry_t *, nBinsNew );
+    pBinsNewI2N = ABC_ALLOC( Nm_Entry_t *, nBinsNew );
+    pBinsNewN2I = ABC_ALLOC( Nm_Entry_t *, nBinsNew );
     memset( pBinsNewI2N, 0, sizeof(Nm_Entry_t *) * nBinsNew );
     memset( pBinsNewN2I, 0, sizeof(Nm_Entry_t *) * nBinsNew );
     // rehash entries in Id->Name table
@@ -285,10 +285,10 @@ 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->pBinsI2N );
-    free( p->pBinsN2I );
+    ABC_FREE( p->pBinsI2N );
+    ABC_FREE( p->pBinsN2I );
     p->pBinsI2N = pBinsNewI2N;
     p->pBinsN2I = pBinsNewN2I;
     p->nBins = nBinsNew;
diff --git a/src/misc/st/st.c b/src/misc/st/st.c
index 2798ae99..13445e9e 100644
--- a/src/misc/st/st.c
+++ b/src/misc/st/st.c
@@ -9,31 +9,13 @@
  */
 #include <stdio.h>
 #include <stdlib.h>
+#include "abc_global.h"
 #include "st.h"
-#include "port_type.h"
-
-#ifndef ABS
-#  define ABS(a)            ((a) < 0 ? -(a) : (a))
-#endif
-
-#ifndef ALLOC
-#define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
-#endif
-
-#ifndef FREE
-#define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
-#endif
-
-#ifndef REALLOC
-#define REALLOC(type, obj, num)    \
-        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-         ((type *) malloc(sizeof(type) * (num))))
-#endif
 
 #define ST_NUMCMP(x,y) ((x) != (y))
-#define ST_NUMHASH(x,size) (ABS((long)x)%(size))
-//#define ST_PTRHASH(x,size) ((int)((PORT_PTRUINT_T)(x)>>2)%size)  // 64-bit bug fix 9/17/2007
-#define ST_PTRHASH(x,size) ((int)(((PORT_PTRUINT_T)(x)>>2)%size))
+#define ST_NUMHASH(x,size) (ABC_ABS((long)x)%(size))
+//#define ST_PTRHASH(x,size) ((int)((ABC_PTRUINT_T)(x)>>2)%size)  // 64-bit bug fix 9/17/2007
+#define ST_PTRHASH(x,size) ((int)(((ABC_PTRUINT_T)(x)>>2)%size))
 #define EQUAL(func, x, y) \
     ((((func) == st_numcmp) || ((func) == st_ptrcmp)) ?\
       (ST_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))
@@ -60,7 +42,7 @@ int reorder_flag;
     int i;
     st_table *new;
 
-    new = ALLOC(st_table, 1);
+    new = ABC_ALLOC(st_table, 1);
     if (new == NULL) {
     return NULL;
     }
@@ -74,9 +56,9 @@ int reorder_flag;
     size = 1;
     }
     new->num_bins = size;
-    new->bins = ALLOC(st_table_entry *, size);
+    new->bins = ABC_ALLOC(st_table_entry *, size);
     if (new->bins == NULL) {
-    FREE(new);
+    ABC_FREE(new);
     return NULL;
     }
     for(i = 0; i < size; i++) {
@@ -107,12 +89,12 @@ st_table *table;
     ptr = table->bins[i];
     while (ptr != NULL) {
         next = ptr->next;
-        FREE(ptr);
+        ABC_FREE(ptr);
         ptr = next;
     }
     }
-    FREE(table->bins);
-    FREE(table);
+    ABC_FREE(table->bins);
+    ABC_FREE(table);
 }
 
 #define PTR_NOT_EQUAL(table, ptr, user_key)\
@@ -184,7 +166,7 @@ int *value;
     hash_val = do_hash(key,table);\
     }\
     \
-    new = ALLOC(st_table_entry, 1);\
+    new = ABC_ALLOC(st_table_entry, 1);\
     \
     new->key = key;\
     new->record = value;\
@@ -214,7 +196,7 @@ char *value;
         }
         hash_val = do_hash(key, table);
     }
-    new = ALLOC(st_table_entry, 1);
+    new = ABC_ALLOC(st_table_entry, 1);
     if (new == NULL) {
         return ST_OUT_OF_MEM;
     }
@@ -246,7 +228,7 @@ char *value;
     }
     }
     hash_val = do_hash(key, table);
-    new = ALLOC(st_table_entry, 1);
+    new = ABC_ALLOC(st_table_entry, 1);
     if (new == NULL) {
     return ST_OUT_OF_MEM;
     }
@@ -278,7 +260,7 @@ char ***slot;
         }
         hash_val = do_hash(key, table);
     }
-    new = ALLOC(st_table_entry, 1);
+    new = ABC_ALLOC(st_table_entry, 1);
     if (new == NULL) {
         return ST_OUT_OF_MEM;
     }
@@ -336,7 +318,7 @@ register st_table *table;
     table->num_bins += 1;
     }
     table->num_entries = 0;
-    table->bins = ALLOC(st_table_entry *, table->num_bins);
+    table->bins = ABC_ALLOC(st_table_entry *, table->num_bins);
     if (table->bins == NULL) {
     table->bins = old_bins;
     table->num_bins = old_num_bins;
@@ -360,7 +342,7 @@ register st_table *table;
         ptr = next;
     }
     }
-    FREE(old_bins);
+    ABC_FREE(old_bins);
 
     return 1;
 }
@@ -373,33 +355,33 @@ st_table *old_table;
     st_table_entry *ptr, *newptr, *next, *new;
     int i, j, num_bins = old_table->num_bins;
 
-    new_table = ALLOC(st_table, 1);
+    new_table = ABC_ALLOC(st_table, 1);
     if (new_table == NULL) {
     return NULL;
     }
     
     *new_table = *old_table;
-    new_table->bins = ALLOC(st_table_entry *, num_bins);
+    new_table->bins = ABC_ALLOC(st_table_entry *, num_bins);
     if (new_table->bins == NULL) {
-    FREE(new_table);
+    ABC_FREE(new_table);
     return NULL;
     }
     for(i = 0; i < num_bins ; i++) {
     new_table->bins[i] = NULL;
     ptr = old_table->bins[i];
     while (ptr != NULL) {
-        new = ALLOC(st_table_entry, 1);
+        new = ABC_ALLOC(st_table_entry, 1);
         if (new == NULL) {
         for (j = 0; j <= i; j++) {
             newptr = new_table->bins[j];
             while (newptr != NULL) {
             next = newptr->next;
-            FREE(newptr);
+            ABC_FREE(newptr);
             newptr = next;
             }
         }
-        FREE(new_table->bins);
-        FREE(new_table);
+        ABC_FREE(new_table->bins);
+        ABC_FREE(new_table);
         return NULL;
         }
         *new = *ptr;
@@ -432,7 +414,7 @@ char **value;
     *last = ptr->next;
     if (value != NULL) *value = ptr->record;
     *keyp = ptr->key;
-    FREE(ptr);
+    ABC_FREE(ptr);
     table->num_entries--;
     return 1;
 }
@@ -458,7 +440,7 @@ char **value;
     *last = ptr->next;
     if (value != NULL) *value = ptr->record;
     *keyp = (long) ptr->key;
-    FREE(ptr);
+    ABC_FREE(ptr);
     table->num_entries--;
     return 1;
 }
@@ -486,7 +468,7 @@ char *arg;
         case ST_DELETE:
         *last = ptr->next;
         table->num_entries--;    /* cstevens@ic */
-        FREE(ptr);
+        ABC_FREE(ptr);
         ptr = *last;
         }
     }
@@ -547,7 +529,7 @@ st_table *table;
 {
     st_generator *gen;
 
-    gen = ALLOC(st_generator, 1);
+    gen = ABC_ALLOC(st_generator, 1);
     if (gen == NULL) {
     return NULL;
     }
@@ -622,5 +604,5 @@ void
 st_free_gen(gen)
 st_generator *gen;
 {
-    FREE(gen);
+    ABC_FREE(gen);
 }
diff --git a/src/misc/st/stmm.c b/src/misc/st/stmm.c
index 7a52c1cd..5aaf8b9d 100644
--- a/src/misc/st/stmm.c
+++ b/src/misc/st/stmm.c
@@ -10,16 +10,11 @@
 #include <stdio.h>
 #include "extra.h"
 #include "stmm.h"
-#include "port_type.h"
-
-#ifndef ABS
-#  define ABS(a)            ((a) < 0 ? -(a) : (a))
-#endif
 
 #define STMM_NUMCMP(x,y) ((x) != (y))
-#define STMM_NUMHASH(x,size) (ABS((long)x)%(size))
-//#define STMM_PTRHASH(x,size) ((int)((PORT_PTRUINT_T)(x)>>2)%size) //  64-bit bug fix 9/17/2007
-#define STMM_PTRHASH(x,size) ((int)(((PORT_PTRUINT_T)(x)>>2)%size))
+#define STMM_NUMHASH(x,size) (ABC_ABS((long)x)%(size))
+//#define STMM_PTRHASH(x,size) ((int)((ABC_PTRUINT_T)(x)>>2)%size) //  64-bit bug fix 9/17/2007
+#define STMM_PTRHASH(x,size) ((int)(((ABC_PTRUINT_T)(x)>>2)%size))
 #define EQUAL(func, x, y) \
     ((((func) == stmm_numcmp) || ((func) == stmm_ptrcmp)) ?\
       (STMM_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))
@@ -46,7 +41,7 @@ stmm_init_table_with_params (compare, hash, size, density, grow_factor,
     int i;
     stmm_table *new;
 
-    new = ALLOC (stmm_table, 1);
+    new = ABC_ALLOC(stmm_table, 1);
     if (new == NULL) {
     return NULL;
     }
@@ -60,9 +55,9 @@ stmm_init_table_with_params (compare, hash, size, density, grow_factor,
     size = 1;
     }
     new->num_bins = size;
-    new->bins = ALLOC (stmm_table_entry *, size);
+    new->bins = ABC_ALLOC(stmm_table_entry *, size);
     if (new->bins == NULL) {
-    FREE (new);
+    ABC_FREE (new);
     return NULL;
     }
     for (i = 0; i < size; i++) {
@@ -99,7 +94,7 @@ stmm_free_table (table)
         while ( ptr != NULL )
         {
             next = ptr->next;
-            FREE( ptr );
+            ABC_FREE( ptr );
             ptr = next;
         }
     }
@@ -108,8 +103,8 @@ stmm_free_table (table)
     // added by alanmi
     if ( table->pMemMan )
         Extra_MmFixedStop (table->pMemMan);
-    FREE (table->bins);
-    FREE (table);
+    ABC_FREE (table->bins);
+    ABC_FREE (table);
 }
 
 // this function recycles all the bins
@@ -194,7 +189,7 @@ stmm_lookup_int (table, key, value)
 }
 
 // This macro contained a line
-//    new = ALLOC(stmm_table_entry, 1);
+//    new = ABC_ALLOC(stmm_table_entry, 1);
 // which was modified by alanmi
 
 
@@ -237,7 +232,7 @@ stmm_insert (table, key, value)
         hash_val = do_hash (key, table);
     }
 
-//              new = ALLOC( stmm_table_entry, 1 );
+//              new = ABC_ALLOC( stmm_table_entry, 1 );
     new = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
     if (new == NULL) {
         return STMM_OUT_OF_MEM;
@@ -273,7 +268,7 @@ stmm_add_direct (table, key, value)
     }
     hash_val = do_hash (key, table);
 
-//      new = ALLOC( stmm_table_entry, 1 );
+//      new = ABC_ALLOC( stmm_table_entry, 1 );
     new = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
     if (new == NULL) {
     return STMM_OUT_OF_MEM;
@@ -308,7 +303,7 @@ stmm_find_or_add (table, key, slot)
         hash_val = do_hash (key, table);
     }
 
-    // new = ALLOC( stmm_table_entry, 1 );
+    // new = ABC_ALLOC( stmm_table_entry, 1 );
     new = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
     if (new == NULL) {
         return STMM_OUT_OF_MEM;
@@ -373,7 +368,7 @@ rehash (table)
     table->num_bins += 1;
     }
     table->num_entries = 0;
-    table->bins = ALLOC (stmm_table_entry *, table->num_bins);
+    table->bins = ABC_ALLOC(stmm_table_entry *, table->num_bins);
     if (table->bins == NULL) {
     table->bins = old_bins;
     table->num_bins = old_num_bins;
@@ -397,7 +392,7 @@ rehash (table)
         ptr = next;
     }
     }
-    FREE (old_bins);
+    ABC_FREE (old_bins);
 
     return 1;
 }
@@ -410,15 +405,15 @@ stmm_copy (old_table)
     stmm_table_entry *ptr, /* *newptr, *next, */ *new;
     int i, /*j, */ num_bins = old_table->num_bins;
 
-    new_table = ALLOC (stmm_table, 1);
+    new_table = ABC_ALLOC(stmm_table, 1);
     if (new_table == NULL) {
     return NULL;
     }
 
     *new_table = *old_table;
-    new_table->bins = ALLOC (stmm_table_entry *, num_bins);
+    new_table->bins = ABC_ALLOC(stmm_table_entry *, num_bins);
     if (new_table->bins == NULL) {
-    FREE (new_table);
+    ABC_FREE (new_table);
     return NULL;
     }
 
@@ -430,7 +425,7 @@ stmm_copy (old_table)
     new_table->bins[i] = NULL;
     ptr = old_table->bins[i];
     while (ptr != NULL) {
-//                      new = ALLOC( stmm_table_entry, 1 );
+//                      new = ABC_ALLOC( stmm_table_entry, 1 );
         new =
         (stmm_table_entry *) Extra_MmFixedEntryFetch (new_table->
                                 pMemMan);
@@ -443,15 +438,15 @@ stmm_copy (old_table)
                     while ( newptr != NULL )
                     {
                         next = newptr->next;
-                        FREE( newptr );
+                        ABC_FREE( newptr );
                         newptr = next;
                     }
                 }
 */
         Extra_MmFixedStop (new_table->pMemMan);
 
-        FREE (new_table->bins);
-        FREE (new_table);
+        ABC_FREE (new_table->bins);
+        ABC_FREE (new_table);
         return NULL;
         }
         *new = *ptr;
@@ -485,7 +480,7 @@ stmm_delete (table, keyp, value)
     if (value != NULL)
      *value = ptr->record;
     *keyp = ptr->key;
-//      FREE( ptr );
+//      ABC_FREE( ptr );
     Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
 
     table->num_entries--;
@@ -514,7 +509,7 @@ stmm_delete_int (table, keyp, value)
     if (value != NULL)
      *value = ptr->record;
     *keyp = (long) ptr->key;
-//      FREE( ptr );
+//      ABC_FREE( ptr );
     Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
 
     table->num_entries--;
@@ -546,7 +541,7 @@ stmm_foreach (table, func, arg)
         case STMM_DELETE:
         *last = ptr->next;
         table->num_entries--;    /* cstevens@ic */
-//                              FREE( ptr );
+//                              ABC_FREE( ptr );
         Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
 
         ptr = *last;
@@ -609,7 +604,7 @@ stmm_init_gen (table)
 {
     stmm_generator *gen;
 
-    gen = ALLOC (stmm_generator, 1);
+    gen = ABC_ALLOC(stmm_generator, 1);
     if (gen == NULL) {
     return NULL;
     }
@@ -685,5 +680,5 @@ void
 stmm_free_gen (gen)
     stmm_generator *gen;
 {
-    FREE (gen);
+    ABC_FREE (gen);
 }
diff --git a/src/misc/st/stmm.h b/src/misc/st/stmm.h
index 4330416e..9dede7d8 100644
--- a/src/misc/st/stmm.h
+++ b/src/misc/st/stmm.h
@@ -14,12 +14,12 @@
 #ifndef STMM_INCLUDED
 #define STMM_INCLUDED
 
+#include "extra.h"
+
 #ifdef __cplusplus
 extern "C" {
 #endif
 
-#include "extra.h"
-
 typedef struct stmm_table_entry stmm_table_entry;
 typedef struct stmm_table stmm_table;
 typedef struct stmm_generator stmm_generator;
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
new file mode 100644
index 00000000..35a391ba
--- /dev/null
+++ b/src/misc/util/abc_global.h
@@ -0,0 +1,178 @@
+/**CFile****************************************************************
+
+  FileName    [abc_global.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Global declarations.]
+
+  Synopsis    [Global declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Jan 30, 2009.]
+
+  Revision    [$Id: abc_global.h,v 1.00 2009/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __ABC_GLOBAL_H__
+#define __ABC_GLOBAL_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+ 
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#pragma warning(disable : 4152) // warning C4152: nonstandard extension, function/data pointer conversion in expression
+#pragma warning(disable : 4244) // warning C4244: '+=' : conversion from 'int ' to 'unsigned short ', possible loss of data
+#pragma warning(disable : 4514) // warning C4514: 'Vec_StrPop' : unreferenced inline function has been removed
+#pragma warning(disable : 4710) // warning C4710: function 'Vec_PtrGrow' not inlined
+//#pragma warning( disable : 4273 )
+#endif
+
+#ifdef WIN32
+#define ABC_DLLEXPORT __declspec(dllexport)
+#define ABC_DLLIMPORT __declspec(dllimport)
+#else  /* defined(WIN32) */
+#define ABC_DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL ABC_DLLIMPORT
+#endif
+
+// catch memory leaks in Visual Studio
+#ifdef _DEBUG
+#define _CRTDBG_MAP_ALLOC
+#include <crtdbg.h>
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+/**
+ * Pointer difference type; replacement for ptrdiff_t.
+ * This is a signed integral type that is the same size as a pointer.
+ * NOTE: This type may be different sizes on different platforms.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type ABC_PTRDIFF_T;
+#elif     defined(LIN64)
+typedef long ABC_PTRDIFF_T;
+#elif     defined(NT64)
+typedef long long ABC_PTRDIFF_T;
+#elif     defined(NT) || defined(LIN) || defined(WIN32)
+typedef int ABC_PTRDIFF_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+/**
+ * Unsigned integral type that can contain a pointer.
+ * This is an unsigned integral type that is the same size as a pointer.
+ * NOTE: This type may be different sizes on different platforms.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type ABC_PTRUINT_T;
+#elif     defined(LIN64)
+typedef unsigned long ABC_PTRUINT_T;
+#elif     defined(NT64)
+typedef unsigned long long ABC_PTRUINT_T;
+#elif     defined(NT) || defined(LIN) || defined(WIN32)
+typedef unsigned int ABC_PTRUINT_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+/**
+ * Signed integral type that can contain a pointer.
+ * This is a signed integral type that is the same size as a pointer.
+ * NOTE: This type may be different sizes on different platforms.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type ABC_PTRINT_T;
+#elif     defined(LIN64)
+typedef long ABC_PTRINT_T;
+#elif     defined(NT64)
+typedef long long ABC_PTRINT_T;
+#elif     defined(NT) || defined(LIN) || defined(WIN32)
+typedef int ABC_PTRINT_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+/**
+ * 64-bit signed integral type.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type ABC_INT64_T;
+#elif     defined(LIN64)
+typedef long ABC_INT64_T;
+#elif     defined(NT64) || defined(LIN)
+typedef long long ABC_INT64_T;
+#elif     defined(WIN32) || defined(NT)
+typedef signed __int64 ABC_INT64_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+/**
+ * 64-bit unsigned integral type.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type ABC_UINT64_T;
+#elif     defined(LIN64)
+typedef unsigned long ABC_UINT64_T;
+#elif     defined(NT64) || defined(LIN)
+typedef unsigned long long ABC_UINT64_T;
+#elif     defined(WIN32) || defined(NT)
+typedef unsigned __int64 ABC_UINT64_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define ABC_ABS(a)            ((a) < 0 ? -(a) : (a))
+#define ABC_MAX(a,b)        ((a) > (b) ? (a) : (b))
+#define ABC_MIN(a,b)        ((a) < (b) ? (a) : (b))
+#define ABC_INFINITY        (100000000)
+
+#define ABC_ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
+#define ABC_CALLOC(type, num)     ((type *) calloc((num), sizeof(type)))
+#define ABC_FALLOC(type, num)     ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num)))
+#define ABC_FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#define ABC_REALLOC(type, obj, num)    \
+        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+         ((type *) malloc(sizeof(type) * (num))))
+
+#define ABC_PRT(a,t)    (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
+#define ABC_PRTn(a,t)   (printf("%s = ", (a)), printf("%6.2f sec  ", (float)(t)/(float)(CLOCKS_PER_SEC)))
+#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
+#define ABC_PRM(a,f)    (printf("%s = ", (a)), printf("%7.2f Mb  ",    1.0*(f)/(1<<20)))
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/misc/util/port_type.h b/src/misc/util/port_type.h
deleted file mode 100644
index 67b7d454..00000000
--- a/src/misc/util/port_type.h
+++ /dev/null
@@ -1,78 +0,0 @@
-// Portable Data Types
-
-#ifndef __PORT_TYPE__
-#define __PORT_TYPE__
-
-/**
- * Pointer difference type; replacement for ptrdiff_t.
- *
- * This is a signed integral type that is the same size as a pointer.
- *
- * NOTE: This type may be different sizes on different platforms.
- */
-#if       defined(__ccdoc__)
-typedef platform_dependent_type PORT_PTRDIFF_T;
-#elif     defined(LIN64)
-typedef long PORT_PTRDIFF_T;
-#elif     defined(NT64)
-typedef long long PORT_PTRDIFF_T;
-#elif     defined(NT) || defined(LIN) || defined(WIN32)
-typedef int PORT_PTRDIFF_T;
-#else
-   #error unknown platform
-#endif /* defined(PLATFORM) */
-
-/**
- * Unsigned integral type that can contain a pointer.
- *
- * This is an unsigned integral type that is the same size as a pointer.
- *
- * NOTE: This type may be different sizes on different platforms.
- */
-#if       defined(__ccdoc__)
-typedef platform_dependent_type PORT_PTRUINT_T;
-#elif     defined(LIN64)
-typedef unsigned long PORT_PTRUINT_T;
-#elif     defined(NT64)
-typedef unsigned long long PORT_PTRUINT_T;
-#elif     defined(NT) || defined(LIN) || defined(WIN32)
-typedef unsigned int PORT_PTRUINT_T;
-#else
-   #error unknown platform
-#endif /* defined(PLATFORM) */
-
-/**
- * Signed integral type that can contain a pointer.
- *
- * This is a signed integral type that is the same size as a pointer.
- *
- * NOTE: This type may be different sizes on different platforms.
- */
-#if       defined(__ccdoc__)
-typedef platform_dependent_type PORT_PTRINT_T;
-#elif     defined(LIN64)
-typedef long PORT_PTRINT_T;
-#elif     defined(NT64)
-typedef long long PORT_PTRINT_T;
-#elif     defined(NT) || defined(LIN) || defined(WIN32)
-typedef int PORT_PTRINT_T;
-#else
-   #error unknown platform
-#endif /* defined(PLATFORM) */
-
-/**
- * 64-bit signed integral type.
- */
-#if       defined(__ccdoc__)
-typedef platform_dependent_type PORT_INT64_T;
-#elif     defined(LIN64)
-typedef long PORT_INT64_T;
-#elif     defined(NT64) || defined(LIN)
-typedef long long PORT_INT64_T;
-#elif     defined(WIN32) || defined(NT)
-typedef signed __int64 PORT_INT64_T;
-#else
-   #error unknown platform
-#endif /* defined(PLATFORM) */
-
-#endif
diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h
index 3fdb7ffb..825c8bee 100644
--- a/src/misc/util/util_hack.h
+++ b/src/misc/util/util_hack.h
@@ -21,16 +21,17 @@
 #ifndef __UTIL_HACK_H__
 #define __UTIL_HACK_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
 #include <time.h>
 #include <math.h>
+#include "abc_global.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
 
 #ifndef EXTERN
 #define EXTERN extern
@@ -60,24 +61,6 @@ extern "C" {
 # endif
 #endif
 
-#ifndef ABS
-#  define ABS(a)            ((a) < 0 ? -(a) : (a))
-#endif
-
-#ifndef MAX
-#  define MAX(a,b)        ((a) > (b) ? (a) : (b))
-#endif
-
-#ifndef MIN
-#  define MIN(a,b)        ((a) < (b) ? (a) : (b))
-#endif
-
-#define ALLOC(type, num)       ((type *) malloc(sizeof(type) * (num)))
-#define FREE(obj)              ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
-#define REALLOC(type, obj, num) \
-        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num))))
-
 extern long        Extra_CpuTime();
 extern int         Extra_GetSoftDataLimit();
 extern void        Extra_UtilGetoptReset();
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index 67ec44aa..915265f3 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -21,93 +21,31 @@
 #ifndef __VEC_H__
 #define __VEC_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-#ifdef _WIN32
-#define inline __inline // compatible with MS VS 6.0
-#pragma warning(disable : 4152) // warning C4152: nonstandard extension, function/data pointer conversion in expression
-#pragma warning(disable : 4244) // warning C4244: '+=' : conversion from 'int ' to 'unsigned short ', possible loss of data
-#pragma warning(disable : 4514) // warning C4514: 'Vec_StrPop' : unreferenced inline function has been removed
-#pragma warning(disable : 4710) // warning C4710: function 'Vec_PtrGrow' not inlined
-#endif
-
-#ifndef SINT64
-#define SINT64
-
-#ifdef _WIN32
-typedef signed __int64     sint64;   // compatible with MS VS 6.0
-#else
-typedef long long          sint64;
-#endif
-
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-// catch memory leaks in Visual Studio
-#ifdef _DEBUG
-#define _CRTDBG_MAP_ALLOC
-#include <crtdbg.h>
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-#ifndef ABS
-#define ABS(a)            ((a) < 0 ? -(a) : (a))
-#endif
-
-#ifndef MAX
-#define MAX(a,b)        ((a) > (b) ? (a) : (b))
-#endif
-
-#ifndef MIN
-#define MIN(a,b)        ((a) < (b) ? (a) : (b))
-#endif
-
-#ifndef ALLOC
-#define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
-#endif
-
-#ifndef CALLOC
-#define CALLOC(type, num)     ((type *) calloc((num), sizeof(type)))
-#endif
-
-#ifndef FREE
-#define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
-#endif
-
-#ifndef REALLOC
-#define REALLOC(type, obj, num)    \
-        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-         ((type *) malloc(sizeof(type) * (num))))
-#endif
-
-#ifndef PRT
-#define PRT(a,t)  printf("%s = ", (a)); printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
-#endif
-
-#ifndef PRTP
-#define PRTP(a,t,T)  printf("%s = ", (a)); printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
-#endif
-
+#include "abc_global.h"
 #include "vecInt.h"
 #include "vecFlt.h"
 #include "vecStr.h"
 #include "vecPtr.h"
 #include "vecVec.h"
 #include "vecAtt.h"
-#include "port_type.h"
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecAtt.h b/src/misc/vec/vecAtt.h
index 8d0a034b..9129321c 100644
--- a/src/misc/vec/vecAtt.h
+++ b/src/misc/vec/vecAtt.h
@@ -65,9 +65,9 @@ struct Vec_Att_t_
     void **          pArrayPtr;            // the pointer attribute array
     // attribute specific info
     void *           pMan;                 // the manager for this attribute
-    void (*pFuncFreeMan) (void *);         // the procedure to free the manager
+    void (*pFuncFreeMan) (void *);         // the procedure to ABC_FREE the manager
     void*(*pFuncStartObj)(void *);         // the procedure to start one attribute
-    void (*pFuncFreeObj) (void *, void *); // the procedure to free one attribute
+    void (*pFuncFreeObj) (void *, void *); // the procedure to ABC_FREE one attribute
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -96,14 +96,14 @@ static inline Vec_Att_t * Vec_AttAlloc(
     void (*pFuncFreeObj) (void *, void *)  )
 {
     Vec_Att_t * p;
-    p = ALLOC( Vec_Att_t, 1 );
+    p = ABC_ALLOC( Vec_Att_t, 1 );
     memset( p, 0, sizeof(Vec_Att_t) );
     p->pMan          = pMan;
     p->pFuncFreeMan  = pFuncFreeMan;
     p->pFuncStartObj = pFuncStartObj;
     p->pFuncFreeObj  = pFuncFreeObj;
     p->nCap = nSize? nSize : 16;
-    p->pArrayPtr = ALLOC( void *, p->nCap );
+    p->pArrayPtr = ABC_ALLOC( void *, p->nCap );
     memset( p->pArrayPtr, 0, sizeof(void *) * p->nCap );
     return p;
 }
@@ -124,7 +124,7 @@ static inline void * Vec_AttFree( Vec_Att_t * p, int fFreeMan )
     void * pMan;
     if ( p == NULL )
         return NULL;
-    // free the attributes of objects
+    // ABC_FREE the attributes of objects
     if ( p->pFuncFreeObj )
     {
         int i;
@@ -132,12 +132,12 @@ static inline void * Vec_AttFree( Vec_Att_t * p, int fFreeMan )
             if ( p->pArrayPtr[i] )
                 p->pFuncFreeObj( p->pMan, p->pArrayPtr[i] );
     }
-    // free the memory manager
+    // ABC_FREE the memory manager
     pMan = fFreeMan? NULL : p->pMan;
     if ( p->pMan && fFreeMan )  
         p->pFuncFreeMan( p->pMan );
-    FREE( p->pArrayPtr );
-    FREE( p );
+    ABC_FREE( p->pArrayPtr );
+    ABC_FREE( p );
     return pMan;
 }
 
@@ -154,7 +154,7 @@ static inline void * Vec_AttFree( Vec_Att_t * p, int fFreeMan )
 ***********************************************************************/
 static inline void Vec_AttClear( Vec_Att_t * p )
 {
-    // free the attributes of objects
+    // ABC_FREE the attributes of objects
     if ( p->pFuncFreeObj )
     {
         int i;
@@ -204,7 +204,7 @@ static inline void Vec_AttGrow( Vec_Att_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArrayPtr = REALLOC( void *, p->pArrayPtr, nCapMin );
+    p->pArrayPtr = ABC_REALLOC( void *, p->pArrayPtr, nCapMin );
     memset( p->pArrayPtr + p->nCap, 0, sizeof(void *) * (nCapMin - p->nCap) );
     p->nCap = nCapMin;
 }
diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h
index 513c7dc6..93402cf2 100644
--- a/src/misc/vec/vecFlt.h
+++ b/src/misc/vec/vecFlt.h
@@ -74,12 +74,12 @@ struct Vec_Flt_t_
 static inline Vec_Flt_t * Vec_FltAlloc( int nCap )
 {
     Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
+    p = ABC_ALLOC( Vec_Flt_t, 1 );
     if ( nCap > 0 && nCap < 16 )
         nCap = 16;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( float, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( float, p->nCap ) : NULL;
     return p;
 }
 
@@ -117,7 +117,7 @@ static inline Vec_Flt_t * Vec_FltStart( int nSize )
 static inline Vec_Flt_t * Vec_FltAllocArray( float * pArray, int nSize )
 {
     Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
+    p = ABC_ALLOC( Vec_Flt_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
     p->pArray = pArray;
@@ -138,10 +138,10 @@ static inline Vec_Flt_t * Vec_FltAllocArray( float * pArray, int nSize )
 static inline Vec_Flt_t * Vec_FltAllocArrayCopy( float * pArray, int nSize )
 {
     Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
+    p = ABC_ALLOC( Vec_Flt_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
-    p->pArray = ALLOC( float, nSize );
+    p->pArray = ABC_ALLOC( float, nSize );
     memcpy( p->pArray, pArray, sizeof(float) * nSize );
     return p;
 }
@@ -160,10 +160,10 @@ static inline Vec_Flt_t * Vec_FltAllocArrayCopy( float * pArray, int nSize )
 static inline Vec_Flt_t * Vec_FltDup( Vec_Flt_t * pVec )
 {
     Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
+    p = ABC_ALLOC( Vec_Flt_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( float, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( float, p->nCap ) : NULL;
     memcpy( p->pArray, pVec->pArray, sizeof(float) * pVec->nSize );
     return p;
 }
@@ -182,7 +182,7 @@ static inline Vec_Flt_t * Vec_FltDup( Vec_Flt_t * pVec )
 static inline Vec_Flt_t * Vec_FltDupArray( Vec_Flt_t * pVec )
 {
     Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
+    p = ABC_ALLOC( Vec_Flt_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
     p->pArray = pVec->pArray;
@@ -205,8 +205,8 @@ static inline Vec_Flt_t * Vec_FltDupArray( Vec_Flt_t * pVec )
 ***********************************************************************/
 static inline void Vec_FltFree( Vec_Flt_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -343,7 +343,7 @@ static inline void Vec_FltGrow( Vec_Flt_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( float, p->pArray, nCapMin ); 
+    p->pArray = ABC_REALLOC( float, p->pArray, nCapMin ); 
     p->nCap   = nCapMin;
 }
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index c944df3f..0f7a41ab 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -51,6 +51,8 @@ struct Vec_Int_t_
     for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
 #define Vec_IntForEachEntryStart( vVec, Entry, i, Start )                                   \
     for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+#define Vec_IntForEachEntryStop( vVec, Entry, i, Stop )                                   \
+    for ( i = 0; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
 #define Vec_IntForEachEntryStartStop( vVec, Entry, i, Start, Stop )                         \
     for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
 #define Vec_IntForEachEntryReverse( vVec, pEntry, i )                                       \
@@ -74,12 +76,12 @@ struct Vec_Int_t_
 static inline Vec_Int_t * Vec_IntAlloc( int nCap )
 {
     Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
+    p = ABC_ALLOC( Vec_Int_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;
 }
 
@@ -139,7 +141,7 @@ static inline Vec_Int_t * Vec_IntStartNatural( int nSize )
 static inline Vec_Int_t * Vec_IntAllocArray( int * pArray, int nSize )
 {
     Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
+    p = ABC_ALLOC( Vec_Int_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
     p->pArray = pArray;
@@ -160,10 +162,10 @@ static inline Vec_Int_t * Vec_IntAllocArray( int * pArray, int nSize )
 static inline Vec_Int_t * Vec_IntAllocArrayCopy( int * pArray, int nSize )
 {
     Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
+    p = ABC_ALLOC( Vec_Int_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;
 }
@@ -182,10 +184,10 @@ static inline Vec_Int_t * Vec_IntAllocArrayCopy( int * pArray, int nSize )
 static inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec )
 {
     Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
+    p = ABC_ALLOC( Vec_Int_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nSize;
-    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;
 }
@@ -204,7 +206,7 @@ static inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec )
 static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
 {
     Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
+    p = ABC_ALLOC( Vec_Int_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
     p->pArray = pVec->pArray;
@@ -227,8 +229,8 @@ static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
 ***********************************************************************/
 static inline void Vec_IntFree( Vec_Int_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -366,7 +368,7 @@ static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( int, p->pArray, nCapMin ); 
+    p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); 
     assert( p->pArray );
     p->nCap   = nCapMin;
 }
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 27643043..4d09acb7 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -77,12 +77,12 @@ struct Vec_Ptr_t_
 static inline Vec_Ptr_t * Vec_PtrAlloc( int nCap )
 {
     Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
+    p = ABC_ALLOC( Vec_Ptr_t, 1 );
     if ( nCap > 0 && nCap < 8 )
         nCap = 8;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL;
     return p;
 }
 
@@ -120,7 +120,7 @@ static inline Vec_Ptr_t * Vec_PtrStart( int nSize )
 static inline Vec_Ptr_t * Vec_PtrAllocArray( void ** pArray, int nSize )
 {
     Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
+    p = ABC_ALLOC( Vec_Ptr_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
     p->pArray = pArray;
@@ -141,10 +141,10 @@ static inline Vec_Ptr_t * Vec_PtrAllocArray( void ** pArray, int nSize )
 static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
 {
     Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
+    p = ABC_ALLOC( Vec_Ptr_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
-    p->pArray = ALLOC( void *, nSize );
+    p->pArray = ABC_ALLOC( void *, nSize );
     memcpy( p->pArray, pArray, sizeof(void *) * nSize );
     return p;
 }
@@ -163,10 +163,10 @@ static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
 static inline Vec_Ptr_t * Vec_PtrDup( Vec_Ptr_t * pVec )
 {
     Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
+    p = ABC_ALLOC( Vec_Ptr_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL;
     memcpy( p->pArray, pVec->pArray, sizeof(void *) * pVec->nSize );
     return p;
 }
@@ -185,7 +185,7 @@ static inline Vec_Ptr_t * Vec_PtrDup( Vec_Ptr_t * pVec )
 static inline Vec_Ptr_t * Vec_PtrDupArray( Vec_Ptr_t * pVec )
 {
     Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
+    p = ABC_ALLOC( Vec_Ptr_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
     p->pArray = pVec->pArray;
@@ -208,8 +208,8 @@ static inline Vec_Ptr_t * Vec_PtrDupArray( Vec_Ptr_t * pVec )
 ***********************************************************************/
 static inline void Vec_PtrFree( Vec_Ptr_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -347,7 +347,7 @@ static inline void Vec_PtrGrow( Vec_Ptr_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( void *, p->pArray, nCapMin ); 
+    p->pArray = ABC_REALLOC( void *, p->pArray, nCapMin ); 
     p->nCap   = nCapMin;
 }
 
@@ -678,7 +678,7 @@ static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
     void ** pMemory;
     unsigned * pInfo;
     int i;
-    pMemory = (void **)ALLOC( char, (sizeof(void *) + sizeof(unsigned) * nWords) * nEntries );
+    pMemory = (void **)ABC_ALLOC( char, (sizeof(void *) + sizeof(unsigned) * nWords) * nEntries );
     pInfo = (unsigned *)(pMemory + nEntries);
     for ( i = 0; i < nEntries; i++ )
         pMemory[i] = pInfo + i * nWords;
@@ -696,6 +696,22 @@ static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_PtrReadWordsSimInfo( Vec_Ptr_t * p )
+{
+    return (unsigned *)Vec_PtrEntry(p,1) - (unsigned *)Vec_PtrEntry(p,0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans simulation info of each entry beginning with iWord.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_PtrCleanSimInfo( Vec_Ptr_t * vInfo, int iWord, int nWords )
 {
     int i;
@@ -743,13 +759,13 @@ static inline void Vec_PtrDoubleSimInfo( Vec_Ptr_t * vInfo )
     // copy the simulation info
     memcpy( Vec_PtrEntry(vInfoNew,0), Vec_PtrEntry(vInfo,0), Vec_PtrSize(vInfo) * nWords * 4 );
     // replace the array
-    free( vInfo->pArray );
+    ABC_FREE( vInfo->pArray );
     vInfo->pArray = vInfoNew->pArray;
     vInfo->nSize *= 2;
     vInfo->nCap *= 2;
-    // free the old array
+    // ABC_FREE the old array
     vInfoNew->pArray = NULL;
-    free( vInfoNew );
+    ABC_FREE( vInfoNew );
 }
 
 /**Function*************************************************************
@@ -775,11 +791,11 @@ static inline void Vec_PtrReallocSimInfo( Vec_Ptr_t * vInfo )
     for ( i = 0; i < vInfo->nSize; i++ )
         memcpy( Vec_PtrEntry(vInfoNew,i), Vec_PtrEntry(vInfo,i), nWords * 4 );
     // replace the array
-    free( vInfo->pArray );
+    ABC_FREE( vInfo->pArray );
     vInfo->pArray = vInfoNew->pArray;
-    // free the old array
+    // ABC_FREE the old array
     vInfoNew->pArray = NULL;
-    free( vInfoNew );
+    ABC_FREE( vInfoNew );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index a00aaa68..dc0b2bad 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -68,12 +68,12 @@ struct Vec_Str_t_
 static inline Vec_Str_t * Vec_StrAlloc( int nCap )
 {
     Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
+    p = ABC_ALLOC( Vec_Str_t, 1 );
     if ( nCap > 0 && nCap < 16 )
         nCap = 16;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( char, p->nCap ) : NULL;
     return p;
 }
 
@@ -111,7 +111,7 @@ static inline Vec_Str_t * Vec_StrStart( int nSize )
 static inline Vec_Str_t * Vec_StrAllocArray( char * pArray, int nSize )
 {
     Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
+    p = ABC_ALLOC( Vec_Str_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
     p->pArray = pArray;
@@ -132,10 +132,10 @@ static inline Vec_Str_t * Vec_StrAllocArray( char * pArray, int nSize )
 static inline Vec_Str_t * Vec_StrAllocArrayCopy( char * pArray, int nSize )
 {
     Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
+    p = ABC_ALLOC( Vec_Str_t, 1 );
     p->nSize  = nSize;
     p->nCap   = nSize;
-    p->pArray = ALLOC( char, nSize );
+    p->pArray = ABC_ALLOC( char, nSize );
     memcpy( p->pArray, pArray, sizeof(char) * nSize );
     return p;
 }
@@ -154,10 +154,10 @@ static inline Vec_Str_t * Vec_StrAllocArrayCopy( char * pArray, int nSize )
 static inline Vec_Str_t * Vec_StrDup( Vec_Str_t * pVec )
 {
     Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
+    p = ABC_ALLOC( Vec_Str_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( char, p->nCap ) : NULL;
     memcpy( p->pArray, pVec->pArray, sizeof(char) * pVec->nSize );
     return p;
 }
@@ -176,7 +176,7 @@ static inline Vec_Str_t * Vec_StrDup( Vec_Str_t * pVec )
 static inline Vec_Str_t * Vec_StrDupArray( Vec_Str_t * pVec )
 {
     Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
+    p = ABC_ALLOC( Vec_Str_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
     p->pArray = pVec->pArray;
@@ -199,8 +199,8 @@ static inline Vec_Str_t * Vec_StrDupArray( Vec_Str_t * pVec )
 ***********************************************************************/
 static inline void Vec_StrFree( Vec_Str_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -321,7 +321,7 @@ static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( char, p->pArray, 2 * nCapMin ); 
+    p->pArray = ABC_REALLOC( char, p->pArray, 2 * nCapMin ); 
     p->nCap   = 2 * nCapMin;
 }
 
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index 0557e9c0..a77cdf76 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -99,12 +99,12 @@ struct Vec_Vec_t_
 static inline Vec_Vec_t * Vec_VecAlloc( int nCap )
 {
     Vec_Vec_t * p;
-    p = ALLOC( Vec_Vec_t, 1 );
+    p = ABC_ALLOC( Vec_Vec_t, 1 );
     if ( nCap > 0 && nCap < 8 )
         nCap = 8;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL;
     return p;
 }