Version abc90215

47 files changed, 1369 insertions, 339 deletions

diff --git a/src/map/amap/amap.h b/src/map/amap/amap.h
index ee845e7f..284af309 100644
--- a/src/map/amap/amap.h
+++ b/src/map/amap/amap.h
@@ -21,10 +21,6 @@
 #ifndef __AMAP_H__
 #define __AMAP_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,7 +45,7 @@ struct Amap_Par_t_
     int    nIterArea;   // iteratoins of exact area
     int    fUseMuxes;   // enables the use of MUXes
     int    fUseXors;    // enables the use of XORs
-    int    fFreeInvs;   // assume inverters are free (area = 0)
+    int    fFreeInvs;   // assume inverters are ABC_FREE (area = 0)
     float  fEpsilon;    // used to compare floating point numbers
     int    fVerbose;    // verbosity flag
 };
@@ -69,7 +69,10 @@ struct Amap_Out_t_
 
 /*=== amapCore.c ==========================================================*/
 extern void        Amap_ManSetDefaultParams( Amap_Par_t * pPars );
-extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
+//extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
+/*=== amapLiberty.c ==========================================================*/
+extern int         Amap_LibertyParse( char * pFileName, char * pFileGenlib, int fVerbose );
+
 
 #ifdef __cplusplus
 }
diff --git a/src/map/amap/amapCore.c b/src/map/amap/amapCore.c
index f1554862..7dedc067 100644
--- a/src/map/amap/amapCore.c
+++ b/src/map/amap/amapCore.c
@@ -46,7 +46,7 @@ void Amap_ManSetDefaultParams( Amap_Par_t * p )
     p->nIterArea = 4;            // iteratoins of exact area
     p->fUseMuxes = 0;            // enables the use of MUXes
     p->fUseXors  = 1;            // enables the use of XORs
-    p->fFreeInvs = 0;            // assume inverters are free (area = 0)
+    p->fFreeInvs = 0;            // assume inverters are ABC_FREE (area = 0)
     p->fEpsilon  = (float)0.001; // used to compare floating point numbers
     p->fVerbose  = 0;            // verbosity flag
 }
@@ -81,8 +81,8 @@ Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars )
     p->fAreaInv = pPars->fFreeInvs? 0.0 : pLib->pGateInv->dArea;
     p->fUseMux = pPars->fUseMuxes && pLib->fHasMux;
     p->fUseXor = pPars->fUseXors && pLib->fHasXor;
-    p->ppCutsTemp = CALLOC( Amap_Cut_t *, 2 * pLib->nNodes );
-    p->pMatsTemp = CALLOC( int, 2 * pLib->nNodes );
+    p->ppCutsTemp = ABC_CALLOC( Amap_Cut_t *, 2 * pLib->nNodes );
+    p->pMatsTemp = ABC_CALLOC( int, 2 * pLib->nNodes );
     Amap_ManCreate( p, pAig );
     Amap_ManMap( p );
     vRes = NULL;
@@ -90,7 +90,7 @@ Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars )
     Amap_ManStop( p );
 if ( pPars->fVerbose )
 {
-PRT( "Total runtime", clock() - clkTotal );
+ABC_PRT( "Total runtime", clock() - clkTotal );
 }
     return vRes;
 }
diff --git a/src/map/amap/amapInt.h b/src/map/amap/amapInt.h
index 954790c9..dec7e799 100644
--- a/src/map/amap/amapInt.h
+++ b/src/map/amap/amapInt.h
@@ -21,10 +21,6 @@
 #ifndef __AMAP_INT_H__
 #define __AMAP_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -36,6 +32,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 // the largest gate size in the library
 // (gates above this size will be ignored)
 #define AMAP_MAXINS 15
@@ -222,10 +222,10 @@ static inline int          Amap_LitNot( int Lit )               { return Lit ^ 1
 static inline int          Amap_LitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
 static inline int          Amap_LitRegular( int Lit )           { return Lit & ~01;          }
 
-static inline Amap_Obj_t * Amap_Regular( Amap_Obj_t * p )                          { return (Amap_Obj_t *)((PORT_PTRUINT_T)(p) & ~01);  }
-static inline Amap_Obj_t * Amap_Not( Amap_Obj_t * p )                              { return (Amap_Obj_t *)((PORT_PTRUINT_T)(p) ^  01);  }
-static inline Amap_Obj_t * Amap_NotCond( Amap_Obj_t * p, int c )                   { return (Amap_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c));  }
-static inline int          Amap_IsComplement( Amap_Obj_t * p )                     { return (int )(((PORT_PTRUINT_T)p) & 01);           }
+static inline Amap_Obj_t * Amap_Regular( Amap_Obj_t * p )                          { return (Amap_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);  }
+static inline Amap_Obj_t * Amap_Not( Amap_Obj_t * p )                              { return (Amap_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);  }
+static inline Amap_Obj_t * Amap_NotCond( Amap_Obj_t * p, int c )                   { return (Amap_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));  }
+static inline int          Amap_IsComplement( Amap_Obj_t * p )                     { return (int )(((ABC_PTRUINT_T)p) & 01);           }
 
 static inline int          Amap_ManPiNum( Amap_Man_t * p )                         { return p->nObjs[AMAP_OBJ_PI];                      }
 static inline int          Amap_ManPoNum( Amap_Man_t * p )                         { return p->nObjs[AMAP_OBJ_PO];                      }
diff --git a/src/map/amap/amapLib.c b/src/map/amap/amapLib.c
index 816f0703..f2e5113f 100644
--- a/src/map/amap/amapLib.c
+++ b/src/map/amap/amapLib.c
@@ -42,7 +42,7 @@
 Amap_Lib_t * Amap_LibAlloc()
 {
     Amap_Lib_t * p;
-    p = (Amap_Lib_t *)ALLOC( Amap_Lib_t, 1 );
+    p = (Amap_Lib_t *)ABC_ALLOC( Amap_Lib_t, 1 );
     memset( p, 0, sizeof(Amap_Lib_t) );
     p->vGates = Vec_PtrAlloc( 100 );
     p->pMemGates = Aig_MmFlexStart();
@@ -79,10 +79,10 @@ void Amap_LibFree( Amap_Lib_t * p )
         Vec_IntFree( p->vRules3 );
     Aig_MmFlexStop( p->pMemGates, 0 );
     Aig_MmFlexStop( p->pMemSet, 0 );
-    FREE( p->pRules );
-    FREE( p->pRulesX );
-    FREE( p->pNodes );
-    free( p );
+    ABC_FREE( p->pRules );
+    ABC_FREE( p->pRulesX );
+    ABC_FREE( p->pNodes );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -341,7 +341,7 @@ Amap_Lib_t * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVe
     {
         printf( "Selected %d functionally unique gates. ",
             Vec_PtrSize(p->vSelect), Vec_PtrSize(p->vSorted) );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     clk = clock();
     Amap_LibCreateRules( p, fVeryVerbose );
@@ -349,7 +349,7 @@ Amap_Lib_t * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVe
     {
         printf( "Created %d rules and %d matches. ", 
             p->nNodes, p->nSets );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     return p;
 }
diff --git a/src/map/amap/amapLiberty.c b/src/map/amap/amapLiberty.c
new file mode 100644
index 00000000..7f46ffdf
--- /dev/null
+++ b/src/map/amap/amapLiberty.c
@@ -0,0 +1,911 @@
+/**CFile****************************************************************
+
+  FileHead    [amapLiberty.c]
+
+  SystemHead  [ABC: Logic synthesis and verification system.]
+
+  PackageHead [Technology mapper for standard cells.]
+
+  Synopsis    [Liberty parser.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapLiberty.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// entry types
+typedef enum { 
+    AMAP_LIBERTY_NONE = 0,        // 0:  unknown
+    AMAP_LIBERTY_PROC,            // 1:  procedure :  key(head){body}
+    AMAP_LIBERTY_EQUA,            // 2:  equation  :  key:head;
+    AMAP_LIBERTY_LIST             // 3:  list      :  key(head) 
+} Amap_LibertyType_t;
+
+typedef struct Amap_Pair_t_ Amap_Pair_t;
+struct Amap_Pair_t_
+{
+    int             Beg;          // item beginning
+    int             End;          // item end
+};
+
+typedef struct Amap_Item_t_ Amap_Item_t;
+struct Amap_Item_t_
+{
+    int             Type;         // Amap_LibertyType_t
+    int             iLine;        // file line where the item's spec begins
+    Amap_Pair_t     Key;          // key part
+    Amap_Pair_t     Head;         // head part 
+    Amap_Pair_t     Body;         // body part
+    int             Next;         // next item in the list 
+    int             Child;        // first child item 
+};
+
+typedef struct Amap_Tree_t_ Amap_Tree_t;
+struct Amap_Tree_t_
+{
+    char *          pFileName;    // input Liberty file name
+    char *          pContents;    // file contents
+    int             nContents;    // file size
+    int             nLines;       // line counter
+    int             nItems;       // number of items
+    int             nItermAlloc;  // number of items allocated
+    Amap_Item_t *   pItems;       // the items
+    char *          pError;       // the error string
+};
+
+static inline Amap_Item_t *  Amap_LibertyRoot( Amap_Tree_t * p )                                       { return p->pItems;                                                 }
+static inline Amap_Item_t *  Amap_LibertyItem( Amap_Tree_t * p, int v )                                { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v;     }
+static inline int            Amap_LibertyCompare( Amap_Tree_t * p, Amap_Pair_t Pair, char * pStr )     { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ); }
+static inline void           Amap_PrintWord( FILE * pFile, Amap_Tree_t * p, Amap_Pair_t Pair )         { char * pBeg = p->pContents+Pair.Beg, * pEnd = p->pContents+Pair.End; while ( pBeg < pEnd ) fputc( *pBeg++, pFile ); }
+static inline void           Amap_PrintSpace( FILE * pFile, int nOffset )                              { int i; for ( i = 0; i < nOffset; i++ ) fputc(' ', pFile);         }
+static inline int            Amap_LibertyItemId( Amap_Tree_t * p, Amap_Item_t * pItem )                { return pItem - p->pItems;                                         }
+
+#define Amap_ItemForEachChild( p, pItem, pChild ) \
+    for ( pChild = Amap_LibertyItem(p, pItem->Child); pChild; pChild = Amap_LibertyItem(p, pChild->Next) )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prints parse tree in Liberty format.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibertyPrintLibertyItem( FILE * pFile, Amap_Tree_t * p, Amap_Item_t * pItem, int nOffset )
+{
+    if ( pItem->Type == AMAP_LIBERTY_PROC )
+    {
+        Amap_PrintSpace( pFile, nOffset );
+        Amap_PrintWord( pFile, p, pItem->Key );
+        fprintf( pFile, "(" );
+        Amap_PrintWord( pFile, p, pItem->Head );
+        fprintf( pFile, ") {\n" );
+        if ( Amap_LibertyItem(p, pItem->Child) )
+            Amap_LibertyPrintLibertyItem( pFile, p, Amap_LibertyItem(p, pItem->Child), nOffset + 1 );
+        Amap_PrintSpace( pFile, nOffset );
+        fprintf( pFile, "}\n" );
+    }
+    else if ( pItem->Type == AMAP_LIBERTY_EQUA )
+    {
+        Amap_PrintSpace( pFile, nOffset );
+        Amap_PrintWord( pFile, p, pItem->Key );
+        fprintf( pFile, " : " );
+        Amap_PrintWord( pFile, p, pItem->Head );
+        fprintf( pFile, ";\n" );
+    }
+    else if ( pItem->Type == AMAP_LIBERTY_LIST )
+    {
+        Amap_PrintSpace( pFile, nOffset );
+        Amap_PrintWord( pFile, p, pItem->Key );
+        fprintf( pFile, "(" );
+        Amap_PrintWord( pFile, p, pItem->Head );
+        fprintf( pFile, ");\n" );
+    }
+    else assert( 0 );
+    if ( Amap_LibertyItem(p, pItem->Next) )
+        Amap_LibertyPrintLibertyItem( pFile, p, Amap_LibertyItem(p, pItem->Next), nOffset );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints parse tree in Liberty format.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyPrintLiberty( Amap_Tree_t * p, char * pFileName )
+{
+    FILE * pFile;
+    if ( pFileName == NULL )
+        pFile = stdout;
+    else
+    {
+        pFile = fopen( pFileName, "w" );
+        if ( pFile == NULL )
+        {
+            printf( "Amap_LibertyPrintLiberty(): The output file is unavailable (absent or open).\n" );
+            return 0;
+        }
+    }
+    Amap_LibertyPrintLibertyItem( pFile, p, Amap_LibertyRoot(p), 0 );
+    if ( pFile != stdout )
+        fclose( pFile );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the time stamp.]
+
+  Description [The file should be closed.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Amap_LibertyTimeStamp()
+{
+    static char Buffer[100];
+    char * TimeStamp;
+    time_t ltime;
+    // get the current time
+    time( &ltime );
+    TimeStamp = asctime( localtime( &ltime ) );
+    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
+    strcpy( Buffer, TimeStamp );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns cell's function.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyCellIsFlop( Amap_Tree_t * p, Amap_Item_t * pCell )
+{
+    Amap_Item_t * pAttr;
+    Amap_ItemForEachChild( p, pCell, pAttr )
+        if ( !Amap_LibertyCompare(p, pAttr->Key, "ff") ||
+             !Amap_LibertyCompare(p, pAttr->Key, "latch") )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns pin's function.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Item_t * Amap_LibertyPinFunction( Amap_Tree_t * p, Amap_Item_t * pPin )
+{
+    Amap_Item_t * pFunc;
+    Amap_ItemForEachChild( p, pPin, pFunc )
+        if ( !Amap_LibertyCompare(p, pFunc->Key, "function") )
+            return pFunc;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns cell's function.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Item_t * Amap_LibertyCellOutput( Amap_Tree_t * p, Amap_Item_t * pCell )
+{
+    Amap_Item_t * pPin;
+    Amap_ItemForEachChild( p, pCell, pPin )
+    {
+        if ( Amap_LibertyCompare(p, pPin->Key, "pin") )
+            continue;
+        if ( Amap_LibertyPinFunction(p, pPin) )
+            return pPin;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns cell's area.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Item_t * Amap_LibertyCellArea( Amap_Tree_t * p, Amap_Item_t * pCell )
+{
+    Amap_Item_t * pArea;
+    Amap_ItemForEachChild( p, pCell, pArea )
+    {
+        if ( Amap_LibertyCompare(p, pArea->Key, "area") )
+            continue;
+        return pArea;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count cell's output pins (pins with a logic function).]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyCellCountOutputs( Amap_Tree_t * p, Amap_Item_t * pCell )
+{
+    Amap_Item_t * pPin;
+    int Counter = 0;
+    Amap_ItemForEachChild( p, pCell, pPin )
+    {
+        if ( Amap_LibertyCompare(p, pPin->Key, "pin") )
+            continue;
+        if ( Amap_LibertyPinFunction(p, pPin) )
+            Counter++;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets the name to write.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Amap_LibertyGetString( Amap_Tree_t * p, Amap_Pair_t Pair )   
+{ 
+    static char Buffer[256]; 
+    strncpy( Buffer, p->pContents+Pair.Beg, Pair.End-Pair.Beg ); 
+    Buffer[Pair.End-Pair.Beg] = 0;
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets the name to write.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Amap_LibertyGetStringFormula( Amap_Tree_t * p, Amap_Pair_t Pair )   
+{ 
+    static char Buffer[256]; 
+    strncpy( Buffer, p->pContents+Pair.Beg+1, Pair.End-Pair.Beg-2 ); 
+    Buffer[Pair.End-Pair.Beg-2] = 0;
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints parse tree in Genlib format.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyPrintGenlib( Amap_Tree_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Amap_Item_t * pCell, * pArea, * pFunc, * pPin, * pOutput;
+    int Counter;
+    if ( pFileName == NULL )
+        pFile = stdout;
+    else
+    {
+        pFile = fopen( pFileName, "w" );
+        if ( pFile == NULL )
+        {
+            printf( "Amap_LibertyPrintGenlib(): The output file is unavailable (absent or open).\n" );
+            return 0;
+        }
+    }
+    fprintf( pFile, "# This Genlib file was generated by ABC on %s\n", Amap_LibertyTimeStamp() );
+    fprintf( pFile, "# The standard cell library \"%s\" is from Liberty file \"%s\"\n", Amap_LibertyGetString(p, Amap_LibertyRoot(p)->Head), p->pFileName );
+    fprintf( pFile, "# (To find out more about Genlib format, google for \"sis_paper.ps\")\n" );
+
+    fprintf( pFile, "GATE  " );
+    fprintf( pFile, "%16s  ", "_const0_" );
+    fprintf( pFile, "%f  ",   0.0 );
+    fprintf( pFile, "%s=",    "z" );
+    fprintf( pFile, "%s;\n",  "CONST0" );
+
+    fprintf( pFile, "GATE  " );
+    fprintf( pFile, "%16s  ", "_const1_" );
+    fprintf( pFile, "%f  ",   0.0 );
+    fprintf( pFile, "%s=",    "z" );
+    fprintf( pFile, "%s;\n",  "CONST1" );
+
+    Amap_ItemForEachChild( p, Amap_LibertyRoot(p), pCell )
+    {
+/*
+    if ( strcmp(Amap_LibertyGetString(p, pCell->Head), "HA1SVTX1") == 0 )
+    {
+        int s = 0;
+    }
+*/
+        if ( Amap_LibertyCompare(p, pCell->Key, "cell") )
+            continue;
+        if ( Amap_LibertyCellIsFlop(p, pCell) )
+        {
+            printf( "Amap_LibertyPrintGenlib() skipped sequential cell \"%s\".\n", Amap_LibertyGetString(p, pCell->Head) );
+            continue;
+        }
+        Counter = Amap_LibertyCellCountOutputs( p, pCell );
+        if ( Counter == 0 )
+        {
+            printf( "Amap_LibertyPrintGenlib() skipped cell \"%s\" without logic function.\n", Amap_LibertyGetString(p, pCell->Head) );
+            continue;
+        }
+        if ( Counter > 1 )
+        {
+            printf( "Amap_LibertyPrintGenlib() skipped multi-output cell \"%s\".\n", Amap_LibertyGetString(p, pCell->Head) );
+            continue;
+        }
+        pArea = Amap_LibertyCellArea( p, pCell );
+        if ( pArea == NULL )
+        {
+            printf( "Amap_LibertyPrintGenlib() skipped cell \"%s\" with unspecified area.\n", Amap_LibertyGetString(p, pCell->Head) );
+            continue;
+        }
+        pOutput = Amap_LibertyCellOutput( p, pCell );
+        pFunc   = Amap_LibertyPinFunction( p, pOutput );
+
+        fprintf( pFile, "GATE  " );
+        fprintf( pFile, "%16s  ", Amap_LibertyGetString(p, pCell->Head) );
+        fprintf( pFile, "%f  ",   atof(Amap_LibertyGetString(p, pArea->Head)) );
+        fprintf( pFile, "%s=",    Amap_LibertyGetString(p, pOutput->Head) );
+        fprintf( pFile, "%s;\n",  Amap_LibertyGetStringFormula(p, pFunc->Head) );
+
+        Amap_ItemForEachChild( p, pCell, pPin )
+            if ( pPin != pOutput && !Amap_LibertyCompare(p, pPin->Key, "pin") )
+                fprintf( pFile, "    PIN  %13s  UNKNOWN  1  999  1.00  0.00  1.00  0.00\n", Amap_LibertyGetString(p, pPin->Head) );
+    }
+    if ( pFile != stdout )
+        fclose( pFile );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description [The file should be closed.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyFileSize( char * pFileName )
+{
+    FILE * pFile;
+    int nFileSize;
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Amap_LibertyFileSize(): The input file is unavailable (absent or open).\n" );
+        return 0;
+    }
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile ); 
+    fclose( pFile );
+    return nFileSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibertyFixFileHead( char * pFileName )
+{
+    char * pHead;
+    for ( pHead = pFileName; *pHead; pHead++ )
+        if ( *pHead == '>' )
+            *pHead = '\\';
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyCountItems( char * pBeg, char * pEnd )
+{
+    int Counter = 0;
+    for ( ; pBeg < pEnd; pBeg++ )
+        Counter += (*pBeg == '(' || *pBeg == ':');
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes C-style comments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibertyWipeOutComments( char * pBeg, char * pEnd )
+{
+    char * pCur, * pStart;
+    for ( pCur = pBeg; pCur < pEnd; pCur++ )
+    if ( pCur[0] == '/' && pCur[1] == '*' )
+        for ( pStart = pCur; pCur < pEnd; pCur++ )
+        if ( pCur[0] == '*' && pCur[1] == '/' )
+        {
+            for ( ; pStart < pCur + 2; pStart++ )
+            if ( *pStart != '\n' ) *pStart = ' ';
+            break;
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the character is space.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Amap_LibertyCharIsSpace( char c )
+{
+    return c == ' ' || c == '\t' || c == '\r' || c == '\n' || c == '\\';
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Skips spaces.]
+
+  Description [Returns 1 if reached the end.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Amap_LibertySkipSpaces( Amap_Tree_t * p, char ** ppPos, char * pEnd )
+{
+    char * pPos = *ppPos;
+    for ( ; pPos < pEnd; pPos++ )
+    {
+        if ( *pPos == '\n' )
+            p->nLines++;
+        if ( !Amap_LibertyCharIsSpace(*pPos) )
+            break;
+    }
+    *ppPos = pPos;
+    return pPos == pEnd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Skips entry delimited by " :;(){}" ]
+
+  Description [Returns 1 if reached the end.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Amap_LibertySkipEntry( char ** ppPos, char * pEnd )
+{
+    char * pPos = *ppPos;
+    if ( *pPos == '\"' )
+    {
+        for ( pPos++; pPos < pEnd; pPos++ )
+            if ( *pPos == '\"' )
+            {
+                pPos++;
+                break;
+            }
+    }
+    else
+    {
+        for ( ; pPos < pEnd; pPos++ )
+            if ( *pPos == ' ' ||
+                 *pPos == ':' || *pPos == ';' || 
+                 *pPos == '(' || *pPos == ')' || 
+                 *pPos == '{' || *pPos == '}' )
+                break;
+    }
+    *ppPos = pPos;
+    return pPos == pEnd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the matching closing symbol.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline char * Amap_LibertyFindMatch( char * pPos, char * pEnd )
+{
+    int Counter = 0;
+    assert( *pPos == '(' || *pPos == '{' );
+    if ( *pPos == '(' )
+    {
+        for ( ; pPos < pEnd; pPos++ )
+        {
+            if ( *pPos == '(' )
+                Counter++;
+            if ( *pPos == ')' )
+                Counter--;
+            if ( Counter == 0 )
+                break;
+        }
+    }
+    else
+    {
+        for ( ; pPos < pEnd; pPos++ )
+        {
+            if ( *pPos == '{' )
+                Counter++;
+            if ( *pPos == '}' )
+                Counter--;
+            if ( Counter == 0 )
+                break;
+        }
+    }
+    assert( *pPos == ')' || *pPos == '}' );
+    return pPos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the matching closing symbol.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Amap_Pair_t Amap_LibertyUpdateHead( Amap_Tree_t * p, Amap_Pair_t Head )
+{
+    Amap_Pair_t Res;
+    char * pBeg = p->pContents + Head.Beg;
+    char * pEnd = p->pContents + Head.End;
+    char * pFirstNonSpace = NULL;
+    char * pLastNonSpace = NULL;
+    char * pChar;
+    for ( pChar = pBeg; pChar < pEnd; pChar++ )
+    {
+        if ( *pChar == '\n' )
+            p->nLines++;
+        if ( Amap_LibertyCharIsSpace(*pChar) )
+            continue;
+        pLastNonSpace = pChar;
+        if ( pFirstNonSpace == NULL )
+            pFirstNonSpace = pChar;
+    }
+    if ( pFirstNonSpace == NULL || pLastNonSpace == NULL )
+        return Head;
+    assert( pFirstNonSpace && pLastNonSpace );
+    Res.Beg = pFirstNonSpace - p->pContents;
+    Res.End = pLastNonSpace  - p->pContents + 1;
+    return Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns free item.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Amap_Item_t * Amap_LibertyNewItem( Amap_Tree_t * p, int Type )
+{
+    p->pItems[p->nItems].iLine = p->nLines;
+    p->pItems[p->nItems].Type  = Type;
+    p->pItems[p->nItems].Child = -1;
+    p->pItems[p->nItems].Next  = -1;
+    return p->pItems + p->nItems++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns free item.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyBuildItem( Amap_Tree_t * p, char ** ppPos, char * pEnd )
+{
+    Amap_Item_t * pItem;
+    Amap_Pair_t Key, Head, Body;
+    char * pNext, * pStop;
+    if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+        return -2;
+    Key.Beg = *ppPos - p->pContents;
+    if ( Amap_LibertySkipEntry( ppPos, pEnd ) )
+        goto exit;
+    Key.End = *ppPos - p->pContents;
+    if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+        goto exit;
+    pNext = *ppPos;
+    if ( *pNext == ':' )
+    {
+        *ppPos = pNext + 1;
+        if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+            goto exit;
+        Head.Beg = *ppPos - p->pContents;
+        if ( Amap_LibertySkipEntry( ppPos, pEnd ) )
+            goto exit;
+        Head.End = *ppPos - p->pContents;
+        if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+            goto exit;
+        pNext = *ppPos;
+        if ( *pNext != ';' )
+            goto exit;
+        *ppPos = pNext + 1;
+        // end of equation
+        pItem = Amap_LibertyNewItem( p, AMAP_LIBERTY_EQUA );
+        pItem->Key  = Key;
+        pItem->Head = Amap_LibertyUpdateHead( p, Head );
+        pItem->Next = Amap_LibertyBuildItem( p, ppPos, pEnd );
+        if ( pItem->Next == -1 )
+            goto exit;
+        return Amap_LibertyItemId( p, pItem );
+    }
+    if ( *pNext == '(' )
+    {
+        pStop = Amap_LibertyFindMatch( pNext, pEnd );
+        Head.Beg = pNext - p->pContents + 1;
+        Head.End = pStop - p->pContents;
+        *ppPos = pStop + 1;
+        if ( Amap_LibertySkipSpaces( p, ppPos, pEnd ) )
+        {
+            // end of list
+            pItem = Amap_LibertyNewItem( p, AMAP_LIBERTY_LIST );
+            pItem->Key  = Key;
+            pItem->Head = Amap_LibertyUpdateHead( p, Head );
+            return Amap_LibertyItemId( p, pItem );
+        }
+        pNext = *ppPos;
+        if ( *pNext == '{' ) // beginning of body
+        {
+            pStop = Amap_LibertyFindMatch( pNext, pEnd );
+            Body.Beg = pNext - p->pContents + 1;
+            Body.End = pStop - p->pContents;
+            // end of body
+            pItem = Amap_LibertyNewItem( p, AMAP_LIBERTY_PROC );
+            pItem->Key  = Key;
+            pItem->Head = Amap_LibertyUpdateHead( p, Head );
+            pItem->Body = Body;
+            *ppPos = pNext + 1;
+            pItem->Child = Amap_LibertyBuildItem( p, ppPos, pStop );
+            if ( pItem->Child == -1 )
+                goto exit;
+            *ppPos = pStop + 1;
+            pItem->Next = Amap_LibertyBuildItem( p, ppPos, pEnd );
+            if ( pItem->Next == -1 )
+                goto exit;
+            return Amap_LibertyItemId( p, pItem );
+        }
+        // end of list
+        if ( *pNext == ';' )
+            *ppPos = pNext + 1;
+        pItem = Amap_LibertyNewItem( p, AMAP_LIBERTY_LIST );
+        pItem->Key  = Key;
+        pItem->Head = Amap_LibertyUpdateHead( p, Head );
+        pItem->Next = Amap_LibertyBuildItem( p, ppPos, pEnd );
+        if ( pItem->Next == -1 )
+            goto exit;
+        return Amap_LibertyItemId( p, pItem );
+    }
+exit:
+    if ( p->pError == NULL )
+    {
+        p->pError = ABC_ALLOC( char, 1000 );
+        sprintf( p->pError, "File \"%s\". Line %6d. Failed to parse entry \"%s\".\n", 
+            p->pFileName, p->nLines, Amap_LibertyGetString(p, Key) );
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the parsing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Tree_t * Amap_LibertyStart( char * pFileName )
+{
+    FILE * pFile;
+    Amap_Tree_t * p;
+    // start the manager
+    p = ABC_ALLOC( Amap_Tree_t, 1 );
+    memset( p, 0, sizeof(Amap_Tree_t) );
+    // read the file into the buffer
+    Amap_LibertyFixFileHead( pFileName );
+    p->nContents = Amap_LibertyFileSize( pFileName );
+    if ( p->nContents == 0 )
+    {
+        ABC_FREE( p );
+        return NULL;
+    }
+    pFile = fopen( pFileName, "rb" );
+    p->pContents = ABC_ALLOC( char, p->nContents+1 );
+    fread( p->pContents, p->nContents, 1, pFile );
+    fclose( pFile );
+    p->pContents[p->nContents] = 0;
+    // other 
+    p->pFileName = Aig_UtilStrsav( pFileName );
+    p->nItermAlloc = 10 + Amap_LibertyCountItems( p->pContents, p->pContents+p->nContents );
+    p->pItems = ABC_CALLOC( Amap_Item_t, p->nItermAlloc );
+    p->nItems = 0;
+    p->nLines = 1;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the parsing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibertyStop( Amap_Tree_t * p )
+{
+    ABC_FREE( p->pFileName );
+    ABC_FREE( p->pContents );
+    ABC_FREE( p->pItems );
+    ABC_FREE( p->pError );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses the standard cell library in Liberty format.]
+
+  Description [Writes the resulting file in Genlib format.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibertyParse( char * pFileName, char * pFileGenlib, int fVerbose )
+{
+    Amap_Tree_t * p;
+    char * pPos;
+    int clk = clock();
+    int RetValue;
+    p = Amap_LibertyStart( pFileName );
+    if ( p == NULL )
+        return 0;
+    pPos = p->pContents;
+    Amap_LibertyWipeOutComments( p->pContents, p->pContents+p->nContents );
+    if ( Amap_LibertyBuildItem( p, &pPos, p->pContents + p->nContents ) == 0 )
+    {
+        if ( fVerbose )
+        printf( "Parsing finished successfully.\n" );
+//        Amap_LibertyPrintLiberty( p, "temp.lib" );
+        Amap_LibertyPrintGenlib( p, "temp.genlib" );
+        RetValue = 1;
+    }
+    else
+    {
+        if ( p->pError )
+            printf( "%s", p->pError );
+        if ( fVerbose )
+        printf( "Parsing failed.\n" );
+        RetValue = 0;
+    }
+    if ( fVerbose )
+    {
+    printf( "Memory = %7.2f Mb. ", 1.0*(p->nContents+p->nItermAlloc*sizeof(Amap_Item_t))/(1<<20) );
+    ABC_PRT( "Time", clock() - clk );
+    }
+    Amap_LibertyStop( p );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapMan.c b/src/map/amap/amapMan.c
index 521b4ffd..a1a66869 100644
--- a/src/map/amap/amapMan.c
+++ b/src/map/amap/amapMan.c
@@ -43,7 +43,7 @@ Amap_Man_t * Amap_ManStart( int nNodes )
 {
     Amap_Man_t * p;
     // start the manager
-    p = ALLOC( Amap_Man_t, 1 );
+    p = ABC_ALLOC( Amap_Man_t, 1 );
     memset( p, 0, sizeof(Amap_Man_t) );
     p->fEpsilonInternal = (float)0.01;
     // allocate arrays for nodes
@@ -86,10 +86,10 @@ void Amap_ManStop( Amap_Man_t * p )
     Aig_MmFlexStop( p->pMemCuts, 0 );
     Aig_MmFlexStop( p->pMemCutBest, 0 );
     Aig_MmFlexStop( p->pMemTemp, 0 );
-    FREE( p->pMatsTemp );
-    FREE( p->ppCutsTemp );
-    FREE( p->pCutsPi );
-    free( p );
+    ABC_FREE( p->pMatsTemp );
+    ABC_FREE( p->ppCutsTemp );
+    ABC_FREE( p->pCutsPi );
+    ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/amap/amapMatch.c b/src/map/amap/amapMatch.c
index 0b15a931..0ea65219 100644
--- a/src/map/amap/amapMatch.c
+++ b/src/map/amap/amapMatch.c
@@ -122,7 +122,7 @@ void Amap_ManCleanData( Amap_Man_t * p )
     Amap_Obj_t * pObj;
     int i;
 //    Amap_ManForEachNode( p, pObj, i )
-//        FREE( pObj->pData );
+//        ABC_FREE( pObj->pData );
     Amap_ManForEachObj( p, pObj, i )
         pObj->pData = NULL;
 }
@@ -496,7 +496,7 @@ if ( p->pPars->fVerbose )
         Area + nInvs * p->fAreaInv, 
         Area, nInvs * p->fAreaInv, nInvs,
         Amap_ManMaxDelay(p) );
-PRT( "Time ", clock() - clk );
+ABC_PRT( "Time ", clock() - clk );
 }
     // test procedures
 //    Amap_ManForEachNode( p, pObj, i )
diff --git a/src/map/amap/amapMerge.c b/src/map/amap/amapMerge.c
index b024616e..1a6e3804 100644
--- a/src/map/amap/amapMerge.c
+++ b/src/map/amap/amapMerge.c
@@ -44,7 +44,7 @@ Amap_Cut_t * Amap_ManSetupPis( Amap_Man_t * p )
     Amap_Obj_t * pObj;
     Amap_Cut_t * pCut;
     int i, nBytes = sizeof(Amap_Cut_t) + sizeof(int);
-    char * pBuffer = ALLOC( char, Amap_ManPiNum(p) * nBytes );
+    char * pBuffer = ABC_ALLOC( char, Amap_ManPiNum(p) * nBytes );
     Amap_ManForEachPi( p, pObj, i )
     {
         pCut = (Amap_Cut_t *)( pBuffer + i*nBytes );
@@ -509,7 +509,7 @@ void Amap_ManMerge( Amap_Man_t * p )
         printf( "Node =%6d. Try =%9d. Try3 =%10d. Used =%7d. R =%6.2f.  ", 
             Amap_ManNodeNum(p), p->nCutsTried, p->nCutsTried3, p->nCutsUsed, 
             1.0*p->nCutsUsed/Amap_ManNodeNum(p) );
-PRT( "Time ", clock() - clk );
+ABC_PRT( "Time ", clock() - clk );
     }
 }
 
diff --git a/src/map/amap/amapParse.c b/src/map/amap/amapParse.c
index 262fbd5a..48dabca2 100644
--- a/src/map/amap/amapParse.c
+++ b/src/map/amap/amapParse.c
@@ -122,7 +122,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
     }
 
     // copy the formula
-    pFormula = ALLOC( char, strlen(pFormInit) + 3 );
+    pFormula = ABC_ALLOC( char, strlen(pFormInit) + 3 );
     sprintf( pFormula, "(%s)", pFormInit );
 
     // start the stacks
@@ -198,10 +198,10 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
         case AMAP_EQN_SYM_OPEN:
             if ( Flag == AMAP_EQN_FLAG_VAR )
             {
-//                Vec_IntPush( pStackOp, AMAP_EQN_OPER_AND );
-                fprintf( pOutput, "Amap_ParseFormula(): An opening paranthesis follows a var without operation sign.\n" ); 
-                Flag = AMAP_EQN_FLAG_ERROR; 
-                break; 
+                Vec_IntPush( pStackOp, AMAP_EQN_OPER_AND );
+//                fprintf( pOutput, "Amap_ParseFormula(): An opening paranthesis follows a var without operation sign.\n" ); 
+//                Flag = AMAP_EQN_FLAG_ERROR; 
+//              break; 
             }
             Vec_IntPush( pStackOp, AMAP_EQN_OPER_MARK );
             // after an opening bracket, it feels like starting over again
@@ -226,7 +226,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                     if ( Amap_ParseFormulaOper( pMan, pStackFn, Oper ) == NULL )
                     {
                         fprintf( pOutput, "Amap_ParseFormula(): Unknown operation\n" );
-                        free( pFormula );
+                        ABC_FREE( pFormula );
                         return NULL;
                     }
                 }
@@ -247,7 +247,8 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
             for ( i = 0; pTemp[i] && 
                          pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' &&
                          pTemp[i] != AMAP_EQN_SYM_AND && pTemp[i] != AMAP_EQN_SYM_OR && 
-                         pTemp[i] != AMAP_EQN_SYM_XOR && pTemp[i] != AMAP_EQN_SYM_CLOSE; i++ )
+                         pTemp[i] != AMAP_EQN_SYM_XOR && pTemp[i] != AMAP_EQN_SYM_NEGAFT && 
+                         pTemp[i] != AMAP_EQN_SYM_CLOSE; i++ )
               {
                     if ( pTemp[i] == AMAP_EQN_SYM_NEG || pTemp[i] == AMAP_EQN_SYM_OPEN )
                     {
@@ -271,12 +272,17 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                 Flag = AMAP_EQN_FLAG_ERROR; 
                 break; 
             }
+/*
             if ( Flag == AMAP_EQN_FLAG_VAR )
             {
                 fprintf( pOutput, "Amap_ParseFormula(): The variable name \"%s\" follows another var without operation sign.\n", pTemp ); 
                 Flag = AMAP_EQN_FLAG_ERROR; 
                 break; 
             }
+*/
+            if ( Flag == AMAP_EQN_FLAG_VAR )
+                Vec_IntPush( pStackOp, AMAP_EQN_OPER_AND );
+
             Vec_PtrPush( pStackFn, Hop_IthVar( pMan, v ) ); // Cudd_Ref( pbVars[v] );
             Flag = AMAP_EQN_FLAG_VAR; 
             break;
@@ -318,7 +324,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                     if ( Amap_ParseFormulaOper( pMan, pStackFn, Oper2 ) == NULL )
                     {
                         fprintf( pOutput, "Amap_ParseFormula(): Unknown operation\n" );
-                        free( pFormula );
+                        ABC_FREE( pFormula );
                         return NULL;
                     }
                     Vec_IntPush( pStackOp,  Oper1 );     // push the last operation back
@@ -343,7 +349,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                     Vec_PtrFree(pStackFn);
                     Vec_IntFree(pStackOp);
 //                    Cudd_Deref( gFunc );
-                    free( pFormula );
+                    ABC_FREE( pFormula );
                     return gFunc;
                 }
                 else
@@ -354,7 +360,7 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
         else
             fprintf( pOutput, "Amap_ParseFormula(): The input string is empty\n" );
     }
-    free( pFormula );
+    ABC_FREE( pFormula );
     return NULL;
 }
 
@@ -414,7 +420,7 @@ int Amap_LibParseEquations( Amap_Lib_t * p, int fVerbose )
         pTruth = Hop_ManConvertAigToTruth( pMan, pObj, pGate->nPins, vTruth, 0 );
         if ( Kit_TruthSupportSize(pTruth, pGate->nPins) < (int)pGate->nPins )
         {
-            printf( "Skipping gate \"%s\" because its formula \"%s\" does not depend on some pin variables.\n", pGate->pName, pGate->pForm );
+            printf( "Skipping gate \"%s\" because its output \"%s\" does not depend on all input variables.\n", pGate->pName, pGate->pForm );
             continue;
         }
         pGate->pFunc = (unsigned *)Aig_MmFlexEntryFetch( p->pMemGates, sizeof(unsigned)*Aig_TruthWordNum(pGate->nPins) );
@@ -447,7 +453,7 @@ void Amap_LibParseTest( char * pFileName )
         return;
     Amap_LibParseEquations( p, fVerbose );
     Amap_LibFree( p );
-    PRT( "Total time", clock() - clk );
+    ABC_PRT( "Total time", clock() - clk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/amap/amapRead.c b/src/map/amap/amapRead.c
index 182de5d1..7ebc239b 100644
--- a/src/map/amap/amapRead.c
+++ b/src/map/amap/amapRead.c
@@ -89,7 +89,7 @@ char * Amap_LoadFile( char * pFileName )
     // move the file current reading position to the beginning
     rewind( pFile ); 
     // load the contents of the file into memory
-    pBuffer = ALLOC( char, nFileSize + 10 );
+    pBuffer = ABC_ALLOC( char, nFileSize + 10 );
     fread( pBuffer, nFileSize, 1, pFile );
     // terminate the string with '\0'
     pBuffer[ nFileSize ] = '\0';
@@ -173,11 +173,11 @@ Vec_Ptr_t * Amap_DeriveTokens( char * pBuffer )
     Vec_Ptr_t * vTokens;
     char * pToken;
     vTokens = Vec_PtrAlloc( 1000 );
-    pToken = strtok( pBuffer, " ;=\t\r\n" );
+    pToken = strtok( pBuffer, " =\t\r\n" );
     while ( pToken )
     {
         Vec_PtrPush( vTokens, pToken );
-        pToken = strtok( NULL, " ;=\t\r\n" );
+        pToken = strtok( NULL, " =\t\r\n" );
     }
     return vTokens;
 }
@@ -288,6 +288,32 @@ Amap_Gat_t * Amap_ParseGateWithSamePins( Amap_Gat_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Amap_CollectFormulaTokens( Vec_Ptr_t * vTokens, char * pToken, int iPos )
+{
+    char * pNext, * pPrev;
+    pPrev = pToken + strlen(pToken);
+    while ( *(pPrev-1) != ';' )
+    {
+        *pPrev++ = ' ';
+        pNext = Vec_PtrEntry(vTokens, iPos++);
+        while ( *pNext )
+            *pPrev++ = *pNext++;
+    }
+    *(pPrev-1) = 0;
+    return iPos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Amap_Lib_t * Amap_ParseTokens( Vec_Ptr_t * vTokens, int fVerbose )
 {
     Amap_Lib_t * p;
@@ -320,6 +346,7 @@ Amap_Lib_t * Amap_ParseTokens( Vec_Ptr_t * vTokens, int fVerbose )
         pToken = Vec_PtrEntry(vTokens, iPos++);
         pGate->pOutName = Amap_ParseStrsav( p->pMemGates, pToken ); 
         pToken = Vec_PtrEntry(vTokens, iPos++);
+        iPos = Amap_CollectFormulaTokens( vTokens, pToken, iPos );
         pGate->pForm = Amap_ParseStrsav( p->pMemGates, pToken ); 
         // read pins
         Amap_GateForEachPin( pGate, pPin )
@@ -401,7 +428,7 @@ Amap_Lib_t * Amap_LibReadFile( char * pFileName, int fVerbose )
         return NULL;
     pLib->pName = Amap_ParseStrsav( pLib->pMemGates, pFileName );
     Vec_PtrFree( vTokens );
-    free( pBuffer );
+    ABC_FREE( pBuffer );
     return pLib;
 }
 
diff --git a/src/map/amap/amapUniq.c b/src/map/amap/amapUniq.c
index 83fce6a2..e57161e4 100644
--- a/src/map/amap/amapUniq.c
+++ b/src/map/amap/amapUniq.c
@@ -134,7 +134,7 @@ Amap_Nod_t * Amap_LibCreateObj( Amap_Lib_t * p )
     Amap_Nod_t * pNode;
     if ( p->nNodes == p->nNodesAlloc )
     {
-        p->pNodes = REALLOC( Amap_Nod_t, p->pNodes, 2*p->nNodesAlloc );
+        p->pNodes = ABC_REALLOC( Amap_Nod_t, p->pNodes, 2*p->nNodesAlloc );
         p->nNodesAlloc *= 2;
     }
     pNode = Amap_LibNod( p, p->nNodes );
@@ -164,7 +164,7 @@ int Amap_LibCreateVar( Amap_Lib_t * p )
     // start the manager
     assert( p->pNodes == NULL );
     p->nNodesAlloc = 256;
-    p->pNodes = ALLOC( Amap_Nod_t, p->nNodesAlloc );
+    p->pNodes = ABC_ALLOC( Amap_Nod_t, p->nNodesAlloc );
     // create the first node
     pNode = Amap_LibCreateObj( p );
     p->pNodes->Type = AMAP_OBJ_PI;
@@ -281,7 +281,7 @@ int ** Amap_LibLookupTableAlloc( Vec_Ptr_t * vVec, int fVerbose )
     nEntries = nSize = Vec_PtrSize( vVec );
     Vec_PtrForEachEntry( vVec, vOne, i )
         nEntries += Vec_IntSize(vOne);
-    pBuffer = ALLOC( int, nSize * sizeof(void *) + nEntries );
+    pBuffer = ABC_ALLOC( int, nSize * sizeof(void *) + nEntries );
     pRes = (int **)pBuffer;
     pRes[0] = pBuffer + nSize * sizeof(void *);
     nTotal = 0;
diff --git a/src/map/amap/module.make b/src/map/amap/module.make
index d5edadb9..2d534009 100644
--- a/src/map/amap/module.make
+++ b/src/map/amap/module.make
@@ -1,6 +1,7 @@
 SRC +=  src/map/amap/amapCore.c \
     src/map/amap/amapGraph.c \
     src/map/amap/amapLib.c \
+    src/map/amap/amapLiberty.c \
     src/map/amap/amapMan.c \
     src/map/amap/amapMatch.c \
     src/map/amap/amapMerge.c \
diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h
index b2ca4882..0479847c 100644
--- a/src/map/fpga/fpga.h
+++ b/src/map/fpga/fpga.h
@@ -19,10 +19,6 @@
 #ifndef __FPGA_H__
 #define __FPGA_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -31,6 +27,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 // the maximum size of LUTs used for mapping
 #define FPGA_MAX_LUTSIZE   32
 
@@ -52,10 +52,10 @@ typedef struct Fpga_LutLibStruct_t_      Fpga_LutLib_t;
 ///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
  
-#define Fpga_IsComplement(p)    (((int)((PORT_PTRUINT_T) (p) & 01)))
-#define Fpga_Regular(p)         ((Fpga_Node_t *)((PORT_PTRUINT_T)(p) & ~01)) 
-#define Fpga_Not(p)             ((Fpga_Node_t *)((PORT_PTRUINT_T)(p) ^ 01)) 
-#define Fpga_NotCond(p,c)       ((Fpga_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)))
+#define Fpga_IsComplement(p)    (((int)((ABC_PTRUINT_T) (p) & 01)))
+#define Fpga_Regular(p)         ((Fpga_Node_t *)((ABC_PTRUINT_T)(p) & ~01)) 
+#define Fpga_Not(p)             ((Fpga_Node_t *)((ABC_PTRUINT_T)(p) ^ 01)) 
+#define Fpga_NotCond(p,c)       ((Fpga_Node_t *)((ABC_PTRUINT_T)(p) ^ (c)))
 
 #define Fpga_Ref(p)   
 #define Fpga_Deref(p)
diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c
index 634a8eb1..17feac7c 100644
--- a/src/map/fpga/fpgaCore.c
+++ b/src/map/fpga/fpgaCore.c
@@ -72,7 +72,7 @@ int Fpga_Mapping( Fpga_Man_t * p )
     if ( !Fpga_MappingPostProcess( p ) )
         return 0;
     p->timeRecover = clock() - clk;
-//PRT( "Total mapping time", clock() - clkTotal );
+//ABC_PRT( "Total mapping time", clock() - clkTotal );
 
     s_MappingTime = clock() - clkTotal;
     s_MappingMem = Fpga_CutCountAll(p) * (sizeof(Fpga_Cut_t) - sizeof(int) * (FPGA_MAX_LEAVES - p->nVarsMax));
@@ -83,7 +83,7 @@ int Fpga_Mapping( Fpga_Man_t * p )
 //        Fpga_MappingPrintOutputArrivals( p );
     if ( p->fVerbose )
     {
-        PRT( "Total time", clock() - clkTotal );
+        ABC_PRT( "Total time", clock() - clkTotal );
     }
     return 1;
 }
@@ -125,7 +125,7 @@ printf( "Switch = %8.1f  ", Fpga_MappingGetSwitching(p,p->vMapping) );
 else
 printf( "Delay = %5.2f  ", Fpga_TimeComputeArrivalMax(p) );
 
-PRT( "Time", p->timeMatch );
+ABC_PRT( "Time", p->timeMatch );
 }
 
     if ( !p->fAreaRecovery )
@@ -150,7 +150,7 @@ if ( fShowSwitching )
 printf( "Switch = %8.1f  ", Fpga_MappingGetSwitching(p,p->vMapping) );
 else
 printf( "Delay = %5.2f  ", Fpga_TimeComputeArrivalMax(p) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
     }
 
@@ -177,7 +177,7 @@ if ( fShowSwitching )
 printf( "Switch = %8.1f  ", Fpga_MappingGetSwitching(p,p->vMapping) );
 else
 printf( "Delay = %5.2f  ", Fpga_TimeComputeArrivalMax(p) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
     }
 
diff --git a/src/map/fpga/fpgaCreate.c b/src/map/fpga/fpgaCreate.c
index c0bae1c7..5245f050 100644
--- a/src/map/fpga/fpgaCreate.c
+++ b/src/map/fpga/fpgaCreate.c
@@ -28,7 +28,7 @@ static void            Fpga_TableResize( Fpga_Man_t * p );
 static Fpga_Node_t *   Fpga_TableLookup( Fpga_Man_t * p, Fpga_Node_t * p1, Fpga_Node_t * p2 );
 
 // hash key for the structural hash table
-static inline unsigned Fpga_HashKey2( Fpga_Node_t * p0, Fpga_Node_t * p1, int TableSize ) { return (unsigned)(((PORT_PTRUINT_T)(p0) + (PORT_PTRUINT_T)(p1) * 12582917) % TableSize); }
+static inline unsigned Fpga_HashKey2( Fpga_Node_t * p0, Fpga_Node_t * p1, int TableSize ) { return (unsigned)(((ABC_PTRUINT_T)(p0) + (ABC_PTRUINT_T)(p1) * 12582917) % TableSize); }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -167,7 +167,7 @@ Fpga_Man_t * Fpga_ManCreate( int nInputs, int nOutputs, int fVerbose )
     int i;
 
     // start the manager
-    p = ALLOC( Fpga_Man_t, 1 );
+    p = ABC_ALLOC( Fpga_Man_t, 1 );
     memset( p, 0, sizeof(Fpga_Man_t) );
     p->pLutLib   = Abc_FrameReadLibLut();
     p->nVarsMax  = p->pLutLib->LutMax;
@@ -193,13 +193,13 @@ Fpga_Man_t * Fpga_ManCreate( int nInputs, int nOutputs, int fVerbose )
 
     // create the PI nodes
     p->nInputs = nInputs;
-    p->pInputs = ALLOC( Fpga_Node_t *, nInputs );
+    p->pInputs = ABC_ALLOC( Fpga_Node_t *, nInputs );
     for ( i = 0; i < nInputs; i++ )
         p->pInputs[i] = Fpga_NodeCreate( p, NULL, NULL );
 
     // create the place for the output nodes
     p->nOutputs = nOutputs;
-    p->pOutputs = ALLOC( Fpga_Node_t *, nOutputs );
+    p->pOutputs = ABC_ALLOC( Fpga_Node_t *, nOutputs );
     memset( p->pOutputs, 0, sizeof(Fpga_Node_t *) * nOutputs );
     return p;
 }
@@ -230,12 +230,12 @@ void Fpga_ManFree( Fpga_Man_t * p )
         Fpga_NodeVecFree( p->vNodesAll );
     Extra_MmFixedStop( p->mmNodes );
     Extra_MmFixedStop( p->mmCuts );
-    FREE( p->ppOutputNames );
-    FREE( p->pInputArrivals );
-    FREE( p->pInputs );
-    FREE( p->pOutputs );
-    FREE( p->pBins );
-    FREE( p );
+    ABC_FREE( p->ppOutputNames );
+    ABC_FREE( p->pInputArrivals );
+    ABC_FREE( p->pInputs );
+    ABC_FREE( p->pOutputs );
+    ABC_FREE( p->pBins );
+    ABC_FREE( p );
 }
 
 
@@ -269,14 +269,14 @@ void Fpga_ManPrintTimeStats( Fpga_Man_t * p )
 
 //    printf( "N-canonical = %d. Matchings = %d.  ", p->nCanons, p->nMatches );
 //    printf( "Choice nodes = %d. Choices = %d.\n", p->nChoiceNodes, p->nChoices );
-    PRT( "ToMap", p->timeToMap );
-    PRT( "Cuts ", p->timeCuts );
-    PRT( "Match", p->timeMatch );
-    PRT( "Area ", p->timeRecover );
-    PRT( "ToNet", p->timeToNet );
-    PRT( "TOTAL", p->timeTotal );
-    if ( p->time1 ) { PRT( "time1", p->time1 ); }
-    if ( p->time2 ) { PRT( "time2", p->time2 ); }
+    ABC_PRT( "ToMap", p->timeToMap );
+    ABC_PRT( "Cuts ", p->timeCuts );
+    ABC_PRT( "Match", p->timeMatch );
+    ABC_PRT( "Area ", p->timeRecover );
+    ABC_PRT( "ToNet", p->timeToNet );
+    ABC_PRT( "TOTAL", p->timeTotal );
+    if ( p->time1 ) { ABC_PRT( "time1", p->time1 ); }
+    if ( p->time2 ) { ABC_PRT( "time2", p->time2 ); }
 }
 
 /**Function*************************************************************
@@ -344,7 +344,7 @@ void Fpga_TableCreate( Fpga_Man_t * pMan )
 {
     assert( pMan->pBins == NULL );
     pMan->nBins = Cudd_Prime(50000);
-    pMan->pBins = ALLOC( Fpga_Node_t *, pMan->nBins );
+    pMan->pBins = ABC_ALLOC( Fpga_Node_t *, pMan->nBins );
     memset( pMan->pBins, 0, sizeof(Fpga_Node_t *) * pMan->nBins );
     pMan->nNodes = 0;
 }
@@ -429,7 +429,7 @@ clk = clock();
     // get the new table size
     nBinsNew = Cudd_Prime(2 * pMan->nBins); 
     // allocate a new array
-    pBinsNew = ALLOC( Fpga_Node_t *, nBinsNew );
+    pBinsNew = ABC_ALLOC( Fpga_Node_t *, nBinsNew );
     memset( pBinsNew, 0, sizeof(Fpga_Node_t *) * nBinsNew );
     // rehash the entries from the old table
     Counter = 0;
@@ -446,10 +446,10 @@ clk = clock();
     if ( pMan->fVerbose )
     {
 //        printf( "Increasing the unique table size from %6d to %6d. ", pMan->nBins, nBinsNew );
-//        PRT( "Time", clock() - clk );
+//        ABC_PRT( "Time", clock() - clk );
     }
     // replace the table and the parameters
-    free( pMan->pBins );
+    ABC_FREE( pMan->pBins );
     pMan->pBins = pBinsNew;
     pMan->nBins = nBinsNew;
 }
diff --git a/src/map/fpga/fpgaCut.c b/src/map/fpga/fpgaCut.c
index de558456..a9108871 100644
--- a/src/map/fpga/fpgaCut.c
+++ b/src/map/fpga/fpgaCut.c
@@ -157,7 +157,7 @@ void Fpga_MappingCuts( Fpga_Man_t * p )
         nCuts = Fpga_CutCountAll(p);
         printf( "Nodes = %6d. Total %d-cuts = %d. Cuts per node = %.1f. ", 
                p->nNodes, p->nVarsMax, nCuts, ((float)nCuts)/p->nNodes );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
 
     // print the cuts for the first primary output
@@ -913,15 +913,15 @@ Fpga_CutTable_t * Fpga_CutTableStart( Fpga_Man_t * pMan )
 {
     Fpga_CutTable_t * p;
     // allocate the table
-    p = ALLOC( Fpga_CutTable_t, 1 );
+    p = ABC_ALLOC( Fpga_CutTable_t, 1 );
     memset( p, 0, sizeof(Fpga_CutTable_t) );
     p->nBins = Cudd_Prime( 10 * FPGA_CUTS_MAX_COMPUTE );
-    p->pBins = ALLOC( Fpga_Cut_t *, p->nBins );
+    p->pBins = ABC_ALLOC( Fpga_Cut_t *, p->nBins );
     memset( p->pBins, 0, sizeof(Fpga_Cut_t *) * p->nBins );
-    p->pCuts = ALLOC( int, 2 * FPGA_CUTS_MAX_COMPUTE );
-    p->pArray = ALLOC( Fpga_Cut_t *, 2 * FPGA_CUTS_MAX_COMPUTE );
-    p->pCuts1 = ALLOC( Fpga_Cut_t *, 2 * FPGA_CUTS_MAX_COMPUTE );
-    p->pCuts2 = ALLOC( Fpga_Cut_t *, 2 * FPGA_CUTS_MAX_COMPUTE );
+    p->pCuts = ABC_ALLOC( int, 2 * FPGA_CUTS_MAX_COMPUTE );
+    p->pArray = ABC_ALLOC( Fpga_Cut_t *, 2 * FPGA_CUTS_MAX_COMPUTE );
+    p->pCuts1 = ABC_ALLOC( Fpga_Cut_t *, 2 * FPGA_CUTS_MAX_COMPUTE );
+    p->pCuts2 = ABC_ALLOC( Fpga_Cut_t *, 2 * FPGA_CUTS_MAX_COMPUTE );
     return p;
 }
 
@@ -938,12 +938,12 @@ Fpga_CutTable_t * Fpga_CutTableStart( Fpga_Man_t * pMan )
 ***********************************************************************/
 void Fpga_CutTableStop( Fpga_CutTable_t * p )
 {
-    free( p->pCuts1 );
-    free( p->pCuts2 );
-    free( p->pArray );
-    free( p->pBins );
-    free( p->pCuts );
-    free( p );
+    ABC_FREE( p->pCuts1 );
+    ABC_FREE( p->pCuts2 );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p->pBins );
+    ABC_FREE( p->pCuts );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -1115,7 +1115,7 @@ Fpga_Cut_t * Fpga_CutSortCuts( Fpga_Man_t * pMan, Fpga_CutTable_t * p, Fpga_Cut_
     if ( nCuts > FPGA_CUTS_MAX_USE - 1 )
     {
 //        printf( "*" );
-        // free the remaining cuts
+        // ABC_FREE the remaining cuts
         for ( i = FPGA_CUTS_MAX_USE - 1; i < nCuts; i++ )
             Extra_MmFixedEntryRecycle( pMan->mmCuts, (char *)p->pCuts1[i] );
         // update the number of cuts
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index f4145e7f..ba9538c2 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -63,19 +63,19 @@
 #define FPGA_INT_LARGE            (10000000)
 
 // the macro to compute the signature
-#define FPGA_SEQ_SIGN(p)        (1 << (((PORT_PTRUINT_T)p)%31));
+#define FPGA_SEQ_SIGN(p)        (1 << (((ABC_PTRUINT_T)p)%31));
 
 // internal macros to work with cuts
-#define Fpga_CutIsComplement(p)  (((int)((PORT_PTRUINT_T)(p) & 01)))
-#define Fpga_CutRegular(p)       ((Fpga_Cut_t *)((PORT_PTRUINT_T)(p) & ~01)) 
-#define Fpga_CutNot(p)           ((Fpga_Cut_t *)((PORT_PTRUINT_T)(p) ^ 01)) 
-#define Fpga_CutNotCond(p,c)     ((Fpga_Cut_t *)((PORT_PTRUINT_T)(p) ^ (c)))
+#define Fpga_CutIsComplement(p)  (((int)((ABC_PTRUINT_T)(p) & 01)))
+#define Fpga_CutRegular(p)       ((Fpga_Cut_t *)((ABC_PTRUINT_T)(p) & ~01)) 
+#define Fpga_CutNot(p)           ((Fpga_Cut_t *)((ABC_PTRUINT_T)(p) ^ 01)) 
+#define Fpga_CutNotCond(p,c)     ((Fpga_Cut_t *)((ABC_PTRUINT_T)(p) ^ (c)))
 
 // the cut nodes
-#define Fpga_SeqIsComplement( p )      (((int)((PORT_PTRUINT_T) (p) & 01)))
-#define Fpga_SeqRegular( p )           ((Fpga_Node_t *)((PORT_PTRUINT_T)(p) & ~015))
-#define Fpga_SeqIndex( p )             ((((PORT_PTRUINT_T)(p)) >> 1) & 07)
-#define Fpga_SeqIndexCreate( p, Ind )  (((PORT_PTRUINT_T)(p)) | (1 << (((PORT_PTRUINT_T)(Ind)) & 07)))
+#define Fpga_SeqIsComplement( p )      (((int)((ABC_PTRUINT_T) (p) & 01)))
+#define Fpga_SeqRegular( p )           ((Fpga_Node_t *)((ABC_PTRUINT_T)(p) & ~015))
+#define Fpga_SeqIndex( p )             ((((ABC_PTRUINT_T)(p)) >> 1) & 07)
+#define Fpga_SeqIndexCreate( p, Ind )  (((ABC_PTRUINT_T)(p)) | (1 << (((ABC_PTRUINT_T)(Ind)) & 07)))
 
 // internal macros for referencing of nodes
 #define Fpga_NodeReadRef(p)      ((Fpga_Regular(p))->nRefs)
diff --git a/src/map/fpga/fpgaLib.c b/src/map/fpga/fpgaLib.c
index b9615a8c..d5b12293 100644
--- a/src/map/fpga/fpgaLib.c
+++ b/src/map/fpga/fpgaLib.c
@@ -66,7 +66,7 @@ Fpga_LutLib_t * Fpga_LutLibRead( char * FileName, int fVerbose )
         return NULL;
     }
 
-    p = ALLOC( Fpga_LutLib_t, 1 );
+    p = ABC_ALLOC( Fpga_LutLib_t, 1 );
     memset( p, 0, sizeof(Fpga_LutLib_t) );
     p->pName = Extra_UtilStrsav( FileName );
 
@@ -81,7 +81,7 @@ Fpga_LutLib_t * Fpga_LutLibRead( char * FileName, int fVerbose )
         if ( i != atoi(pToken) )
         {
             printf( "Error in the LUT library file \"%s\".\n", FileName );
-            free( p );
+            ABC_FREE( p );
             return NULL;
         }
 
@@ -162,7 +162,7 @@ Fpga_LutLib_t * Fpga_LutLibRead( char * FileName, int fVerbose )
 Fpga_LutLib_t * Fpga_LutLibDup( Fpga_LutLib_t * p )
 {
     Fpga_LutLib_t * pNew;
-    pNew = ALLOC( Fpga_LutLib_t, 1 );
+    pNew = ABC_ALLOC( Fpga_LutLib_t, 1 );
     *pNew = *p;
     pNew->pName = Extra_UtilStrsav( pNew->pName );
     return pNew;
@@ -183,8 +183,8 @@ void Fpga_LutLibFree( Fpga_LutLib_t * pLutLib )
 {
     if ( pLutLib == NULL )
         return;
-    FREE( pLutLib->pName );
-    FREE( pLutLib );
+    ABC_FREE( pLutLib->pName );
+    ABC_FREE( pLutLib );
 }
 
 
diff --git a/src/map/fpga/fpgaTruth.c b/src/map/fpga/fpgaTruth.c
index 8ffb7819..7eca8e3e 100644
--- a/src/map/fpga/fpgaTruth.c
+++ b/src/map/fpga/fpgaTruth.c
@@ -44,7 +44,7 @@ DdNode * Fpga_TruthsCutBdd_rec( DdManager * dd, Fpga_Cut_t * pCut, Fpga_NodeVec_
     assert( !Fpga_IsComplement(pCut) );
     // if the cut is visited, return the result
     if ( pCut->uSign )
-        return (DdNode *)(PORT_PTRUINT_T)pCut->uSign;
+        return (DdNode *)(ABC_PTRUINT_T)pCut->uSign;
     // compute the functions of the children
     bFunc0 = Fpga_TruthsCutBdd_rec( dd, Fpga_CutRegular(pCut->pOne), vVisited );   Cudd_Ref( bFunc0 );
     bFunc0 = Cudd_NotCond( bFunc0, Fpga_CutIsComplement(pCut->pOne) );
@@ -56,7 +56,7 @@ DdNode * Fpga_TruthsCutBdd_rec( DdManager * dd, Fpga_Cut_t * pCut, Fpga_NodeVec_
     Cudd_RecursiveDeref( dd, bFunc0 );
     Cudd_RecursiveDeref( dd, bFunc1 );
     assert( pCut->uSign == 0 );
-    pCut->uSign = (unsigned)(PORT_PTRUINT_T)bFunc;
+    pCut->uSign = (unsigned)(ABC_PTRUINT_T)bFunc;
     // add this cut to the visited list
     Fpga_NodeVecPush( vVisited, (Fpga_Node_t *)pCut );
     return bFunc;
@@ -81,7 +81,7 @@ void * Fpga_TruthsCutBdd( void * dd, Fpga_Cut_t * pCut )
     assert( pCut->nLeaves > 1 );
     // set the leaf variables
     for ( i = 0; i < pCut->nLeaves; i++ )
-        pCut->ppLeaves[i]->pCuts->uSign = (unsigned)(PORT_PTRUINT_T)Cudd_bddIthVar( dd, i );
+        pCut->ppLeaves[i]->pCuts->uSign = (unsigned)(ABC_PTRUINT_T)Cudd_bddIthVar( dd, i );
     // recursively compute the function
     vVisited = Fpga_NodeVecAlloc( 10 );
     bFunc = Fpga_TruthsCutBdd_rec( dd, pCut, vVisited );   Cudd_Ref( bFunc );
@@ -91,7 +91,7 @@ void * Fpga_TruthsCutBdd( void * dd, Fpga_Cut_t * pCut )
     for ( i = 0; i < vVisited->nSize; i++ )
     {
         pCut = (Fpga_Cut_t *)vVisited->pArray[i];
-        Cudd_RecursiveDeref( dd, (DdNode*)(PORT_PTRUINT_T)pCut->uSign );
+        Cudd_RecursiveDeref( dd, (DdNode*)(ABC_PTRUINT_T)pCut->uSign );
         pCut->uSign = 0;
     }
 //    printf( "%d ", vVisited->nSize );
diff --git a/src/map/fpga/fpgaUtils.c b/src/map/fpga/fpgaUtils.c
index 77c2e2b0..f360254b 100644
--- a/src/map/fpga/fpgaUtils.c
+++ b/src/map/fpga/fpgaUtils.c
@@ -305,7 +305,7 @@ float Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan )
 
     // allocate place to store the nodes
     LevelMax = Fpga_MappingMaxLevel( pMan );
-    ppStore = ALLOC( Fpga_Node_t *, LevelMax + 1 );
+    ppStore = ABC_ALLOC( Fpga_Node_t *, LevelMax + 1 );
     memset( ppStore, 0, sizeof(Fpga_Node_t *) * (LevelMax + 1) );
 
     // collect nodes reachable from POs in the DFS order through the best cuts
@@ -324,7 +324,7 @@ float Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan )
     for ( i = LevelMax; i >= 0; i-- )
         for ( pNode = ppStore[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 )
             Fpga_NodeVecPush( pMan->vMapping, pNode );
-    free( ppStore );
+    ABC_FREE( ppStore );
     return aArea;
 }
 
diff --git a/src/map/fpga/fpgaVec.c b/src/map/fpga/fpgaVec.c
index 79b6b43d..b17697dd 100644
--- a/src/map/fpga/fpgaVec.c
+++ b/src/map/fpga/fpgaVec.c
@@ -42,12 +42,12 @@ static int Fpga_NodeVecCompareLevels( Fpga_Node_t ** pp1, Fpga_Node_t ** pp2 );
 Fpga_NodeVec_t * Fpga_NodeVecAlloc( int nCap )
 {
     Fpga_NodeVec_t * p;
-    p = ALLOC( Fpga_NodeVec_t, 1 );
+    p = ABC_ALLOC( Fpga_NodeVec_t, 1 );
     if ( nCap > 0 && nCap < 16 )
         nCap = 16;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( Fpga_Node_t *, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( Fpga_Node_t *, p->nCap ) : NULL;
     return p;
 }
 
@@ -64,8 +64,8 @@ Fpga_NodeVec_t * Fpga_NodeVecAlloc( int nCap )
 ***********************************************************************/
 void Fpga_NodeVecFree( Fpga_NodeVec_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -115,7 +115,7 @@ void Fpga_NodeVecGrow( Fpga_NodeVec_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( Fpga_Node_t *, p->pArray, nCapMin ); 
+    p->pArray = ABC_REALLOC( Fpga_Node_t *, p->pArray, nCapMin ); 
     p->nCap   = nCapMin;
 }
 
diff --git a/src/map/if/if.h b/src/map/if/if.h
index ce2cb483..91d6e037 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -21,10 +21,6 @@
 #ifndef __IF_H__
 #define __IF_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -38,6 +34,10 @@ extern "C" {
 #include "mem.h"
 #include "tim.h"
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
@@ -166,7 +166,7 @@ struct If_Man_t_
     Mem_Fixed_t *      pMemSet;       // memory manager for sets of cuts (entrysize = nCutSize*(nCutsMax+1))
     If_Set_t *         pMemCi;        // memory for CI cutsets
     If_Set_t *         pMemAnd;       // memory for AND cutsets
-    If_Set_t *         pFreeList;     // the list of free cutsets
+    If_Set_t *         pFreeList;     // the list of ABC_FREE cutsets
     int                nSmallSupp;    // the small support
     // timing manager
     Tim_Man_t *        pManTim;
@@ -198,7 +198,7 @@ struct If_Set_t_
 {
     short              nCutsMax;      // the max number of cuts
     short              nCuts;         // the current number of cuts
-    If_Set_t *         pNext;         // next cutset in the free list
+    If_Set_t *         pNext;         // next cutset in the ABC_FREE list
     If_Cut_t **        ppCuts;        // the array of pointers to the cuts
 };
 
@@ -229,10 +229,10 @@ struct If_Obj_t_
     If_Cut_t           CutBest;       // the best cut selected 
 };
 
-static inline If_Obj_t * If_Regular( If_Obj_t * p )                          { return (If_Obj_t *)((PORT_PTRUINT_T)(p) & ~01);  }
-static inline If_Obj_t * If_Not( If_Obj_t * p )                              { return (If_Obj_t *)((PORT_PTRUINT_T)(p) ^  01);  }
-static inline If_Obj_t * If_NotCond( If_Obj_t * p, int c )                   { return (If_Obj_t *)((PORT_PTRUINT_T)(p) ^ (c));  }
-static inline int        If_IsComplement( If_Obj_t * p )                     { return (int )(((PORT_PTRUINT_T)p) & 01);         }
+static inline If_Obj_t * If_Regular( If_Obj_t * p )                          { return (If_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);  }
+static inline If_Obj_t * If_Not( If_Obj_t * p )                              { return (If_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);  }
+static inline If_Obj_t * If_NotCond( If_Obj_t * p, int c )                   { return (If_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));  }
+static inline int        If_IsComplement( If_Obj_t * p )                     { return (int )(((ABC_PTRUINT_T)p) & 01);         }
 
 static inline int        If_ManCiNum( If_Man_t * p )                         { return p->nObjs[IF_CI];               }
 static inline int        If_ManCoNum( If_Man_t * p )                         { return p->nObjs[IF_CO];               }
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index 99b99af7..0f0ca002 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -134,7 +134,7 @@ int If_ManPerformMappingComb( If_Man_t * p )
 //        printf( "Total memory = %7.2f Mb. Peak cut memory = %7.2f Mb.  ", 
 //            1.0 * (p->nObjBytes + 2*sizeof(void *)) * If_ManObjNum(p) / (1<<20), 
 //            1.0 * p->nSetBytes * Mem_FixedReadMaxEntriesUsed(p->pMemSet) / (1<<20) );
-        PRT( "Total time", clock() - clkTotal );
+        ABC_PRT( "Total time", clock() - clkTotal );
     }
 //    printf( "Cross cut memory = %d.\n", Mem_FixedReadMaxEntriesUsed(p->pMemSet) );
     s_MappingTime = clock() - clkTotal;
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index af1f5213..d3ce5397 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -1349,7 +1349,7 @@ int If_CutGetCones( If_Man_t * p )
         }
     }
     printf( "Cound not find boundary for %d nodes.\n", Counter );
-    PRT( "Cones", clock() - clk );
+    ABC_PRT( "Cones", clock() - clk );
     return 1;
 }
 
@@ -1406,7 +1406,7 @@ int If_CutCountTotalFanins( If_Man_t * p )
         }
     }
     printf( "Total cut inputs = %d. Total fanins incremental = %d.\n", nFaninsTotal, Counter );
-    PRT( "Fanins", clock() - clk );
+    ABC_PRT( "Fanins", clock() - clk );
     Vec_IntFree( vLeaves );
     return 1;
 }
diff --git a/src/map/if/ifLib.c b/src/map/if/ifLib.c
index 51630164..176edb24 100644
--- a/src/map/if/ifLib.c
+++ b/src/map/if/ifLib.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline char * If_UtilStrsav( char *s ) {  return !s ? s : strcpy(ALLOC(char, strlen(s)+1), s);  }
+static inline char * If_UtilStrsav( char *s ) {  return !s ? s : strcpy(ABC_ALLOC(char, strlen(s)+1), s);  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -55,7 +55,7 @@ If_Lib_t * If_LutLibRead( char * FileName )
         return NULL;
     }
 
-    p = ALLOC( If_Lib_t, 1 );
+    p = ABC_ALLOC( If_Lib_t, 1 );
     memset( p, 0, sizeof(If_Lib_t) );
     p->pName = If_UtilStrsav( FileName );
 
@@ -70,7 +70,7 @@ If_Lib_t * If_LutLibRead( char * FileName )
         if ( i != atoi(pToken) )
         {
             printf( "Error in the LUT library file \"%s\".\n", FileName );
-            free( p );
+            ABC_FREE( p );
             return NULL;
         }
 
@@ -145,7 +145,7 @@ If_Lib_t * If_LutLibRead( char * FileName )
 If_Lib_t * If_LutLibDup( If_Lib_t * p )
 {
     If_Lib_t * pNew;
-    pNew = ALLOC( If_Lib_t, 1 );
+    pNew = ABC_ALLOC( If_Lib_t, 1 );
     *pNew = *p;
     pNew->pName = If_UtilStrsav( pNew->pName );
     return pNew;
@@ -166,8 +166,8 @@ void If_LutLibFree( If_Lib_t * pLutLib )
 {
     if ( pLutLib == NULL )
         return;
-    FREE( pLutLib->pName );
-    FREE( pLutLib );
+    ABC_FREE( pLutLib->pName );
+    ABC_FREE( pLutLib );
 }
 
 
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 82ee6728..97f2a06a 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -48,7 +48,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
 {
     If_Man_t * p;
     // start the manager
-    p = ALLOC( If_Man_t, 1 );
+    p = ABC_ALLOC( If_Man_t, 1 );
     memset( p, 0, sizeof(If_Man_t) );
     p->pPars = pPars;
     p->fEpsilon = pPars->Epsilon;
@@ -71,7 +71,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
         printf( "K = %d. Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d.\n", 
             p->pPars->nLutSize, 4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes );
     // room for temporary truth tables
-    p->puTemp[0] = p->pPars->fTruth? ALLOC( unsigned, 4 * p->nTruthWords ) : NULL;
+    p->puTemp[0] = p->pPars->fTruth? ABC_ALLOC( unsigned, 4 * p->nTruthWords ) : NULL;
     p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
     p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
     p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
@@ -96,7 +96,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
 ***********************************************************************/
 void If_ManRestart( If_Man_t * p )
 {
-    FREE( p->pMemCi );
+    ABC_FREE( p->pMemCi );
     Vec_PtrClear( p->vCis );
     Vec_PtrClear( p->vCos );
     Vec_PtrClear( p->vObjs );
@@ -124,7 +124,7 @@ void If_ManRestart( If_Man_t * p )
 ***********************************************************************/
 void If_ManStop( If_Man_t * p )
 {
-//    PRT( "Truth", p->timeTruth );
+//    ABC_PRT( "Truth", p->timeTruth );
 //    printf( "Small support = %d.\n", p->nSmallSupp );
     Vec_PtrFree( p->vCis );
     Vec_PtrFree( p->vCos );
@@ -135,19 +135,19 @@ void If_ManStop( If_Man_t * p )
     if ( p->vLatchOrder ) Vec_PtrFree( p->vLatchOrder );
     if ( p->vLags )       Vec_IntFree( p->vLags );
     Mem_FixedStop( p->pMemObj, 0 );
-    FREE( p->pMemCi );
-    FREE( p->pMemAnd );
-    FREE( p->puTemp[0] );
-    // free pars memory
+    ABC_FREE( p->pMemCi );
+    ABC_FREE( p->pMemAnd );
+    ABC_FREE( p->puTemp[0] );
+    // ABC_FREE pars memory
     if ( p->pPars->pTimesArr )
-        FREE( p->pPars->pTimesArr );
+        ABC_FREE( p->pPars->pTimesArr );
     if ( p->pPars->pTimesReq )
-        FREE( p->pPars->pTimesReq );
+        ABC_FREE( p->pPars->pTimesReq );
     if ( p->pManTim )
         Tim_ManStop( p->pManTim );
     if ( p->vSwitching )
         Vec_IntFree( p->vSwitching );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -427,7 +427,7 @@ void If_ManSetupCiCutSets( If_Man_t * p )
     If_ManForEachCi( p, pObj, i )
         If_ManSetupCutTriv( p, &pObj->CutBest, pObj->Id );
     // create elementary cutsets for the CIs
-    p->pMemCi = (If_Set_t *)malloc( If_ManCiNum(p) * (sizeof(If_Set_t) + sizeof(void *)) );
+    p->pMemCi = (If_Set_t *)ABC_ALLOC( char, If_ManCiNum(p) * (sizeof(If_Set_t) + sizeof(void *)) );
     If_ManForEachCi( p, pObj, i )
     {
         pObj->pCutSet = (If_Set_t *)((char *)p->pMemCi + i * (sizeof(If_Set_t) + sizeof(void *)));
@@ -552,7 +552,7 @@ void If_ManSetupSetAll( If_Man_t * p, int nCrossCut )
     If_Set_t * pCutSet;
     int i, nCutSets;
     nCutSets = 128 + nCrossCut;
-    p->pFreeList = p->pMemAnd = pCutSet = (If_Set_t *)malloc( nCutSets * p->nSetBytes );
+    p->pFreeList = p->pMemAnd = pCutSet = (If_Set_t *)ABC_ALLOC( char, nCutSets * p->nSetBytes );
     for ( i = 0; i < nCutSets; i++ )
     {
         If_ManSetupSet( p, pCutSet );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index fc3d7cd3..2879081c 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -106,7 +106,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
     If_ObjForEachCut( pObj->pFanin0, pCut0, i )
     If_ObjForEachCut( pObj->pFanin1, pCut1, k )
     {
-        // get the next free cut
+        // get the next ABC_FREE cut
         assert( pCutSet->nCuts <= pCutSet->nCutsMax );
         pCut = pCutSet->ppCuts[pCutSet->nCuts];
         // make sure K-feasible cut exists
@@ -169,7 +169,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         If_ObjForEachCut( pObj, pCut, i )
             p->pPars->pFuncUser( p, pObj, pCut );
 
-    // free the cuts
+    // ABC_FREE the cuts
     If_ManDerefNodeCutSet( p, pObj );
 }
 
@@ -212,7 +212,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
         If_ObjForEachCut( pTemp, pCutTemp, i )
         {
             assert( p->pPars->fSeqMap || pCutTemp->nLeaves > 1 );
-            // get the next free cut
+            // get the next ABC_FREE cut
             assert( pCutSet->nCuts <= pCutSet->nCutsMax );
             pCut = pCutSet->ppCuts[pCutSet->nCuts];
             // copy the cut into storage
@@ -253,7 +253,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
     if ( Mode && pObj->nRefs > 0 )
         If_CutAreaRef( p, If_ObjCutBest(pObj) );
 
-    // free the cuts
+    // ABC_FREE the cuts
     If_ManDerefChoiceCutSet( p, pObj );
 }
 
@@ -342,7 +342,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
         char Symb = fPreprocess? 'P' : ((Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'));
         printf( "%c: Del = %7.2f. Ar = %9.1f. Edge = %8d. Switch = %7.2f. Cut = %8d. ", 
             Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->dPower, p->nCutsMerged );
-        PRT( "T", clock() - clk );
+        ABC_PRT( "T", clock() - clk );
 //    printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n", 
 //        p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
     }
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index a5fa7d86..b3130600 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -57,7 +57,7 @@ void If_ManImproveMapping( If_Man_t * p )
     {
         printf( "E: Del = %7.2f. Ar = %9.1f. Edge = %8d. Switch = %7.2f. Cut = %8d. ", 
             p->RequiredGlo, p->AreaGlo, p->nNets, p->dPower, p->nCutsMerged );
-        PRT( "T", clock() - clk );
+        ABC_PRT( "T", clock() - clk );
     }
  
 /*
@@ -68,7 +68,7 @@ void If_ManImproveMapping( If_Man_t * p )
     {
         printf( "R:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
             p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
-        PRT( "T", clock() - clk );
+        ABC_PRT( "T", clock() - clk );
     }
 */
 /*
@@ -79,7 +79,7 @@ void If_ManImproveMapping( If_Man_t * p )
     {
         printf( "E:  Del = %6.2f. Area = %8.2f. Nets = %6d. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
             p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
-        PRT( "T", clock() - clk );
+        ABC_PRT( "T", clock() - clk );
     }
 */
 }
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index 06015b06..1e6d7704 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -333,7 +333,7 @@ float If_ManScanMapping( If_Man_t * p )
         pObj->nRefs    = 0;
     }
     // allocate place to store the nodes
-    ppStore = ALLOC( If_Obj_t *, p->nLevelMax + 1 );
+    ppStore = ABC_ALLOC( If_Obj_t *, p->nLevelMax + 1 );
     memset( ppStore, 0, sizeof(If_Obj_t *) * (p->nLevelMax + 1) );
     // collect nodes reachable from POs in the DFS order through the best cuts
     aArea = 0;
@@ -344,7 +344,7 @@ float If_ManScanMapping( If_Man_t * p )
     for ( i = p->nLevelMax; i >= 0; i-- )
         for ( pObj = ppStore[i]; pObj; pObj = pObj->pCopy )
             Vec_PtrPush( p->vMapped, pObj );
-    free( ppStore );
+    ABC_FREE( ppStore );
     return aArea;
 }
 
@@ -374,7 +374,7 @@ float If_ManScanMappingDirect( If_Man_t * p )
         pObj->nRefs    = 0;
     }
     // allocate place to store the nodes
-    ppStore = ALLOC( If_Obj_t *, p->nLevelMax + 1 );
+    ppStore = ABC_ALLOC( If_Obj_t *, p->nLevelMax + 1 );
     memset( ppStore, 0, sizeof(If_Obj_t *) * (p->nLevelMax + 1) );
     // collect nodes reachable from POs in the DFS order through the best cuts
     aArea = 0;
@@ -386,7 +386,7 @@ float If_ManScanMappingDirect( If_Man_t * p )
     for ( i = 0; i <= p->nLevelMax; i++ )
         for ( pObj = ppStore[i]; pObj; pObj = pObj->pCopy )
             Vec_PtrPush( p->vMapped, pObj );
-    free( ppStore );
+    ABC_FREE( ppStore );
     return aArea;
 }
 
@@ -550,7 +550,7 @@ Vec_Ptr_t * If_ManReverseOrder( If_Man_t * p )
     If_Obj_t * pObj, ** ppStore;
     int i;
     // allocate place to store the nodes
-    ppStore = ALLOC( If_Obj_t *, p->nLevelMax + 1 );
+    ppStore = ABC_ALLOC( If_Obj_t *, p->nLevelMax + 1 );
     memset( ppStore, 0, sizeof(If_Obj_t *) * (p->nLevelMax + 1) );
     // add the nodes
     If_ManForEachObj( p, pObj, i )
@@ -563,7 +563,7 @@ Vec_Ptr_t * If_ManReverseOrder( If_Man_t * p )
     for ( i = p->nLevelMax; i >= 0; i-- )
         for ( pObj = ppStore[i]; pObj; pObj = pObj->pCopy )
             Vec_PtrPush( vOrder, pObj );
-    free( ppStore );
+    ABC_FREE( ppStore );
     // print the order
 //    Vec_PtrForEachEntry( vOrder, pObj, i )
 //        printf( "Obj %2d   Type %d  Level = %d\n", pObj->Id, pObj->Type, pObj->Level );
diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h
index 673f7538..ac31feac 100644
--- a/src/map/mapper/mapper.h
+++ b/src/map/mapper/mapper.h
@@ -19,19 +19,18 @@
 #ifndef __MAPPER_H__
 #define __MAPPER_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -63,10 +62,10 @@ struct Map_TimeStruct_t_
 ///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
  
-#define Map_IsComplement(p)    (((int)((PORT_PTRUINT_T) (p) & 01)))
-#define Map_Regular(p)         ((Map_Node_t *)((PORT_PTRUINT_T)(p) & ~01)) 
-#define Map_Not(p)             ((Map_Node_t *)((PORT_PTRUINT_T)(p) ^ 01)) 
-#define Map_NotCond(p,c)       ((Map_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)))
+#define Map_IsComplement(p)    (((int)((ABC_PTRUINT_T) (p) & 01)))
+#define Map_Regular(p)         ((Map_Node_t *)((ABC_PTRUINT_T)(p) & ~01)) 
+#define Map_Not(p)             ((Map_Node_t *)((ABC_PTRUINT_T)(p) ^ 01)) 
+#define Map_NotCond(p,c)       ((Map_Node_t *)((ABC_PTRUINT_T)(p) ^ (c)))
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c
index 5d4854e6..fc0d9609 100644
--- a/src/map/mapper/mapperCore.c
+++ b/src/map/mapper/mapperCore.c
@@ -70,7 +70,7 @@ int Map_Mapping( Map_Man_t * p )
     Map_MappingTruths( p );
     p->timeTruth = clock() - clk;
     //////////////////////////////////////////////////////////////////////
-//PRT( "Truths", clock() - clk );
+//ABC_PRT( "Truths", clock() - clk );
 
     //////////////////////////////////////////////////////////////////////
     // compute the minimum-delay mapping
@@ -88,7 +88,7 @@ printf( "Delay    : %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ",
                     fShowSwitching? "Switch" : "Delay", 
                     fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
                     Map_MappingGetAreaFlow(p), p->AreaBase, 0.0 );
-PRT( "Time", p->timeMatch );
+ABC_PRT( "Time", p->timeMatch );
 }
     //////////////////////////////////////////////////////////////////////
 
@@ -119,7 +119,7 @@ printf( "AreaFlow : %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ",
                     fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
                     Map_MappingGetAreaFlow(p), p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
     }
     p->timeArea += clock() - clk;
@@ -145,7 +145,7 @@ printf( "Area     : %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ",
                     fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
                     0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
     }
     p->timeArea += clock() - clk;
@@ -171,7 +171,7 @@ printf( "Area     : %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ",
                     fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
                     0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
     }
     p->timeArea += clock() - clk;
@@ -197,7 +197,7 @@ printf( "Switching: %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ",
                     fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
                     0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
 
         // compute the required times
@@ -215,7 +215,7 @@ printf( "Switching: %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ",
                     fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
                     0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
     }
     p->timeArea += clock() - clk;
diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c
index 0a971542..ee2b089c 100644
--- a/src/map/mapper/mapperCreate.c
+++ b/src/map/mapper/mapperCreate.c
@@ -27,7 +27,7 @@ static void            Map_TableResize( Map_Man_t * p );
 static Map_Node_t *    Map_TableLookup( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 );
 
 // hash key for the structural hash table
-static inline unsigned Map_HashKey2( Map_Node_t * p0, Map_Node_t * p1, int TableSize ) { return (unsigned)(((PORT_PTRUINT_T)(p0) + (PORT_PTRUINT_T)(p1) * 12582917) % TableSize); }
+static inline unsigned Map_HashKey2( Map_Node_t * p0, Map_Node_t * p1, int TableSize ) { return (unsigned)(((ABC_PTRUINT_T)(p0) + (ABC_PTRUINT_T)(p1) * 12582917) % TableSize); }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -190,7 +190,7 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     }
 
     // start the manager
-    p = ALLOC( Map_Man_t, 1 );
+    p = ABC_ALLOC( Map_Man_t, 1 );
     memset( p, 0, sizeof(Map_Man_t) );
     p->pSuperLib = Abc_FrameReadLibSuper();
     p->nVarsMax  = p->pSuperLib->nVarsMax;
@@ -220,13 +220,13 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
 
     // create the PI nodes
     p->nInputs = nInputs;
-    p->pInputs = ALLOC( Map_Node_t *, nInputs );
+    p->pInputs = ABC_ALLOC( Map_Node_t *, nInputs );
     for ( i = 0; i < nInputs; i++ )
         p->pInputs[i] = Map_NodeCreate( p, NULL, NULL );
 
     // create the place for the output nodes
     p->nOutputs = nOutputs;
-    p->pOutputs = ALLOC( Map_Node_t *, nOutputs );
+    p->pOutputs = ABC_ALLOC( Map_Node_t *, nOutputs );
     memset( p->pOutputs, 0, sizeof(Map_Node_t *) * nOutputs );
     return p;
 }
@@ -258,17 +258,17 @@ void Map_ManFree( Map_Man_t * p )
         Map_NodeVecFree( p->vMapping );
     if ( p->vVisited )    
         Map_NodeVecFree( p->vVisited );
-    if ( p->uCanons )   free( p->uCanons );
-    if ( p->uPhases )   free( p->uPhases );
-    if ( p->pCounters ) free( p->pCounters );
+    if ( p->uCanons )   ABC_FREE( p->uCanons );
+    if ( p->uPhases )   ABC_FREE( p->uPhases );
+    if ( p->pCounters ) ABC_FREE( p->pCounters );
     Extra_MmFixedStop( p->mmNodes );
     Extra_MmFixedStop( p->mmCuts );
-    FREE( p->pInputArrivals );
-    FREE( p->pInputs );
-    FREE( p->pOutputs );
-    FREE( p->pBins );
-    FREE( p->ppOutputNames );
-    FREE( p );
+    ABC_FREE( p->pInputArrivals );
+    ABC_FREE( p->pInputs );
+    ABC_FREE( p->pOutputs );
+    ABC_FREE( p->pBins );
+    ABC_FREE( p->ppOutputNames );
+    ABC_FREE( p );
 }
 
 
@@ -287,17 +287,17 @@ void Map_ManPrintTimeStats( Map_Man_t * p )
 {
     printf( "N-canonical = %d. Matchings = %d.  Phases = %d.  ", p->nCanons, p->nMatches, p->nPhases );
     printf( "Choice nodes = %d. Choices = %d.\n", p->nChoiceNodes, p->nChoices );
-    PRT( "ToMap", p->timeToMap );
-    PRT( "Cuts ", p->timeCuts  );
-    PRT( "Truth", p->timeTruth );
-    PRT( "Match", p->timeMatch );
-    PRT( "Area ", p->timeArea  );
-    PRT( "Sweep", p->timeSweep );
-    PRT( "ToNet", p->timeToNet );
-    PRT( "TOTAL", p->timeTotal );
-    if ( p->time1 ) { PRT( "time1", p->time1 ); }
-    if ( p->time2 ) { PRT( "time2", p->time2 ); }
-    if ( p->time3 ) { PRT( "time3", p->time3 ); }
+    ABC_PRT( "ToMap", p->timeToMap );
+    ABC_PRT( "Cuts ", p->timeCuts  );
+    ABC_PRT( "Truth", p->timeTruth );
+    ABC_PRT( "Match", p->timeMatch );
+    ABC_PRT( "Area ", p->timeArea  );
+    ABC_PRT( "Sweep", p->timeSweep );
+    ABC_PRT( "ToNet", p->timeToNet );
+    ABC_PRT( "TOTAL", p->timeTotal );
+    if ( p->time1 ) { ABC_PRT( "time1", p->time1 ); }
+    if ( p->time2 ) { ABC_PRT( "time2", p->time2 ); }
+    if ( p->time3 ) { ABC_PRT( "time3", p->time3 ); }
 }
 
 /**Function*************************************************************
@@ -388,7 +388,7 @@ void Map_TableCreate( Map_Man_t * pMan )
 {
     assert( pMan->pBins == NULL );
     pMan->nBins = Cudd_Prime(5000);
-    pMan->pBins = ALLOC( Map_Node_t *, pMan->nBins );
+    pMan->pBins = ABC_ALLOC( Map_Node_t *, pMan->nBins );
     memset( pMan->pBins, 0, sizeof(Map_Node_t *) * pMan->nBins );
     pMan->nNodes = 0;
 }
@@ -473,7 +473,7 @@ clk = clock();
     // get the new table size
     nBinsNew = Cudd_Prime(2 * pMan->nBins); 
     // allocate a new array
-    pBinsNew = ALLOC( Map_Node_t *, nBinsNew );
+    pBinsNew = ABC_ALLOC( Map_Node_t *, nBinsNew );
     memset( pBinsNew, 0, sizeof(Map_Node_t *) * nBinsNew );
     // rehash the entries from the old table
     Counter = 0;
@@ -490,10 +490,10 @@ clk = clock();
     if ( pMan->fVerbose )
     {
 //        printf( "Increasing the unique table size from %6d to %6d. ", pMan->nBins, nBinsNew );
-//        PRT( "Time", clock() - clk );
+//        ABC_PRT( "Time", clock() - clk );
     }
     // replace the table and the parameters
-    free( pMan->pBins );
+    ABC_FREE( pMan->pBins );
     pMan->pBins = pBinsNew;
     pMan->nBins = nBinsNew;
 }
diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c
index 46405547..00ec9fe5 100644
--- a/src/map/mapper/mapperCut.c
+++ b/src/map/mapper/mapperCut.c
@@ -151,7 +151,7 @@ void Map_MappingCuts( Map_Man_t * p )
         nCuts = Map_MappingCountAllCuts(p);
         printf( "Nodes = %6d.  Total %d-feasible cuts = %10d.  Per node = %.1f. ", 
                p->nNodes, p->nVarsMax, nCuts, ((float)nCuts)/p->nNodes );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
 
     // print the cuts for the first primary output
@@ -809,15 +809,15 @@ Map_CutTable_t * Map_CutTableStart( Map_Man_t * pMan )
 {
     Map_CutTable_t * p;
     // allocate the table
-    p = ALLOC( Map_CutTable_t, 1 );
+    p = ABC_ALLOC( Map_CutTable_t, 1 );
     memset( p, 0, sizeof(Map_CutTable_t) );
     p->nBins = Cudd_Prime( 10 * MAP_CUTS_MAX_COMPUTE );
-    p->pBins = ALLOC( Map_Cut_t *, p->nBins );
+    p->pBins = ABC_ALLOC( Map_Cut_t *, p->nBins );
     memset( p->pBins, 0, sizeof(Map_Cut_t *) * p->nBins );
-    p->pCuts = ALLOC( int, 2 * MAP_CUTS_MAX_COMPUTE );
-    p->pArray = ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
-    p->pCuts1 = ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
-    p->pCuts2 = ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
+    p->pCuts = ABC_ALLOC( int, 2 * MAP_CUTS_MAX_COMPUTE );
+    p->pArray = ABC_ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
+    p->pCuts1 = ABC_ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
+    p->pCuts2 = ABC_ALLOC( Map_Cut_t *, 2 * MAP_CUTS_MAX_COMPUTE );
     return p;
 }
 
@@ -834,12 +834,12 @@ Map_CutTable_t * Map_CutTableStart( Map_Man_t * pMan )
 ***********************************************************************/
 void Map_CutTableStop( Map_CutTable_t * p )
 {
-    free( p->pCuts1 );
-    free( p->pCuts2 );
-    free( p->pArray );
-    free( p->pBins );
-    free( p->pCuts );
-    free( p );
+    ABC_FREE( p->pCuts1 );
+    ABC_FREE( p->pCuts2 );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p->pBins );
+    ABC_FREE( p->pCuts );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -1005,7 +1005,7 @@ Map_Cut_t * Map_CutSortCuts( Map_Man_t * pMan, Map_CutTable_t * p, Map_Cut_t * p
     // move them back into the list
     if ( nCuts > MAP_CUTS_MAX_USE - 1 )
     {
-        // free the remaining cuts
+        // ABC_FREE the remaining cuts
         for ( i = MAP_CUTS_MAX_USE - 1; i < nCuts; i++ )
             Extra_MmFixedEntryRecycle( pMan->mmCuts, (char *)p->pCuts1[i] );
         // update the number of cuts
diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h
index 00550deb..7f4c93dc 100644
--- a/src/map/mapper/mapperInt.h
+++ b/src/map/mapper/mapperInt.h
@@ -60,10 +60,10 @@
 #define MAP_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
 
 // internal macros to work with cuts
-#define Map_CutIsComplement(p)  (((int)((PORT_PTRUINT_T) (p) & 01)))
-#define Map_CutRegular(p)       ((Map_Cut_t *)((PORT_PTRUINT_T)(p) & ~01)) 
-#define Map_CutNot(p)           ((Map_Cut_t *)((PORT_PTRUINT_T)(p) ^ 01)) 
-#define Map_CutNotCond(p,c)     ((Map_Cut_t *)((PORT_PTRUINT_T)(p) ^ (c)))
+#define Map_CutIsComplement(p)  (((int)((ABC_PTRUINT_T) (p) & 01)))
+#define Map_CutRegular(p)       ((Map_Cut_t *)((ABC_PTRUINT_T)(p) & ~01)) 
+#define Map_CutNot(p)           ((Map_Cut_t *)((ABC_PTRUINT_T)(p) ^ 01)) 
+#define Map_CutNotCond(p,c)     ((Map_Cut_t *)((ABC_PTRUINT_T)(p) ^ (c)))
 
 // internal macros for referencing of nodes
 #define Map_NodeReadRef(p)      ((Map_Regular(p))->nRefs)
diff --git a/src/map/mapper/mapperLib.c b/src/map/mapper/mapperLib.c
index 9c47ed03..942caa8e 100644
--- a/src/map/mapper/mapperLib.c
+++ b/src/map/mapper/mapperLib.c
@@ -56,7 +56,7 @@ Map_SuperLib_t * Map_SuperLibCreate( char * pFileName, char * pExcludeFile, bool
     int clk;
 
     // start the supergate library
-    p = ALLOC( Map_SuperLib_t, 1 );
+    p = ABC_ALLOC( Map_SuperLib_t, 1 );
     memset( p, 0, sizeof(Map_SuperLib_t) );
     p->pName     = pFileName;
     p->fVerbose  = fVerbose;
@@ -98,7 +98,7 @@ clk = clock();
 if ( fVerbose ) {
     printf( "Loaded %d unique %d-input supergates from \"%s\".  ", 
         p->nSupersReal, p->nVarsMax, pFileName );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 }
 
     // assign the interver parameters
@@ -155,8 +155,8 @@ void Map_SuperLibFree( Map_SuperLib_t * p )
     Extra_MmFixedStop( p->mmSupers );
     Extra_MmFixedStop( p->mmEntries );
     Extra_MmFlexStop( p->mmForms );
-    FREE( p->ppSupers );
-    FREE( p );
+    ABC_FREE( p->ppSupers );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -192,7 +192,7 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
     // get the file name with the library
     pNameGeneric = Extra_FileNameGeneric( Mio_LibraryReadName(pLib) );
     sprintf( FileNameSuper, "%s.super", pNameGeneric );
-    free( pNameGeneric );
+    ABC_FREE( pNameGeneric );
 
     sprintf( CommandSuper,  "super -l 1 -i 5 -d 10000000 -a 10000000 -t 100 %s", FileNameGenlib ); 
     if ( Cmd_CommandExecute( pAbc, CommandSuper ) )
diff --git a/src/map/mapper/mapperRefs.c b/src/map/mapper/mapperRefs.c
index a50b134a..852e759f 100644
--- a/src/map/mapper/mapperRefs.c
+++ b/src/map/mapper/mapperRefs.c
@@ -430,7 +430,7 @@ void Map_MappingSetRefs( Map_Man_t * pMan )
             LevelMax = Map_Regular(pMan->pOutputs[i])->Level;
 
     // allocate place to store the nodes
-    ppStore = ALLOC( Map_Node_t *, LevelMax + 1 );
+    ppStore = ABC_ALLOC( Map_Node_t *, LevelMax + 1 );
     memset( ppStore, 0, sizeof(Map_Node_t *) * (LevelMax + 1) );
 
     // visit nodes reachable from POs in the DFS order through the best cuts
@@ -447,7 +447,7 @@ void Map_MappingSetRefs( Map_Man_t * pMan )
     for ( i = LevelMax; i >= 0; i-- )
         for ( pNode = ppStore[i]; pNode; pNode = (Map_Node_t *)pNode->pData0 )
             Map_NodeVecPush( pMan->vMapping, pNode );
-    free( ppStore );
+    ABC_FREE( ppStore );
 }
 
 /**Function*************************************************************
diff --git a/src/map/mapper/mapperTable.c b/src/map/mapper/mapperTable.c
index 3feba352..a0805991 100644
--- a/src/map/mapper/mapperTable.c
+++ b/src/map/mapper/mapperTable.c
@@ -46,12 +46,12 @@ Map_HashTable_t * Map_SuperTableCreate( Map_SuperLib_t * pLib )
 {
     Map_HashTable_t * p;
     // allocate the table
-    p = ALLOC( Map_HashTable_t, 1 );
+    p = ABC_ALLOC( Map_HashTable_t, 1 );
     memset( p, 0, sizeof(Map_HashTable_t) );
     p->mmMan = pLib->mmEntries;
     // allocate and clean the bins
     p->nBins = Cudd_Prime(20000);
-    p->pBins = ALLOC( Map_HashEntry_t *, p->nBins );
+    p->pBins = ABC_ALLOC( Map_HashEntry_t *, p->nBins );
     memset( p->pBins, 0, sizeof(Map_HashEntry_t *) * p->nBins );
     return p;
 }
@@ -70,8 +70,8 @@ Map_HashTable_t * Map_SuperTableCreate( Map_SuperLib_t * pLib )
 ***********************************************************************/
 void Map_SuperTableFree( Map_HashTable_t * p )
 {
-    FREE( p->pBins );
-    FREE( p );
+    ABC_FREE( p->pBins );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -236,7 +236,7 @@ void Map_SuperTableResize( Map_HashTable_t * p )
     // get the new table size
     nBinsNew = Cudd_Prime(2 * p->nBins); 
     // allocate a new array
-    pBinsNew = ALLOC( Map_HashEntry_t *, nBinsNew );
+    pBinsNew = ABC_ALLOC( Map_HashEntry_t *, nBinsNew );
     memset( pBinsNew, 0, sizeof(Map_HashEntry_t *) * nBinsNew );
     // rehash the entries from the old table
     Counter = 0;
@@ -251,7 +251,7 @@ void Map_SuperTableResize( Map_HashTable_t * p )
         }
     assert( Counter == p->nEntries );
     // replace the table and the parameters
-    free( p->pBins );
+    ABC_FREE( p->pBins );
     p->pBins = pBinsNew;
     p->nBins = nBinsNew;
 }
@@ -317,7 +317,7 @@ void Map_SuperTableSortSupergates( Map_HashTable_t * p, int nSupersMax )
     int nSupers, i;
 
     // copy all the supergates into one array
-    ppSupers = ALLOC( Map_Super_t *, nSupersMax );
+    ppSupers = ABC_ALLOC( Map_Super_t *, nSupersMax );
     nSupers = 0;
     for ( i = 0; i < p->nBins; i++ )
         for ( pEnt = p->pBins[i]; pEnt; pEnt = pEnt->pNext )
@@ -342,7 +342,7 @@ void Map_SuperTableSortSupergates( Map_HashTable_t * p, int nSupersMax )
         printf( "%s",            ppSupers[i]->pFormula );
         printf( "\n" );
     }
-    free( ppSupers );
+    ABC_FREE( ppSupers );
 }
 
 /**Function*************************************************************
@@ -363,7 +363,7 @@ void Map_SuperTableSortSupergatesByDelay( Map_HashTable_t * p, int nSupersMax )
     Map_Super_t * pSuper;
     int nSupers, i, k;
 
-    ppSupers = ALLOC( Map_Super_t *, nSupersMax );
+    ppSupers = ABC_ALLOC( Map_Super_t *, nSupersMax );
     for ( i = 0; i < p->nBins; i++ )
         for ( pEnt = p->pBins[i]; pEnt; pEnt = pEnt->pNext )
         {
@@ -392,7 +392,7 @@ void Map_SuperTableSortSupergatesByDelay( Map_HashTable_t * p, int nSupersMax )
             // save the number of supergates in the list
             pEnt->pGates->nSupers = nSupers;
         }
-    FREE( ppSupers );
+    ABC_FREE( ppSupers );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index 6e69bc69..4cabf86c 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -198,7 +198,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     }
 
     // allocate room for supergate pointers
-    pLib->ppSupers = ALLOC( Map_Super_t *, pLib->nLines + 10000 );
+    pLib->ppSupers = ABC_ALLOC( Map_Super_t *, pLib->nLines + 10000 );
 
     // create the elementary supergates
     for ( i = 0; i < pLib->nVarsMax; i++ )
diff --git a/src/map/mapper/mapperVec.c b/src/map/mapper/mapperVec.c
index f75138fb..f675e0c5 100644
--- a/src/map/mapper/mapperVec.c
+++ b/src/map/mapper/mapperVec.c
@@ -42,12 +42,12 @@ static int Map_NodeVecCompareLevels( Map_Node_t ** pp1, Map_Node_t ** pp2 );
 Map_NodeVec_t * Map_NodeVecAlloc( int nCap )
 {
     Map_NodeVec_t * p;
-    p = ALLOC( Map_NodeVec_t, 1 );
+    p = ABC_ALLOC( Map_NodeVec_t, 1 );
     if ( nCap > 0 && nCap < 16 )
         nCap = 16;
     p->nSize  = 0;
     p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( Map_Node_t *, p->nCap ) : NULL;
+    p->pArray = p->nCap? ABC_ALLOC( Map_Node_t *, p->nCap ) : NULL;
     return p;
 }
 
@@ -64,8 +64,8 @@ Map_NodeVec_t * Map_NodeVecAlloc( int nCap )
 ***********************************************************************/
 void Map_NodeVecFree( Map_NodeVec_t * p )
 {
-    FREE( p->pArray );
-    FREE( p );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -115,7 +115,7 @@ void Map_NodeVecGrow( Map_NodeVec_t * p, int nCapMin )
 {
     if ( p->nCap >= nCapMin )
         return;
-    p->pArray = REALLOC( Map_Node_t *, p->pArray, nCapMin ); 
+    p->pArray = ABC_REALLOC( Map_Node_t *, p->pArray, nCapMin ); 
     p->nCap   = nCapMin;
 }
 
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index 1326dbbf..b7dd2895 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -27,6 +27,7 @@
 #include "mainInt.h"
 #include "mioInt.h"
 #include "mapper.h"
+#include "amap.h"
 
 extern void Amap_LibFree( void * p );
 extern void Amap_LibPrintSelectedGates( void * p, int fAllGates );
@@ -36,6 +37,8 @@ extern void * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryV
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static int Mio_CommandReadLiberty( Abc_Frame_t * pAbc, int argc, char **argv );
+
 static int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv );
 static int Mio_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv );
 
@@ -106,6 +109,8 @@ void Mio_Init( Abc_Frame_t * pAbc )
         unlink( pFileTemp );
 #endif
 
+    Cmd_CommandAdd( pAbc, "SC mapping", "read_liberty",   Mio_CommandReadLiberty,  0 ); 
+
     Cmd_CommandAdd( pAbc, "SC mapping", "read_library",   Mio_CommandReadLibrary,  0 ); 
     Cmd_CommandAdd( pAbc, "SC mapping", "print_library",  Mio_CommandPrintLibrary, 0 ); 
 
@@ -143,6 +148,82 @@ void Mio_End()
   SeeAlso     []
 
 ***********************************************************************/
+int Mio_CommandReadLiberty( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    FILE * pFile;
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNet;
+    char * FileName;
+    int fVerbose;
+    int c;
+
+    pNet = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set the defaults
+    fVerbose = 1;
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = Io_FileOpen( FileName, "open_path", "r", 0 )) == NULL )
+    {
+        fprintf( pErr, "Cannot open input file \"%s\". ", FileName );
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".genlib", ".lib", ".gen", ".g", NULL )) )
+            fprintf( pErr, "Did you mean \"%s\"?", FileName );
+        fprintf( pErr, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    if ( !Amap_LibertyParse( FileName, "temp.genlib", fVerbose ) )
+        return 0;
+    Cmd_CommandExecute( pAbc, "read_library temp.genlib" );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: read_liberty [-vh]\n");
+    fprintf( pErr, "\t         read standard cell library in Liberty format\n" );  
+    fprintf( pErr, "\t         (if the library contains more than one gate\n" );  
+    fprintf( pErr, "\t         with the same Boolean function, only the gate\n" );  
+    fprintf( pErr, "\t         with the smallest area will be used)\n" );  
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : enable verbose output\n");
+    return 1;       /* error exit */
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     FILE * pFile;
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index 0e5a39d3..66fea292 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -19,10 +19,6 @@
 #ifndef __MIO_H__
 #define __MIO_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -31,6 +27,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c
index 1fca5764..a06151f0 100644
--- a/src/map/mio/mioFunc.c
+++ b/src/map/mio/mioFunc.c
@@ -144,7 +144,7 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
     {
         // get the topmost (generic) pin
         pPin = pGate->pPins;
-        FREE( pPin->pName );
+        ABC_FREE( pPin->pName );
 
         // create individual pins from the generic pin
         ppPin = &pPin->pNext;
@@ -173,10 +173,10 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
             {
                 if ( pPinNames[i] && strcmp( pPinNames[i], pPin->pName ) == 0 )
                 {
-                    // free pPinNames[i] because it is already available as pPin->pName
+                    // ABC_FREE pPinNames[i] because it is already available as pPin->pName
                     // setting pPinNames[i] to NULL is useful to make sure that
                     // this name is not assigned to two pins in the list
-                    FREE( pPinNames[i] );
+                    ABC_FREE( pPinNames[i] );
                     pPinNamesCopy[iPin++] = pPin->pName;
                     break;
                 }
@@ -212,6 +212,8 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
 
     // derive the formula as the BDD
     pGate->bFunc = Parse_FormulaParser( stdout, pGate->pForm, nPins, 0, pPinNames, dd, dd->vars );
+    if ( pGate->bFunc == NULL )
+        return 1;
     Cudd_Ref( pGate->bFunc );
 
     // derive the cover (SOP)
diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c
index ae33c942..fdb340aa 100644
--- a/src/map/mio/mioRead.c
+++ b/src/map/mio/mioRead.c
@@ -94,7 +94,7 @@ Mio_Library_t * Mio_LibraryReadOne( Abc_Frame_t * pAbc, char * FileName, bool fE
     char * pBuffer = 0;
 
     // allocate the genlib structure
-    pLib = ALLOC( Mio_Library_t, 1 );
+    pLib = ABC_ALLOC( Mio_Library_t, 1 );
     memset( pLib, 0, sizeof(Mio_Library_t) );
     pLib->pName = Extra_UtilStrsav( FileName );
     pLib->tName2Gate = st_init_table(strcmp, st_strhash);
@@ -122,7 +122,7 @@ Mio_Library_t * Mio_LibraryReadOne( Abc_Frame_t * pAbc, char * FileName, bool fE
         // move the file current reading position to the beginning
         rewind( pFile ); 
         // load the contents of the file into memory
-        pBuffer   = ALLOC( char, nFileSize + 10 );
+        pBuffer   = ABC_ALLOC( char, nFileSize + 10 );
         fread( pBuffer, nFileSize, 1, pFile );
         // terminate the string with '\0'
         pBuffer[ nFileSize ] = '\0';
@@ -137,10 +137,10 @@ Mio_Library_t * Mio_LibraryReadOne( Abc_Frame_t * pAbc, char * FileName, bool fE
     if ( Mio_LibraryReadInternal( pLib, pBuffer, fExtendedFormat, tExcludeGate, fVerbose ) )
     {
         Mio_LibraryDelete( pLib );
-        free( pBuffer );
+        ABC_FREE( pBuffer );
         return NULL;
     }
-    free( pBuffer );
+    ABC_FREE( pBuffer );
 
     // derive the functinality of gates
     if ( Mio_LibraryParseFormulas( pLib ) )
@@ -243,7 +243,7 @@ Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, bool fExtendedFormat )
     char * pToken = *ppToken;
 
     // allocate the gate structure
-    pGate = ALLOC( Mio_Gate_t, 1 );
+    pGate = ABC_ALLOC( Mio_Gate_t, 1 );
     memset( pGate, 0, sizeof(Mio_Gate_t) );
 
     // read the name
@@ -311,7 +311,7 @@ Mio_Pin_t * Mio_LibraryReadPin( char ** ppToken, bool fExtendedFormat )
     char * pToken = *ppToken;
 
     // allocate the gate structure
-    pPin = ALLOC( Mio_Pin_t, 1 );
+    pPin = ABC_ALLOC( Mio_Pin_t, 1 );
     memset( pPin, 0, sizeof(Mio_Pin_t) );
 
     // read the name
@@ -397,7 +397,7 @@ char * chomp( char *s )
         if ( !isspace(*b) )
             break;
     // strsav the string
-    a = strcpy( ALLOC(char, strlen(b)+1), b );
+    a = strcpy( ABC_ALLOC(char, strlen(b)+1), b );
     // remove trailing spaces
     for ( c = a+strlen(a); c > a; c-- )
         if ( *c == 0 || isspace(*c) )
@@ -464,12 +464,12 @@ void Mio_LibrarySortGates( Mio_Library_t * pLib )
 {
     Mio_Gate_t ** ppGates, * pGate;
     int i = 0;
-    ppGates = ALLOC( Mio_Gate_t *, pLib->nGates );
+    ppGates = ABC_ALLOC( Mio_Gate_t *, pLib->nGates );
     Mio_LibraryForEachGate( pLib, pGate )
         ppGates[i++] = pGate;
     assert( i == pLib->nGates );
     // sort gates by area
-    pLib->ppGates0 = ALLOC( Mio_Gate_t *, pLib->nGates );
+    pLib->ppGates0 = ABC_ALLOC( Mio_Gate_t *, pLib->nGates );
     for ( i = 0; i < pLib->nGates; i++ )
         pLib->ppGates0[i] = ppGates[i];
     qsort( (void *)ppGates, pLib->nGates, sizeof(void *), 
@@ -477,9 +477,9 @@ void Mio_LibrarySortGates( Mio_Library_t * pLib )
     for ( i = 0; i < pLib->nGates; i++ )
         ppGates[i]->pNext = (i < pLib->nGates-1)? ppGates[i+1] : NULL;
     pLib->pGates = ppGates[0];
-    free( ppGates );
+    ABC_FREE( ppGates );
     // sort gates by name
-    pLib->ppGatesName = ALLOC( Mio_Gate_t *, pLib->nGates );
+    pLib->ppGatesName = ABC_ALLOC( Mio_Gate_t *, pLib->nGates );
     for ( i = 0; i < pLib->nGates; i++ )
         pLib->ppGatesName[i] = pLib->ppGates0[i];
     qsort( (void *)pLib->ppGatesName, pLib->nGates, sizeof(void *), 
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index 2a1d1f30..3f42d2bb 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -47,10 +47,10 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
     Mio_Gate_t * pGate, * pGate2;
     if ( pLib == NULL )
         return;
-    // free the bindings of nodes to gates from this library for all networks
+    // ABC_FREE the bindings of nodes to gates from this library for all networks
     Abc_FrameUnmapAllNetworks( Abc_FrameGetGlobalFrame() );
-    // free the library
-    FREE( pLib->pName );
+    // ABC_FREE the library
+    ABC_FREE( pLib->pName );
     Mio_LibraryForEachGateSafe( pLib, pGate, pGate2 )
         Mio_GateDelete( pGate );
     Extra_MmFlexStop( pLib->pMmFlex );
@@ -59,9 +59,9 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
         st_free_table( pLib->tName2Gate );
     if ( pLib->dd )
         Cudd_Quit( pLib->dd );
-    FREE( pLib->ppGates0 );
-    FREE( pLib->ppGatesName );
-    free( pLib );
+    ABC_FREE( pLib->ppGates0 );
+    ABC_FREE( pLib->ppGatesName );
+    ABC_FREE( pLib );
 }
 
 /**Function*************************************************************
@@ -78,14 +78,14 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
 void Mio_GateDelete( Mio_Gate_t * pGate )
 {
     Mio_Pin_t * pPin, * pPin2;
-    FREE( pGate->pOutName );
-    FREE( pGate->pName );
-    FREE( pGate->pForm );
+    ABC_FREE( pGate->pOutName );
+    ABC_FREE( pGate->pName );
+    ABC_FREE( pGate->pForm );
     if ( pGate->bFunc )
         Cudd_RecursiveDeref( pGate->pLib->dd, pGate->bFunc );
     Mio_GateForEachPinSafe( pGate, pPin, pPin2 )
         Mio_PinDelete( pPin );   
-    free( pGate );
+    ABC_FREE( pGate );
 }
 
 /**Function*************************************************************
@@ -101,8 +101,8 @@ void Mio_GateDelete( Mio_Gate_t * pGate )
 ***********************************************************************/
 void Mio_PinDelete( Mio_Pin_t * pPin )
 {
-    FREE( pPin->pName );
-    free( pPin );
+    ABC_FREE( pPin->pName );
+    ABC_FREE( pPin );
 }
 
 /**Function*************************************************************
@@ -120,7 +120,7 @@ Mio_Pin_t * Mio_PinDup( Mio_Pin_t * pPin )
 {
     Mio_Pin_t * pPinNew;
 
-    pPinNew = ALLOC( Mio_Pin_t, 1 );
+    pPinNew = ABC_ALLOC( Mio_Pin_t, 1 );
     *pPinNew = *pPin;
     pPinNew->pName = (pPinNew->pName ? Extra_UtilStrsav(pPinNew->pName) : NULL);
     pPinNew->pNext = NULL;
@@ -256,7 +256,7 @@ Mio_Gate_t ** Mio_CollectRoots( Mio_Library_t * pLib, int nInputs, float tDelay,
     }
 
     // collect the gates into the array
-    ppGates = ALLOC( Mio_Gate_t *, nGates );
+    ppGates = ABC_ALLOC( Mio_Gate_t *, nGates );
     iGate = 0;
     st_foreach_item( tFuncs, gen, (char **)&bFunc, (char **)&pGate )
         ppGates[ iGate++ ] = pGate;
@@ -265,7 +265,7 @@ Mio_Gate_t ** Mio_CollectRoots( Mio_Library_t * pLib, int nInputs, float tDelay,
 
     */
 
-    ppGates = ALLOC( Mio_Gate_t *, nGates );
+    ppGates = ABC_ALLOC( Mio_Gate_t *, nGates );
     iGate = 0;
     Mio_LibraryForEachGate( pLib, pGate )
     {
@@ -515,13 +515,13 @@ Mio_Gate_t * Mio_GateCreatePseudo( int nInputs )
     Mio_Pin_t * pPin;
     int i;
     // allocate the gate structure
-    pGate = ALLOC( Mio_Gate_t, 1 );
+    pGate = ABC_ALLOC( Mio_Gate_t, 1 );
     memset( pGate, 0, sizeof(Mio_Gate_t) );
     pGate->nInputs = nInputs;
     // create pins
     for ( i = 0; i < nInputs; i++ )
     {
-        pPin = ALLOC( Mio_Pin_t, 1 );
+        pPin = ABC_ALLOC( Mio_Pin_t, 1 );
         memset( pPin, 0, sizeof(Mio_Pin_t) );
         pPin->pNext = pGate->pPins;
         pGate->pPins = pPin;
diff --git a/src/map/super/super.h b/src/map/super/super.h
index a7169924..9f5e83ae 100644
--- a/src/map/super/super.h
+++ b/src/map/super/super.h
@@ -19,10 +19,6 @@
 #ifndef __SUPER_H__
 #define __SUPER_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -31,6 +27,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/super/superAnd.c b/src/map/super/superAnd.c
index 8e831952..3014d505 100644
--- a/src/map/super/superAnd.c
+++ b/src/map/super/superAnd.c
@@ -61,10 +61,10 @@ struct Super2_GateStruct_t_
 
 
 // manipulation of complemented attributes
-#define Super2_IsComplement(p)    (((int)((PORT_PTRUINT_T) (p) & 01)))
-#define Super2_Regular(p)         ((Super2_Gate_t *)((PORT_PTRUINT_T)(p) & ~01)) 
-#define Super2_Not(p)             ((Super2_Gate_t *)((PORT_PTRUINT_T)(p) ^ 01)) 
-#define Super2_NotCond(p,c)       ((Super2_Gate_t *)((PORT_PTRUINT_T)(p) ^ (c)))
+#define Super2_IsComplement(p)    (((int)((ABC_PTRUINT_T) (p) & 01)))
+#define Super2_Regular(p)         ((Super2_Gate_t *)((ABC_PTRUINT_T)(p) & ~01)) 
+#define Super2_Not(p)             ((Super2_Gate_t *)((ABC_PTRUINT_T)(p) ^ 01)) 
+#define Super2_NotCond(p,c)       ((Super2_Gate_t *)((ABC_PTRUINT_T)(p) ^ (c)))
 
 // iterating through the gates in the library
 #define Super2_LibForEachGate( Lib, Gate )                        \
@@ -132,7 +132,7 @@ clk = clock();
         Super2_LibStop( pLibCur );
         pLibCur = pLibNext;
 printf( "Level %d:  Tried = %7d.  Computed = %7d.  ", Level, pMan->nTried, pLibCur->nGates );
-PRT( "Runtime", clock() - clk );
+ABC_PRT( "Runtime", clock() - clk );
 fflush( stdout );
     }
 
@@ -163,7 +163,7 @@ fflush( stdout );
 Super2_Man_t * Super2_ManStart()
 {
     Super2_Man_t * pMan;
-    pMan = ALLOC( Super2_Man_t, 1 );
+    pMan = ABC_ALLOC( Super2_Man_t, 1 );
     memset( pMan, 0, sizeof(Super2_Man_t) );
     pMan->pMem   = Extra_MmFixedStart( sizeof(Super2_Gate_t) );
     pMan->tTable = stmm_init_table( st_ptrcmp, st_ptrhash );
@@ -185,7 +185,7 @@ void Super2_ManStop( Super2_Man_t * pMan )
 {
     Extra_MmFixedStop( pMan->pMem );
     stmm_free_table( pMan->tTable );
-    free( pMan );
+    ABC_FREE( pMan );
 }
 
 /**Function*************************************************************
@@ -202,7 +202,7 @@ void Super2_ManStop( Super2_Man_t * pMan )
 Super2_Lib_t * Super2_LibStart()
 {
     Super2_Lib_t * pLib;
-    pLib = ALLOC( Super2_Lib_t, 1 );
+    pLib = ABC_ALLOC( Super2_Lib_t, 1 );
     memset( pLib, 0, sizeof(Super2_Lib_t) );
     return pLib;
 }
@@ -228,7 +228,7 @@ Super2_Lib_t * Super2_LibDup( Super2_Lib_t * pLib )
     pLibNew->nGates      = pLib->nGates;
     pLibNew->uMaskBit    = pLib->uMaskBit;
     pLibNew->nGatesAlloc = 1000 + pLib->nGatesAlloc;
-    pLibNew->pGates      = ALLOC( Super2_Gate_t *, pLibNew->nGatesAlloc );
+    pLibNew->pGates      = ABC_ALLOC( Super2_Gate_t *, pLibNew->nGatesAlloc );
     memcpy( pLibNew->pGates, pLib->pGates, pLibNew->nGates * sizeof(Super2_Gate_t *) );
     return pLibNew;
 }
@@ -248,7 +248,7 @@ void Super2_LibAddGate( Super2_Lib_t * pLib, Super2_Gate_t * pGate )
 {
     if ( pLib->nGates == pLib->nGatesAlloc )
     {
-        pLib->pGates  = REALLOC( Super2_Gate_t *, pLib->pGates,  3 * pLib->nGatesAlloc );
+        pLib->pGates  = ABC_REALLOC( Super2_Gate_t *, pLib->pGates,  3 * pLib->nGatesAlloc );
         pLib->nGatesAlloc *= 3;
     }
     pLib->pGates[ pLib->nGates++ ] = pGate;
@@ -267,8 +267,8 @@ void Super2_LibAddGate( Super2_Lib_t * pLib, Super2_Gate_t * pGate )
 ***********************************************************************/
 void Super2_LibStop( Super2_Lib_t * pLib )
 {
-    free( pLib->pGates );
-    free( pLib );
+    ABC_FREE( pLib->pGates );
+    ABC_FREE( pLib );
 }
 
 /**Function*************************************************************
@@ -297,7 +297,7 @@ Super2_Lib_t * Super2_LibFirst( Super2_Man_t * pMan, int nInputs )
     pLib->nGates      = nInputs + 1;
     pLib->nGatesAlloc = nInputs + 1;
     pLib->uMaskBit    = (1 << (pLib->nMints-1));
-    pLib->pGates      = ALLOC( Super2_Gate_t *, nInputs + 1 );
+    pLib->pGates      = ABC_ALLOC( Super2_Gate_t *, nInputs + 1 );
     // add the constant 0
     pLib->pGates[0] = (Super2_Gate_t *)Extra_MmFixedEntryFetch( pMan->pMem );
     memset( pLib->pGates[0], 0, sizeof(Super2_Gate_t) );
@@ -306,7 +306,7 @@ Super2_Lib_t * Super2_LibFirst( Super2_Man_t * pMan, int nInputs )
     {
         pLib->pGates[v+1] = (Super2_Gate_t *)Extra_MmFixedEntryFetch( pMan->pMem );
         memset( pLib->pGates[v+1], 0, sizeof(Super2_Gate_t) );
-        pLib->pGates[v+1]->pTwo = (Super2_Gate_t *)(PORT_PTRUINT_T)v;
+        pLib->pGates[v+1]->pTwo = (Super2_Gate_t *)(ABC_PTRUINT_T)v;
     }
 
     // set up their truth tables
@@ -347,7 +347,7 @@ Super2_Lib_t * Super2_LibCompute( Super2_Man_t * pMan, Super2_Lib_t * pLib )
     {
         uTruthR = ((pGate1->uTruth & pLibNew->uMaskBit)? Mask & ~pGate1->uTruth : pGate1->uTruth);
 
-        if ( stmm_lookup( pMan->tTable, (char *)(PORT_PTRUINT_T)uTruthR, (char **)&pGate2 ) )
+        if ( stmm_lookup( pMan->tTable, (char *)(ABC_PTRUINT_T)uTruthR, (char **)&pGate2 ) )
         {
             printf( "New gate:\n" );
             Super2_LibWriteGate( stdout, pLibNew, pGate1 );
@@ -355,7 +355,7 @@ Super2_Lib_t * Super2_LibCompute( Super2_Man_t * pMan, Super2_Lib_t * pLib )
             Super2_LibWriteGate( stdout, pLibNew, pGate2 );
             assert( 0 );
         }
-        stmm_insert( pMan->tTable, (char *)(PORT_PTRUINT_T)uTruthR, (char *)(PORT_PTRUINT_T)pGate1 );
+        stmm_insert( pMan->tTable, (char *)(ABC_PTRUINT_T)uTruthR, (char *)(ABC_PTRUINT_T)pGate1 );
     }
 
 
@@ -382,7 +382,7 @@ Super2_Lib_t * Super2_LibCompute( Super2_Man_t * pMan, Super2_Lib_t * pLib )
             uTruth  = uTruth1  & uTruth2;
             uTruthR = ((uTruth & pLibNew->uMaskBit)? Mask & ~uTruth : uTruth);
 
-            if ( !stmm_find_or_add( pMan->tTable, (char *)(PORT_PTRUINT_T)uTruthR, (char ***)&ppGate ) )
+            if ( !stmm_find_or_add( pMan->tTable, (char *)(ABC_PTRUINT_T)uTruthR, (char ***)&ppGate ) )
             {
                 pGateNew = (Super2_Gate_t *)Extra_MmFixedEntryFetch( pMan->pMem );
                 pGateNew->pOne  = pGate1;
@@ -396,7 +396,7 @@ Super2_Lib_t * Super2_LibCompute( Super2_Man_t * pMan, Super2_Lib_t * pLib )
             uTruth  = uTruth1c & uTruth2;
             uTruthR = ((uTruth & pLibNew->uMaskBit)? Mask & ~uTruth : uTruth);
 
-            if ( !stmm_find_or_add( pMan->tTable, (char *)(PORT_PTRUINT_T)uTruthR, (char ***)&ppGate ) )
+            if ( !stmm_find_or_add( pMan->tTable, (char *)(ABC_PTRUINT_T)uTruthR, (char ***)&ppGate ) )
             {
                 pGateNew = (Super2_Gate_t *)Extra_MmFixedEntryFetch( pMan->pMem );
                 pGateNew->pOne  = Super2_Not(pGate1);
@@ -410,7 +410,7 @@ Super2_Lib_t * Super2_LibCompute( Super2_Man_t * pMan, Super2_Lib_t * pLib )
             uTruth  = uTruth1  & uTruth2c;
             uTruthR = ((uTruth & pLibNew->uMaskBit)? Mask & ~uTruth : uTruth);
 
-            if ( !stmm_find_or_add( pMan->tTable, (char *)(PORT_PTRUINT_T)uTruthR, (char ***)&ppGate ) )
+            if ( !stmm_find_or_add( pMan->tTable, (char *)(ABC_PTRUINT_T)uTruthR, (char ***)&ppGate ) )
             {
                 pGateNew = (Super2_Gate_t *)Extra_MmFixedEntryFetch( pMan->pMem );
                 pGateNew->pOne  = pGate1;
@@ -424,7 +424,7 @@ Super2_Lib_t * Super2_LibCompute( Super2_Man_t * pMan, Super2_Lib_t * pLib )
             uTruth  = uTruth1c & uTruth2c;
             uTruthR = ((uTruth & pLibNew->uMaskBit)? Mask & ~uTruth : uTruth);
 
-            if ( !stmm_find_or_add( pMan->tTable, (char *)(PORT_PTRUINT_T)uTruthR, (char ***)&ppGate ) )
+            if ( !stmm_find_or_add( pMan->tTable, (char *)(ABC_PTRUINT_T)uTruthR, (char ***)&ppGate ) )
             {
                 pGateNew = (Super2_Gate_t *)Extra_MmFixedEntryFetch( pMan->pMem );
                 pGateNew->pOne  = Super2_Not(pGate1);
@@ -475,7 +475,7 @@ clk = clock();
     qsort( (void *)pLib->pGates, pLib->nGates, sizeof(Super2_Gate_t *), 
             (int (*)(const void *, const void *)) Super2_LibCompareGates );
     assert( Super2_LibCompareGates( pLib->pGates, pLib->pGates + pLib->nGates - 1 ) < 0 );
-PRT( "Sorting", clock() - clk );
+ABC_PRT( "Sorting", clock() - clk );
 
 
     // start the file
@@ -600,7 +600,7 @@ char * Super2_LibWriteGate_rec( Super2_Gate_t * pGate, int fInv, int Level )
         }
         else
         {
-            pBuffer1[0] = (fInv? 'A' + ((int)(PORT_PTRUINT_T)pGate->pTwo): 'a' + ((int)(PORT_PTRUINT_T)pGate->pTwo));
+            pBuffer1[0] = (fInv? 'A' + ((int)(ABC_PTRUINT_T)pGate->pTwo): 'a' + ((int)(ABC_PTRUINT_T)pGate->pTwo));
             pBuffer1[1] = 0;
         }
         return pBuffer1;
diff --git a/src/map/super/superGate.c b/src/map/super/superGate.c
index c8aa02ba..7bc5e703 100644
--- a/src/map/super/superGate.c
+++ b/src/map/super/superGate.c
@@ -164,7 +164,7 @@ void Super_Precompute( Mio_Library_t * pLibGen, int nVarsMax, int nLevels, float
 
         // stop the manager
         Super_ManStop( pMan );
-        free( ppGates );
+        ABC_FREE( ppGates );
 
         return;
     }
@@ -193,7 +193,7 @@ if ( fVerbose )
 {
         printf( "Lev %d: Try =%12d. Add =%6d. Rem =%5d. Save =%6d. Lookups =%12d. Aliases =%12d. ",
            Level, pMan->nTried, pMan->nAdded, pMan->nRemoved, pMan->nAdded - pMan->nRemoved, pMan->nLookups, pMan->nAliases );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 fflush( stdout );
 }
     }
@@ -209,7 +209,7 @@ fflush( stdout );
 
     // stop the manager
     Super_ManStop( pMan );
-    free( ppGates );
+    ABC_FREE( ppGates );
 }
 
 
@@ -235,7 +235,7 @@ void Super_First( Super_Man_t * pMan, int nVarsMax )
     pMan->nLevels   = 0;
     // allocate room for the gates
     pMan->nGates    = nVarsMax;  
-    pMan->pGates    = ALLOC( Super_Gate_t *, nVarsMax + 2 ); 
+    pMan->pGates    = ABC_ALLOC( Super_Gate_t *, nVarsMax + 2 ); 
     // create the gates corresponding to the elementary variables
     for ( v = 0; v < nVarsMax; v++ )
     {
@@ -329,7 +329,7 @@ Super_Man_t * Super_Compute( Super_Man_t * pMan, Mio_Gate_t ** ppGates, int nGat
 
     pProgress = Extra_ProgressBarStart( stdout, pMan->TimeLimit );
     pMan->TimePrint = clock() + CLOCKS_PER_SEC;
-    ppGatesLimit = ALLOC( Super_Gate_t *, pMan->nGates );
+    ppGatesLimit = ABC_ALLOC( Super_Gate_t *, pMan->nGates );
     // go through the root gates
     // the root gates are sorted in the increasing gelay
     fTimeOut = 0;
@@ -658,7 +658,7 @@ Super_Man_t * Super_Compute( Super_Man_t * pMan, Mio_Gate_t ** ppGates, int nGat
     }
 done: 
     Extra_ProgressBarStop( pProgress );
-    free( ppGatesLimit );
+    ABC_FREE( ppGatesLimit );
     return pMan;
 }
 
@@ -709,8 +709,8 @@ void Super_TranferGatesToArray( Super_Man_t * pMan )
     unsigned Key;
 
     // put the gates fron the table into the array
-    free( pMan->pGates );
-    pMan->pGates = ALLOC( Super_Gate_t *, pMan->nAdded );
+    ABC_FREE( pMan->pGates );
+    pMan->pGates = ABC_ALLOC( Super_Gate_t *, pMan->nAdded );
     pMan->nGates = 0;
     stmm_foreach_item( pMan->tTable, gen, (char **)&Key, (char **)&pList )
     {
@@ -737,7 +737,7 @@ void Super_AddGateToTable( Super_Man_t * pMan, Super_Gate_t * pGate )
     unsigned Key;
 //    Key = pGate->uTruth[0] + 2003 * pGate->uTruth[1];
     Key = pGate->uTruth[0] ^ pGate->uTruth[1];
-    if ( !stmm_find_or_add( pMan->tTable, (char *)(PORT_PTRUINT_T)Key, (char ***)&ppList ) )
+    if ( !stmm_find_or_add( pMan->tTable, (char *)(ABC_PTRUINT_T)Key, (char ***)&ppList ) )
         *ppList = NULL;
     pGate->pNext = *ppList;
     *ppList = pGate;
@@ -778,7 +778,7 @@ bool Super_CompareGates( Super_Man_t * pMan, unsigned uTruth[], float Area, floa
     // get hold of the place where the entry is stored
 //    Key = uTruth[0] + 2003 * uTruth[1];
     Key = uTruth[0] ^ uTruth[1];
-    if ( !stmm_find( pMan->tTable, (char *)(PORT_PTRUINT_T)Key, (char ***)&ppList ) )
+    if ( !stmm_find( pMan->tTable, (char *)(ABC_PTRUINT_T)Key, (char ***)&ppList ) )
         return 1; 
     // the entry with this truth table is found
     pPrev = NULL;
@@ -872,7 +872,7 @@ Super_Gate_t * Super_CreateGateNew( Super_Man_t * pMan, Mio_Gate_t * pRoot, Supe
 Super_Man_t * Super_ManStart()
 {
     Super_Man_t * pMan;
-    pMan = ALLOC( Super_Man_t, 1 );
+    pMan = ABC_ALLOC( Super_Man_t, 1 );
     memset( pMan, 0, sizeof(Super_Man_t) );
     pMan->pMem     = Extra_MmFixedStart( sizeof(Super_Gate_t) );
     pMan->tTable   = stmm_init_table( st_ptrcmp, st_ptrhash );
@@ -894,8 +894,8 @@ void Super_ManStop( Super_Man_t * pMan )
 {
     Extra_MmFixedStop( pMan->pMem );
     if ( pMan->tTable ) stmm_free_table( pMan->tTable );
-    FREE( pMan->pGates );
-    free( pMan );
+    ABC_FREE( pMan->pGates );
+    ABC_FREE( pMan );
 }
 
 
@@ -930,8 +930,8 @@ void Super_Write( Super_Man_t * pMan )
     // the given limit, provided that the inputs are not consequtive. 
     // For example, NAND2(a,c) is removed, but NAND2(a,b) is left, 
     // because a and b are consequtive.
-    FREE( pMan->pGates );
-    pMan->pGates = ALLOC( Super_Gate_t *, pMan->nAdded );
+    ABC_FREE( pMan->pGates );
+    pMan->pGates = ABC_ALLOC( Super_Gate_t *, pMan->nAdded );
     pMan->nGates = 0;
     stmm_foreach_item( pMan->tTable, gen, (char **)&Key, (char **)&pGateRoot )
     {
@@ -961,7 +961,7 @@ clk = clock();
     assert( Super_WriteCompare( pMan->pGates, pMan->pGates + pMan->nGates - 1 ) <= 0 );
 if ( pMan->fVerbose )
 {
-PRT( "Sorting", clock() - clk );
+ABC_PRT( "Sorting", clock() - clk );
 }
 
 
@@ -971,7 +971,7 @@ clk = clock();
         Super_WriteLibrary( pMan );
 if ( pMan->fVerbose )
 {
-PRT( "Writing old format", clock() - clk );
+ABC_PRT( "Writing old format", clock() - clk );
 }
 
     // write the tree-like structure of supergates
@@ -979,7 +979,7 @@ clk = clock();
     Super_WriteLibraryTree( pMan );
 if ( pMan->fVerbose )
 {
-PRT( "Writing new format", clock() - clk );
+ABC_PRT( "Writing new format", clock() - clk );
 }
 }
 
@@ -1114,7 +1114,7 @@ void Super_WriteLibrary( Super_Man_t * pMan )
     // get the file name
     pNameGeneric = Extra_FileNameGeneric( pMan->pName );
     sprintf( FileName, "%s.super_old", pNameGeneric );
-    free( pNameGeneric );
+    ABC_FREE( pNameGeneric );
 
     // count the number of unique functions
     pMan->nUnique = 1;
@@ -1259,7 +1259,7 @@ void Super_WriteLibraryTree( Super_Man_t * pMan )
     // get the file name
     pNameGeneric = Extra_FileNameGeneric( pMan->pName );
     sprintf( FileName, "%s.super", pNameGeneric );
-    free( pNameGeneric );
+    ABC_FREE( pNameGeneric );
  
     // write the elementary variables
     pFile = fopen( FileName, "w" );