Version abc90118

31 files changed, 5152 insertions, 108 deletions

diff --git a/src/map/amap/amap.h b/src/map/amap/amap.h
new file mode 100644
index 00000000..ee845e7f
--- /dev/null
+++ b/src/map/amap/amap.h
@@ -0,0 +1,83 @@
+/**CFile****************************************************************
+
+  FileName    [amap.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amap.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __AMAP_H__
+#define __AMAP_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+typedef struct Amap_Par_t_ Amap_Par_t;
+struct Amap_Par_t_
+{
+    int    nIterFlow;   // iterations of area flow
+    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)
+    float  fEpsilon;    // used to compare floating point numbers
+    int    fVerbose;    // verbosity flag
+};
+
+typedef struct Amap_Out_t_ Amap_Out_t;
+struct Amap_Out_t_
+{
+    char * pName;     // gate name
+    short  Type;      // node type   (-1=input; 0=internal; 1=output)
+    short  nFans;     // number of fanins
+    int    pFans[0];  // fanin
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== amapCore.c ==========================================================*/
+extern void        Amap_ManSetDefaultParams( Amap_Par_t * pPars );
+extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/map/amap/amapCore.c b/src/map/amap/amapCore.c
new file mode 100644
index 00000000..f1554862
--- /dev/null
+++ b/src/map/amap/amapCore.c
@@ -0,0 +1,103 @@
+/**CFile****************************************************************
+
+  FileName    [amapCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Core mapping procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManSetDefaultParams( Amap_Par_t * p )
+{
+    memset( p, 0, sizeof(Amap_Par_t) );
+    p->nIterFlow = 1;            // iterations of area flow
+    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->fEpsilon  = (float)0.001; // used to compare floating point numbers
+    p->fVerbose  = 0;            // verbosity flag
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars )
+{
+    extern void * Abc_FrameReadLibGen2();
+    Vec_Ptr_t * vRes;
+    Amap_Man_t * p;
+    Amap_Lib_t * pLib;
+    int clkTotal = clock();
+    pLib = Abc_FrameReadLibGen2();
+    if ( pLib == NULL )
+    {
+        printf( "Library is not available.\n" );
+        return NULL;
+    }
+    p = Amap_ManStart( Aig_ManNodeNum(pAig) );
+    p->pPars = pPars;
+    p->pLib  = pLib;
+    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 );
+    Amap_ManCreate( p, pAig );
+    Amap_ManMap( p );
+    vRes = NULL;
+    vRes = Amap_ManProduceMapped( p );
+    Amap_ManStop( p );
+if ( pPars->fVerbose )
+{
+PRT( "Total runtime", clock() - clkTotal );
+}
+    return vRes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapGraph.c b/src/map/amap/amapGraph.c
new file mode 100644
index 00000000..83cadc2c
--- /dev/null
+++ b/src/map/amap/amapGraph.c
@@ -0,0 +1,389 @@
+/**CFile****************************************************************
+
+  FileName    [amapGraph.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Internal AIG manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapGraph.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Obj_t * Amap_ManSetupObj( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    pObj = (Amap_Obj_t *)Aig_MmFixedEntryFetch( p->pMemObj );
+    memset( pObj, 0, sizeof(Amap_Obj_t) );
+    pObj->nFouts[0] = 1; // needed for flow to work in the first pass
+    pObj->Id = Vec_PtrSize(p->vObjs);
+    Vec_PtrPush( p->vObjs, pObj );
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates constant 1 node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Obj_t * Amap_ManCreateConst1( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    pObj = Amap_ManSetupObj( p );
+    pObj->Type   = AMAP_OBJ_CONST1;
+    pObj->fPhase = 1;
+    p->nObjs[AMAP_OBJ_CONST1]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates primary input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Obj_t * Amap_ManCreatePi( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    pObj = Amap_ManSetupObj( p );
+    pObj->Type  = AMAP_OBJ_PI;
+    pObj->IdPio = Vec_PtrSize( p->vPis );
+    Vec_PtrPush( p->vPis, pObj );
+    p->nObjs[AMAP_OBJ_PI]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates primary output with the given driver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Obj_t * Amap_ManCreatePo( Amap_Man_t * p, Amap_Obj_t * pFan0 )
+{
+    Amap_Obj_t * pObj;
+    pObj = Amap_ManSetupObj( p );
+    pObj->IdPio  = Vec_PtrSize( p->vPos );
+    Vec_PtrPush( p->vPos, pObj );
+    pObj->Type   = AMAP_OBJ_PO;
+    pObj->Fan[0] = Amap_ObjToLit(pFan0);  Amap_Regular(pFan0)->nRefs++;
+    pObj->Level  = Amap_Regular(pFan0)->Level;
+    if ( p->nLevelMax < (int)pObj->Level )
+        p->nLevelMax = (int)pObj->Level;
+    p->nObjs[AMAP_OBJ_PO]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Obj_t * Amap_ManCreateAnd( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pFan1 )
+{
+    Amap_Obj_t * pObj;
+    pObj = Amap_ManSetupObj( p );
+    pObj->Type   = AMAP_OBJ_AND;
+    pObj->Fan[0] = Amap_ObjToLit(pFan0);  Amap_Regular(pFan0)->nRefs++;
+    pObj->Fan[1] = Amap_ObjToLit(pFan1);  Amap_Regular(pFan1)->nRefs++;
+    assert( Amap_Lit2Var(pObj->Fan[0]) != Amap_Lit2Var(pObj->Fan[1]) );
+    pObj->fPhase = Amap_ObjPhaseReal(pFan0) & Amap_ObjPhaseReal(pFan1);
+    pObj->Level  = 1 + AIG_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
+    if ( p->nLevelMax < (int)pObj->Level )
+        p->nLevelMax = (int)pObj->Level;
+    p->nObjs[AMAP_OBJ_AND]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Obj_t * Amap_ManCreateXor( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pFan1 )
+{
+    Amap_Obj_t * pObj;
+    pObj = Amap_ManSetupObj( p );
+    pObj->Type   = AMAP_OBJ_XOR;
+    pObj->Fan[0] = Amap_ObjToLit(pFan0);  Amap_Regular(pFan0)->nRefs++;
+    pObj->Fan[1] = Amap_ObjToLit(pFan1);  Amap_Regular(pFan1)->nRefs++;
+    pObj->fPhase = Amap_ObjPhaseReal(pFan0) ^ Amap_ObjPhaseReal(pFan1);
+    pObj->Level  = 2 + AIG_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
+    if ( p->nLevelMax < (int)pObj->Level )
+        p->nLevelMax = (int)pObj->Level;
+    p->nObjs[AMAP_OBJ_XOR]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Obj_t * Amap_ManCreateMux( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pFan1, Amap_Obj_t * pFanC )
+{
+    Amap_Obj_t * pObj;
+    pObj = Amap_ManSetupObj( p );
+    pObj->Type   = AMAP_OBJ_MUX;
+    pObj->Fan[0] = Amap_ObjToLit(pFan0);  Amap_Regular(pFan0)->nRefs++;
+    pObj->Fan[1] = Amap_ObjToLit(pFan1);  Amap_Regular(pFan1)->nRefs++;
+    pObj->Fan[2] = Amap_ObjToLit(pFanC);  Amap_Regular(pFanC)->nRefs++;
+    pObj->fPhase = (Amap_ObjPhaseReal(pFan1) &  Amap_ObjPhaseReal(pFanC)) | 
+                   (Amap_ObjPhaseReal(pFan0) & ~Amap_ObjPhaseReal(pFanC));
+    pObj->Level  = AIG_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
+    pObj->Level  = 2 + AIG_MAX( pObj->Level, Amap_Regular(pFanC)->Level );
+    if ( p->nLevelMax < (int)pObj->Level )
+        p->nLevelMax = (int)pObj->Level;
+    p->nObjs[AMAP_OBJ_MUX]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the choice node.]
+
+  Description [Should be called after the equivalence class nodes are linked.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManCreateChoice( Amap_Man_t * p, Amap_Obj_t * pObj )
+{
+    Amap_Obj_t * pTemp;
+    // mark the node as a representative if its class
+//    assert( pObj->fRepr == 0 );
+    pObj->fRepr = 1;
+    // update the level of this node (needed for correct required time computation)
+    for ( pTemp = pObj; pTemp; pTemp = Amap_ObjChoice(p, pTemp) )
+    {
+        pObj->Level = AIG_MAX( pObj->Level, pTemp->Level );
+//        pTemp->nVisits++; pTemp->nVisitsCopy++;
+    }
+    // mark the largest level
+    if ( p->nLevelMax < (int)pObj->Level )
+        p->nLevelMax = (int)pObj->Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates XOR/MUX choices for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManCreateXorChoices( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pFan1, Amap_Obj_t * pChoices[] )
+{
+    pChoices[0] = Amap_ManCreateXor( p, pFan0,           pFan1 );
+    pChoices[1] = Amap_ManCreateXor( p, Amap_Not(pFan0), pFan1 );
+    pChoices[2] = Amap_ManCreateXor( p, pFan0,           Amap_Not(pFan1) );
+    pChoices[3] = Amap_ManCreateXor( p, Amap_Not(pFan0), Amap_Not(pFan1) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates XOR/MUX choices for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManCreateMuxChoices( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pFan1, Amap_Obj_t * pFanC, Amap_Obj_t * pChoices[] )
+{
+    pChoices[0] = Amap_ManCreateMux( p, pFan0,           pFan1,           pFanC           );
+    pChoices[1] = Amap_ManCreateMux( p, Amap_Not(pFan0), Amap_Not(pFan1), pFanC           );
+    pChoices[2] = Amap_ManCreateMux( p, pFan1,           pFan0,           Amap_Not(pFanC) );
+    pChoices[3] = Amap_ManCreateMux( p, Amap_Not(pFan1), Amap_Not(pFan0), Amap_Not(pFanC) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Drags pointer out through the copy.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Amap_Obj_t * Amap_AndToObj( Aig_Obj_t * pObj )
+{
+    return Amap_NotCond( (Amap_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Obj_t * Amap_ManGetLast_rec( Amap_Man_t * p, Amap_Obj_t * pObj )
+{
+    if ( pObj->Equiv == 0 )
+        return pObj;
+    return Amap_ManGetLast_rec( p, Amap_ObjChoice(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManCreate( Amap_Man_t * p, Aig_Man_t * pAig )
+{
+    Vec_Ptr_t * vNodes;
+    Amap_Obj_t * pChoices[4];
+    Aig_Obj_t * pObj, * pFanin, * pPrev, * pFan0, * pFan1, * pFanC;
+    int i, fChoices;
+    if ( pAig->pEquivs )
+        vNodes = Aig_ManDfsChoices( pAig );
+    else
+        vNodes = Aig_ManDfs( pAig, 1 );
+    p->pConst1 = Amap_ManCreateConst1( p );
+    // print warning about excessive memory usage
+    if ( p->pPars->fVerbose )
+    {
+        if ( 1.0 * Aig_ManObjNum(pAig) * sizeof(Amap_Obj_t) / (1<<30) > 0.1 )
+        printf( "Warning: Mapper allocates %.3f Gb for subject graph with %d objects.\n", 
+            1.0 * Aig_ManObjNum(pAig) * sizeof(Amap_Obj_t) / (1<<30), Aig_ManObjNum(pAig) );
+    }
+    // create PIs and remember them in the old nodes
+    Aig_ManCleanData(pAig);
+    Aig_ManConst1(pAig)->pData = Amap_ManConst1( p );
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Amap_ManCreatePi( p );
+    // load the AIG into the mapper
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        fChoices = 0;
+        if ( p->fUseXor && Aig_ObjRecognizeExor(pObj, &pFan0, &pFan1 ) )
+        {
+            Amap_ManCreateXorChoices( p, Amap_AndToObj(pFan0), Amap_AndToObj(pFan1), pChoices );
+            fChoices = 1;
+        }
+        else if ( p->fUseMux && Aig_ObjIsMuxType(pObj) )
+        {
+            pFanC = Aig_ObjRecognizeMux( pObj, &pFan1, &pFan0 );
+            Amap_ManCreateMuxChoices( p, Amap_AndToObj(pFan0), Amap_AndToObj(pFan1), Amap_AndToObj(pFanC), pChoices );
+            fChoices = 1;
+        }
+        pObj->pData = Amap_ManCreateAnd( p, (Amap_Obj_t *)Aig_ObjChild0Copy(pObj), (Amap_Obj_t *)Aig_ObjChild1Copy(pObj) );
+        if ( fChoices )
+        {
+            p->nChoicesAdded++;
+            Amap_ObjSetChoice( (Amap_Obj_t *)pObj->pData, pChoices[0] );
+            Amap_ObjSetChoice( pChoices[0], pChoices[1] );
+            Amap_ObjSetChoice( pChoices[1], pChoices[2] );
+            Amap_ObjSetChoice( pChoices[2], pChoices[3] );
+            Amap_ManCreateChoice( p, (Amap_Obj_t *)pObj->pData );
+        }
+        if ( Aig_ObjIsChoice( pAig, pObj ) )
+        {
+//            assert( !fChoices );
+            p->nChoicesGiven++;
+            for ( pPrev = pObj, pFanin = Aig_ObjEquiv(pAig, pObj); pFanin; pPrev = pFanin, pFanin = Aig_ObjEquiv(pAig, pFanin) )
+            {
+                ((Amap_Obj_t *)pFanin->pData)->fRepr = 0;
+                Amap_ObjSetChoice( Amap_ManGetLast_rec(p, (Amap_Obj_t *)pPrev->pData), 
+                    (Amap_Obj_t *)pFanin->pData );
+            }
+            Amap_ManCreateChoice( p, (Amap_Obj_t *)pObj->pData );
+        }
+    }
+    Vec_PtrFree( vNodes );
+    // set the primary outputs without copying the phase
+    Aig_ManForEachPo( pAig, pObj, i )
+        pObj->pData = Amap_ManCreatePo( p, (Amap_Obj_t *)Aig_ObjChild0Copy(pObj) );
+    if ( p->pPars->fVerbose )
+        printf( "Performing mapping with %d given and %d created choices.\n", 
+            p->nChoicesGiven, p->nChoicesAdded );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapInt.h b/src/map/amap/amapInt.h
new file mode 100644
index 00000000..954790c9
--- /dev/null
+++ b/src/map/amap/amapInt.h
@@ -0,0 +1,380 @@
+/**CFile****************************************************************
+
+  FileName    [amapInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __AMAP_INT_H__
+#define __AMAP_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+#include "amap.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+// the largest gate size in the library
+// (gates above this size will be ignored)
+#define AMAP_MAXINS 15
+
+#define AMAP_STRING_CONST0     "CONST0"
+#define AMAP_STRING_CONST1     "CONST1"
+
+// object types
+typedef enum { 
+    AMAP_OBJ_NONE,    // 0: non-existent object
+    AMAP_OBJ_CONST1,  // 1: constant 1 
+    AMAP_OBJ_PI,      // 2: primary input
+    AMAP_OBJ_PO,      // 3: primary output
+    AMAP_OBJ_AND,     // 4: AND node
+    AMAP_OBJ_XOR,     // 5: XOR node
+    AMAP_OBJ_MUX,     // 6: MUX node
+    AMAP_OBJ_VOID     // 7: unused object
+} Amap_Type_t;
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Amap_Lib_t_ Amap_Lib_t;
+typedef struct Amap_Pin_t_ Amap_Pin_t;
+typedef struct Amap_Gat_t_ Amap_Gat_t;
+typedef struct Amap_Nod_t_ Amap_Nod_t;
+typedef struct Amap_Set_t_ Amap_Set_t;
+
+typedef struct Amap_Man_t_ Amap_Man_t;
+typedef struct Amap_Obj_t_ Amap_Obj_t;
+typedef struct Amap_Cut_t_ Amap_Cut_t;
+typedef struct Amap_Mat_t_ Amap_Mat_t;
+
+struct Amap_Man_t_
+{
+    // user data
+    Amap_Par_t *       pPars;
+    Amap_Lib_t *       pLib;
+    // internal parameters
+    float              fEpsilonInternal;
+    float              fAreaInv;
+    int                fUseXor;    
+    int                fUseMux;    
+    // internal AIG with choices
+    Vec_Ptr_t *        vPis;
+    Vec_Ptr_t *        vPos;
+    Vec_Ptr_t *        vObjs;
+    Aig_MmFixed_t *    pMemObj;
+    Aig_MmFlex_t *     pMemCuts;
+    Aig_MmFlex_t *     pMemCutBest;
+    Aig_MmFlex_t *     pMemTemp;
+    Amap_Obj_t *       pConst1;
+    int                nObjs[AMAP_OBJ_VOID];
+    int                nLevelMax;
+    int                nChoicesGiven;
+    int                nChoicesAdded;
+    // mapping data-structures
+    Vec_Int_t *        vTemp;
+    int *              pMatsTemp;
+    Amap_Cut_t **      ppCutsTemp;
+    Amap_Cut_t *       pCutsPi;
+    Vec_Ptr_t *        vCuts0;
+    Vec_Ptr_t *        vCuts1;
+    Vec_Ptr_t *        vCuts2;
+    // statistics
+    int                nCutsUsed;
+    int                nCutsTried;
+    int                nCutsTried3;
+    int                nBytesUsed;
+};
+struct Amap_Lib_t_
+{
+    char *             pName;       // library name
+    Vec_Ptr_t *        vGates;      // represenation of gates
+    Vec_Ptr_t *        vSorted;     // gates sorted for area-only mapping
+    Vec_Ptr_t *        vSelect;     // gates selected for area-only mapping
+    Amap_Gat_t *       pGate0;      // the constant zero gate
+    Amap_Gat_t *       pGate1;      // the constant one gate
+    Amap_Gat_t *       pGateBuf;    // the buffer
+    Amap_Gat_t *       pGateInv;    // the inverter
+    Aig_MmFlex_t *     pMemGates;   // memory manager for objects
+    int                fHasXor;     // XOR/NXOR gates are present
+    int                fHasMux;     // MUX/NMUX gates are present
+    // structural representation
+    int                fVerbose;    // enable detailed statistics
+    Amap_Nod_t *       pNodes;      // representation nodes
+    int                nNodes;      // the number of nodes used
+    int                nNodesAlloc; // the number of nodes allocated
+    Vec_Ptr_t *        vRules;      // the rule of AND gate
+    Vec_Ptr_t *        vRulesX;     // the rule of XOR gate
+    Vec_Int_t *        vRules3;     // the rule of MUX gate
+    int **             pRules;      // simplified representation
+    int **             pRulesX;     // simplified representation
+    Aig_MmFlex_t *     pMemSet;     // memory manager for sets
+    int                nSets;       // the number of sets created
+};
+struct Amap_Pin_t_
+{
+    char *             pName;
+    int                Phase;
+    double             dLoadInput;
+    double             dLoadMax;
+    double             dDelayBlockRise;
+    double             dDelayFanoutRise;
+    double             dDelayBlockFall;
+    double             dDelayFanoutFall;
+    double             dDelayBlockMax;
+};
+struct Amap_Gat_t_
+{
+    Amap_Lib_t *       pLib;            // library   
+    char *             pName;           // the name of the gate
+    char *             pOutName;        // name of the output
+    double             dArea;           // the area of the gate
+    char *             pForm;           // the formula describing functionality
+    unsigned *         pFunc;           // truth table
+    unsigned           Id     :   23;   // unique number of the gate
+    unsigned           fMux   :    1;   // denotes MUX-gates
+    unsigned           nPins  :    8;   // number of inputs
+    Amap_Pin_t         Pins[0];         // description of inputs
+};
+struct Amap_Set_t_
+{
+    Amap_Set_t *       pNext;
+    unsigned           iGate    : 16;
+    unsigned           fInv     :  1;
+    unsigned           nIns     : 15;
+    char               Ins[AMAP_MAXINS];// mapping from gate inputs into fanins
+};
+struct Amap_Nod_t_
+{
+    unsigned           Id       : 16;   // ID of the node
+    unsigned           nSuppSize:  8;   // support size
+    unsigned           Type     :  8;   // the type of node
+    short              iFan0;           // fanin0
+    short              iFan1;           // fanin1
+    short              iFan2;           // fanin2
+    short              Unused;          // 
+    Amap_Set_t *       pSets;           // implementable gates
+};
+struct Amap_Cut_t_
+{
+    unsigned           iMat     : 16;
+    unsigned           fInv     :  1;
+    unsigned           nFans  : 15;
+    int                Fans[0];
+};
+struct Amap_Mat_t_
+{
+    Amap_Cut_t *       pCut;           // the cut
+    Amap_Set_t *       pSet;           // the set
+    float              Area;           // area flow / exact area of the node
+    float              AveFan;         // edge flow of the node
+    float              Delay;          // delay of the node
+};
+struct Amap_Obj_t_
+{
+    unsigned           Type     :  3;   
+    unsigned           Id       : 29;
+    unsigned           IdPio    : 29;
+    unsigned           fPhase   :  1;
+    unsigned           fRepr    :  1;
+    unsigned           fPolar   :  1;  // pCutBest->fInv ^ pSetBest->fInv
+    unsigned           Level    : 20;
+    unsigned           nCuts    : 12;
+    int                nRefs;
+    int                Equiv;
+    int                Fan[3];
+    union {
+    void *             pData;
+    int                iData;
+    };
+    // match of the node
+    float              EstRefs;        // the number of estimated fanouts
+    int                nFouts[2];      // the number of refs in each polarity
+    Amap_Mat_t         Best;           // the best match of the node
+};
+
+static inline int          Amap_Var2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
+static inline int          Amap_Lit2Var( int Lit )              { return Lit >> 1;           }
+static inline int          Amap_LitIsCompl( int Lit )           { return Lit & 1;            }
+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 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];                      }
+static inline int          Amap_ManAndNum( Amap_Man_t * p )                        { return p->nObjs[AMAP_OBJ_AND];                     }
+static inline int          Amap_ManXorNum( Amap_Man_t * p )                        { return p->nObjs[AMAP_OBJ_XOR];                     }
+static inline int          Amap_ManMuxNum( Amap_Man_t * p )                        { return p->nObjs[AMAP_OBJ_MUX];                     }
+static inline int          Amap_ManObjNum( Amap_Man_t * p )                        { return Vec_PtrSize(p->vObjs);                      }
+static inline int          Amap_ManNodeNum( Amap_Man_t * p )                       { return p->nObjs[AMAP_OBJ_AND] + p->nObjs[AMAP_OBJ_XOR] + p->nObjs[AMAP_OBJ_MUX];   }
+
+static inline Amap_Obj_t * Amap_ManConst1( Amap_Man_t * p )                        { return p->pConst1;                                 }
+static inline Amap_Obj_t * Amap_ManPi( Amap_Man_t * p, int i )                     { return (Amap_Obj_t *)Vec_PtrEntry( p->vPis, i );   }
+static inline Amap_Obj_t * Amap_ManPo( Amap_Man_t * p, int i )                     { return (Amap_Obj_t *)Vec_PtrEntry( p->vPos, i );   }
+static inline Amap_Obj_t * Amap_ManObj( Amap_Man_t * p, int i )                    { return (Amap_Obj_t *)Vec_PtrEntry( p->vObjs, i );  }
+
+static inline int          Amap_ObjIsConst1( Amap_Obj_t * pObj )                   { return pObj->Type == AMAP_OBJ_CONST1;              }
+static inline int          Amap_ObjIsPi( Amap_Obj_t * pObj )                       { return pObj->Type == AMAP_OBJ_PI;                  }
+static inline int          Amap_ObjIsPo( Amap_Obj_t * pObj )                       { return pObj->Type == AMAP_OBJ_PO;                  }
+static inline int          Amap_ObjIsAnd( Amap_Obj_t * pObj )                      { return pObj->Type == AMAP_OBJ_AND;                 }
+static inline int          Amap_ObjIsXor( Amap_Obj_t * pObj )                      { return pObj->Type == AMAP_OBJ_XOR;                 }
+static inline int          Amap_ObjIsMux( Amap_Obj_t * pObj )                      { return pObj->Type == AMAP_OBJ_MUX;                 }
+static inline int          Amap_ObjIsNode( Amap_Obj_t * pObj )                     { return pObj->Type == AMAP_OBJ_AND || pObj->Type == AMAP_OBJ_XOR || pObj->Type == AMAP_OBJ_MUX;  }
+
+static inline int          Amap_ObjToLit( Amap_Obj_t * pObj )                      { return Amap_Var2Lit( Amap_Regular(pObj)->Id, Amap_IsComplement(pObj) ); }
+static inline Amap_Obj_t * Amap_ObjFanin0( Amap_Man_t * p, Amap_Obj_t * pObj )     { return Amap_ManObj(p, Amap_Lit2Var(pObj->Fan[0])); }
+static inline Amap_Obj_t * Amap_ObjFanin1( Amap_Man_t * p, Amap_Obj_t * pObj )     { return Amap_ManObj(p, Amap_Lit2Var(pObj->Fan[1])); }
+static inline Amap_Obj_t * Amap_ObjFanin2( Amap_Man_t * p, Amap_Obj_t * pObj )     { return Amap_ManObj(p, Amap_Lit2Var(pObj->Fan[2])); }
+static inline int          Amap_ObjFaninC0( Amap_Obj_t * pObj )                    { return Amap_LitIsCompl(pObj->Fan[0]);              }
+static inline int          Amap_ObjFaninC1( Amap_Obj_t * pObj )                    { return Amap_LitIsCompl(pObj->Fan[1]);              }
+static inline int          Amap_ObjFaninC2( Amap_Obj_t * pObj )                    { return Amap_LitIsCompl(pObj->Fan[2]);              }
+static inline void *       Amap_ObjCopy( Amap_Obj_t * pObj )                       { return pObj->pData;                                }
+static inline int          Amap_ObjLevel( Amap_Obj_t * pObj )                      { return pObj->Level;                                }
+static inline void         Amap_ObjSetLevel( Amap_Obj_t * pObj, int Level )        { pObj->Level = Level;                               }
+static inline void         Amap_ObjSetCopy( Amap_Obj_t * pObj, void * pCopy )      { pObj->pData = pCopy;                               }
+static inline Amap_Obj_t * Amap_ObjChoice( Amap_Man_t * p, Amap_Obj_t * pObj )     { return pObj->Equiv? Amap_ManObj(p, pObj->Equiv) : NULL; }
+static inline void         Amap_ObjSetChoice( Amap_Obj_t * pObj, Amap_Obj_t * pEqu){ assert(pObj->Equiv==0); pObj->Equiv = pEqu->Id;                            }
+static inline int          Amap_ObjPhaseReal( Amap_Obj_t * pObj )                  { return Amap_Regular(pObj)->fPhase ^ Amap_IsComplement(pObj);   }
+static inline int          Amap_ObjRefsTotal( Amap_Obj_t * pObj )                  { return pObj->nFouts[0] + pObj->nFouts[1];          }
+
+static inline Amap_Gat_t * Amap_LibGate( Amap_Lib_t * p, int i ) { return Vec_PtrEntry(p->vGates, i); }
+static inline Amap_Nod_t * Amap_LibNod( Amap_Lib_t * p, int i )  { return p->pNodes + i;           }
+
+// returns pointer to the next cut (internal cuts only)
+static inline Amap_Cut_t * Amap_ManCutNext( Amap_Cut_t * pCut )
+{ return (Amap_Cut_t *)(((int *)pCut)+pCut->nFans+1); }
+// returns pointer to the place of the next cut (temporary cuts only)
+static inline Amap_Cut_t ** Amap_ManCutNextP( Amap_Cut_t * pCut )
+{ return (Amap_Cut_t **)(((int *)pCut)+pCut->nFans+1); }
+
+extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// iterator over the primary inputs
+#define Amap_ManForEachPi( p, pObj, i )                                    \
+    Vec_PtrForEachEntry( p->vPis, pObj, i )
+// iterator over the primary outputs
+#define Amap_ManForEachPo( p, pObj, i )                                    \
+    Vec_PtrForEachEntry( p->vPos, pObj, i )
+// iterator over all objects, including those currently not used
+#define Amap_ManForEachObj( p, pObj, i )                                   \
+    Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
+// iterator over all nodes
+#define Amap_ManForEachNode( p, pObj, i )                                  \
+    Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Amap_ObjIsNode(pObj) ) {} else
+
+// iterator through all gates of the library
+#define Amap_LibForEachGate( pLib, pGate, i )                              \
+    Vec_PtrForEachEntry( pLib->vGates, pGate, i )
+// iterator through all pins of the gate
+#define Amap_GateForEachPin( pGate, pPin )                                 \
+    for ( pPin = pGate->Pins; pPin < pGate->Pins + pGate->nPins; pPin++ )
+
+// iterator through all cuts of the node
+#define Amap_NodeForEachCut( pNode, pCut, i )                              \
+    for ( i = 0, pCut = (Amap_Cut_t *)pNode->pData; i < (int)pNode->nCuts; \
+        i++, pCut = Amap_ManCutNext(pCut) )
+
+// iterator through all sets of one library node
+#define Amap_LibNodeForEachSet( pNod, pSet )                               \
+    for ( pSet = pNod->pSets; pSet; pSet = pSet->pNext )
+
+// iterates through each fanin of the match
+#define Amap_MatchForEachFaninCompl( p, pM, pFanin, fCompl, i )            \
+    for ( i = 0; i < (int)(pM)->pCut->nFans &&                             \
+        ((pFanin = Amap_ManObj((p), Amap_Lit2Var((pM)->pCut->Fans[Amap_Lit2Var((pM)->pSet->Ins[i])]))), 1) && \
+        ((fCompl = Amap_LitIsCompl((pM)->pSet->Ins[i]) ^ Amap_LitIsCompl((pM)->pCut->Fans[Amap_Lit2Var((pM)->pSet->Ins[i])])), 1); \
+        i++ )
+
+// iterates through each fanin of the match
+#define Amap_MatchForEachFanin( p, pM, pFanin, i )                         \
+    for ( i = 0; i < (int)(pM)->pCut->nFans &&                             \
+        ((pFanin = Amap_ManObj((p), Amap_Lit2Var((pM)->pCut->Fans[Amap_Lit2Var((pM)->pSet->Ins[i])]))), 1); \
+        i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== amapCore.c ==========================================================*/
+/*=== amapGraph.c ==========================================================*/
+extern Amap_Obj_t *  Amap_ManCreatePi( Amap_Man_t * p );
+extern Amap_Obj_t *  Amap_ManCreatePo( Amap_Man_t * p, Amap_Obj_t * pFan0 );
+extern Amap_Obj_t *  Amap_ManCreateAnd( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pFan1 );
+extern Amap_Obj_t *  Amap_ManCreateXor( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t * pFan1 );
+extern Amap_Obj_t *  Amap_ManCreateMux( Amap_Man_t * p, Amap_Obj_t * pFanC, Amap_Obj_t * pFan1, Amap_Obj_t * pFan0 );
+extern void          Amap_ManCreateChoice( Amap_Man_t * p, Amap_Obj_t * pObj );
+extern void          Amap_ManCreate( Amap_Man_t * p, Aig_Man_t * pAig );
+/*=== amapLib.c ==========================================================*/
+extern Amap_Lib_t *  Amap_LibAlloc();
+extern void          Amap_LibFree( Amap_Lib_t * p );
+extern int           Amap_LibNumPinsMax( Amap_Lib_t * p );
+extern void          Amap_LibWrite( FILE * pFile, Amap_Lib_t * pLib, int fPrintDsd );
+extern Vec_Ptr_t *   Amap_LibSelectGates( Amap_Lib_t * p, int fVerbose );
+extern void          Amap_LibPrintSelectedGates( Amap_Lib_t * p, int fAllGates );
+extern Amap_Lib_t *  Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVerbose );
+/*=== amapMan.c ==========================================================*/
+extern Amap_Man_t *  Amap_ManStart( int nNodes );
+extern void          Amap_ManStop( Amap_Man_t * p );
+/*=== amapMatch.c ==========================================================*/
+extern void          Amap_ManMap( Amap_Man_t * p );
+/*=== amapMerge.c ==========================================================*/
+extern void          Amap_ManMerge( Amap_Man_t * p );
+/*=== amapOutput.c ==========================================================*/
+extern Vec_Ptr_t *   Amap_ManProduceMapped( Amap_Man_t * p );
+/*=== amapParse.c ==========================================================*/
+extern int           Amap_LibParseEquations( Amap_Lib_t * p, int fVerbose );
+/*=== amapPerm.c ==========================================================*/
+/*=== amapRead.c ==========================================================*/
+extern Amap_Lib_t *  Amap_LibReadFile( char * pFileName, int fVerbose );
+/*=== amapRule.c ==========================================================*/
+extern short *       Amap_LibTableFindNode( Amap_Lib_t * p, int iFan0, int iFan1, int fXor );
+extern void          Amap_LibCreateRules( Amap_Lib_t * p, int fVeryVerbose );
+/*=== amapUniq.c ==========================================================*/
+extern int           Amap_LibFindNode( Amap_Lib_t * pLib, int iFan0, int iFan1, int fXor );
+extern int           Amap_LibFindMux( Amap_Lib_t * p, int iFan0, int iFan1, int iFan2 );
+extern int           Amap_LibCreateVar( Amap_Lib_t * p );
+extern int           Amap_LibCreateNode( Amap_Lib_t * p, int iFan0, int iFan1, int fXor );
+extern int           Amap_LibCreateMux( Amap_Lib_t * p, int iFan0, int iFan1, int iFan2 );
+extern int **        Amap_LibLookupTableAlloc( Vec_Ptr_t * vVec, int fVerbose );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/map/amap/amapLib.c b/src/map/amap/amapLib.c
new file mode 100644
index 00000000..816f0703
--- /dev/null
+++ b/src/map/amap/amapLib.c
@@ -0,0 +1,361 @@
+/**CFile****************************************************************
+
+  FileName    [amapLib.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Standard-cell library.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocs a library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Lib_t * Amap_LibAlloc()
+{
+    Amap_Lib_t * p;
+    p = (Amap_Lib_t *)ALLOC( Amap_Lib_t, 1 );
+    memset( p, 0, sizeof(Amap_Lib_t) );
+    p->vGates = Vec_PtrAlloc( 100 );
+    p->pMemGates = Aig_MmFlexStart();
+    p->pMemSet = Aig_MmFlexStart();
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocs a library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibFree( Amap_Lib_t * p )
+{
+    if ( p == NULL )
+        return;
+    if ( p->vSelect )
+        Vec_PtrFree( p->vSelect );
+    if ( p->vSorted )
+        Vec_PtrFree( p->vSorted );
+    if ( p->vGates )
+        Vec_PtrFree( p->vGates );
+    if ( p->vRules )
+        Vec_VecFree( (Vec_Vec_t *)p->vRules );
+    if ( p->vRulesX )
+        Vec_VecFree( (Vec_Vec_t *)p->vRulesX );
+    if ( p->vRules3 )
+        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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the largest gate size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibNumPinsMax( Amap_Lib_t * p )
+{
+    Amap_Gat_t * pGate;
+    int i, Counter = 0;
+    Amap_LibForEachGate( p, pGate, i )
+        if ( Counter < (int)pGate->nPins )
+            Counter = pGate->nPins;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one pin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibWritePin( FILE * pFile, Amap_Pin_t * pPin )
+{
+    char * pPhaseNames[10] = { "UNKNOWN", "INV", "NONINV" };
+    fprintf( pFile, "    PIN " );
+    fprintf( pFile, "%9s ",     pPin->pName );
+    fprintf( pFile, "%10s ",    pPhaseNames[pPin->Phase] );
+    fprintf( pFile, "%6d ",     (int)pPin->dLoadInput );
+    fprintf( pFile, "%6d ",     (int)pPin->dLoadMax );
+    fprintf( pFile, "%6.2f ",   pPin->dDelayBlockRise );
+    fprintf( pFile, "%6.2f ",   pPin->dDelayFanoutRise );
+    fprintf( pFile, "%6.2f ",   pPin->dDelayBlockFall );
+    fprintf( pFile, "%6.2f",    pPin->dDelayFanoutFall );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibWriteGate( FILE * pFile, Amap_Gat_t * pGate, int fPrintDsd )
+{
+    Amap_Pin_t * pPin;
+    fprintf( pFile, "GATE " );
+    fprintf( pFile, "%12s ",      pGate->pName );
+    fprintf( pFile, "%10.2f   ",  pGate->dArea );
+    fprintf( pFile, "%s=%s;\n",   pGate->pOutName,    pGate->pForm );
+    if ( fPrintDsd )
+    {
+        if ( pGate->pFunc == NULL )
+            printf( "Truth table is not available.\n" );
+        else
+            Kit_DsdPrintFromTruth( pGate->pFunc, pGate->nPins );
+    }
+    Amap_GateForEachPin( pGate, pPin )
+        Amap_LibWritePin( pFile, pPin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibWrite( FILE * pFile, Amap_Lib_t * pLib, int fPrintDsd )
+{
+    Amap_Gat_t * pGate;
+    int i;
+    fprintf( pFile, "# The genlib library \"%s\".\n", pLib->pName );
+    Amap_LibForEachGate( pLib, pGate, i )
+        Amap_LibWriteGate( pFile, pGate, fPrintDsd );
+}
+        
+/**Function*************************************************************
+
+  Synopsis    [Compares two gates by area.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibCompareGatesByArea( Amap_Gat_t ** pp1, Amap_Gat_t ** pp2 )
+{
+    double Diff = (*pp1)->dArea - (*pp2)->dArea;
+    if ( Diff < 0.0 )
+        return -1;
+    if ( Diff > 0.0 ) 
+        return 1;
+    return 0; 
+}
+        
+/**Function*************************************************************
+
+  Synopsis    [Compares gates by area.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Amap_LibSortGatesByArea( Amap_Lib_t * pLib )
+{
+    Vec_Ptr_t * vSorted;
+    vSorted = Vec_PtrDup( pLib->vGates );
+    qsort( (void *)Vec_PtrArray(vSorted), Vec_PtrSize(vSorted), sizeof(void *), 
+            (int (*)(const void *, const void *)) Amap_LibCompareGatesByArea );
+    return vSorted;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds min-area gate with the given function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Gat_t * Amap_LibFindGate( Amap_Lib_t * p, unsigned uTruth )
+{
+    Amap_Gat_t * pGate;
+    int i;
+    Vec_PtrForEachEntry( p->vSorted, pGate, i )
+        if ( pGate->nPins <= 5 && pGate->pFunc[0] == uTruth )
+            return pGate;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects gates useful for area-only mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Amap_LibSelectGates( Amap_Lib_t * p, int fVerbose )
+{
+    Vec_Ptr_t * vSelect;
+    Amap_Gat_t * pGate, * pGate2;
+    int i, k, clk = clock();
+    p->pGate0   = Amap_LibFindGate( p, 0 );
+    p->pGate1   = Amap_LibFindGate( p, ~0 );
+    p->pGateBuf = Amap_LibFindGate( p, 0xAAAAAAAA );
+    p->pGateInv = Amap_LibFindGate( p, ~0xAAAAAAAA );
+    vSelect = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( p->vSorted, pGate, i )
+    {
+        if ( pGate->pFunc == NULL )
+            continue;
+        Vec_PtrForEachEntryStop( p->vSorted, pGate2, k, i )
+        {
+            if ( pGate2->pFunc == NULL )
+                continue;
+            if ( pGate2->nPins != pGate->nPins )
+                continue;
+            if ( !memcmp( pGate2->pFunc, pGate->pFunc, sizeof(unsigned) * Aig_TruthWordNum(pGate->nPins) ) )
+                break;
+        }
+        if ( k < i )
+            continue;
+        Vec_PtrPush( vSelect, pGate );            
+    }
+    return vSelect;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects gates useful for area-only mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibPrintSelectedGates( Amap_Lib_t * p, int fAllGates )
+{
+    Vec_Ptr_t * vArray;
+    Amap_Gat_t * pGate;
+    int i;
+    vArray = fAllGates? p->vGates : p->vSelect;
+    Vec_PtrForEachEntry( vArray, pGate, i )
+    {
+        printf( "Gate %4d : %15s   Area = %9.2f\n", pGate->Id, pGate->pName, pGate->dArea );
+        printf( "    Formula: %s=%s\n", pGate->pOutName, pGate->pForm );
+        printf( "    DSD:     " );
+        Kit_DsdPrintFromTruth( pGate->pFunc, pGate->nPins );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses equations for the gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Lib_t * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVerbose )
+{
+    Amap_Lib_t * p;
+    int clk = clock();
+    p = Amap_LibReadFile( pFileName, fVerbose );
+    if ( fVerbose )
+        printf( "Read %d gates from file \"%s\".\n", Vec_PtrSize(p->vGates), pFileName );
+    if ( p == NULL )
+        return NULL;
+    if ( !Amap_LibParseEquations( p, fVerbose ) )
+    {
+        Amap_LibFree( p );
+        return NULL;
+    }
+    p->vSorted = Amap_LibSortGatesByArea( p );
+    p->vSelect = Amap_LibSelectGates( p, fVerbose );
+    if ( fVerbose )
+    {
+        printf( "Selected %d functionally unique gates. ",
+            Vec_PtrSize(p->vSelect), Vec_PtrSize(p->vSorted) );
+        PRT( "Time", clock() - clk );
+    }
+    clk = clock();
+    Amap_LibCreateRules( p, fVeryVerbose );
+    if ( fVerbose )
+    {
+        printf( "Created %d rules and %d matches. ", 
+            p->nNodes, p->nSets );
+        PRT( "Time", clock() - clk );
+    }
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapMan.c b/src/map/amap/amapMan.c
new file mode 100644
index 00000000..521b4ffd
--- /dev/null
+++ b/src/map/amap/amapMan.c
@@ -0,0 +1,99 @@
+/**CFile****************************************************************
+
+  FileName    [amapMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Mapping manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Man_t * Amap_ManStart( int nNodes )
+{
+    Amap_Man_t * p;
+    // start the manager
+    p = ALLOC( Amap_Man_t, 1 );
+    memset( p, 0, sizeof(Amap_Man_t) );
+    p->fEpsilonInternal = (float)0.01;
+    // allocate arrays for nodes
+    p->vPis    = Vec_PtrAlloc( 100 );
+    p->vPos    = Vec_PtrAlloc( 100 );
+    p->vObjs   = Vec_PtrAlloc( 100 );
+    p->vTemp   = Vec_IntAlloc( 100 );
+    p->vCuts0  = Vec_PtrAlloc( 100 );
+    p->vCuts1  = Vec_PtrAlloc( 100 );
+    p->vCuts2  = Vec_PtrAlloc( 100 );
+    // prepare the memory manager
+    p->pMemObj = Aig_MmFixedStart( sizeof(Amap_Obj_t), nNodes );
+    p->pMemCuts = Aig_MmFlexStart();
+    p->pMemCutBest = Aig_MmFlexStart();
+    p->pMemTemp = Aig_MmFlexStart();
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManStop( Amap_Man_t * p )
+{
+    Vec_PtrFree( p->vPis );
+    Vec_PtrFree( p->vPos );
+    Vec_PtrFree( p->vObjs );
+    Vec_PtrFree( p->vCuts0 );
+    Vec_PtrFree( p->vCuts1 );
+    Vec_PtrFree( p->vCuts2 );
+    Vec_IntFree( p->vTemp );
+    Aig_MmFixedStop( p->pMemObj, 0 );
+    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 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapMatch.c b/src/map/amap/amapMatch.c
new file mode 100644
index 00000000..0b15a931
--- /dev/null
+++ b/src/map/amap/amapMatch.c
@@ -0,0 +1,538 @@
+/**CFile****************************************************************
+
+  FileName    [amapMatch.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapMatch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the cut using new memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Cut_t * Amap_ManDupCut( Amap_Man_t * p, Amap_Cut_t * pCut )
+{
+    Amap_Cut_t * pNew;
+    int nBytes = sizeof(Amap_Cut_t) + sizeof(int) * pCut->nFans;
+    pNew = (Amap_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCutBest, nBytes );
+    memcpy( pNew, pCut, nBytes );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the match with cut and set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Amap_ManMatchStart( Amap_Mat_t * p, Amap_Cut_t * pCut, Amap_Set_t * pSet )
+{
+    memset( p, 0, sizeof(Amap_Mat_t) );
+    p->pCut = pCut;
+    p->pSet = pSet;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans reference counters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManCleanRefs( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    int i;
+    Amap_ManForEachObj( p, pObj, i )
+        pObj->nFouts[0] = pObj->nFouts[1] = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes delay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Amap_ManMaxDelay( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    float Delay = 0.0;
+    int i;
+    Amap_ManForEachPo( p, pObj, i )
+        Delay = AIG_MAX( Delay, Amap_ObjFanin0(p,pObj)->Best.Delay );
+    return Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans reference counters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManCleanData( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    int i;
+//    Amap_ManForEachNode( p, pObj, i )
+//        FREE( pObj->pData );
+    Amap_ManForEachObj( p, pObj, i )
+        pObj->pData = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute nodes used in the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Amap_ManComputeMapping_rec( Amap_Man_t * p, Amap_Obj_t * pObj, int fCompl )
+{
+    Amap_Mat_t * pM = &pObj->Best;
+    Amap_Obj_t * pFanin;
+    Amap_Gat_t * pGate;
+    int i, iFanin, fComplFanin;
+    float Area;
+    if ( pObj->nFouts[fCompl]++ + pObj->nFouts[!fCompl] > 0 )
+        return 0.0;
+    if ( Amap_ObjIsPi(pObj) || Amap_ObjIsConst1(pObj) )
+        return 0.0;
+    pGate = Amap_LibGate( p->pLib, pM->pSet->iGate );
+    assert( pGate->nPins == pM->pCut->nFans );
+    Area = pGate->dArea;
+    for ( i = 0; i < (int)pGate->nPins; i++ )
+    {
+        iFanin = Amap_Lit2Var( pM->pSet->Ins[i] );
+        pFanin = Amap_ManObj( p, Amap_Lit2Var(pM->pCut->Fans[iFanin]) );
+        fComplFanin = Amap_LitIsCompl( pM->pSet->Ins[i] ) ^ Amap_LitIsCompl( pM->pCut->Fans[iFanin] );
+        Area += Amap_ManComputeMapping_rec( p, pFanin, fComplFanin );
+    }
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute nodes used in the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Amap_ManComputeMapping( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    float Area = 0.0;
+    int i;
+    Amap_ManCleanRefs( p );
+    Amap_ManForEachPo( p, pObj, i )
+        Area += Amap_ManComputeMapping_rec( p, Amap_ObjFanin0(p, pObj), Amap_ObjFaninC0(pObj) );
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of inverters to be added.]
+
+  Description [Should be called after mapping has been set.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_ManCountInverters( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    int i, Counter = 0;
+    Amap_ManForEachObj( p, pObj, i )
+        Counter += (int)(pObj->nFouts[!pObj->fPolar] > 0);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compare two matches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Amap_CutCompare( Amap_Man_t * p, Amap_Mat_t * pM0, Amap_Mat_t * pM1 )
+{
+    // compare area flows
+    if ( pM0->Area < pM1->Area - p->pPars->fEpsilon )
+        return -1;
+    if ( pM0->Area > pM1->Area + p->pPars->fEpsilon )
+        return 1;
+
+    // compare average fanouts
+    if ( pM0->AveFan > pM1->AveFan - p->pPars->fEpsilon )
+        return -1;
+    if ( pM0->AveFan < pM1->AveFan + p->pPars->fEpsilon )
+        return 1;
+
+    // compare delay
+    if ( pM0->Delay < pM1->Delay - p->pPars->fEpsilon )
+        return -1;
+    if ( pM0->Delay > pM1->Delay + p->pPars->fEpsilon )
+        return 1;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts area while dereferencing the match.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline float Amap_CutAreaDeref( Amap_Man_t * p, Amap_Mat_t * pM )
+{
+    Amap_Obj_t * pFanin;
+    int i, fCompl;
+    float Area = Amap_LibGate( p->pLib, pM->pSet->iGate )->dArea;
+    Amap_MatchForEachFaninCompl( p, pM, pFanin, fCompl, i )
+    {
+        assert( Amap_ObjRefsTotal(pFanin) > 0 );
+        if ( (int)pFanin->fPolar != fCompl && pFanin->nFouts[fCompl] == 1 )
+            Area += p->fAreaInv;
+        if ( --pFanin->nFouts[fCompl] + pFanin->nFouts[!fCompl] == 0 && Amap_ObjIsNode(pFanin) )
+            Area += Amap_CutAreaDeref( p, &pFanin->Best );
+    }
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts area while referencing the match.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline float Amap_CutAreaRef( Amap_Man_t * p, Amap_Mat_t * pM )
+{
+    Amap_Obj_t * pFanin;
+    int i, fCompl;
+    float Area = Amap_LibGate( p->pLib, pM->pSet->iGate )->dArea;
+    Amap_MatchForEachFaninCompl( p, pM, pFanin, fCompl, i )
+    {
+        assert( Amap_ObjRefsTotal(pFanin) >= 0 );
+        if ( (int)pFanin->fPolar != fCompl && pFanin->nFouts[fCompl] == 0 )
+            Area += p->fAreaInv;
+        if ( pFanin->nFouts[fCompl]++ + pFanin->nFouts[!fCompl] == 0 && Amap_ObjIsNode(pFanin) )
+            Area += Amap_CutAreaRef( p, &pFanin->Best );
+    }
+    return Area;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives area of the match for a non-referenced node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline float Amap_CutAreaDerefed( Amap_Man_t * p, Amap_Obj_t * pNode, Amap_Mat_t * pM )
+{
+    float aResult, aResult2;
+    int fComplNew;
+    aResult2 = Amap_CutAreaRef( p, pM );
+    aResult  = Amap_CutAreaDeref( p, pM );
+    assert( aResult > aResult2 - p->fEpsilonInternal );
+    assert( aResult < aResult2 + p->fEpsilonInternal );
+    // if node is needed in another polarity, add inverter
+    fComplNew = pM->pCut->fInv ^ pM->pSet->fInv;
+    if ( pNode->nFouts[fComplNew] == 0 && pNode->nFouts[!fComplNew] > 0 )
+        aResult += p->fAreaInv;
+    return aResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Amap_CutAreaTest( Amap_Man_t * p, Amap_Obj_t * pNode )
+{
+    float aResult, aResult2;
+    if ( Amap_ObjRefsTotal(pNode) == 0 )
+    {
+        aResult2 = Amap_CutAreaRef( p, &pNode->Best );
+        aResult  = Amap_CutAreaDeref( p, &pNode->Best );
+        assert( aResult > aResult2 - p->fEpsilonInternal );
+        assert( aResult < aResult2 + p->fEpsilonInternal );
+    }
+    else
+    {
+        aResult  = Amap_CutAreaDeref( p, &pNode->Best );
+        aResult2 = Amap_CutAreaRef( p, &pNode->Best );
+        assert( aResult > aResult2 - p->fEpsilonInternal );
+        assert( aResult < aResult2 + p->fEpsilonInternal );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives parameters for the match.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Amap_ManMatchGetFlows( Amap_Man_t * p, Amap_Mat_t * pM )
+{
+    Amap_Mat_t * pMFanin;
+    Amap_Obj_t * pFanin;
+    Amap_Gat_t * pGate;
+    int i;
+    pGate = Amap_LibGate( p->pLib, pM->pSet->iGate );
+    assert( pGate->nPins == pM->pCut->nFans );
+    assert( pM->Area == 0.0 );
+    pM->Area = pGate->dArea;
+    pM->AveFan = 0.0;
+    pM->Delay = 0.0;
+    Amap_MatchForEachFanin( p, pM, pFanin, i )
+    {
+        pMFanin = &pFanin->Best;
+        pM->Delay = AIG_MAX( pM->Delay, pMFanin->Delay );
+        pM->AveFan += Amap_ObjRefsTotal(pFanin);
+        if ( Amap_ObjRefsTotal(pFanin) == 0 )
+            pM->Area += pMFanin->Area;
+        else
+            pM->Area += pMFanin->Area / pFanin->EstRefs;
+    }
+    pM->AveFan /= pGate->nPins;
+    pM->Delay += 1.0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives parameters for the match.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Amap_ManMatchGetExacts( Amap_Man_t * p, Amap_Obj_t * pNode, Amap_Mat_t * pM )
+{
+    Amap_Mat_t * pMFanin;
+    Amap_Obj_t * pFanin;
+    Amap_Gat_t * pGate;
+    int i;
+    pGate = Amap_LibGate( p->pLib, pM->pSet->iGate );
+    assert( pGate->nPins == pM->pCut->nFans );
+    assert( pM->Area == 0.0 );
+    pM->AveFan = 0.0;
+    pM->Delay = 0.0;
+    Amap_MatchForEachFanin( p, pM, pFanin, i )
+    {
+        pMFanin = &pFanin->Best;
+        pM->Delay = AIG_MAX( pM->Delay, pMFanin->Delay );
+        pM->AveFan += Amap_ObjRefsTotal(pFanin);
+    }
+    pM->AveFan /= pGate->nPins;
+    pM->Delay += 1.0;
+    pM->Area = Amap_CutAreaDerefed( p, pNode, pM );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the best match at each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManMatchNode( Amap_Man_t * p, Amap_Obj_t * pNode, int fFlow, int fRefs )
+{
+    Amap_Mat_t M1, M2, * pMBest = &M1, * pMThis = &M2;
+    Amap_Cut_t * pCut;
+    Amap_Set_t * pSet;
+    Amap_Nod_t * pNod;
+    int i;
+    if ( fRefs )
+        pNode->EstRefs = (float)((2.0 * pNode->EstRefs + Amap_ObjRefsTotal(pNode)) / 3.0);
+    else
+        pNode->EstRefs = (float)pNode->nRefs;
+    if ( fRefs && Amap_ObjRefsTotal(pNode) > 0 )
+        Amap_CutAreaDeref( p, &pNode->Best );
+    pMBest->pCut = NULL;
+    Amap_NodeForEachCut( pNode, pCut, i )
+    {
+        if ( pCut->iMat == 0 )
+            continue;
+        pNod = Amap_LibNod( p->pLib, pCut->iMat );
+        Amap_LibNodeForEachSet( pNod, pSet )
+        {
+            Amap_ManMatchStart( pMThis, pCut, pSet );
+            if ( fFlow )
+                Amap_ManMatchGetFlows( p, pMThis );
+            else
+                Amap_ManMatchGetExacts( p, pNode, pMThis );
+            if ( pMBest->pCut == NULL || Amap_CutCompare(p, pMBest, pMThis) == 1 )
+                *pMBest = *pMThis;
+        }
+    }
+    pNode->fPolar = pMBest->pCut->fInv ^ pMBest->pSet->fInv;
+    pNode->Best = *pMBest;
+    pNode->Best.pCut = Amap_ManDupCut( p, pNode->Best.pCut );
+    if ( fRefs && Amap_ObjRefsTotal(pNode) > 0 )
+        Amap_CutAreaRef( p, &pNode->Best );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManMatch( Amap_Man_t * p, int fFlow, int fRefs )
+{
+    Aig_MmFlex_t * pMemOld;
+    Amap_Obj_t * pObj;
+    float Area;
+    int i, nInvs, clk = clock();
+    pMemOld = p->pMemCutBest;
+    p->pMemCutBest = Aig_MmFlexStart();
+    Amap_ManForEachNode( p, pObj, i )
+        if ( pObj->pData )
+            Amap_ManMatchNode( p, pObj, fFlow, fRefs );
+    Aig_MmFlexStop( pMemOld, 0 );
+    Area = Amap_ManComputeMapping( p );
+    nInvs = Amap_ManCountInverters( p );
+if ( p->pPars->fVerbose )
+{
+    printf( "Area =%9.2f. Gate =%9.2f. Inv =%9.2f. (%6d.) Delay =%6.2f. ", 
+        Area + nInvs * p->fAreaInv, 
+        Area, nInvs * p->fAreaInv, nInvs,
+        Amap_ManMaxDelay(p) );
+PRT( "Time ", clock() - clk );
+}
+    // test procedures
+//    Amap_ManForEachNode( p, pObj, i )
+//        Amap_CutAreaTest( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManMap( Amap_Man_t * p )
+{
+    int i;
+    Amap_ManMerge( p );
+    for ( i = 0; i < p->pPars->nIterFlow; i++ )
+        Amap_ManMatch( p, 1, i>0 );
+    for ( i = 0; i < p->pPars->nIterArea; i++ )
+        Amap_ManMatch( p, 0, p->pPars->nIterFlow>0||i>0 );
+/*
+    for ( i = 0; i < p->pPars->nIterFlow; i++ )
+        Amap_ManMatch( p, 1, 1 );
+    for ( i = 0; i < p->pPars->nIterArea; i++ )
+        Amap_ManMatch( p, 0, 1 );
+*/
+    Amap_ManCleanData( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapMerge.c b/src/map/amap/amapMerge.c
new file mode 100644
index 00000000..b024616e
--- /dev/null
+++ b/src/map/amap/amapMerge.c
@@ -0,0 +1,521 @@
+/**CFile****************************************************************
+
+  FileName    [amapMerge.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Computing cuts for the node.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates new cut and adds it to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+    Amap_ManForEachPi( p, pObj, i )
+    {
+        pCut = (Amap_Cut_t *)( pBuffer + i*nBytes );
+        pCut->iMat = 0;
+        pCut->fInv = 0;
+        pCut->nFans = 1;
+        pCut->Fans[0] = Amap_Var2Lit( pObj->Id, 0 );
+        pObj->pData = pCut;
+        pObj->nCuts = 1;
+        pObj->EstRefs = (float)1.0;
+    }
+    return (Amap_Cut_t *)pBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates new cut and adds it to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Cut_t * Amap_ManCutStore( Amap_Man_t * p, Amap_Cut_t * pCut, int fCompl )
+{
+    Amap_Cut_t * pNew;
+    int iFan, nBytes = sizeof(Amap_Cut_t) + sizeof(int) * pCut->nFans + sizeof(Amap_Cut_t *);
+    pNew = (Amap_Cut_t *)Aig_MmFlexEntryFetch( p->pMemTemp, nBytes );
+    pNew->iMat  = pCut->iMat;
+    pNew->fInv  = pCut->fInv ^ fCompl;
+    pNew->nFans = pCut->nFans;
+    memcpy( pNew->Fans, pCut->Fans, sizeof(int) * pCut->nFans );
+    // add it to storage
+    iFan = Amap_Var2Lit( pNew->iMat, pNew->fInv );
+    if ( p->ppCutsTemp[ iFan ] == NULL )
+        Vec_IntPushOrder( p->vTemp, iFan );
+    *Amap_ManCutNextP( pNew ) = p->ppCutsTemp[ iFan ];
+    p->ppCutsTemp[ iFan ] = pNew;
+    return pNew;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Creates new cut and adds it to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Cut_t * Amap_ManCutCreate( Amap_Man_t * p, 
+    Amap_Cut_t * pCut0, Amap_Cut_t * pCut1, int iMat )
+{
+    Amap_Cut_t * pCut;
+    int i, nSize  = pCut0->nFans + pCut1->nFans;
+    int nBytes = sizeof(Amap_Cut_t) + sizeof(int) * nSize + sizeof(Amap_Cut_t *);
+    assert( pCut0->iMat >= pCut1->iMat );
+    pCut = (Amap_Cut_t *)Aig_MmFlexEntryFetch( p->pMemTemp, nBytes );
+    pCut->iMat  = iMat;
+    pCut->fInv  = 0;
+    pCut->nFans = nSize;
+    for ( i = 0; i < (int)pCut0->nFans; i++ )
+        pCut->Fans[i] = pCut0->Fans[i];
+    for ( i = 0; i < (int)pCut1->nFans; i++ )
+        pCut->Fans[pCut0->nFans+i] = pCut1->Fans[i];
+    // add it to storage
+    if ( p->ppCutsTemp[ pCut->iMat ] == NULL )
+        Vec_IntPushOrder( p->vTemp, pCut->iMat );
+    *Amap_ManCutNextP( pCut ) = p->ppCutsTemp[ pCut->iMat ];
+    p->ppCutsTemp[ pCut->iMat ] = pCut;
+    return pCut;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Creates new cut and adds it to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Cut_t * Amap_ManCutCreate3( Amap_Man_t * p, 
+    Amap_Cut_t * pCut0, Amap_Cut_t * pCut1, Amap_Cut_t * pCut2, int iMat )
+{
+    Amap_Cut_t * pCut;
+    int i, nSize  = pCut0->nFans + pCut1->nFans + pCut2->nFans;
+    int nBytes = sizeof(Amap_Cut_t) + sizeof(int) * nSize + sizeof(Amap_Cut_t *);
+    pCut = (Amap_Cut_t *)Aig_MmFlexEntryFetch( p->pMemTemp, nBytes );
+    pCut->iMat  = iMat;
+    pCut->fInv  = 0;
+    pCut->nFans = nSize;
+    for ( i = 0; i < (int)pCut0->nFans; i++ )
+        pCut->Fans[i] = pCut0->Fans[i];
+    for ( i = 0; i < (int)pCut1->nFans; i++ )
+        pCut->Fans[pCut0->nFans+i] = pCut1->Fans[i];
+    for ( i = 0; i < (int)pCut2->nFans; i++ )
+        pCut->Fans[pCut0->nFans+pCut1->nFans+i] = pCut2->Fans[i];
+    // add it to storage
+    if ( p->ppCutsTemp[ pCut->iMat ] == NULL )
+        Vec_IntPushOrder( p->vTemp, pCut->iMat );
+    *Amap_ManCutNextP( pCut ) = p->ppCutsTemp[ pCut->iMat ];
+    p->ppCutsTemp[ pCut->iMat ] = pCut;
+    return pCut;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Removes cuts from the temporary storage.]
+
+  Description [] 
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
+{
+    int * pBuffer;
+    Amap_Cut_t * pNext, * pCut;
+    int i, nWords, Entry, nCuts;
+    assert( pNode->pData == NULL );
+    // count memory needed
+    nCuts = 1;
+    nWords = 2;
+    Vec_IntForEachEntry( p->vTemp, Entry, i )
+    {
+        for ( pCut = p->ppCutsTemp[Entry]; pCut; pCut = *Amap_ManCutNextP(pCut) )
+        {
+            nCuts++;
+            nWords += pCut->nFans + 1;
+        }
+    }
+    p->nBytesUsed += 4*nWords;
+    // allocate memory
+    pBuffer = (int *)Aig_MmFlexEntryFetch( p->pMemCuts, 4*nWords );
+    pNext = (Amap_Cut_t *)pBuffer;
+    // add the first cut
+    pNext->iMat  = 0; 
+    pNext->fInv  = 0;
+    pNext->nFans = 1;
+    pNext->Fans[0] = Amap_Var2Lit(pNode->Id, 0);
+    pNext = (Amap_Cut_t *)(pBuffer + 2);
+    // add other cuts
+    Vec_IntForEachEntry( p->vTemp, Entry, i )
+    {
+        for ( pCut = p->ppCutsTemp[Entry]; pCut; pCut = *Amap_ManCutNextP(pCut) )
+        {
+            memcpy( pNext, pCut, sizeof(int) * (pCut->nFans + 1) );
+            pNext = (Amap_Cut_t *)((int *)pNext + pCut->nFans + 1);
+        }
+        p->ppCutsTemp[Entry] = NULL;
+    }
+    assert( (int *)pNext - pBuffer == nWords );
+    // restore the storage
+    Vec_IntClear( p->vTemp );
+    Aig_MmFlexRestart( p->pMemTemp );
+    for ( i = 0; i < 2*p->pLib->nNodes; i++ )
+        if ( p->ppCutsTemp[i] != NULL )
+            printf( "Amap_ManCutSaveStored(): Error!\n" );
+    pNode->pData = (Amap_Cut_t *)pBuffer;
+    pNode->nCuts = nCuts;
+//    printf("%d ", nCuts );
+    // verify cuts
+    pCut = NULL;
+    Amap_NodeForEachCut( pNode, pNext, i )
+//        for ( i = 0, pNext = (Amap_Cut_t *)pNode->pData; i < (int)pNode->nCuts; 
+//        i++, pNext = Amap_ManCutNext(pNext) )
+    {
+        assert( pCut == NULL || pCut->iMat <= pNext->iMat );
+        pCut = pNext;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of possible new cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_ManMergeCountCuts( Amap_Man_t * p, Amap_Obj_t * pNode )
+{
+    Amap_Obj_t * pFanin0 = Amap_ObjFanin0( p, pNode );
+    Amap_Obj_t * pFanin1 = Amap_ObjFanin1( p, pNode );
+    Amap_Cut_t * pCut0, * pCut1;
+    int Entry, c0, c1, iCompl0, iCompl1, iFan0, iFan1;
+    int Counter = 1;
+    Amap_NodeForEachCut( pFanin0, pCut0, c0 )
+    Amap_NodeForEachCut( pFanin1, pCut1, c1 )
+    {
+        iCompl0 = pCut0->fInv ^ Amap_ObjFaninC0(pNode);
+        iCompl1 = pCut1->fInv ^ Amap_ObjFaninC1(pNode);
+        iFan0   = !pCut0->iMat? 0: Amap_Var2Lit( pCut0->iMat, iCompl0 );
+        iFan1   = !pCut1->iMat? 0: Amap_Var2Lit( pCut1->iMat, iCompl1 );
+        Entry = Amap_LibFindNode( p->pLib, iFan0, iFan1, pNode->Type == AMAP_OBJ_XOR );
+        Counter += ( Entry >=0 );
+//        if ( Entry >=0 )
+//            printf( "Full: %d + %d = %d\n", iFan0, iFan1, Entry );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManPrintCuts( Amap_Obj_t * pNode )
+{
+    Amap_Cut_t * pCut;
+    int c, i;
+    printf( "NODE %5d : Type = ", pNode->Id );
+    if ( pNode->Type == AMAP_OBJ_AND )
+        printf( "AND" );
+    else if ( pNode->Type == AMAP_OBJ_XOR )
+        printf( "XOR" );
+    else if ( pNode->Type == AMAP_OBJ_MUX )
+        printf( "MUX" );
+    printf( "  Cuts = %d\n", pNode->nCuts );
+    Amap_NodeForEachCut( pNode, pCut, c )
+    {
+        printf( "%3d :  Mat= %3d  Inv=%d  ", c, pCut->iMat, pCut->fInv );
+        for ( i = 0; i < (int)pCut->nFans; i++ )
+            printf( "%d%c ", Amap_Lit2Var(pCut->Fans[i]), Amap_LitIsCompl(pCut->Fans[i])?'-':'+' );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives cuts for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManMergeNodeChoice( Amap_Man_t * p, Amap_Obj_t * pNode )
+{
+    Amap_Obj_t * pTemp;
+    Amap_Cut_t * pCut;
+    int c;
+    // go through the nodes of the choice node
+    for ( pTemp = pNode; pTemp; pTemp = Amap_ObjChoice(p, pTemp) )
+    {
+        Amap_NodeForEachCut( pTemp, pCut, c )
+            if ( pCut->iMat )
+                Amap_ManCutStore( p, pCut, pNode->fPhase ^ pTemp->fPhase );
+        pTemp->pData = NULL;
+    }
+    Amap_ManCutSaveStored( p, pNode );
+
+//    Amap_ManPrintCuts( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives cuts for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_ManFindCut( Amap_Obj_t * pNode, Amap_Obj_t * pFanin, int fComplFanin, int Val, Vec_Ptr_t * vCuts )
+{
+    Amap_Cut_t * pCut;
+    int c, iCompl, iFan;
+    Vec_PtrClear( vCuts );
+    Amap_NodeForEachCut( pFanin, pCut, c )
+    {
+        iCompl = pCut->fInv ^ fComplFanin;
+        iFan   = !pCut->iMat? 0: Amap_Var2Lit( pCut->iMat, iCompl );
+        if ( iFan == Val )
+            Vec_PtrPush( vCuts, pCut );
+    }
+    return Vec_PtrSize(vCuts) == 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives cuts for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManMergeNodeCutsMux( Amap_Man_t * p, Amap_Obj_t * pNode )
+{
+    Vec_Int_t * vRules = p->pLib->vRules3;
+    Amap_Obj_t * pFanin0 = Amap_ObjFanin0( p, pNode );
+    Amap_Obj_t * pFanin1 = Amap_ObjFanin1( p, pNode );
+    Amap_Obj_t * pFanin2 = Amap_ObjFanin2( p, pNode );
+    int fComplFanin0 = Amap_ObjFaninC0( pNode );
+    int fComplFanin1 = Amap_ObjFaninC1( pNode );
+    int fComplFanin2 = Amap_ObjFaninC2( pNode );
+    Amap_Cut_t * pCut0, * pCut1, * pCut2;
+    int x, c0, c1, c2;
+    assert( pNode->pData == NULL );
+    assert( pNode->Type == AMAP_OBJ_MUX );
+    assert( pNode->fRepr == 0 );
+    // go through the rules
+    for ( x = 0; x < Vec_IntSize(vRules); x += 4 )
+    {
+        if ( Amap_ManFindCut( pNode, pFanin0, fComplFanin0, Vec_IntEntry(vRules, x), p->vCuts0 ) )
+            continue;
+        if ( Amap_ManFindCut( pNode, pFanin1, fComplFanin1, Vec_IntEntry(vRules, x+1), p->vCuts1 ) )
+            continue;
+        if ( Amap_ManFindCut( pNode, pFanin2, fComplFanin2, Vec_IntEntry(vRules, x+2), p->vCuts2 ) )
+            continue;
+        Vec_PtrForEachEntry( p->vCuts0, pCut0, c0 )
+        Vec_PtrForEachEntry( p->vCuts1, pCut1, c1 )
+        Vec_PtrForEachEntry( p->vCuts2, pCut2, c2 )
+        {
+            Amap_Nod_t * pNod = Amap_LibNod( p->pLib, Vec_IntEntry(vRules, x+3) );
+            if ( pNod->pSets == NULL )
+                continue;
+            // complement literals
+            if ( pCut0->nFans == 1 && (pCut0->fInv ^ fComplFanin0) )
+                pCut0->Fans[0] = Amap_LitNot(pCut0->Fans[0]);
+            if ( pCut1->nFans == 1 && (pCut1->fInv ^ fComplFanin1) )
+                pCut1->Fans[0] = Amap_LitNot(pCut1->Fans[0]);
+            if ( pCut2->nFans == 1 && (pCut2->fInv ^ fComplFanin2) )
+                pCut2->Fans[0] = Amap_LitNot(pCut2->Fans[0]);
+            // create new cut
+            Amap_ManCutCreate3( p, pCut0, pCut1, pCut2, Vec_IntEntry(vRules, x+3) );
+            // uncomplement literals
+            if ( pCut0->nFans == 1 && (pCut0->fInv ^ fComplFanin0) )
+                pCut0->Fans[0] = Amap_LitNot(pCut0->Fans[0]);
+            if ( pCut1->nFans == 1 && (pCut1->fInv ^ fComplFanin1) )
+                pCut1->Fans[0] = Amap_LitNot(pCut1->Fans[0]);
+            if ( pCut2->nFans == 1 && (pCut2->fInv ^ fComplFanin2) )
+                pCut2->Fans[0] = Amap_LitNot(pCut2->Fans[0]);
+        }
+    }
+    Amap_ManCutSaveStored( p, pNode );
+    p->nCutsUsed += pNode->nCuts;
+    p->nCutsTried3 += pFanin0->nCuts * pFanin1->nCuts * pFanin2->nCuts;
+
+//    Amap_ManPrintCuts( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives cuts for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManMergeNodeCuts( Amap_Man_t * p, Amap_Obj_t * pNode )
+{
+    Amap_Obj_t * pFanin0 = Amap_ObjFanin0( p, pNode );
+    Amap_Obj_t * pFanin1 = Amap_ObjFanin1( p, pNode );
+    Amap_Cut_t * pCut0, * pCut1;
+    int ** pRules, Entry, i, k, c, iCompl0, iCompl1, iFan0, iFan1;
+    assert( pNode->pData == NULL );
+    if ( pNode->Type == AMAP_OBJ_MUX )
+    {
+        Amap_ManMergeNodeCutsMux( p, pNode );
+        return;
+    }
+    assert( pNode->Type != AMAP_OBJ_MUX );
+    pRules = (pNode->Type == AMAP_OBJ_AND)? p->pLib->pRules: p->pLib->pRulesX;
+    Amap_NodeForEachCut( pFanin0, pCut0, c )
+    {
+        iCompl0 = pCut0->fInv ^ Amap_ObjFaninC0(pNode);
+        iFan0   = !pCut0->iMat? 0: Amap_Var2Lit( pCut0->iMat, iCompl0 );
+        // complement literals
+        if ( pCut0->nFans == 1 && iCompl0 )
+            pCut0->Fans[0] = Amap_LitNot(pCut0->Fans[0]);
+        // label resulting sets
+        for ( i = 0; (Entry = pRules[iFan0][i]); i++ )
+            p->pMatsTemp[Entry & 0xffff] = (Entry >> 16);
+        // iterate through the cuts
+        Amap_NodeForEachCut( pFanin1, pCut1, k )
+        {
+            iCompl1 = pCut1->fInv ^ Amap_ObjFaninC1(pNode);
+            iFan1   = !pCut1->iMat? 0: Amap_Var2Lit( pCut1->iMat, iCompl1 );
+            if ( p->pMatsTemp[iFan1] == 0 )
+                continue;
+            // complement literals
+            if ( pCut1->nFans == 1 && iCompl1 )
+                pCut1->Fans[0] = Amap_LitNot(pCut1->Fans[0]);
+            // create new cut
+            if ( iFan0 >= iFan1 )
+                Amap_ManCutCreate( p, pCut0, pCut1, p->pMatsTemp[iFan1] );
+            else
+                Amap_ManCutCreate( p, pCut1, pCut0, p->pMatsTemp[iFan1] );
+            // uncomplement literals
+            if ( pCut1->nFans == 1 && iCompl1 )
+                pCut1->Fans[0] = Amap_LitNot(pCut1->Fans[0]);
+        }
+        // uncomplement literals
+        if ( pCut0->nFans == 1 && iCompl0 )
+            pCut0->Fans[0] = Amap_LitNot(pCut0->Fans[0]);
+        // label resulting sets
+        for ( i = 0; (Entry = pRules[iFan0][i]); i++ )
+            p->pMatsTemp[Entry & 0xffff] = 0;
+    }
+    Amap_ManCutSaveStored( p, pNode );
+    p->nCutsUsed += pNode->nCuts;
+    p->nCutsTried += pFanin0->nCuts * pFanin1->nCuts;
+//    assert( (int)pNode->nCuts == Amap_ManMergeCountCuts(p, pNode) );
+    if ( pNode->fRepr )
+        Amap_ManMergeNodeChoice( p, pNode );
+
+//    Amap_ManPrintCuts( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives cuts for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_ManMerge( Amap_Man_t * p )
+{
+    Amap_Obj_t * pObj;
+    int i, clk = clock();
+    p->pCutsPi = Amap_ManSetupPis( p );
+    Amap_ManForEachNode( p, pObj, i )
+        Amap_ManMergeNodeCuts( p, pObj );
+    if ( p->pPars->fVerbose )
+    {
+        printf( "AIG object is %d bytes.  ", sizeof(Amap_Obj_t) );
+        printf( "Internal AIG = %5.2f Mb.  Cuts = %5.2f Mb.\n", 
+            1.0*Amap_ManObjNum(p)*sizeof(Amap_Obj_t)/(1<<20), 1.0*p->nBytesUsed/(1<<20) );
+        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 );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapOutput.c b/src/map/amap/amapOutput.c
new file mode 100644
index 00000000..1decc52e
--- /dev/null
+++ b/src/map/amap/amapOutput.c
@@ -0,0 +1,181 @@
+/**CFile****************************************************************
+
+  FileName    [amapOutput.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Core mapping procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapOutput.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline char * Amap_OuputStrsav( Aig_MmFlex_t * p, char * pStr ) 
+{ return pStr ? strcpy(Aig_MmFlexEntryFetch(p, strlen(pStr)+1), pStr) : NULL; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates structure for storing one gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Out_t * Amap_OutputStructAlloc( Aig_MmFlex_t * pMem, Amap_Gat_t * pGate )
+{
+    Amap_Out_t * pRes;
+    int nFans = pGate? pGate->nPins : 1;
+    pRes = (Amap_Out_t *)Aig_MmFlexEntryFetch( pMem, sizeof(Amap_Out_t)+sizeof(int)*nFans );
+    memset( pRes, 0, sizeof(Amap_Out_t) );
+    memset( pRes->pFans, 0xff, sizeof(int)*nFans );
+    pRes->pName = pGate? Amap_OuputStrsav( pMem, pGate->pName ) : NULL;
+    pRes->nFans = nFans;
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns mapped network as an array of structures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Amap_ManProduceMapped( Amap_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_MmFlex_t * pMem;
+    Amap_Obj_t * pObj, * pFanin;
+    Amap_Gat_t * pGate;
+    Amap_Out_t * pRes;
+    int i, k, iFanin, fCompl;
+    float TotalArea = 0.0;
+    pMem = Aig_MmFlexStart();
+    // create mapping object for each node used in the mapping
+    vNodes = Vec_PtrAlloc( 10 );
+    Amap_ManForEachObj( p, pObj, i )
+    {
+        if ( Amap_ObjIsPi(pObj) )
+        {
+            assert( pObj->fPolar == 0 );
+            pRes = Amap_OutputStructAlloc( pMem, NULL );
+            pRes->Type  = -1;
+            pRes->nFans = 0;
+            // save this structure
+            pObj->iData = Vec_PtrSize( vNodes );
+            Vec_PtrPush( vNodes, pRes );
+            // create invertor if needed
+            if ( pObj->nFouts[1] ) // this PI is used in the neg polarity
+            {
+                pRes = Amap_OutputStructAlloc( pMem, p->pLib->pGateInv );
+                pRes->pFans[0] = pObj->iData;
+                // save this structure
+                Vec_PtrPush( vNodes, pRes );
+                TotalArea += p->pLib->pGateInv->dArea;
+            }
+            continue;
+        }
+        if ( Amap_ObjIsNode(pObj) )
+        {
+            // skip the node that is not used in the mapping
+            if ( Amap_ObjRefsTotal(pObj) == 0 )
+                continue;
+            // get the gate
+            pGate = Amap_LibGate( p->pLib, pObj->Best.pSet->iGate );
+            assert( pGate->nPins == pObj->Best.pCut->nFans );
+            // allocate structure
+            pRes = Amap_OutputStructAlloc( pMem, pGate );
+            Amap_MatchForEachFaninCompl( p, &pObj->Best, pFanin, fCompl, k )
+            {
+                assert( Amap_ObjRefsTotal(pFanin) );
+                if ( (int)pFanin->fPolar == fCompl )
+                    pRes->pFans[k] = pFanin->iData;
+                else
+                    pRes->pFans[k] = pFanin->iData + 1;
+            }
+            // save this structure
+            pObj->iData = Vec_PtrSize( vNodes );
+            Vec_PtrPush( vNodes, pRes );
+            TotalArea += pGate->dArea;
+            // create invertor if needed
+            if ( pObj->nFouts[!pObj->fPolar] ) // needed in the opposite polarity
+            {
+                pRes = Amap_OutputStructAlloc( pMem, p->pLib->pGateInv );
+                pRes->pFans[0] = pObj->iData;
+                // save this structure
+                Vec_PtrPush( vNodes, pRes );
+                TotalArea += p->pLib->pGateInv->dArea;
+            }
+            continue;
+        }
+        if ( Amap_ObjIsPo(pObj) )
+        {
+            assert( pObj->fPolar == 0 );
+            pFanin = Amap_ObjFanin0(p, pObj);
+            assert( Amap_ObjRefsTotal(pFanin) );
+            if ( Amap_ObjIsConst1(pFanin)  )
+            { // create constant node
+                if ( Amap_ObjFaninC0(pObj) )
+                {
+                    pRes = Amap_OutputStructAlloc( pMem, p->pLib->pGate0 );
+                    TotalArea += p->pLib->pGate0->dArea;
+                }
+                else
+                {
+                    pRes = Amap_OutputStructAlloc( pMem, p->pLib->pGate1 );
+                    TotalArea += p->pLib->pGate1->dArea;
+                }
+                // save this structure
+                iFanin = Vec_PtrSize( vNodes );
+                Vec_PtrPush( vNodes, pRes );
+            }
+            else 
+            {
+                if ( (int)pFanin->fPolar == Amap_ObjFaninC0(pObj) )
+                    iFanin = pFanin->iData;
+                else
+                    iFanin = pFanin->iData + 1;
+            }
+            // create PO node
+            pRes = Amap_OutputStructAlloc( pMem, NULL );
+            pRes->Type     = 1;
+            pRes->pFans[0] = iFanin;
+            // save this structure
+            Vec_PtrPush( vNodes, pRes );
+        }
+    }
+    // return memory manager in the last entry of the array
+    Vec_PtrPush( vNodes, pMem );
+    return vNodes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapParse.c b/src/map/amap/amapParse.c
new file mode 100644
index 00000000..262fbd5a
--- /dev/null
+++ b/src/map/amap/amapParse.c
@@ -0,0 +1,457 @@
+/**CFile****************************************************************
+
+  FileName    [amapParse.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Parses representations of gates.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapParse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+#include "hop.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the list of operation symbols to be used in expressions
+#define AMAP_EQN_SYM_OPEN    '('   // opening paranthesis
+#define AMAP_EQN_SYM_CLOSE   ')'   // closing paranthesis
+#define AMAP_EQN_SYM_CONST0  '0'   // constant 0
+#define AMAP_EQN_SYM_CONST1  '1'   // constant 1
+#define AMAP_EQN_SYM_NEG     '!'   // negation before the variable
+#define AMAP_EQN_SYM_NEGAFT  '\''  // negation after the variable
+#define AMAP_EQN_SYM_AND     '*'   // logic AND
+#define AMAP_EQN_SYM_XOR     '^'   // logic XOR
+#define AMAP_EQN_SYM_OR      '+'   // logic OR
+
+// the list of opcodes (also specifying operation precedence)
+#define AMAP_EQN_OPER_NEG    10    // negation
+#define AMAP_EQN_OPER_AND     9    // logic AND
+#define AMAP_EQN_OPER_XOR     8    // logic XOR
+#define AMAP_EQN_OPER_OR      7    // logic OR
+#define AMAP_EQN_OPER_MARK    1    // OpStack token standing for an opening paranthesis
+
+// these are values of the internal Flag
+#define AMAP_EQN_FLAG_START   1    // after the opening parenthesis 
+#define AMAP_EQN_FLAG_VAR     2    // after operation is received
+#define AMAP_EQN_FLAG_OPER    3    // after operation symbol is received
+#define AMAP_EQN_FLAG_ERROR   4    // when error is detected
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs the operation on the top entries in the stack.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Amap_ParseFormulaOper( Hop_Man_t * pMan, Vec_Ptr_t * pStackFn, int Oper )
+{
+    Hop_Obj_t * gArg1, * gArg2, * gFunc;
+    // perform the given operation
+    gArg2 = Vec_PtrPop( pStackFn );
+    gArg1 = Vec_PtrPop( pStackFn );
+    if ( Oper == AMAP_EQN_OPER_AND )
+        gFunc = Hop_And( pMan, gArg1, gArg2 );
+    else if ( Oper == AMAP_EQN_OPER_OR )
+        gFunc = Hop_Or( pMan, gArg1, gArg2 );
+    else if ( Oper == AMAP_EQN_OPER_XOR )
+        gFunc = Hop_Exor( pMan, gArg1, gArg2 );
+    else
+        return NULL;
+//    Cudd_Ref( gFunc );
+//    Cudd_RecursiveDeref( dd, gArg1 );
+//    Cudd_RecursiveDeref( dd, gArg2 );
+    Vec_PtrPush( pStackFn,  gFunc );
+    return gFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the AIG corresponding to the equation.]
+
+  Description [Takes the stream to output messages, the formula, the vector
+  of variable names and the AIG manager.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVarNames, Hop_Man_t * pMan )
+{
+    char * pFormula;
+    Vec_Ptr_t * pStackFn;
+    Vec_Int_t * pStackOp;
+    Hop_Obj_t * gFunc;
+    char * pTemp, * pName;
+    int nParans, fFound, Flag;
+    int Oper, Oper1, Oper2;
+    int i, v;
+
+    // make sure that the number of opening and closing parantheses is the same
+    nParans = 0;
+    for ( pTemp = pFormInit; *pTemp; pTemp++ )
+        if ( *pTemp == '(' )
+            nParans++;
+        else if ( *pTemp == ')' )
+            nParans--;
+    if ( nParans != 0 )
+    {
+        fprintf( pOutput, "Amap_ParseFormula(): Different number of opening and closing parantheses ().\n" );
+        return NULL;
+    }
+
+    // copy the formula
+    pFormula = ALLOC( char, strlen(pFormInit) + 3 );
+    sprintf( pFormula, "(%s)", pFormInit );
+
+    // start the stacks
+    pStackFn = Vec_PtrAlloc( 100 );
+    pStackOp = Vec_IntAlloc( 100 );
+
+    Flag = AMAP_EQN_FLAG_START;
+    for ( pTemp = pFormula; *pTemp; pTemp++ )
+    {
+        switch ( *pTemp )
+        {
+        // skip all spaces, tabs, and end-of-lines
+        case ' ':
+        case '\t':
+        case '\r':
+        case '\n':
+            continue;
+        case AMAP_EQN_SYM_CONST0:
+            Vec_PtrPush( pStackFn, Hop_ManConst0(pMan) );  // Cudd_Ref( b0 );
+            if ( Flag == AMAP_EQN_FLAG_VAR )
+            {
+                fprintf( pOutput, "Amap_ParseFormula(): No operation symbol before constant 0.\n" );
+                Flag = AMAP_EQN_FLAG_ERROR; 
+                break;
+            }
+            Flag = AMAP_EQN_FLAG_VAR; 
+            break;
+        case AMAP_EQN_SYM_CONST1:
+            Vec_PtrPush( pStackFn, Hop_ManConst1(pMan) );  //  Cudd_Ref( b1 );
+            if ( Flag == AMAP_EQN_FLAG_VAR )
+            {
+                fprintf( pOutput, "Amap_ParseFormula(): No operation symbol before constant 1.\n" );
+                Flag = AMAP_EQN_FLAG_ERROR; 
+                break;
+            }
+            Flag = AMAP_EQN_FLAG_VAR; 
+            break;
+        case AMAP_EQN_SYM_NEG:
+            if ( Flag == AMAP_EQN_FLAG_VAR )
+            {// if NEGBEF follows a variable, AND is assumed
+                Vec_IntPush( pStackOp, AMAP_EQN_OPER_AND );
+                Flag = AMAP_EQN_FLAG_OPER;
+            }
+            Vec_IntPush( pStackOp, AMAP_EQN_OPER_NEG );
+            break;
+        case AMAP_EQN_SYM_NEGAFT:
+            if ( Flag != AMAP_EQN_FLAG_VAR )
+            {// if there is no variable before NEGAFT, it is an error
+                fprintf( pOutput, "Amap_ParseFormula(): No variable is specified before the negation suffix.\n" );
+                Flag = AMAP_EQN_FLAG_ERROR; 
+                break;
+            }
+            else // if ( Flag == PARSE_FLAG_VAR )
+                Vec_PtrPush( pStackFn, Hop_Not( Vec_PtrPop(pStackFn) ) );
+            break;
+        case AMAP_EQN_SYM_AND:
+        case AMAP_EQN_SYM_OR:
+        case AMAP_EQN_SYM_XOR:
+            if ( Flag != AMAP_EQN_FLAG_VAR )
+            {
+                fprintf( pOutput, "Amap_ParseFormula(): There is no variable before AND, EXOR, or OR.\n" );
+                Flag = AMAP_EQN_FLAG_ERROR; 
+                break;
+            }
+            if ( *pTemp == AMAP_EQN_SYM_AND )
+                Vec_IntPush( pStackOp, AMAP_EQN_OPER_AND );
+            else if ( *pTemp == AMAP_EQN_SYM_OR )
+                Vec_IntPush( pStackOp, AMAP_EQN_OPER_OR );
+            else //if ( *pTemp == AMAP_EQN_SYM_XOR )
+                Vec_IntPush( pStackOp, AMAP_EQN_OPER_XOR );
+            Flag = AMAP_EQN_FLAG_OPER; 
+            break;
+        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_MARK );
+            // after an opening bracket, it feels like starting over again
+            Flag = AMAP_EQN_FLAG_START; 
+            break;
+        case AMAP_EQN_SYM_CLOSE:
+            if ( Vec_IntSize( pStackOp ) != 0 )
+            {
+                while ( 1 )
+                {
+                    if ( Vec_IntSize( pStackOp ) == 0 )
+                    {
+                        fprintf( pOutput, "Amap_ParseFormula(): There is no opening paranthesis\n" );
+                        Flag = AMAP_EQN_FLAG_ERROR; 
+                        break;
+                    }
+                    Oper = Vec_IntPop( pStackOp );
+                    if ( Oper == AMAP_EQN_OPER_MARK )
+                        break;
+
+                    // perform the given operation
+                    if ( Amap_ParseFormulaOper( pMan, pStackFn, Oper ) == NULL )
+                    {
+                        fprintf( pOutput, "Amap_ParseFormula(): Unknown operation\n" );
+                        free( pFormula );
+                        return NULL;
+                    }
+                }
+            }
+            else
+            {
+                fprintf( pOutput, "Amap_ParseFormula(): There is no opening paranthesis\n" );
+                Flag = AMAP_EQN_FLAG_ERROR; 
+                break;
+            }
+            if ( Flag != AMAP_EQN_FLAG_ERROR )
+                Flag = AMAP_EQN_FLAG_VAR; 
+            break;
+
+
+        default:
+            // scan the next name
+            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++ )
+              {
+                    if ( pTemp[i] == AMAP_EQN_SYM_NEG || pTemp[i] == AMAP_EQN_SYM_OPEN )
+                    {
+                        fprintf( pOutput, "Amap_ParseFormula(): The negation sign or an opening paranthesis inside the variable name.\n" );
+                        Flag = AMAP_EQN_FLAG_ERROR; 
+                        break;
+                    }
+              }
+            // variable name is found
+            fFound = 0;
+            Vec_PtrForEachEntry( vVarNames, pName, v )
+                if ( strncmp(pTemp, pName, i) == 0 && strlen(pName) == (unsigned)i )
+                {
+                    pTemp += i-1;
+                    fFound = 1;
+                    break;
+                }
+            if ( !fFound )
+            { 
+                fprintf( pOutput, "Amap_ParseFormula(): The parser cannot find var \"%s\" in the input var list.\n", pTemp ); 
+                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; 
+            }
+            Vec_PtrPush( pStackFn, Hop_IthVar( pMan, v ) ); // Cudd_Ref( pbVars[v] );
+            Flag = AMAP_EQN_FLAG_VAR; 
+            break;
+        }
+
+        if ( Flag == AMAP_EQN_FLAG_ERROR )
+            break;      // error exit
+        else if ( Flag == AMAP_EQN_FLAG_START )
+            continue;  //  go on parsing
+        else if ( Flag == AMAP_EQN_FLAG_VAR )
+            while ( 1 )
+            {  // check if there are negations in the OpStack     
+                if ( Vec_IntSize( pStackOp ) == 0 )
+                    break;
+                Oper = Vec_IntPop( pStackOp );
+                if ( Oper != AMAP_EQN_OPER_NEG )
+                {
+                    Vec_IntPush( pStackOp, Oper );
+                    break;
+                }
+                else
+                {
+                      Vec_PtrPush( pStackFn, Hop_Not(Vec_PtrPop(pStackFn)) );
+                }
+            }
+        else // if ( Flag == AMAP_EQN_FLAG_OPER )
+            while ( 1 )
+            {  // execute all the operations in the OpStack
+               // with precedence higher or equal than the last one
+                Oper1 = Vec_IntPop( pStackOp ); // the last operation
+                if ( Vec_IntSize( pStackOp ) == 0 ) 
+                {  // if it is the only operation, push it back
+                    Vec_IntPush( pStackOp, Oper1 );
+                    break;
+                }
+                Oper2 = Vec_IntPop( pStackOp ); // the operation before the last one
+                if ( Oper2 >= Oper1 )  
+                {  // if Oper2 precedence is higher or equal, execute it
+                    if ( Amap_ParseFormulaOper( pMan, pStackFn, Oper2 ) == NULL )
+                    {
+                        fprintf( pOutput, "Amap_ParseFormula(): Unknown operation\n" );
+                        free( pFormula );
+                        return NULL;
+                    }
+                    Vec_IntPush( pStackOp,  Oper1 );     // push the last operation back
+                }
+                else
+                {  // if Oper2 precedence is lower, push them back and done
+                    Vec_IntPush( pStackOp, Oper2 );
+                    Vec_IntPush( pStackOp, Oper1 );
+                    break;
+                }
+            }
+    }
+
+    if ( Flag != AMAP_EQN_FLAG_ERROR )
+    {
+        if ( Vec_PtrSize(pStackFn) != 0 )
+        {    
+            gFunc = Vec_PtrPop(pStackFn);
+            if ( Vec_PtrSize(pStackFn) == 0 )
+                if ( Vec_IntSize( pStackOp ) == 0 )
+                {
+                    Vec_PtrFree(pStackFn);
+                    Vec_IntFree(pStackOp);
+//                    Cudd_Deref( gFunc );
+                    free( pFormula );
+                    return gFunc;
+                }
+                else
+                    fprintf( pOutput, "Amap_ParseFormula(): Something is left in the operation stack\n" );
+            else
+                fprintf( pOutput, "Amap_ParseFormula(): Something is left in the function stack\n" );
+        }
+        else
+            fprintf( pOutput, "Amap_ParseFormula(): The input string is empty\n" );
+    }
+    free( pFormula );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses equations for the gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibParseEquations( Amap_Lib_t * p, int fVerbose )
+{
+    extern int Kit_TruthSupportSize( unsigned * pTruth, int nVars );
+    Hop_Man_t * pMan;
+    Hop_Obj_t * pObj;
+    Vec_Ptr_t * vNames;
+    Vec_Int_t * vTruth;
+    Amap_Gat_t * pGate;
+    Amap_Pin_t * pPin;
+    unsigned * pTruth;
+    int i, nPinMax;
+    nPinMax = Amap_LibNumPinsMax(p);
+    if ( nPinMax > AMAP_MAXINS )
+        printf( "Gates with more than %d inputs will be ignored.\n", AMAP_MAXINS );
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    vNames = Vec_PtrAlloc( 100 );
+    pMan = Hop_ManStart();
+    Hop_IthVar( pMan, nPinMax - 1 );
+    Vec_PtrForEachEntry( p->vGates, pGate, i )
+    {
+        if ( pGate->nPins == 0 )
+        {
+            pGate->pFunc = (unsigned *)Aig_MmFlexEntryFetch( p->pMemGates, 4 );
+            if ( strcmp( pGate->pForm, AMAP_STRING_CONST0 ) == 0 )
+                pGate->pFunc[0] = 0;
+            else if ( strcmp( pGate->pForm, AMAP_STRING_CONST1 ) == 0 )
+                pGate->pFunc[0] = ~0;
+            else
+            {
+                printf( "Cannot parse formula \"%s\" of gate \"%s\" with no pins.\n", pGate->pForm, pGate->pName );
+                break;
+            }
+            continue;
+        }
+        if ( pGate->nPins > AMAP_MAXINS )
+            continue;
+        Vec_PtrClear( vNames );
+        Amap_GateForEachPin( pGate, pPin )
+            Vec_PtrPush( vNames, pPin->pName );
+        pObj = Amap_ParseFormula( stdout, pGate->pForm, vNames, pMan );
+        if ( pObj == NULL )
+            break;
+        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 );
+            continue;
+        }
+        pGate->pFunc = (unsigned *)Aig_MmFlexEntryFetch( p->pMemGates, sizeof(unsigned)*Aig_TruthWordNum(pGate->nPins) );
+        memcpy( pGate->pFunc, pTruth, sizeof(unsigned)*Aig_TruthWordNum(pGate->nPins) );
+    }
+    Vec_PtrFree( vNames );
+    Vec_IntFree( vTruth );
+    Hop_ManStop( pMan );
+    return i == Vec_PtrSize(p->vGates);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses equations for the gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibParseTest( char * pFileName )
+{
+    int fVerbose = 1;
+    Amap_Lib_t * p;
+    int clk = clock();
+    p = Amap_LibReadFile( pFileName, fVerbose );
+    if ( p == NULL )
+        return;
+    Amap_LibParseEquations( p, fVerbose );
+    Amap_LibFree( p );
+    PRT( "Total time", clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapPerm.c b/src/map/amap/amapPerm.c
new file mode 100644
index 00000000..17fb57e2
--- /dev/null
+++ b/src/map/amap/amapPerm.c
@@ -0,0 +1,344 @@
+/**CFile****************************************************************
+
+  FileName    [amapPerm.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Deriving permutation for the gate.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapPerm.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects fanins of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibCollectFanins_rec( Amap_Lib_t * pLib, Amap_Nod_t * pNod, Vec_Int_t * vFanins )
+{
+    Amap_Nod_t * pFan0, * pFan1;
+    if ( pNod->Id == 0 )
+    {
+        Vec_IntPush( vFanins, 0 );
+        return;
+    }
+    pFan0 = Amap_LibNod( pLib, Amap_Lit2Var(pNod->iFan0) );
+    if ( Amap_LitIsCompl(pNod->iFan0) || pFan0->Type != pNod->Type )
+        Vec_IntPush( vFanins, pNod->iFan0 );
+    else
+        Amap_LibCollectFanins_rec( pLib, pFan0, vFanins );
+    pFan1 = Amap_LibNod( pLib, Amap_Lit2Var(pNod->iFan1) );
+    if ( Amap_LitIsCompl(pNod->iFan1) || pFan1->Type != pNod->Type )
+        Vec_IntPush( vFanins, pNod->iFan1 );
+    else
+        Amap_LibCollectFanins_rec( pLib, pFan1, vFanins );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects fanins of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Amap_LibCollectFanins( Amap_Lib_t * pLib, Amap_Nod_t * pNod )
+{
+    Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
+    Amap_LibCollectFanins_rec( pLib, pNod, vFanins );
+    return vFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Matches the node with the DSD node.]
+
+  Description [Returns perm if the node can be matched.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Amap_LibDeriveGatePerm_rec( Amap_Lib_t * pLib, Kit_DsdNtk_t * pNtk, int iLit, Amap_Nod_t * pNod )
+{
+    Vec_Int_t * vPerm, * vPermFanin, * vNodFanin, * vDsdLits;
+    Kit_DsdObj_t * pDsdObj, * pDsdFanin;
+    Amap_Nod_t * pNodFanin;
+    int iDsdFanin, iNodFanin, Value, iDsdLit, i, k, j;
+    assert( !Kit_DsdLitIsCompl(iLit) );
+    pDsdObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
+    if ( pDsdObj == NULL )
+    {
+        vPerm = Vec_IntAlloc( 1 );
+        Vec_IntPush( vPerm, iLit );
+        return vPerm;
+    }
+    if ( pDsdObj->Type == KIT_DSD_PRIME && pNod->Type == AMAP_OBJ_MUX )
+    {
+        vPerm = Vec_IntAlloc( 10 );
+
+        iDsdFanin  = Kit_DsdLitRegular(pDsdObj->pFans[0]);
+        pNodFanin  = Amap_LibNod( pLib, Amap_Lit2Var(pNod->iFan0) );
+        vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
+        Vec_IntForEachEntry( vPermFanin, Value, k )
+            Vec_IntPush( vPerm, Value );
+        Vec_IntFree( vPermFanin );
+
+        iDsdFanin  = Kit_DsdLitRegular(pDsdObj->pFans[1]);
+        pNodFanin  = Amap_LibNod( pLib, Amap_Lit2Var(pNod->iFan1) );
+        vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
+        Vec_IntForEachEntry( vPermFanin, Value, k )
+            Vec_IntPush( vPerm, Value );
+        Vec_IntFree( vPermFanin );
+
+        iDsdFanin  = Kit_DsdLitRegular(pDsdObj->pFans[2]);
+        pNodFanin  = Amap_LibNod( pLib, Amap_Lit2Var(pNod->iFan2) );
+        vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
+        Vec_IntForEachEntry( vPermFanin, Value, k )
+            Vec_IntPush( vPerm, Value );
+        Vec_IntFree( vPermFanin );
+
+        return vPerm;
+    }
+    // return if wrong types
+    if ( pDsdObj->Type == KIT_DSD_PRIME || pNod->Type == AMAP_OBJ_MUX )
+        return NULL;
+    // return if sizes do not agree
+    vNodFanin = Amap_LibCollectFanins( pLib, pNod );
+    if ( Vec_IntSize(vNodFanin) != (int)pDsdObj->nFans )
+    {
+        Vec_IntFree( vNodFanin );
+        return NULL;
+    }
+    // match fanins of DSD with fanins of nodes
+    // clean the mark and save variable literals
+    vPerm = Vec_IntAlloc( 10 );
+    vDsdLits = Vec_IntAlloc( 10 );
+    Kit_DsdObjForEachFaninReverse( pNtk, pDsdObj, iDsdFanin, i )
+    {
+        pDsdFanin = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iDsdFanin) );
+        if ( pDsdFanin )
+            pDsdFanin->fMark = 0;
+        else
+            Vec_IntPush( vDsdLits, iDsdFanin );
+    }
+    // match each fanins of the node
+    iDsdLit = 0;
+    Vec_IntForEachEntry( vNodFanin, iNodFanin, k )
+    {
+        if ( iNodFanin == 0 )
+        {
+            iDsdFanin = Vec_IntEntry( vDsdLits, iDsdLit++ );
+            Vec_IntPush( vPerm, iDsdFanin );
+            continue;
+        }
+        // find a matching component
+        pNodFanin = Amap_LibNod( pLib, Amap_Lit2Var(iNodFanin) );
+        Kit_DsdObjForEachFaninReverse( pNtk, pDsdObj, iDsdFanin, i )
+        {
+            pDsdFanin = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iDsdFanin) );
+            if ( pDsdFanin == NULL )
+                continue;
+            if ( pDsdFanin->fMark == 1 )
+                continue;
+            if ( !((pDsdFanin->Type == KIT_DSD_AND && pNodFanin->Type == AMAP_OBJ_AND) ||
+                   (pDsdFanin->Type == KIT_DSD_XOR && pNodFanin->Type == AMAP_OBJ_XOR) ||
+                   (pDsdFanin->Type == KIT_DSD_PRIME && pNodFanin->Type == AMAP_OBJ_MUX)) )
+                   continue;
+            vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, Kit_DsdLitRegular(iDsdFanin), pNodFanin );
+            if ( vPermFanin == NULL )
+                continue;
+            pDsdFanin->fMark = 1;
+            Vec_IntForEachEntry( vPermFanin, Value, j )
+                Vec_IntPush( vPerm, Value );
+            Vec_IntFree( vPermFanin );
+            break;
+        }
+    }
+    assert( iDsdLit == Vec_IntSize(vDsdLits) );
+    Vec_IntFree( vNodFanin );
+    Vec_IntFree( vDsdLits );
+    return vPerm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs verification of one gate and one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Amap_LibVerifyPerm_rec( Amap_Lib_t * pLib, Amap_Nod_t * pNod, 
+    Vec_Ptr_t * vTtElems, Vec_Int_t * vTruth, int nWords, int * piInput )
+{
+    Amap_Nod_t * pFan0, * pFan1;
+    unsigned * pTruth0, * pTruth1, * pTruth;
+    int i;
+    assert( pNod->Type != AMAP_OBJ_MUX );
+    if ( pNod->Id == 0 )
+        return Vec_PtrEntry( vTtElems, (*piInput)++ );
+    pFan0 = Amap_LibNod( pLib, Amap_Lit2Var(pNod->iFan0) );
+    pTruth0 = Amap_LibVerifyPerm_rec( pLib, pFan0, vTtElems, vTruth, nWords, piInput );
+    pFan1 = Amap_LibNod( pLib, Amap_Lit2Var(pNod->iFan1) );
+    pTruth1 = Amap_LibVerifyPerm_rec( pLib, pFan1, vTtElems, vTruth, nWords, piInput );
+    pTruth  = Vec_IntFetch( vTruth, nWords );
+    if ( pNod->Type == AMAP_OBJ_XOR )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] ^ pTruth1[i];
+    else if ( !Amap_LitIsCompl(pNod->iFan0) && !Amap_LitIsCompl(pNod->iFan1) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & pTruth1[i];
+    else if ( !Amap_LitIsCompl(pNod->iFan0) && Amap_LitIsCompl(pNod->iFan1) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & ~pTruth1[i];
+    else if ( Amap_LitIsCompl(pNod->iFan0) && !Amap_LitIsCompl(pNod->iFan1) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & pTruth1[i];
+    else // if ( Amap_LitIsCompl(pNod->iFan0) && Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs verification of one gate and one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibVerifyPerm( Amap_Lib_t * pLib, Amap_Gat_t * pGate, Kit_DsdNtk_t * pNtk, Amap_Nod_t * pNod, int * pArray )
+{
+    Vec_Ptr_t * vTtElems;
+    Vec_Ptr_t * vTtElemsPol;
+    Vec_Int_t * vTruth;
+    unsigned * pTruth;
+    int i, nWords;
+    int iInput = 0;
+
+    // allocate storage for truth tables
+    assert( pGate->nPins > 1 );
+    nWords = Kit_TruthWordNum( pGate->nPins );
+    vTruth = Vec_IntAlloc( nWords * AMAP_MAXINS );
+    vTtElems = Vec_PtrAllocTruthTables( pGate->nPins );
+    vTtElemsPol = Vec_PtrAlloc( pGate->nPins );
+    for ( i = 0; i < (int)pGate->nPins; i++ )
+    {
+        pTruth = Vec_PtrEntry( vTtElems, Amap_Lit2Var(pArray[i]) );
+        if ( Amap_LitIsCompl( pArray[i] ) )
+            Kit_TruthNot( pTruth, pTruth, pGate->nPins );
+        Vec_PtrPush( vTtElemsPol, pTruth );
+    }
+//Extra_PrintBinary( stdout, Vec_PtrEntry(vTtElemsPol, 0), 4 ); printf("\n" );
+//Extra_PrintBinary( stdout, Vec_PtrEntry(vTtElemsPol, 1), 4 ); printf("\n" );
+    // compute the truth table recursively
+    pTruth = Amap_LibVerifyPerm_rec( pLib, pNod, vTtElemsPol, vTruth, nWords, &iInput );
+    assert( iInput == (int)pGate->nPins );
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
+        Kit_TruthNot( pTruth, pTruth, pGate->nPins );
+//Extra_PrintBinary( stdout, pTruth, 4 ); printf("\n" );
+//Extra_PrintBinary( stdout, pGate->pFunc, 4 ); printf("\n" );
+    // compare
+    if ( !Kit_TruthIsEqual(pGate->pFunc, pTruth, pGate->nPins) )
+        printf( "Verification failed for gate %d (%s) and node %d.\n",
+            pGate->Id, pGate->pForm, pNod->Id );
+    Vec_IntFree( vTruth );
+    Vec_PtrFree( vTtElems );
+    Vec_PtrFree( vTtElemsPol );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Matches the node with the DSD of a gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibDeriveGatePerm( Amap_Lib_t * pLib, Amap_Gat_t * pGate, Kit_DsdNtk_t * pNtk, Amap_Nod_t * pNod, char * pArray )
+{
+    int fVerbose = 0;
+    Vec_Int_t * vPerm;
+    int Entry, Entry2, i, k;
+    vPerm = Amap_LibDeriveGatePerm_rec( pLib, pNtk, Kit_DsdLitRegular(pNtk->Root), pNod );
+    if ( vPerm == NULL )
+        return 0;
+    // check that the permutation is valid
+    assert( Vec_IntSize(vPerm) == (int)pNod->nSuppSize );
+    Vec_IntForEachEntry( vPerm, Entry, i )
+        Vec_IntForEachEntryStart( vPerm, Entry2, k, i+1 )
+            if ( Amap_Lit2Var(Entry) == Amap_Lit2Var(Entry2) )
+            {
+                Vec_IntFree( vPerm );
+                return 0;
+            }
+
+    // reverse the permutation
+    Vec_IntForEachEntry( vPerm, Entry, i )
+    {
+        assert( Entry < 2 * (int)pNod->nSuppSize );
+        pArray[Kit_DsdLit2Var(Entry)] = Amap_Var2Lit( i, Kit_DsdLitIsCompl(Entry) );
+//        pArray[i] = Entry;
+//printf( "%d=%d%c ", Kit_DsdLit2Var(Entry), i, Kit_DsdLitIsCompl(Entry)?'-':'+' );
+    }
+//printf( "\n" );
+//    if ( Kit_DsdNonDsdSizeMax(pNtk) < 3 )
+//        Amap_LibVerifyPerm( pLib, pGate, pNtk, pNod, Vec_IntArray(vPerm) );
+    Vec_IntFree( vPerm );
+    // print the result
+    if ( fVerbose )
+    {
+    printf( "node %4d : ", pNod->Id );
+    for ( i = 0; i < (int)pNod->nSuppSize; i++ )
+        printf( "%d=%d%c ", i, Amap_Lit2Var(pArray[i]), Amap_LitIsCompl(pArray[i])?'-':'+' );
+    printf( "\n" );
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapRead.c b/src/map/amap/amapRead.c
new file mode 100644
index 00000000..182de5d1
--- /dev/null
+++ b/src/map/amap/amapRead.c
@@ -0,0 +1,412 @@
+/**CFile****************************************************************
+
+  FileName    [amapRead.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapRead.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define AMAP_STRING_GATE       "GATE"
+#define AMAP_STRING_PIN        "PIN"
+#define AMAP_STRING_NONINV     "NONINV"
+#define AMAP_STRING_INV        "INV"
+#define AMAP_STRING_UNKNOWN    "UNKNOWN"
+
+// these symbols (and no other) can appear in the formulas
+#define AMAP_SYMB_AND    '*'
+#define AMAP_SYMB_OR1    '+'
+#define AMAP_SYMB_OR2    '|'
+#define AMAP_SYMB_XOR    '^'
+#define AMAP_SYMB_NOT    '!'
+#define AMAP_SYMB_AFTNOT '\''
+#define AMAP_SYMB_OPEN   '('
+#define AMAP_SYMB_CLOSE  ')'
+
+typedef enum { 
+    AMAP_PHASE_UNKNOWN, 
+    AMAP_PHASE_INV, 
+    AMAP_PHASE_NONINV 
+} Amap_PinPhase_t;
+
+static inline Amap_Gat_t * Amap_ParseGateAlloc( Aig_MmFlex_t * p, int nPins ) 
+{ return (Amap_Gat_t *)Aig_MmFlexEntryFetch( p, sizeof(Amap_Gat_t)+sizeof(Amap_Pin_t)*nPins ); }
+static inline char * Amap_ParseStrsav( Aig_MmFlex_t * p, char * pStr ) 
+{ return pStr ? strcpy(Aig_MmFlexEntryFetch(p, strlen(pStr)+1), pStr) : NULL; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Loads the file into temporary buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Amap_LoadFile( char * pFileName )
+{
+    extern FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose );
+    FILE * pFile;
+    char * pBuffer;
+    int nFileSize;
+    // open the BLIF file for binary reading
+    pFile = Io_FileOpen( pFileName, "open_path", "rb", 1 );
+//    pFile = fopen( FileName, "rb" );
+    // if we got this far, file should be okay otherwise would
+    // have been detected by caller
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\".\n", pFileName );
+        return NULL;
+    }
+    assert ( pFile != NULL );
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile );  
+    // move the file current reading position to the beginning
+    rewind( pFile ); 
+    // load the contents of the file into memory
+    pBuffer = ALLOC( char, nFileSize + 10 );
+    fread( pBuffer, nFileSize, 1, pFile );
+    // terminate the string with '\0'
+    pBuffer[ nFileSize ] = '\0';
+    strcat( pBuffer, "\n.end\n" );
+    // close file
+    fclose( pFile );
+    return pBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Eliminates comments from the input file.]
+
+  Description [As a byproduct, this procedure also counts the number
+  lines and dot-statements in the input file. This also joins non-comment 
+  lines that are joined with a backspace '\']
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_RemoveComments( char * pBuffer, int * pnDots, int * pnLines )
+{
+    char * pCur;
+    int nDots, nLines;
+    // scan through the buffer and eliminate comments
+    // (in the BLIF file, comments are lines starting with "#")
+    nDots = nLines = 0;
+    for ( pCur = pBuffer; *pCur; pCur++ )
+    {
+        // if this is the beginning of comment
+        // clean it with spaces until the new line statement
+        if ( *pCur == '#' )
+            while ( *pCur != '\n' )
+                *pCur++ = ' ';
+    
+        // count the number of new lines and dots
+        if ( *pCur == '\n' ) {
+        if (*(pCur-1)=='\r') {
+        // DOS(R) file support
+        if (*(pCur-2)!='\\') nLines++;
+        else {
+            // rewind to backslash and overwrite with a space
+            *(pCur-2) = ' ';
+            *(pCur-1) = ' ';
+            *pCur = ' ';
+        }
+        } else {
+        // UNIX(TM) file support
+        if (*(pCur-1)!='\\') nLines++;
+        else {
+            // rewind to backslash and overwrite with a space
+            *(pCur-1) = ' ';
+            *pCur = ' ';
+        }
+        }
+    }
+        else if ( *pCur == '.' )
+            nDots++;
+    }
+    if ( pnDots )
+        *pnDots = nDots; 
+    if ( pnLines )
+        *pnLines = nLines; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Splits the stream into tokens.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Amap_DeriveTokens( char * pBuffer )
+{
+    Vec_Ptr_t * vTokens;
+    char * pToken;
+    vTokens = Vec_PtrAlloc( 1000 );
+    pToken = strtok( pBuffer, " ;=\t\r\n" );
+    while ( pToken )
+    {
+        Vec_PtrPush( vTokens, pToken );
+        pToken = strtok( NULL, " ;=\t\r\n" );
+    }
+    return vTokens;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the number of pins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_ParseCountPins( Vec_Ptr_t * vTokens, int iPos )
+{
+    char * pToken;
+    int i, Counter = 0;
+    Vec_PtrForEachEntryStart( vTokens, pToken, i, iPos )
+        if ( !strcmp( pToken, AMAP_STRING_PIN ) )
+            Counter++;
+        else if ( !strcmp( pToken, AMAP_STRING_GATE ) )
+            return Counter;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect the pin names used in the formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_GateCollectNames( Aig_MmFlex_t * pMem, char * pForm, char * pPinNames[] )
+{
+    char Buffer[1000];
+    char * pTemp;
+    int nPins, i;
+    // save the formula as it was
+    strcpy( Buffer, pForm );
+    // remove the non-name symbols
+    for ( pTemp = Buffer; *pTemp; pTemp++ )
+        if ( *pTemp == AMAP_SYMB_AND || *pTemp == AMAP_SYMB_OR1 || *pTemp == AMAP_SYMB_OR2 
+          || *pTemp == AMAP_SYMB_XOR || *pTemp == AMAP_SYMB_NOT || *pTemp == AMAP_SYMB_OPEN 
+          || *pTemp == AMAP_SYMB_CLOSE || *pTemp == AMAP_SYMB_AFTNOT )
+            *pTemp = ' ';
+    // save the names
+    nPins = 0;
+    pTemp = strtok( Buffer, " " );
+    while ( pTemp )
+    {
+        for ( i = 0; i < nPins; i++ )
+            if ( strcmp( pTemp, pPinNames[i] ) == 0 )
+                break;
+        if ( i == nPins )
+        { // cannot find this name; save it
+            pPinNames[nPins++] = Amap_ParseStrsav( pMem, pTemp );
+        }
+        // get the next name
+        pTemp = strtok( NULL, " " );
+    }
+    return nPins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a duplicate gate with pins specified.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Gat_t * Amap_ParseGateWithSamePins( Amap_Gat_t * p )
+{
+    Amap_Gat_t * pGate;
+    Amap_Pin_t * pPin;
+    char * pPinNames[128];
+    int nPinNames;
+    assert( p->nPins == 1 && !strcmp( p->Pins->pName, "*" ) );
+    nPinNames = Amap_GateCollectNames( p->pLib->pMemGates, p->pForm, pPinNames );
+    pGate = Amap_ParseGateAlloc( p->pLib->pMemGates, nPinNames );
+    *pGate = *p;
+    pGate->nPins = nPinNames;
+    Amap_GateForEachPin( pGate, pPin )
+    {
+        *pPin = *p->Pins;
+        pPin->pName = pPinNames[pPin - pGate->Pins];
+    }
+    return pGate;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Lib_t * Amap_ParseTokens( Vec_Ptr_t * vTokens, int fVerbose )
+{
+    Amap_Lib_t * p;
+    Amap_Gat_t * pGate;
+    Amap_Pin_t * pPin;
+    char * pToken;
+    int nPins, iPos = 0;
+    p = Amap_LibAlloc();
+    pToken = Vec_PtrEntry(vTokens, iPos++);
+    do 
+    {
+        if ( strcmp( pToken, AMAP_STRING_GATE ) )
+        {
+            printf( "The first line should begin with %s.\n", AMAP_STRING_GATE );
+            return NULL;
+        }
+        // start gate
+        nPins = Amap_ParseCountPins( vTokens, iPos );
+        pGate = Amap_ParseGateAlloc( p->pMemGates, nPins );
+        memset( pGate, 0, sizeof(Amap_Gat_t) );
+        pGate->Id = Vec_PtrSize( p->vGates );
+        Vec_PtrPush( p->vGates, pGate );
+        pGate->pLib = p;
+        pGate->nPins = nPins;
+        // read gate
+        pToken = Vec_PtrEntry(vTokens, iPos++);
+        pGate->pName = Amap_ParseStrsav( p->pMemGates, pToken );    
+        pToken = Vec_PtrEntry(vTokens, iPos++);
+        pGate->dArea = atof( pToken );
+        pToken = Vec_PtrEntry(vTokens, iPos++);
+        pGate->pOutName = Amap_ParseStrsav( p->pMemGates, pToken ); 
+        pToken = Vec_PtrEntry(vTokens, iPos++);
+        pGate->pForm = Amap_ParseStrsav( p->pMemGates, pToken ); 
+        // read pins
+        Amap_GateForEachPin( pGate, pPin )
+        {
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            if ( strcmp( pToken, AMAP_STRING_PIN ) )
+            {
+                printf( "Cannot parse gate %s.\n", pGate->pName );
+                return NULL;
+            }
+            // read pin
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            pPin->pName = Amap_ParseStrsav( p->pMemGates, pToken );   
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            if ( strcmp( pToken, AMAP_STRING_UNKNOWN ) == 0 )
+                pPin->Phase = AMAP_PHASE_UNKNOWN;
+            else if ( strcmp( pToken, AMAP_STRING_INV ) == 0 )
+                pPin->Phase = AMAP_PHASE_INV;
+            else if ( strcmp( pToken, AMAP_STRING_NONINV ) == 0 )
+                pPin->Phase = AMAP_PHASE_NONINV;
+            else 
+            {
+                printf( "Cannot read phase of pin %s of gate %s\n", pPin->pName, pGate->pName );
+                return NULL;
+            }
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            pPin->dLoadInput = atof( pToken );
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            pPin->dLoadMax = atof( pToken );
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            pPin->dDelayBlockRise = atof( pToken );
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            pPin->dDelayFanoutRise = atof( pToken );
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            pPin->dDelayBlockFall = atof( pToken );
+            pToken = Vec_PtrEntry(vTokens, iPos++);
+            pPin->dDelayFanoutFall = atof( pToken );
+            if ( pPin->dDelayBlockRise > pPin->dDelayBlockFall )
+                pPin->dDelayBlockMax = pPin->dDelayBlockRise;
+            else
+                pPin->dDelayBlockMax = pPin->dDelayBlockFall;
+        }
+        // fix the situation when all pins are represented as one
+        if ( pGate->nPins == 1 && !strcmp( pGate->Pins->pName, "*" ) )
+        {
+            pGate = Amap_ParseGateWithSamePins( pGate );
+            Vec_PtrPop( p->vGates );
+            Vec_PtrPush( p->vGates, pGate );
+        }
+        pToken = Vec_PtrEntry(vTokens, iPos++);
+    }
+    while ( strcmp( pToken, ".end" ) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the library from the input file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Amap_Lib_t * Amap_LibReadFile( char * pFileName, int fVerbose )
+{
+    Amap_Lib_t * pLib;
+    Vec_Ptr_t * vTokens;
+    char * pBuffer;
+    pBuffer = Amap_LoadFile( pFileName );
+    if ( pBuffer == NULL )
+        return NULL;
+    Amap_RemoveComments( pBuffer, NULL, NULL );
+    vTokens = Amap_DeriveTokens( pBuffer );
+    pLib = Amap_ParseTokens( vTokens, fVerbose );
+    if ( pLib == NULL )
+        return NULL;
+    pLib->pName = Amap_ParseStrsav( pLib->pMemGates, pFileName );
+    Vec_PtrFree( vTokens );
+    free( pBuffer );
+    return pLib;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapRule.c b/src/map/amap/amapRule.c
new file mode 100644
index 00000000..212f7631
--- /dev/null
+++ b/src/map/amap/amapRule.c
@@ -0,0 +1,368 @@
+/**CFile****************************************************************
+
+  FileName    [amapRule.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Matching rules.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapRule.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Amap_LibDeriveGatePerm( Amap_Lib_t * pLib, Amap_Gat_t * pGate, Kit_DsdNtk_t * pNtk, Amap_Nod_t * pNod, char * pArray );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the three-argument rule exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Amap_CreateRulesPrime( Amap_Lib_t * p, Vec_Int_t * vNods0, Vec_Int_t * vNods1, Vec_Int_t * vNods2 )
+{
+    Vec_Int_t * vRes;
+    int i, k, j, iNod, iNod0, iNod1, iNod2;
+    if ( p->vRules3 == NULL )
+        p->vRules3 = Vec_IntAlloc( 100 );
+    vRes = Vec_IntAlloc( 10 );
+    Vec_IntForEachEntry( vNods0, iNod0, i )
+    Vec_IntForEachEntry( vNods1, iNod1, k )
+    Vec_IntForEachEntry( vNods2, iNod2, j )
+    {
+        iNod = Amap_LibFindMux( p, iNod0, iNod1, iNod2 );
+        if ( iNod == -1 )
+            iNod = Amap_LibCreateMux( p, iNod0, iNod1, iNod2 );
+        Vec_IntPush( vRes, Amap_Var2Lit(iNod, 0) );
+    }
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_CreateRulesTwo( Amap_Lib_t * p, Vec_Int_t * vNods, Vec_Int_t * vNods0, Vec_Int_t * vNods1, int fXor )
+{
+    int i, k, iNod, iNod0, iNod1;
+    Vec_IntForEachEntry( vNods0, iNod0, i )
+    Vec_IntForEachEntry( vNods1, iNod1, k )
+    {
+        iNod = Amap_LibFindNode( p, iNod0, iNod1, fXor );
+        if ( iNod == -1 )
+            iNod = Amap_LibCreateNode( p, iNod0, iNod1, fXor );
+        Vec_IntPushUnique( vNods, Amap_Var2Lit(iNod, 0) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_CreateCheckAllZero( Vec_Ptr_t * vVecNods )
+{
+    Vec_Int_t * vNods;
+    int i;
+    Vec_PtrForEachEntryReverse( vVecNods, vNods, i )
+        if ( Vec_IntSize(vNods) != 1 || Vec_IntEntry(vNods,0) != 0 )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Amap_CreateRulesVector_rec( Amap_Lib_t * p, Vec_Ptr_t * vVecNods, int fXor )
+{
+    Vec_Ptr_t * vVecNods0, * vVecNods1;
+    Vec_Int_t * vRes, * vNods, * vNods0, * vNods1;
+    int i, k;
+    if ( Vec_PtrSize(vVecNods) == 1 )
+        return Vec_IntDup( Vec_PtrEntry(vVecNods, 0) );
+    vRes = Vec_IntAlloc( 10 );
+    vVecNods0 = Vec_PtrAlloc( Vec_PtrSize(vVecNods) );
+    vVecNods1 = Vec_PtrAlloc( Vec_PtrSize(vVecNods) );
+    if ( Amap_CreateCheckAllZero(vVecNods) )
+    {
+        for ( i = Vec_PtrSize(vVecNods)-1; i > 0; i-- )
+        {
+            Vec_PtrClear( vVecNods0 );
+            Vec_PtrClear( vVecNods1 );
+            Vec_PtrForEachEntryStop( vVecNods, vNods, k, i )
+                Vec_PtrPush( vVecNods0, vNods );
+            Vec_PtrForEachEntryStart( vVecNods, vNods, k, i )
+                Vec_PtrPush( vVecNods1, vNods );
+            vNods0 = Amap_CreateRulesVector_rec( p, vVecNods0, fXor );
+            vNods1 = Amap_CreateRulesVector_rec( p, vVecNods1, fXor );
+            Amap_CreateRulesTwo( p, vRes, vNods0, vNods1, fXor );
+            Vec_IntFree( vNods0 );
+            Vec_IntFree( vNods1 );
+        }
+    }
+    else
+    {
+        int Limit = (1 << Vec_PtrSize(vVecNods))-2;
+        for ( i = 1; i < Limit; i++ )
+        {
+            Vec_PtrClear( vVecNods0 );
+            Vec_PtrClear( vVecNods1 );
+            Vec_PtrForEachEntryReverse( vVecNods, vNods, k )
+            {
+                if ( i & (1 << k) )
+                    Vec_PtrPush( vVecNods1, vNods );
+                else
+                    Vec_PtrPush( vVecNods0, vNods );
+            }
+            assert( Vec_PtrSize(vVecNods0) > 0 );
+            assert( Vec_PtrSize(vVecNods1) > 0 );
+            assert( Vec_PtrSize(vVecNods0) < Vec_PtrSize(vVecNods) );
+            assert( Vec_PtrSize(vVecNods1) < Vec_PtrSize(vVecNods) );
+            vNods0 = Amap_CreateRulesVector_rec( p, vVecNods0, fXor );
+            vNods1 = Amap_CreateRulesVector_rec( p, vVecNods1, fXor );
+            Amap_CreateRulesTwo( p, vRes, vNods0, vNods1, fXor );
+            Vec_IntFree( vNods0 );
+            Vec_IntFree( vNods1 );
+        }
+    }
+    Vec_PtrFree( vVecNods0 );
+    Vec_PtrFree( vVecNods1 );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Amap_CreateRulesFromDsd_rec( Amap_Lib_t * pLib, Kit_DsdNtk_t * p, int iLit )
+{
+    Vec_Int_t * vRes;
+    Vec_Ptr_t * vVecNods;
+    Vec_Int_t * vNodsFanin;
+    Kit_DsdObj_t * pObj;
+    unsigned i;
+    int iFanin, iNod, k;
+    assert( !Kit_DsdLitIsCompl(iLit) );
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+        return Vec_IntStartNatural( 1 );
+    // solve for the inputs
+    vVecNods = Vec_PtrAlloc( pObj->nFans );
+    Kit_DsdObjForEachFanin( p, pObj, iFanin, i )
+    {
+        vNodsFanin = Amap_CreateRulesFromDsd_rec( pLib, p, Kit_DsdLitRegular(iFanin) );
+        if ( Kit_DsdLitIsCompl(iFanin) )
+        {
+            Vec_IntForEachEntry( vNodsFanin, iNod, k )
+                if ( iNod > 0 )
+                    Vec_IntWriteEntry( vNodsFanin, k, Amap_LitNot(iNod) );
+        }
+        Vec_PtrPush( vVecNods, vNodsFanin );
+    }
+    if ( pObj->Type == KIT_DSD_AND )
+        vRes = Amap_CreateRulesVector_rec( pLib, vVecNods, 0 );
+    else if ( pObj->Type == KIT_DSD_XOR )
+        vRes = Amap_CreateRulesVector_rec( pLib, vVecNods, 1 );
+    else if ( pObj->Type == KIT_DSD_PRIME )
+    {
+        assert( pObj->nFans == 3 );
+        assert( Kit_DsdObjTruth(pObj)[0] == 0xCACACACA );
+        vRes = Amap_CreateRulesPrime( pLib, Vec_PtrEntry(vVecNods, 0),
+            Vec_PtrEntry(vVecNods, 1), Vec_PtrEntry(vVecNods, 2) );
+    }
+    else assert( 0 );
+    Vec_PtrForEachEntry( vVecNods, vNodsFanin, k )
+        Vec_IntFree( vNodsFanin );
+    Vec_PtrFree( vVecNods );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Amap_CreateRulesFromDsd( Amap_Lib_t * pLib, Kit_DsdNtk_t * p )
+{
+    Vec_Int_t * vNods;
+    int iNod, i;
+    assert( p->nVars >= 2 );
+    vNods = Amap_CreateRulesFromDsd_rec( pLib, p, Kit_DsdLitRegular(p->Root) );
+    if ( vNods == NULL )
+        return NULL;
+    if ( Kit_DsdLitIsCompl(p->Root) )
+    {
+        Vec_IntForEachEntry( vNods, iNod, i )
+            Vec_IntWriteEntry( vNods, i, Amap_LitNot(iNod) );
+    }
+    return vNods;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates rules for the given gate]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_CreateRulesForGate( Amap_Lib_t * pLib, Amap_Gat_t * pGate )
+{ 
+    Kit_DsdNtk_t * pNtk, * pTemp;
+    Vec_Int_t * vNods;
+    Amap_Nod_t * pNod;
+    Amap_Set_t * pSet;
+    int iNod, i;
+//    if ( pGate->nPins > 4 )
+//        return;
+    pNtk = Kit_DsdDecomposeMux( pGate->pFunc, pGate->nPins, 2 );
+    if ( pGate->nPins == 2 && (pGate->pFunc[0] == 0x66666666 || pGate->pFunc[0] == ~0x66666666) )
+         pLib->fHasXor = 1;
+    if ( Kit_DsdNonDsdSizeMax(pNtk) == 3 )
+        pLib->fHasMux = pGate->fMux = 1;
+    pNtk = Kit_DsdExpand( pTemp = pNtk );
+    Kit_DsdNtkFree( pTemp );
+    Kit_DsdVerify( pNtk, pGate->pFunc, pGate->nPins ); 
+if ( pLib->fVerbose )
+//if ( pGate->fMux )
+{
+printf( "\nProcessing library gate %4d: %10s ", pGate->Id, pGate->pName );
+Kit_DsdPrint( stdout, pNtk );
+}
+    vNods = Amap_CreateRulesFromDsd( pLib, pNtk );
+    if ( vNods )
+    {
+        Vec_IntForEachEntry( vNods, iNod, i )
+        {
+            assert( iNod > 1 );
+            pNod = Amap_LibNod( pLib, Amap_Lit2Var(iNod) );
+            assert( pNod->Type == AMAP_OBJ_MUX || pNod->nSuppSize == pGate->nPins );
+            pSet = (Amap_Set_t *)Aig_MmFlexEntryFetch( pLib->pMemSet, sizeof(Amap_Set_t) );
+            memset( pSet, 0, sizeof(Amap_Set_t) );
+            pSet->iGate = pGate->Id;
+            pSet->fInv  = Amap_LitIsCompl(iNod);
+            pSet->nIns  = pGate->nPins;
+            if ( Amap_LibDeriveGatePerm( pLib, pGate, pNtk, pNod, pSet->Ins ) == 0 )
+            {
+if ( pLib->fVerbose )
+{
+                printf( "Cound not prepare gate \"%s\": ", pGate->pName );
+                Kit_DsdPrint( stdout, pNtk );
+}
+                continue;
+            }
+            pSet->pNext = pNod->pSets;
+            pNod->pSets = pSet;
+            pLib->nSets++;
+        }
+        Vec_IntFree( vNods );
+    }
+    Kit_DsdNtkFree( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates rules for the given gate]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Amap_LibCreateRules( Amap_Lib_t * pLib, int fVeryVerbose )
+{
+    Amap_Gat_t * pGate;
+    int i, nGates = 0;
+    int clk = clock();
+    pLib->fVerbose = fVeryVerbose;
+    pLib->vRules   = Vec_PtrAlloc( 100 );
+    pLib->vRulesX  = Vec_PtrAlloc( 100 );
+    pLib->vRules3  = Vec_IntAlloc( 100 );
+    Amap_LibCreateVar( pLib );
+    Vec_PtrForEachEntry( pLib->vSelect, pGate, i )
+    {
+        if ( pGate->nPins < 2 )
+            continue;
+        if ( pGate->pFunc == NULL )
+        {
+            printf( "Amap_LibCreateRules(): Skipping gate %s (%s).\n", pGate->pName, pGate->pForm );
+            continue;
+        }
+        Amap_CreateRulesForGate( pLib, pGate );
+        nGates++;
+    }
+    assert( Vec_PtrSize(pLib->vRules)  == 2*pLib->nNodes );
+    assert( Vec_PtrSize(pLib->vRulesX) == 2*pLib->nNodes );
+    pLib->pRules  = Amap_LibLookupTableAlloc( pLib->vRules, 0 );
+    pLib->pRulesX = Amap_LibLookupTableAlloc( pLib->vRulesX, 0 );
+    Vec_VecFree( (Vec_Vec_t *)pLib->vRules );  pLib->vRules  = NULL;
+    Vec_VecFree( (Vec_Vec_t *)pLib->vRulesX ); pLib->vRulesX = NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/amapUniq.c b/src/map/amap/amapUniq.c
new file mode 100644
index 00000000..83fce6a2
--- /dev/null
+++ b/src/map/amap/amapUniq.c
@@ -0,0 +1,312 @@
+/**CFile****************************************************************
+
+  FileName    [amapUniq.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Technology mapper for standard cells.]
+
+  Synopsis    [Checks if the structural node already exists.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: amapUniq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "amapInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the entry exists and returns value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntCheckWithMask( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( (0xffff & p->pArray[i]) == (0xffff & Entry) )
+            return p->pArray[i] >> 16;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Pushes entry in the natural order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntPushOrderWithMask( Vec_Int_t * p, int Entry )
+{
+    int i;
+    if ( p->nSize == p->nCap )
+        Vec_IntGrow( p, 2 * p->nCap );
+    p->nSize++;
+    for ( i = p->nSize-2; i >= 0; i-- )
+        if ( (0xffff & p->pArray[i]) > (0xffff & Entry) )
+            p->pArray[i+1] = p->pArray[i];
+        else
+            break;
+    p->pArray[i+1] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibFindNode( Amap_Lib_t * pLib, int iFan0, int iFan1, int fXor )
+{
+    if ( fXor )
+        return Vec_IntCheckWithMask( Vec_PtrEntry(pLib->vRulesX, iFan0), iFan1 );
+    else
+        return Vec_IntCheckWithMask( Vec_PtrEntry(pLib->vRules, iFan0), iFan1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the three-argument rule exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibFindMux( Amap_Lib_t * p, int iFan0, int iFan1, int iFan2 )
+{
+    int x;
+    for ( x = 0; x < Vec_IntSize(p->vRules3); x += 4 )
+    {
+        if ( Vec_IntEntry(p->vRules3, x)   == iFan0 &&
+             Vec_IntEntry(p->vRules3, x+1) == iFan1 &&
+             Vec_IntEntry(p->vRules3, x+2) == iFan2 )
+        {
+            return Vec_IntEntry(p->vRules3, x+3);
+        }
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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->nNodesAlloc *= 2;
+    }
+    pNode = Amap_LibNod( p, p->nNodes );
+    memset( pNode, 0, sizeof(Amap_Nod_t) );
+    pNode->Id = p->nNodes++;
+    Vec_PtrPush( p->vRules, Vec_IntAlloc(8) );
+    Vec_PtrPush( p->vRules, Vec_IntAlloc(8) );
+    Vec_PtrPush( p->vRulesX, Vec_IntAlloc(8) );
+    Vec_PtrPush( p->vRulesX, Vec_IntAlloc(8) );
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibCreateVar( Amap_Lib_t * p )
+{
+    Amap_Nod_t * pNode;
+    // start the manager
+    assert( p->pNodes == NULL );
+    p->nNodesAlloc = 256;
+    p->pNodes = ALLOC( Amap_Nod_t, p->nNodesAlloc );
+    // create the first node
+    pNode = Amap_LibCreateObj( p );
+    p->pNodes->Type = AMAP_OBJ_PI;
+    p->pNodes->nSuppSize = 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibCreateNode( Amap_Lib_t * p, int iFan0, int iFan1, int fXor )
+{
+    Amap_Nod_t * pNode;
+    int iFan;
+    if ( iFan0 < iFan1 )
+    {
+        iFan  = iFan0;
+        iFan0 = iFan1;
+        iFan1 = iFan;
+    }
+    pNode = Amap_LibCreateObj( p );
+    pNode->Type  = fXor? AMAP_OBJ_XOR : AMAP_OBJ_AND;
+    pNode->nSuppSize = p->pNodes[Amap_Lit2Var(iFan0)].nSuppSize + p->pNodes[Amap_Lit2Var(iFan1)].nSuppSize;
+    pNode->iFan0 = iFan0;
+    pNode->iFan1 = iFan1;
+if ( p->fVerbose )
+printf( "Creating node %5d %c :  iFan0 = %5d%c  iFan1 = %5d%c\n", 
+pNode->Id, (fXor?'x':' '), 
+Amap_Lit2Var(iFan0), (Amap_LitIsCompl(iFan0)?'-':'+'), 
+Amap_Lit2Var(iFan1), (Amap_LitIsCompl(iFan1)?'-':'+') );
+
+    if ( fXor )
+    {
+        if ( iFan0 == iFan1 )
+            Vec_IntPushOrderWithMask( Vec_PtrEntry(p->vRulesX, iFan0), (pNode->Id << 16) | iFan1 );
+        else
+        {
+            Vec_IntPushOrderWithMask( Vec_PtrEntry(p->vRulesX, iFan0), (pNode->Id << 16) | iFan1 );
+            Vec_IntPushOrderWithMask( Vec_PtrEntry(p->vRulesX, iFan1), (pNode->Id << 16) | iFan0 );
+        }
+    }
+    else
+    {
+        if ( iFan0 == iFan1 )
+            Vec_IntPushOrderWithMask( Vec_PtrEntry(p->vRules, iFan0), (pNode->Id << 16) | iFan1 );
+        else
+        {
+            Vec_IntPushOrderWithMask( Vec_PtrEntry(p->vRules, iFan0), (pNode->Id << 16) | iFan1 );
+            Vec_IntPushOrderWithMask( Vec_PtrEntry(p->vRules, iFan1), (pNode->Id << 16) | iFan0 );
+        }
+    }
+    return pNode->Id;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Amap_LibCreateMux( Amap_Lib_t * p, int iFan0, int iFan1, int iFan2 )
+{
+    Amap_Nod_t * pNode;
+    pNode = Amap_LibCreateObj( p );
+    pNode->Type  = AMAP_OBJ_MUX;
+    pNode->nSuppSize = p->pNodes[Amap_Lit2Var(iFan0)].nSuppSize + p->pNodes[Amap_Lit2Var(iFan1)].nSuppSize + p->pNodes[Amap_Lit2Var(iFan2)].nSuppSize;
+    pNode->iFan0 = iFan0;
+    pNode->iFan1 = iFan1;
+    pNode->iFan2 = iFan2;
+if ( p->fVerbose )
+printf( "Creating node %5d %c :  iFan0 = %5d%c  iFan1 = %5d%c  iFan2 = %5d%c\n", 
+pNode->Id, 'm', 
+Amap_Lit2Var(iFan0), (Amap_LitIsCompl(iFan0)?'-':'+'), 
+Amap_Lit2Var(iFan1), (Amap_LitIsCompl(iFan1)?'-':'+'), 
+Amap_Lit2Var(iFan2), (Amap_LitIsCompl(iFan2)?'-':'+') );
+
+    Vec_IntPush( p->vRules3, iFan0 );
+    Vec_IntPush( p->vRules3, iFan1 );
+    Vec_IntPush( p->vRules3, iFan2 );
+    Vec_IntPush( p->vRules3, pNode->Id );
+    return pNode->Id;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates triangular lookup table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int ** Amap_LibLookupTableAlloc( Vec_Ptr_t * vVec, int fVerbose )
+{
+    Vec_Int_t * vOne;
+    int ** pRes, * pBuffer;
+    int i, k, nTotal, nSize, nEntries, Value;
+    // count the total size
+    nEntries = nSize = Vec_PtrSize( vVec );
+    Vec_PtrForEachEntry( vVec, vOne, i )
+        nEntries += Vec_IntSize(vOne);
+    pBuffer = ALLOC( int, nSize * sizeof(void *) + nEntries );
+    pRes = (int **)pBuffer;
+    pRes[0] = pBuffer + nSize * sizeof(void *);
+    nTotal = 0;
+    Vec_PtrForEachEntry( vVec, vOne, i )
+    {
+        pRes[i] = pRes[0] + nTotal;
+        nTotal += Vec_IntSize(vOne) + 1;
+        if ( fVerbose )
+        printf( "%d : ", i );
+        Vec_IntForEachEntry( vOne, Value, k )
+        {
+            pRes[i][k] = Value;
+            if ( fVerbose )
+            printf( "%d(%d) ", Value&0xffff, Value>>16 );
+        }
+        if ( fVerbose )
+        printf( "\n" );
+        pRes[i][k] = 0;
+    }
+    assert( nTotal == nEntries );
+    return pRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/map/amap/module.make b/src/map/amap/module.make
new file mode 100644
index 00000000..d5edadb9
--- /dev/null
+++ b/src/map/amap/module.make
@@ -0,0 +1,12 @@
+SRC +=  src/map/amap/amapCore.c \
+    src/map/amap/amapGraph.c \
+    src/map/amap/amapLib.c \
+    src/map/amap/amapMan.c \
+    src/map/amap/amapMatch.c \
+    src/map/amap/amapMerge.c \
+    src/map/amap/amapOutput.c \
+    src/map/amap/amapParse.c \
+    src/map/amap/amapPerm.c \
+    src/map/amap/amapRead.c \
+    src/map/amap/amapRule.c \
+    src/map/amap/amapUniq.c
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 24046f06..ce2cb483 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -88,6 +88,7 @@ struct If_Par_t_
     int                fExpRed;       // expand/reduce of the best cuts
     int                fLatchPaths;   // reset timing on latch paths
     int                fEdge;         // uses edge-based cut selection heuristics
+    int                fPower;        // uses power-aware cut selection heuristics
     int                fCutMin;       // performs cut minimization by removing functionally reducdant variables
     int                fSeqMap;       // sequential mapping
     int                fBidec;        // use bi-decomposition
@@ -141,12 +142,14 @@ struct If_Man_t_
     float              RequiredGlo2;  // global required times
     float              AreaGlo;       // global area
     int                nNets;         // the sum total of fanins of all LUTs in the mapping
+    float              dPower;        // the sum total of switching activities of all LUTs in the mapping
     int                nCutsUsed;     // the number of cuts currently used
     int                nCutsMerged;   // the total number of cuts merged
     unsigned *         puTemp[4];     // used for the truth table computation
     int                SortMode;      // one of the three sorting modes
     int                fNextRound;    // set to 1 after the first round
     int                nChoices;      // the number of choice nodes
+    Vec_Int_t *        vSwitching;    // switching activity of each node
     // sequential mapping
     Vec_Ptr_t *        vLatchOrder;   // topological ordering of latches
     Vec_Int_t *        vLags;         // sequentail lags of all nodes
@@ -177,6 +180,7 @@ struct If_Cut_t_
     float              Area;          // area (or area-flow) of the cut
     float              AveRefs;       // the average number of leaf references
     float              Edge;          // the edge flow
+    float              Power;         // the power flow
     float              Delay;         // delay of the cut
     unsigned           uSign;         // cut signature
     unsigned           Cost    : 14;  // the user's cost of the cut
@@ -351,6 +355,7 @@ extern void            If_CutLift( If_Cut_t * pCut );
 extern void            If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
 extern float           If_CutAreaFlow( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutPowerFlow( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot );
 extern float           If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutAreaDeref( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutAreaRef( If_Man_t * p, If_Cut_t * pCut );
@@ -360,6 +365,10 @@ extern float           If_CutEdgeDeref( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutEdgeRef( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut );
 extern float           If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut );
+extern float           If_CutPowerDeref( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot );
+extern float           If_CutPowerRef( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot );
+extern float           If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot );
+extern float           If_CutPowerRefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot );
 /*=== ifLib.c =============================================================*/
 extern If_Lib_t *      If_LutLibRead( char * FileName );
 extern If_Lib_t *      If_LutLibDup( If_Lib_t * p );
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index afaae239..af1f5213 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -432,40 +432,144 @@ void If_ManSortCuts( If_Man_t * p, int Mode )
 ***********************************************************************/
 static inline int If_ManSortCompare( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1 )
 {
-    if ( p->SortMode == 1 ) // area
+    if ( p->pPars->fPower )
     {
-        if ( pC0->Area < pC1->Area - p->fEpsilon )
+        if ( p->SortMode == 1 ) // area flow       
+        {
+            if ( pC0->Area < pC1->Area - p->fEpsilon )
+                return -1;
+            if ( pC0->Area > pC1->Area + p->fEpsilon )
+                return 1;
+            //printf("area(%.2f, %.2f), power(%.2f, %.2f), edge(%.2f, %.2f)\n",
+            //         pC0->Area, pC1->Area, pC0->Power, pC1->Power, pC0->Edge, pC1->Edge);
+            if ( pC0->Power < pC1->Power - p->fEpsilon )
+                return -1;
+            if ( pC0->Power > pC1->Power + p->fEpsilon )
+                return 1;
+            if ( pC0->Edge < pC1->Edge - p->fEpsilon )
+                return -1;
+            if ( pC0->Edge > pC1->Edge + p->fEpsilon )
+                return 1;
+            if ( pC0->AveRefs > pC1->AveRefs )
+                return -1;
+            if ( pC0->AveRefs < pC1->AveRefs )
+                return 1;
+            if ( pC0->nLeaves < pC1->nLeaves )
+                return -1;
+            if ( pC0->nLeaves > pC1->nLeaves )
+                return 1;
+            if ( pC0->Delay < pC1->Delay - p->fEpsilon )
+                return -1;
+            if ( pC0->Delay > pC1->Delay + p->fEpsilon )
+                return 1;
+            return 0;
+        }
+        if ( p->SortMode == 0 ) // delay
+        {
+            if ( pC0->Delay < pC1->Delay - p->fEpsilon )
+                return -1;
+            if ( pC0->Delay > pC1->Delay + p->fEpsilon )
+                return 1;
+            if ( pC0->nLeaves < pC1->nLeaves )
+                return -1;
+            if ( pC0->nLeaves > pC1->nLeaves )
+                return 1;
+            if ( pC0->Area < pC1->Area - p->fEpsilon )
+                return -1;
+            if ( pC0->Area > pC1->Area + p->fEpsilon )
+                return 1;
+            if ( pC0->Power < pC1->Power - p->fEpsilon  )
+                return -1;
+            if ( pC0->Power > pC1->Power + p->fEpsilon  )
+                return 1;
+            if ( pC0->Edge < pC1->Edge - p->fEpsilon )
+                return -1;
+            if ( pC0->Edge > pC1->Edge + p->fEpsilon )
+                return 1;
+            return 0;
+        }
+        assert( p->SortMode == 2 ); // delay old, exact area
+        if ( pC0->Delay < pC1->Delay - p->fEpsilon )
             return -1;
-        if ( pC0->Area > pC1->Area + p->fEpsilon )
+        if ( pC0->Delay > pC1->Delay + p->fEpsilon )
+            return 1;
+        if ( pC0->Power < pC1->Power - p->fEpsilon  )
+            return -1;
+        if ( pC0->Power > pC1->Power + p->fEpsilon  )
             return 1;
         if ( pC0->Edge < pC1->Edge - p->fEpsilon )
             return -1;
         if ( pC0->Edge > pC1->Edge + p->fEpsilon )
             return 1;
-        if ( pC0->AveRefs > pC1->AveRefs )
+        if ( pC0->Area < pC1->Area - p->fEpsilon )
             return -1;
-        if ( pC0->AveRefs < pC1->AveRefs )
+        if ( pC0->Area > pC1->Area + p->fEpsilon )
             return 1;
         if ( pC0->nLeaves < pC1->nLeaves )
             return -1;
         if ( pC0->nLeaves > pC1->nLeaves )
             return 1;
-        if ( pC0->Delay < pC1->Delay - p->fEpsilon )
-            return -1;
-        if ( pC0->Delay > pC1->Delay + p->fEpsilon )
-            return 1;
         return 0;
-    }
-    if ( p->SortMode == 0 ) // delay
+    } 
+    else  // reglar
     {
+        if ( p->SortMode == 1 ) // area
+        {
+            if ( pC0->Area < pC1->Area - p->fEpsilon )
+                return -1;
+            if ( pC0->Area > pC1->Area + p->fEpsilon )
+                return 1;
+            if ( pC0->Edge < pC1->Edge - p->fEpsilon )
+                return -1;
+            if ( pC0->Edge > pC1->Edge + p->fEpsilon )
+                return 1;
+            if ( pC0->Power < pC1->Power - p->fEpsilon )
+                return -1;
+            if ( pC0->Power > pC1->Power + p->fEpsilon )
+                return 1;
+            if ( pC0->AveRefs > pC1->AveRefs )
+                return -1;
+            if ( pC0->AveRefs < pC1->AveRefs )
+                return 1;
+            if ( pC0->nLeaves < pC1->nLeaves )
+                return -1;
+            if ( pC0->nLeaves > pC1->nLeaves )
+                return 1;
+            if ( pC0->Delay < pC1->Delay - p->fEpsilon )
+                return -1;
+            if ( pC0->Delay > pC1->Delay + p->fEpsilon )
+                return 1;
+            return 0;
+        }
+        if ( p->SortMode == 0 ) // delay
+        {
+            if ( pC0->Delay < pC1->Delay - p->fEpsilon )
+                return -1;
+            if ( pC0->Delay > pC1->Delay + p->fEpsilon )
+                return 1;
+            if ( pC0->nLeaves < pC1->nLeaves )
+                return -1;
+            if ( pC0->nLeaves > pC1->nLeaves )
+                return 1;
+            if ( pC0->Area < pC1->Area - p->fEpsilon )
+                return -1;
+            if ( pC0->Area > pC1->Area + p->fEpsilon )
+                return 1;
+            if ( pC0->Edge < pC1->Edge - p->fEpsilon )
+                return -1;
+            if ( pC0->Edge > pC1->Edge + p->fEpsilon )
+                return 1;
+            if ( pC0->Power < pC1->Power - p->fEpsilon )
+                return -1;
+            if ( pC0->Power > pC1->Power + p->fEpsilon )
+                return 1;
+            return 0;
+        }
+        assert( p->SortMode == 2 ); // delay old
         if ( pC0->Delay < pC1->Delay - p->fEpsilon )
             return -1;
         if ( pC0->Delay > pC1->Delay + p->fEpsilon )
             return 1;
-        if ( pC0->nLeaves < pC1->nLeaves )
-            return -1;
-        if ( pC0->nLeaves > pC1->nLeaves )
-            return 1;
         if ( pC0->Area < pC1->Area - p->fEpsilon )
             return -1;
         if ( pC0->Area > pC1->Area + p->fEpsilon )
@@ -474,26 +578,16 @@ static inline int If_ManSortCompare( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC
             return -1;
         if ( pC0->Edge > pC1->Edge + p->fEpsilon )
             return 1;
+        if ( pC0->Power < pC1->Power - p->fEpsilon )
+            return -1;
+        if ( pC0->Power > pC1->Power + p->fEpsilon )
+            return 1;
+        if ( pC0->nLeaves < pC1->nLeaves )
+            return -1;
+        if ( pC0->nLeaves > pC1->nLeaves )
+            return 1;
         return 0;
     }
-    assert( p->SortMode == 2 ); // delay old
-    if ( pC0->Delay < pC1->Delay - p->fEpsilon )
-        return -1;
-    if ( pC0->Delay > pC1->Delay + p->fEpsilon )
-        return 1;
-    if ( pC0->Area < pC1->Area - p->fEpsilon )
-        return -1;
-    if ( pC0->Area > pC1->Area + p->fEpsilon )
-        return 1;
-    if ( pC0->Edge < pC1->Edge - p->fEpsilon )
-        return -1;
-    if ( pC0->Edge > pC1->Edge + p->fEpsilon )
-        return 1;
-    if ( pC0->nLeaves < pC1->nLeaves )
-        return -1;
-    if ( pC0->nLeaves > pC1->nLeaves )
-        return 1;
-    return 0;
 }
 
 /**Function*************************************************************
@@ -820,6 +914,40 @@ float If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes area flow.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutPowerFlow( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
+{
+    If_Obj_t * pLeaf;
+    float * pSwitching = (float *)p->vSwitching->pArray;
+    float Power = 0;
+    int i;
+    assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        Power += pSwitching[pLeaf->Id];
+        if ( pLeaf->nRefs == 0 )
+            Power += If_ObjCutBest(pLeaf)->Power;
+        else if ( p->pPars->fSeqMap ) // seq
+            Power += If_ObjCutBest(pLeaf)->Power / pLeaf->nRefs;
+        else 
+        {
+            assert( pLeaf->EstRefs > p->fEpsilon );
+            Power += If_ObjCutBest(pLeaf)->Power / pLeaf->EstRefs;
+        }
+    }
+    return Power;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Average number of references of the leaves.]
 
   Description []
@@ -1038,6 +1166,107 @@ float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut )
     return aResult;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+float If_CutPowerDeref( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
+{
+    If_Obj_t * pLeaf;
+    float * pSwitching = (float *)p->vSwitching->pArray;
+    float Power = 0;
+    int i;
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        Power += pSwitching[pLeaf->Id];
+        assert( pLeaf->nRefs > 0 );
+        if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) )
+            continue;
+        Power += If_CutPowerDeref( p, If_ObjCutBest(pLeaf), pRoot );
+    }
+    return Power;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutPowerRef( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
+{
+    If_Obj_t * pLeaf;
+    float * pSwitching = (float *)p->vSwitching->pArray;
+    float Power = 0;
+    int i;
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+    {
+        Power += pSwitching[pLeaf->Id];
+        assert( pLeaf->nRefs >= 0 );
+        if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) )
+            continue;
+        Power += If_CutPowerRef( p, If_ObjCutBest(pLeaf), pRoot );
+    }
+    return Power;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes Power of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
+{
+    float aResult, aResult2;
+    assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+    aResult2 = If_CutPowerRef( p, pCut, pRoot );
+    aResult  = If_CutPowerDeref( p, pCut, pRoot );
+    assert( aResult > aResult2 - p->fEpsilon );
+    assert( aResult < aResult2 + p->fEpsilon );
+    return aResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area of the first level.]
+
+  Description [The cut need to be derefed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float If_CutPowerRefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
+{
+    float aResult, aResult2;
+    assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+    aResult2 = If_CutPowerDeref( p, pCut, pRoot );
+    aResult  = If_CutPowerRef( p, pCut, pRoot );
+    assert( aResult > aResult2 - p->fEpsilon );
+    assert( aResult < aResult2 + p->fEpsilon );
+    return aResult;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Computes the cone of the cut in AIG with choices.]
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 35b0cccc..82ee6728 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -145,6 +145,8 @@ void If_ManStop( If_Man_t * p )
         FREE( p->pPars->pTimesReq );
     if ( p->pManTim )
         Tim_ManStop( p->pManTim );
+    if ( p->vSwitching )
+        Vec_IntFree( p->vSwitching );
     free( p );
 }
 
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 75370dff..fc3d7cd3 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -95,6 +95,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
         if ( p->pPars->fEdge )
             pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
+        if ( p->pPars->fPower )
+            pCut->Power = (Mode == 2)? If_CutPowerDerefed( p, pCut, pObj ) : If_CutPowerFlow( p, pCut, pObj );
         // save the best cut from the previous iteration
         if ( !fPreprocess )
             If_CutCopy( p, pCutSet->ppCuts[pCutSet->nCuts++], pCut );
@@ -141,6 +143,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
         if ( p->pPars->fEdge )
             pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
+        if ( p->pPars->fPower )
+            pCut->Power = (Mode == 2)? If_CutPowerDerefed( p, pCut, pObj ) : If_CutPowerFlow( p, pCut, pObj );
         pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
         // insert the cut into storage
         If_CutSort( p, pCutSet, pCut );
@@ -227,6 +231,8 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
             pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
             if ( p->pPars->fEdge )
                 pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
+            if ( p->pPars->fPower )
+                pCut->Power = (Mode == 2)? If_CutPowerDerefed( p, pCut, pObj ) : If_CutPowerFlow( p, pCut, pObj );
             pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
             // insert the cut into storage
             If_CutSort( p, pCutSet, pCut );
@@ -334,8 +340,8 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
     if ( p->pPars->fVerbose )
     {
         char Symb = fPreprocess? 'P' : ((Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'));
-        printf( "%c: Del = %7.2f. Ar = %9.1f. Edge = %8d. Cut = %8d. ", 
-            Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged );
+        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 );
 //    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 fd1af0d7..a5fa7d86 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -55,8 +55,8 @@ void If_ManImproveMapping( If_Man_t * p )
     If_ManComputeRequired( p );
     if ( p->pPars->fVerbose )
     {
-        printf( "E: Del = %7.2f. Ar = %9.1f. Edge = %8d. Cut = %8d. ", 
-            p->RequiredGlo, p->AreaGlo, p->nNets, p->nCutsMerged );
+        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 );
     }
  
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index 57e1ad13..06015b06 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -585,6 +585,7 @@ float If_ManMarkMapping_rec( If_Man_t * p, If_Obj_t * pObj )
 {
     If_Obj_t * pLeaf;
     If_Cut_t * pCutBest;
+    float * pSwitching = p->vSwitching? (float*)p->vSwitching->pArray : NULL;
     float aArea;
     int i;
     if ( pObj->nRefs++ || If_ObjIsCi(pObj) || If_ObjIsConst1(pObj) )
@@ -596,7 +597,10 @@ float If_ManMarkMapping_rec( If_Man_t * p, If_Obj_t * pObj )
     p->nNets += pCutBest->nLeaves;
     aArea = If_CutLutArea( p, pCutBest );
     If_CutForEachLeaf( p, pCutBest, pLeaf, i )
+    {
+        p->dPower += pSwitching? pSwitching[pLeaf->Id] : 0.0;
         aArea += If_ManMarkMapping_rec( p, pLeaf );
+    }
     return aArea;
 }
 
@@ -622,6 +626,7 @@ void If_ManMarkMapping( If_Man_t * p )
         pObj->nRefs = 0;
     }
     p->nNets = 0;
+    p->dPower = 0.0;
     p->AreaGlo = 0.0;
     If_ManForEachCo( p, pObj, i )
         p->AreaGlo += If_ManMarkMapping_rec( p, If_ObjFanin0(pObj) );
diff --git a/src/map/mapper/mapperTime.c b/src/map/mapper/mapperTime.c
index cc4173cf..309863fd 100644
--- a/src/map/mapper/mapperTime.c
+++ b/src/map/mapper/mapperTime.c
@@ -206,7 +206,7 @@ void Map_TimeComputeRequiredGlobal( Map_Man_t * p )
         }
         else if ( p->fRequiredGlo < p->DelayTarget - p->fEpsilon )
         {
-            if ( p->fMappingMode == 1 )
+            if ( p->fMappingMode == 1 && p->fVerbose )
                 printf( "Relaxing the required times from (%4.2f) to the target (%4.2f).\n", p->fRequiredGlo, p->DelayTarget );
             p->fRequiredGlo = p->DelayTarget;
         }
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index 37ba82c2..1326dbbf 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -28,6 +28,10 @@
 #include "mioInt.h"
 #include "mapper.h"
 
+extern void Amap_LibFree( void * p );
+extern void Amap_LibPrintSelectedGates( void * p, int fAllGates );
+extern void * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVerbose );
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,6 +39,9 @@
 static int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv );
 static int Mio_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv );
 
+static int Mio_CommandReadLibrary2( Abc_Frame_t * pAbc, int argc, char **argv );
+static int Mio_CommandPrintLibrary2( Abc_Frame_t * pAbc, int argc, char **argv );
+
 // internal version of GENLIB library
 static char * pMcncGenlib[25] = {
     "GATE inv1    1   O=!a;             PIN * INV     1 999 0.9 0.0 0.9 0.0\n",
@@ -78,7 +85,7 @@ static char * pMcncGenlib[25] = {
 void Mio_Init( Abc_Frame_t * pAbc )
 {
     char * pFileTemp = "mcnc_temp.genlib";
-    Mio_Library_t * pLibGen;
+    void * pLibGen;
     FILE * pFile;
     int i;
 
@@ -90,6 +97,9 @@ void Mio_Init( Abc_Frame_t * pAbc )
     // read genlib from file
     pLibGen = Mio_LibraryRead( pAbc, pFileTemp, NULL, 0 );
     Abc_FrameSetLibGen( pLibGen );
+    pLibGen = Amap_LibReadAndPrepare( pFileTemp, 0, 0 );
+    Abc_FrameSetLibGen2( pLibGen );
+
 #ifdef WIN32
         _unlink( pFileTemp );
 #else
@@ -98,6 +108,9 @@ void Mio_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "SC mapping", "read_library",   Mio_CommandReadLibrary,  0 ); 
     Cmd_CommandAdd( pAbc, "SC mapping", "print_library",  Mio_CommandPrintLibrary, 0 ); 
+
+    Cmd_CommandAdd( pAbc, "SC mapping", "read_library2",   Mio_CommandReadLibrary2,  0 ); 
+    Cmd_CommandAdd( pAbc, "SC mapping", "print_library2",  Mio_CommandPrintLibrary2, 0 ); 
 }
 
 /**Function*************************************************************
@@ -115,6 +128,7 @@ void Mio_End()
 {
 //    Mio_LibraryDelete( s_pLib );
     Mio_LibraryDelete( Abc_FrameReadLibGen() );
+    Amap_LibFree( Abc_FrameReadLibGen2() );
 }
 
 
@@ -190,25 +204,124 @@ int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
     if ( Abc_FrameReadLibSuper() )
     {
         extern void Map_SuperLibFree( Map_SuperLib_t * p );
-//        Map_SuperLibFree( s_pSuperLib );
-//        s_pSuperLib = NULL;
         Map_SuperLibFree( Abc_FrameReadLibSuper() );
         Abc_FrameSetLibSuper( NULL );
     }
 
     // replace the current library
-//    Mio_LibraryDelete( s_pLib );
-//    s_pLib = pLib;
     Mio_LibraryDelete( Abc_FrameReadLibGen() );
     Abc_FrameSetLibGen( pLib );
+
+    // set the new network
+    pLib = Amap_LibReadAndPrepare( FileName, 1, 0 );  
+    if ( pLib == NULL )
+    {
+        fprintf( pErr, "Reading GENLIB library has failed.\n" );
+        return 1;
+    }
+    // replace the current library
+    Amap_LibFree( Abc_FrameReadLibGen2() );
+    Abc_FrameSetLibGen2( pLib );
     return 0;
 
 usage:
     fprintf( pErr, "usage: read_library [-vh]\n");
     fprintf( pErr, "\t         read the library from a genlib file\n" );  
     fprintf( pErr, "\t         (if the library contains more than one gate\n" );  
-    fprintf( pErr, "\t         with the same Boolean function, only the first gate\n" );  
-    fprintf( pErr, "\t         in the order of their appearance in the file is used)\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_CommandReadLibrary2( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    FILE * pFile;
+    FILE * pOut, * pErr;
+    Mio_Library_t * pLib;
+    Abc_Ntk_t * pNet;
+    char * FileName;
+    int fVerbose;
+    int fVeryVerbose;
+    int c;
+
+    pNet = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set the defaults
+    fVerbose     = 1;
+    fVeryVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "vwh")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'w':
+                fVeryVerbose ^= 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 );
+
+    // set the new network
+    pLib = Amap_LibReadAndPrepare( FileName, fVerbose, fVeryVerbose );  
+    if ( pLib == NULL )
+    {
+        fprintf( pErr, "Reading GENLIB library has failed.\n" );
+        return 1;
+    }
+
+    // replace the current library
+    Amap_LibFree( Abc_FrameReadLibGen2() );
+    Abc_FrameSetLibGen2( pLib );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: read_library2 [-vh]\n");
+    fprintf( pErr, "\t         read the library from a genlib file\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-w     : toggle detailed printout [default = %s]\n", fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : enable verbose output\n");
     return 1;       /* error exit */
 }
@@ -271,6 +384,72 @@ usage:
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;       /* error exit */
 }
+
+
+/**Function*************************************************************
+
+  Synopsis    [Command procedure to read LUT libraries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_CommandPrintLibrary2( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNet;
+    int fPrintAll;
+    int fVerbose;
+    int c;
+
+    pNet = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set the defaults
+    fPrintAll = 0;
+    fVerbose = 1;
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "avh")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'a':
+                fPrintAll ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+
+    if ( argc != globalUtilOptind )
+    {
+        goto usage;
+    }
+
+    // set the new network
+    Amap_LibPrintSelectedGates( Abc_FrameReadLibGen2(), fPrintAll );
+    return 0;
+
+usage:
+    fprintf( pErr, "\nusage: print_library2 [-avh]\n");
+    fprintf( pErr, "\t          print gates used for area-oriented tech-mapping\n" );  
+    fprintf( pErr, "\t-a      : toggles printing all gates [default = %s]\n", (fPrintAll? "yes" : "no") );
+    fprintf( pErr, "\t-v      : toggles enabling of verbose output [default = %s]\n", (fVerbose? "yes" : "no") );
+    fprintf( pErr, "\t-h      : print the command usage\n");
+    return 1;       /* error exit */
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index dbe2420b..0e5a39d3 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -79,6 +79,7 @@ typedef struct  Mio_PinStruct_t_          Mio_Pin_t;
 extern char *            Mio_LibraryReadName       ( Mio_Library_t * pLib );
 extern int               Mio_LibraryReadGateNum    ( Mio_Library_t * pLib );
 extern Mio_Gate_t *      Mio_LibraryReadGates      ( Mio_Library_t * pLib );
+extern Mio_Gate_t **     Mio_LibraryReadGatesByName( Mio_Library_t * pLib );
 extern DdManager *       Mio_LibraryReadDd         ( Mio_Library_t * pLib );
 extern Mio_Gate_t *      Mio_LibraryReadGateByName ( Mio_Library_t * pLib, char * pName );
 extern char *            Mio_LibraryReadSopByName  ( Mio_Library_t * pLib, char * pName );    
@@ -110,6 +111,8 @@ extern int               Mio_GateReadInputs        ( Mio_Gate_t * pGate );
 extern double            Mio_GateReadDelayMax      ( Mio_Gate_t * pGate );      
 extern char *            Mio_GateReadSop           ( Mio_Gate_t * pGate );      
 extern DdNode *          Mio_GateReadFunc          ( Mio_Gate_t * pGate );
+extern int               Mio_GateReadValue         ( Mio_Gate_t * pGate );
+extern void              Mio_GateSetValue          ( Mio_Gate_t * pGate, int Value );
 extern char *            Mio_PinReadName           ( Mio_Pin_t * pPin );  
 extern Mio_PinPhase_t    Mio_PinReadPhase          ( Mio_Pin_t * pPin );  
 extern double            Mio_PinReadInputLoad      ( Mio_Pin_t * pPin );  
diff --git a/src/map/mio/mio81214.zip b/src/map/mio/mio81214.zip
new file mode 100644
index 00000000..12f766a9
--- /dev/null
+++ b/src/map/mio/mio81214.zip
diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c
index 73473f8b..61cc2509 100644
--- a/src/map/mio/mioApi.c
+++ b/src/map/mio/mioApi.c
@@ -40,6 +40,7 @@
 char *            Mio_LibraryReadName          ( Mio_Library_t * pLib )  { return pLib->pName;    }
 int               Mio_LibraryReadGateNum       ( Mio_Library_t * pLib )  { return pLib->nGates;   }
 Mio_Gate_t *      Mio_LibraryReadGates         ( Mio_Library_t * pLib )  { return pLib->pGates;   }
+Mio_Gate_t **     Mio_LibraryReadGatesByName   ( Mio_Library_t * pLib )  { return pLib->ppGatesName;}
 DdManager *       Mio_LibraryReadDd            ( Mio_Library_t * pLib )  { return pLib->dd;       }
 Mio_Gate_t *      Mio_LibraryReadBuf           ( Mio_Library_t * pLib )  { return pLib->pGateBuf; }
 Mio_Gate_t *      Mio_LibraryReadInv           ( Mio_Library_t * pLib )  { return pLib->pGateInv; }
@@ -131,17 +132,19 @@ char * Mio_LibraryReadSopByName( Mio_Library_t * pLib, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-char *            Mio_GateReadName    ( Mio_Gate_t * pGate )           { return pGate->pName;     }
-char *            Mio_GateReadOutName ( Mio_Gate_t * pGate )           { return pGate->pOutName;  }
-double            Mio_GateReadArea    ( Mio_Gate_t * pGate )           { return pGate->dArea;     }
-char *            Mio_GateReadForm    ( Mio_Gate_t * pGate )           { return pGate->pForm;     }
-Mio_Pin_t *       Mio_GateReadPins    ( Mio_Gate_t * pGate )           { return pGate->pPins;     }
-Mio_Library_t *   Mio_GateReadLib     ( Mio_Gate_t * pGate )           { return pGate->pLib;      }
-Mio_Gate_t *      Mio_GateReadNext    ( Mio_Gate_t * pGate )           { return pGate->pNext;     }
-int               Mio_GateReadInputs  ( Mio_Gate_t * pGate )           { return pGate->nInputs;   }
-double            Mio_GateReadDelayMax( Mio_Gate_t * pGate )           { return pGate->dDelayMax; }
-char *            Mio_GateReadSop     ( Mio_Gate_t * pGate )           { return pGate->pSop;      }
-DdNode *          Mio_GateReadFunc    ( Mio_Gate_t * pGate )           { return pGate->bFunc;     }
+char *            Mio_GateReadName    ( Mio_Gate_t * pGate )            { return pGate->pName;     }
+char *            Mio_GateReadOutName ( Mio_Gate_t * pGate )            { return pGate->pOutName;  }
+double            Mio_GateReadArea    ( Mio_Gate_t * pGate )            { return pGate->dArea;     }
+char *            Mio_GateReadForm    ( Mio_Gate_t * pGate )            { return pGate->pForm;     }
+Mio_Pin_t *       Mio_GateReadPins    ( Mio_Gate_t * pGate )            { return pGate->pPins;     }
+Mio_Library_t *   Mio_GateReadLib     ( Mio_Gate_t * pGate )            { return pGate->pLib;      }
+Mio_Gate_t *      Mio_GateReadNext    ( Mio_Gate_t * pGate )            { return pGate->pNext;     }
+int               Mio_GateReadInputs  ( Mio_Gate_t * pGate )            { return pGate->nInputs;   }
+double            Mio_GateReadDelayMax( Mio_Gate_t * pGate )            { return pGate->dDelayMax; }
+char *            Mio_GateReadSop     ( Mio_Gate_t * pGate )            { return pGate->pSop;      }
+DdNode *          Mio_GateReadFunc    ( Mio_Gate_t * pGate )            { return pGate->bFunc;     }
+int               Mio_GateReadValue   ( Mio_Gate_t * pGate )            { return pGate->Value;     }
+void              Mio_GateSetValue    ( Mio_Gate_t * pGate, int Value ) { pGate->Value = Value;    }
 
 /**Function*************************************************************
 
diff --git a/src/map/mio/mioGENERIC.c b/src/map/mio/mioGENERIC.c
deleted file mode 100644
index 972c4ffc..00000000
--- a/src/map/mio/mioGENERIC.c
+++ /dev/null
@@ -1,46 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [mio___.c]
-
-  PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
-
-  Synopsis    [File reading/writing for technology mapping.]
-
-  Author      [MVSIS Group]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - September 8, 2003.]
-
-  Revision    [$Id: mio___.h,v 1.0 2003/09/08 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "mioInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/map/mio/mioInt.h b/src/map/mio/mioInt.h
index 3f90b625..654b7e19 100644
--- a/src/map/mio/mioInt.h
+++ b/src/map/mio/mioInt.h
@@ -54,6 +54,8 @@ struct  Mio_LibraryStruct_t_
 {
     char *             pName;       // the name of the library
     int                nGates;      // the number of the gates
+    Mio_Gate_t **      ppGates0;    // the array of gates in the original order
+    Mio_Gate_t **      ppGatesName; // the array of gates sorted by name
     Mio_Gate_t *       pGates;      // the linked list of all gates in no particular order
     Mio_Gate_t *       pGate0;      // the constant zero gate
     Mio_Gate_t *       pGate1;      // the constant one gate
@@ -84,7 +86,8 @@ struct  Mio_GateStruct_t_
     int                nInputs;     // the number of inputs
     double             dDelayMax;   // the maximum delay
     DdNode *           bFunc;       // the functionality
-    char *             pSop;
+    char *             pSop;        // sum-of-products
+    int                Value;       // user's information
 };
 
 struct  Mio_PinStruct_t_
diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c
index 5b92d3e1..ae33c942 100644
--- a/src/map/mio/mioRead.c
+++ b/src/map/mio/mioRead.c
@@ -418,11 +418,92 @@ char * chomp( char *s )
   SeeAlso     []
 
 ***********************************************************************/
+int Mio_LibraryCompareGatesByArea( Mio_Gate_t ** pp1, Mio_Gate_t ** pp2 )
+{
+    double Diff = (*pp1)->dArea - (*pp2)->dArea;
+    if ( Diff < 0.0 )
+        return -1;
+    if ( Diff > 0.0 ) 
+        return 1;
+    return 0; 
+}
+        
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mio_LibraryCompareGatesByName( Mio_Gate_t ** pp1, Mio_Gate_t ** pp2 )
+{
+    int Diff = strcmp( (*pp1)->pName, (*pp2)->pName );
+    if ( Diff < 0.0 )
+        return -1;
+    if ( Diff > 0.0 ) 
+        return 1;
+    return 0; 
+}
+        
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mio_LibrarySortGates( Mio_Library_t * pLib )
+{
+    Mio_Gate_t ** ppGates, * pGate;
+    int i = 0;
+    ppGates = 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 );
+    for ( i = 0; i < pLib->nGates; i++ )
+        pLib->ppGates0[i] = ppGates[i];
+    qsort( (void *)ppGates, pLib->nGates, sizeof(void *), 
+            (int (*)(const void *, const void *)) Mio_LibraryCompareGatesByArea );
+    for ( i = 0; i < pLib->nGates; i++ )
+        ppGates[i]->pNext = (i < pLib->nGates-1)? ppGates[i+1] : NULL;
+    pLib->pGates = ppGates[0];
+    free( ppGates );
+    // sort gates by name
+    pLib->ppGatesName = 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 *), 
+            (int (*)(const void *, const void *)) Mio_LibraryCompareGatesByName );
+}
+        
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Mio_LibraryDetectSpecialGates( Mio_Library_t * pLib )
 {
     Mio_Gate_t * pGate;
     DdNode * bFuncBuf, * bFuncInv, * bFuncNand2, * bFuncAnd2;
 
+    Mio_LibrarySortGates( pLib );
+
     bFuncBuf   = pLib->dd->vars[0];                                              Cudd_Ref( bFuncBuf );
     bFuncInv   = Cudd_Not( pLib->dd->vars[0] );                                  Cudd_Ref( bFuncInv );
     bFuncNand2 = Cudd_bddNand( pLib->dd, pLib->dd->vars[0], pLib->dd->vars[1] ); Cudd_Ref( bFuncNand2 );
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index bd3d01f7..2a1d1f30 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -59,6 +59,8 @@ 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 );
 }
 
@@ -82,7 +84,7 @@ void Mio_GateDelete( Mio_Gate_t * pGate )
     if ( pGate->bFunc )
         Cudd_RecursiveDeref( pGate->pLib->dd, pGate->bFunc );
     Mio_GateForEachPinSafe( pGate, pPin, pPin2 )
-        Mio_PinDelete( pPin );    
+        Mio_PinDelete( pPin );   
     free( pGate );
 }
 
@@ -142,11 +144,14 @@ Mio_Pin_t * Mio_PinDup( Mio_Pin_t * pPin )
 ***********************************************************************/
 void Mio_WriteLibrary( FILE * pFile, Mio_Library_t * pLib, int fPrintSops )
 {
-    Mio_Gate_t * pGate;
+//    Mio_Gate_t * pGate;
+    int i;
 
     fprintf( pFile, "# The genlib library \"%s\".\n", pLib->pName );
-    Mio_LibraryForEachGate( pLib, pGate )
-        Mio_WriteGate( pFile, pGate, fPrintSops );
+//    Mio_LibraryForEachGate( pLib, pGate )
+//        Mio_WriteGate( pFile, pGate, fPrintSops );
+    for ( i = 0; i < pLib->nGates; i++ )
+        Mio_WriteGate( pFile, pLib->ppGates0[i], fPrintSops );
 }
 
 /**Function*************************************************************
diff --git a/src/map/super/superGate.c b/src/map/super/superGate.c
index 915ff86d..c8aa02ba 100644
--- a/src/map/super/superGate.c
+++ b/src/map/super/superGate.c
@@ -345,7 +345,12 @@ Super_Man_t * Super_Compute( Super_Man_t * pMan, Mio_Gate_t ** ppGates, int nGat
                     continue;
             }
         }
-
+/*
+        if ( strcmp(Mio_GateReadName(ppGates[k]), "MUX2IX0") == 0 )
+        {
+            int s = 0;
+        }
+*/
         // select the subset of gates to be considered with this root gate
         // all the gates past this point will lead to delay larger than the limit
         tDelayMio = (float)Mio_GateReadDelayMax(ppGates[k]);