Integrating barrier buffers into the mapper.

12 files changed, 710 insertions, 1127 deletions

diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h
index fa468234..2a52ee08 100644
--- a/src/map/mapper/mapper.h
+++ b/src/map/mapper/mapper.h
@@ -82,8 +82,11 @@ extern void            Map_ManPrintTimeStats( Map_Man_t * p );
 extern void            Map_ManPrintStatsToFile( char * pName, float Area, float Delay, abctime Time );
 extern int             Map_ManReadInputNum( Map_Man_t * p );
 extern int             Map_ManReadOutputNum( Map_Man_t * p );
+extern int             Map_ManReadBufNum( Map_Man_t * p );
 extern Map_Node_t **   Map_ManReadInputs ( Map_Man_t * p );
 extern Map_Node_t **   Map_ManReadOutputs( Map_Man_t * p );
+extern Map_Node_t **   Map_ManReadBufs( Map_Man_t * p );
+extern Map_Node_t *    Map_ManReadBufDriver( Map_Man_t * p, int i );
 extern Map_Node_t *    Map_ManReadConst1 ( Map_Man_t * p );
 extern Map_Time_t *    Map_ManReadInputArrivals( Map_Man_t * p );
 extern Mio_Library_t * Map_ManReadGenLib ( Map_Man_t * p );
@@ -121,6 +124,7 @@ extern void            Map_NodeSetSwitching( Map_Node_t * p, float Switching );
 
 extern int             Map_NodeIsConst( Map_Node_t * p );
 extern int             Map_NodeIsVar( Map_Node_t * p );
+extern int             Map_NodeIsBuf( Map_Node_t * p );
 extern int             Map_NodeIsAnd( Map_Node_t * p );
 extern int             Map_NodeComparePhase( Map_Node_t * p1, Map_Node_t * p2 );
 
@@ -150,9 +154,7 @@ extern Map_Time_t      Map_SuperLibReadDelayInv( Map_SuperLib_t * p );
 extern int             Map_SuperLibReadVarsMax( Map_SuperLib_t * p );
 
 extern Map_Node_t *    Map_NodeAnd( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 );
-extern Map_Node_t *    Map_NodeOr( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 );
-extern Map_Node_t *    Map_NodeExor( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 );
-extern Map_Node_t *    Map_NodeMux( Map_Man_t * p, Map_Node_t * pNode, Map_Node_t * pNodeT, Map_Node_t * pNodeE );
+extern Map_Node_t *    Map_NodeBuf( Map_Man_t * p, Map_Node_t * p1 );
 extern void            Map_NodeSetChoice( Map_Man_t * pMan, Map_Node_t * pNodeOld, Map_Node_t * pNodeNew );
 
 /*=== resmCanon.c =============================================================*/
diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c
index 2f3263b3..1e96d7e2 100644
--- a/src/map/mapper/mapperCore.c
+++ b/src/map/mapper/mapperCore.c
@@ -57,8 +57,6 @@ int Map_Mapping( Map_Man_t * p )
 
     //////////////////////////////////////////////////////////////////////
     // perform pre-mapping computations
-    // collect the nodes reachable from POs in the DFS order (including the choices)
-    p->vAnds = Map_MappingDfs( p, 1 );
     if ( p->fVerbose )
         Map_MappingReportChoices( p ); 
     Map_MappingSetChoiceLevels( p ); // should always be called before mapping!
@@ -84,12 +82,12 @@ int Map_Mapping( Map_Man_t * p )
     p->timeMatch = Abc_Clock() - clk;
     // compute the references and collect the nodes used in the mapping
     Map_MappingSetRefs( p );
-    p->AreaBase = Map_MappingGetArea( p, p->vMapping );
+    p->AreaBase = Map_MappingGetArea( p );
 if ( p->fVerbose )
 {
 printf( "Delay    : %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
                     fShowSwitching? "Switch" : "Delay", 
-                    fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
+                    fShowSwitching? Map_MappingGetSwitching(p) : p->fRequiredGlo, 
                     Map_MappingGetAreaFlow(p), p->AreaBase, 0.0 );
 ABC_PRT( "Time", p->timeMatch );
 }
@@ -114,12 +112,12 @@ ABC_PRT( "Time", p->timeMatch );
         Map_MappingMatches( p );
         // compute the references and collect the nodes used in the mapping
         Map_MappingSetRefs( p );
-        p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
+        p->AreaFinal = Map_MappingGetArea( p );
 if ( p->fVerbose )
 {
 printf( "AreaFlow : %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
                     fShowSwitching? "Switch" : "Delay", 
-                    fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
+                    fShowSwitching? Map_MappingGetSwitching(p) : p->fRequiredGlo, 
                     Map_MappingGetAreaFlow(p), p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 ABC_PRT( "Time", Abc_Clock() - clk );
@@ -140,12 +138,12 @@ ABC_PRT( "Time", Abc_Clock() - clk );
         Map_MappingMatches( p );
         // compute the references and collect the nodes used in the mapping
         Map_MappingSetRefs( p );
-        p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
+        p->AreaFinal = Map_MappingGetArea( p );
 if ( p->fVerbose )
 {
 printf( "Area     : %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
                     fShowSwitching? "Switch" : "Delay", 
-                    fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
+                    fShowSwitching? Map_MappingGetSwitching(p) : p->fRequiredGlo, 
                     0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 ABC_PRT( "Time", Abc_Clock() - clk );
@@ -166,12 +164,12 @@ ABC_PRT( "Time", Abc_Clock() - clk );
         Map_MappingMatches( p );
         // compute the references and collect the nodes used in the mapping
         Map_MappingSetRefs( p );
-        p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
+        p->AreaFinal = Map_MappingGetArea( p );
 if ( p->fVerbose )
 {
 printf( "Area     : %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
                     fShowSwitching? "Switch" : "Delay", 
-                    fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
+                    fShowSwitching? Map_MappingGetSwitching(p) : p->fRequiredGlo, 
                     0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 ABC_PRT( "Time", Abc_Clock() - clk );
@@ -192,12 +190,12 @@ ABC_PRT( "Time", Abc_Clock() - clk );
         Map_MappingMatches( p );
         // compute the references and collect the nodes used in the mapping
         Map_MappingSetRefs( p );
-        p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
+        p->AreaFinal = Map_MappingGetArea( p );
 if ( p->fVerbose )
 {
 printf( "Switching: %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
                     fShowSwitching? "Switch" : "Delay", 
-                    fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
+                    fShowSwitching? Map_MappingGetSwitching(p) : p->fRequiredGlo, 
                     0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 ABC_PRT( "Time", Abc_Clock() - clk );
@@ -210,12 +208,12 @@ ABC_PRT( "Time", Abc_Clock() - clk );
         Map_MappingMatches( p );
         // compute the references and collect the nodes used in the mapping
         Map_MappingSetRefs( p );
-        p->AreaFinal = Map_MappingGetArea( p, p->vMapping );
+        p->AreaFinal = Map_MappingGetArea( p );
 if ( p->fVerbose )
 {
 printf( "Switching: %s = %8.2f  Flow = %11.1f  Area = %11.1f  %4.1f %%   ", 
                     fShowSwitching? "Switch" : "Delay", 
-                    fShowSwitching? Map_MappingGetSwitching(p,p->vMapping) : p->fRequiredGlo, 
+                    fShowSwitching? Map_MappingGetSwitching(p) : p->fRequiredGlo, 
                     0.0, p->AreaFinal, 
                     100.0*(p->AreaBase-p->AreaFinal)/p->AreaBase );
 ABC_PRT( "Time", Abc_Clock() - clk );
diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c
index baf21858..6914724c 100644
--- a/src/map/mapper/mapperCreate.c
+++ b/src/map/mapper/mapperCreate.c
@@ -27,7 +27,6 @@ ABC_NAMESPACE_IMPL_START
 
 static void            Map_TableCreate( Map_Man_t * p );
 static void            Map_TableResize( Map_Man_t * p );
-static Map_Node_t *    Map_TableLookup( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 );
 
 // hash key for the structural hash table
 static inline unsigned Map_HashKey2( Map_Node_t * p0, Map_Node_t * p1, int TableSize ) { return (unsigned)(((ABC_PTRUINT_T)(p0) + (ABC_PTRUINT_T)(p1) * 12582917) % TableSize); }
@@ -49,8 +48,11 @@ static inline unsigned Map_HashKey2( Map_Node_t * p0, Map_Node_t * p1, int Table
 ***********************************************************************/
 int             Map_ManReadInputNum( Map_Man_t * p )                    { return p->nInputs;    }
 int             Map_ManReadOutputNum( Map_Man_t * p )                   { return p->nOutputs;   }
+int             Map_ManReadBufNum( Map_Man_t * p )                      { return Map_NodeVecReadSize(p->vMapBufs);   }
 Map_Node_t **   Map_ManReadInputs ( Map_Man_t * p )                     { return p->pInputs;    }
 Map_Node_t **   Map_ManReadOutputs( Map_Man_t * p )                     { return p->pOutputs;   }
+Map_Node_t **   Map_ManReadBufs( Map_Man_t * p )                        { return Map_NodeVecReadArray(p->vMapBufs);  }
+Map_Node_t *    Map_ManReadBufDriver( Map_Man_t * p, int i )            { return Map_ManReadBufs(p)[i]->p1;           }
 Map_Node_t *    Map_ManReadConst1 ( Map_Man_t * p )                     { return p->pConst1;    }
 Map_Time_t *    Map_ManReadInputArrivals( Map_Man_t * p )               { return p->pInputArrivals; }
 Map_Time_t *    Map_ManReadOutputRequireds( Map_Man_t * p )             { return p->pOutputRequireds; }
@@ -109,7 +111,8 @@ void            Map_NodeSetSwitching( Map_Node_t * p, float Switching )     { p-
 ***********************************************************************/
 int             Map_NodeIsConst( Map_Node_t * p )    {  return (Map_Regular(p))->Num == -1;    }
 int             Map_NodeIsVar( Map_Node_t * p )      {  return (Map_Regular(p))->p1 == NULL && (Map_Regular(p))->Num >= 0; }
-int             Map_NodeIsAnd( Map_Node_t * p )      {  return (Map_Regular(p))->p1 != NULL;  }
+int             Map_NodeIsBuf( Map_Node_t * p )      {  return (Map_Regular(p))->p1 != NULL && (Map_Regular(p))->p2 == NULL;  }
+int             Map_NodeIsAnd( Map_Node_t * p )      {  return (Map_Regular(p))->p1 != NULL && (Map_Regular(p))->p2 != NULL;  }
 int             Map_NodeComparePhase( Map_Node_t * p1, Map_Node_t * p2 ) { assert( !Map_IsComplement(p1) ); assert( !Map_IsComplement(p2) ); return p1->fInv ^ p2->fInv; }
 
 /**Function*************************************************************
@@ -214,9 +217,8 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->nNodes = -1;
     // create the constant node
     p->pConst1    = Map_NodeCreate( p, NULL, NULL );
-    p->vNodesAll  = Map_NodeVecAlloc( 100 );
-    p->vNodesTemp = Map_NodeVecAlloc( 100 );
-    p->vMapping   = Map_NodeVecAlloc( 100 );
+    p->vMapObjs   = Map_NodeVecAlloc( 100 );
+    p->vMapBufs   = Map_NodeVecAlloc( 100 );
     p->vVisited   = Map_NodeVecAlloc( 100 );
 
     // create the PI nodes
@@ -246,19 +248,12 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
 void Map_ManFree( Map_Man_t * p )
 {
 //    int i;
-//    for ( i = 0; i < p->vNodesAll->nSize; i++ )
-//        Map_NodeVecFree( p->vNodesAll->pArray[i]->vFanouts );
+//    for ( i = 0; i < p->vMapObjs->nSize; i++ )
+//        Map_NodeVecFree( p->vMapObjs->pArray[i]->vFanouts );
 //    Map_NodeVecFree( p->pConst1->vFanouts );
-    if ( p->vAnds )    
-        Map_NodeVecFree( p->vAnds );
-    if ( p->vNodesAll )    
-        Map_NodeVecFree( p->vNodesAll );
-    if ( p->vNodesTemp )    
-        Map_NodeVecFree( p->vNodesTemp );
-    if ( p->vMapping )    
-        Map_NodeVecFree( p->vMapping );
-    if ( p->vVisited )    
-        Map_NodeVecFree( p->vVisited );
+    Map_NodeVecFree( p->vMapObjs );
+    Map_NodeVecFree( p->vMapBufs );
+    Map_NodeVecFree( p->vVisited );
     if ( p->uCanons )   ABC_FREE( p->uCanons );
     if ( p->uPhases )   ABC_FREE( p->uPhases );
     if ( p->pCounters ) ABC_FREE( p->pCounters );
@@ -291,10 +286,10 @@ void Map_ManCreateNodeDelays( Map_Man_t * p, int LogFan )
     Map_Node_t * pNode;
     int k;
     assert( p->pNodeDelays == NULL );
-    p->pNodeDelays = ABC_CALLOC( float, p->vNodesAll->nSize );
-    for ( k = 0; k < p->vNodesAll->nSize; k++ )
+    p->pNodeDelays = ABC_CALLOC( float, p->vMapObjs->nSize );
+    for ( k = 0; k < p->vMapObjs->nSize; k++ )
     {
-        pNode = p->vNodesAll->pArray[k];
+        pNode = p->vMapObjs->pArray[k];
         if ( pNode->nRefs == 0 )
             continue;
         p->pNodeDelays[k] = 0.014426 * LogFan * p->pSuperLib->tDelayInv.Worst * log( (double)pNode->nRefs ); // 1.4426 = 1/ln(2)
@@ -383,7 +378,7 @@ Map_Node_t * Map_NodeCreate( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 )
 //    pNode->vFanouts = Map_NodeVecAlloc( 5 );
     // store this node in the internal array
     if ( pNode->Num >= 0 )
-        Map_NodeVecPush( p->vNodesAll, pNode );
+        Map_NodeVecPush( p->vMapObjs, pNode );
     else
         pNode->fInv = 1;
     // set the level of this node
@@ -392,10 +387,20 @@ Map_Node_t * Map_NodeCreate( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 )
 #ifdef MAP_ALLOCATE_FANOUT
         // create the fanout info
         Map_NodeAddFaninFanout( Map_Regular(p1), pNode );
+        if ( p2 )
         Map_NodeAddFaninFanout( Map_Regular(p2), pNode );
 #endif
-        pNode->Level = 1 + MAP_MAX(Map_Regular(pNode->p1)->Level, Map_Regular(pNode->p2)->Level);
-        pNode->fInv  = Map_NodeIsSimComplement(p1) & Map_NodeIsSimComplement(p2);
+
+        if ( p2 )
+        {
+            pNode->Level = 1 + MAP_MAX(Map_Regular(pNode->p1)->Level, Map_Regular(pNode->p2)->Level);
+            pNode->fInv  = Map_NodeIsSimComplement(p1) & Map_NodeIsSimComplement(p2);
+        }
+        else
+        {
+            pNode->Level = Map_Regular(pNode->p1)->Level;
+            pNode->fInv  = Map_NodeIsSimComplement(p1);
+        }
     }
     // reference the inputs (will be used to compute the number of fanouts)
     if ( p1 ) Map_NodeRef(p1);
@@ -439,7 +444,7 @@ void Map_TableCreate( Map_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Map_Node_t * Map_TableLookup( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2 )
+Map_Node_t * Map_NodeAnd( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2 )
 {
     Map_Node_t * pEnt;
     unsigned Key;
@@ -544,70 +549,15 @@ clk = Abc_Clock();
   SeeAlso     []
 
 ***********************************************************************/
-Map_Node_t * Map_NodeAnd( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 )
-{
-    Map_Node_t * pNode;
-    pNode = Map_TableLookup( p, p1, p2 );    
-    return pNode;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Map_Node_t * Map_NodeOr( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 )
+Map_Node_t * Map_NodeBuf( Map_Man_t * p, Map_Node_t * p1 )
 {
-    Map_Node_t * pNode;
-    pNode = Map_Not( Map_TableLookup( p, Map_Not(p1), Map_Not(p2) ) ); 
+    Map_Node_t * pNode = Map_NodeCreate( p, p1, NULL );
+    Map_NodeVecPush( p->vMapBufs, pNode );
     return pNode;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Map_Node_t * Map_NodeExor( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 )
-{
-    return Map_NodeMux( p, p1, Map_Not(p2), p2 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Map_Node_t * Map_NodeMux( Map_Man_t * p, Map_Node_t * pC, Map_Node_t * pT, Map_Node_t * pE )
-{
-    Map_Node_t * pAnd1, * pAnd2, * pRes;
-    pAnd1 = Map_TableLookup( p, pC,          pT ); 
-    pAnd2 = Map_TableLookup( p, Map_Not(pC), pE ); 
-    pRes  = Map_NodeOr( p, pAnd1, pAnd2 );                 
-    return pRes;
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Sets the node to be equivalent to the given one.]
 
   Description [This procedure is a work-around for the equivalence check.
diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c
index 84580387..681625ac 100644
--- a/src/map/mapper/mapperCut.c
+++ b/src/map/mapper/mapperCut.c
@@ -88,6 +88,51 @@ static unsigned         Map_CutComputeTruth( Map_Man_t * p, Map_Cut_t * pCut, Ma
 
 /**Function*************************************************************
 
+  Synopsis    [Counts all the cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingCountAllCuts( Map_Man_t * pMan )
+{
+    Map_Node_t * pNode;
+    Map_Cut_t * pCut;
+    int i, nCuts;
+//    int nCuts55 = 0, nCuts5x = 0, nCuts4x = 0, nCuts3x = 0;
+//    int pCounts[7] = {0};
+    nCuts = 0;
+    for ( i = 0; i < pMan->nBins; i++ )
+        for ( pNode = pMan->pBins[i]; pNode; pNode = pNode->pNext )
+            for ( pCut = pNode->pCuts; pCut; pCut = pCut->pNext )
+                if ( pCut->nLeaves > 1 ) // skip the elementary cuts
+                {
+                    nCuts++;
+/*
+                    if ( Map_CutRegular(pCut->pOne)->nLeaves == 5 && Map_CutRegular(pCut->pTwo)->nLeaves == 5 )
+                        nCuts55++;
+                    if ( Map_CutRegular(pCut->pOne)->nLeaves == 5 || Map_CutRegular(pCut->pTwo)->nLeaves == 5 )
+                        nCuts5x++;
+                    else if ( Map_CutRegular(pCut->pOne)->nLeaves == 4 || Map_CutRegular(pCut->pTwo)->nLeaves == 4 )
+                        nCuts4x++;
+                    else if ( Map_CutRegular(pCut->pOne)->nLeaves == 3 || Map_CutRegular(pCut->pTwo)->nLeaves == 3 )
+                        nCuts3x++;
+*/                  
+//                    pCounts[ Map_CutRegular(pCut->pOne)->nLeaves ]++;
+//                    pCounts[ Map_CutRegular(pCut->pTwo)->nLeaves ]++;
+                }
+//    printf( "Total cuts = %6d. 55 = %6d. 5x = %6d. 4x = %6d. 3x = %6d.\n", nCuts, nCuts55, nCuts5x, nCuts4x, nCuts3x );
+
+//    printf( "Total cuts = %6d. 6= %6d. 5= %6d. 4= %6d. 3= %6d. 2= %6d. 1= %6d.\n", 
+//        nCuts, pCounts[6], pCounts[5], pCounts[4], pCounts[3], pCounts[2], pCounts[1] );
+    return nCuts;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the cuts for each node in the object graph.]
 
   Description [The cuts are computed in one sweep over the mapping graph. 
@@ -110,39 +155,44 @@ static unsigned         Map_CutComputeTruth( Map_Man_t * p, Map_Cut_t * pCut, Ma
   SeeAlso     []
 
 ***********************************************************************/
+void Map_MappingCutsInput( Map_Man_t * p, Map_Node_t * pNode )
+{
+    Map_Cut_t * pCut;
+    assert( Map_NodeIsVar(pNode) || Map_NodeIsBuf(pNode) );
+    pCut = Map_CutAlloc( p );
+    pCut->nLeaves = 1;
+    pCut->ppLeaves[0] = pNode;
+    pNode->pCuts   = pCut;
+    pNode->pCutBest[0] = NULL; // negative polarity is not mapped
+    pNode->pCutBest[1] = pCut; // positive polarity is a trivial cut
+    pCut->uTruth = 0xAAAAAAAA; // the first variable "1010"
+    pCut->M[0].AreaFlow = 0.0;
+    pCut->M[1].AreaFlow = 0.0;
+}
 void Map_MappingCuts( Map_Man_t * p )
 {
     ProgressBar * pProgress;
     Map_CutTable_t * pTable;
     Map_Node_t * pNode;
-    Map_Cut_t * pCut;
     int nCuts, nNodes, i;
     abctime clk = Abc_Clock();
     // set the elementary cuts for the PI variables
     assert( p->nVarsMax > 1 && p->nVarsMax < 7 );
     for ( i = 0; i < p->nInputs; i++ )
-    {
-        pCut = Map_CutAlloc( p );
-        pCut->nLeaves = 1;
-        pCut->ppLeaves[0] = p->pInputs[i];
-        p->pInputs[i]->pCuts   = pCut;
-        p->pInputs[i]->pCutBest[0] = NULL; // negative polarity is not mapped
-        p->pInputs[i]->pCutBest[1] = pCut; // positive polarity is a trivial cut
-        pCut->uTruth = 0xAAAAAAAA;         // the first variable "10101010"
-        pCut->M[0].AreaFlow = 0.0;
-        pCut->M[1].AreaFlow = 0.0;
-    }
+        Map_MappingCutsInput( p, p->pInputs[i] );
 
     // compute the cuts for the internal nodes
-    nNodes = p->vAnds->nSize;
+    nNodes = p->vMapObjs->nSize;
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
     pTable = Map_CutTableStart( p );
     for ( i = 0; i < nNodes; i++ )
     {
-        pNode = p->vAnds->pArray[i];
-        if ( !Map_NodeIsAnd( pNode ) )
-            continue;
-        Map_CutCompute( p, pTable, pNode );
+        pNode = p->vMapObjs->pArray[i];
+        if ( Map_NodeIsBuf(pNode) )
+            Map_MappingCutsInput( p, pNode );
+        else if ( Map_NodeIsAnd(pNode) )
+            Map_CutCompute( p, pTable, pNode );
+        else continue;
         Extra_ProgressBarUpdate( pProgress, i, "Cuts ..." );
     }
     Extra_ProgressBarStop( pProgress );
@@ -679,51 +729,6 @@ int Map_CutBelongsToList( Map_Cut_t * pList, Map_Node_t * ppNodes[], int nNodes
     return 0;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Counts all the cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Map_MappingCountAllCuts( Map_Man_t * pMan )
-{
-    Map_Node_t * pNode;
-    Map_Cut_t * pCut;
-    int i, nCuts;
-//    int nCuts55 = 0, nCuts5x = 0, nCuts4x = 0, nCuts3x = 0;
-//    int pCounts[7] = {0};
-    nCuts = 0;
-    for ( i = 0; i < pMan->nBins; i++ )
-        for ( pNode = pMan->pBins[i]; pNode; pNode = pNode->pNext )
-            for ( pCut = pNode->pCuts; pCut; pCut = pCut->pNext )
-                if ( pCut->nLeaves > 1 ) // skip the elementary cuts
-                {
-                    nCuts++;
-/*
-                    if ( Map_CutRegular(pCut->pOne)->nLeaves == 5 && Map_CutRegular(pCut->pTwo)->nLeaves == 5 )
-                        nCuts55++;
-                    if ( Map_CutRegular(pCut->pOne)->nLeaves == 5 || Map_CutRegular(pCut->pTwo)->nLeaves == 5 )
-                        nCuts5x++;
-                    else if ( Map_CutRegular(pCut->pOne)->nLeaves == 4 || Map_CutRegular(pCut->pTwo)->nLeaves == 4 )
-                        nCuts4x++;
-                    else if ( Map_CutRegular(pCut->pOne)->nLeaves == 3 || Map_CutRegular(pCut->pTwo)->nLeaves == 3 )
-                        nCuts3x++;
-*/                  
-//                    pCounts[ Map_CutRegular(pCut->pOne)->nLeaves ]++;
-//                    pCounts[ Map_CutRegular(pCut->pTwo)->nLeaves ]++;
-                }
-//    printf( "Total cuts = %6d. 55 = %6d. 5x = %6d. 4x = %6d. 3x = %6d.\n", nCuts, nCuts55, nCuts5x, nCuts4x, nCuts3x );
-
-//    printf( "Total cuts = %6d. 6= %6d. 5= %6d. 4= %6d. 3= %6d. 2= %6d. 1= %6d.\n", 
-//        nCuts, pCounts[6], pCounts[5], pCounts[4], pCounts[3], pCounts[2], pCounts[1] );
-    return nCuts;
-}
-
 
 /**Function*************************************************************
 
diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h
index e6dbab97..cd6ac81c 100644
--- a/src/map/mapper/mapperInt.h
+++ b/src/map/mapper/mapperInt.h
@@ -98,10 +98,8 @@ struct Map_ManStruct_t_
     int                 nOutputs;      // the number of outputs
     int                 nNodes;        // the total number of nodes
     Map_Node_t *        pConst1;       // the constant 1 node
-    Map_NodeVec_t *     vAnds;         // the array of nodes in the DFS order
-    Map_NodeVec_t *     vNodesAll;     // the array of all nodes
-    Map_NodeVec_t *     vNodesTemp;    // the array of all nodes
-    Map_NodeVec_t *     vMapping;      // the array of internal nodes used in the mapping
+    Map_NodeVec_t *     vMapObjs;      // the array of all nodes
+    Map_NodeVec_t *     vMapBufs;      // the array of all nodes
     float *             pNodeDelays;   // the array of node delays
 
     // info about the original circuit
@@ -358,10 +356,6 @@ struct Map_HashEntryStruct_t_
 /*=== mapperCanon.c =============================================================*/
 /*=== mapperCut.c ===============================================================*/
 extern void              Map_MappingCuts( Map_Man_t * p );
-extern int               Map_MappingCountAllCuts( Map_Man_t * p );
-/*=== mapperCutDcs.c ===============================================================*/
-extern void              Map_ComputeDcs( Map_Man_t * p );
-extern unsigned          Map_ComputeIsop_rec( Map_Man_t * p, unsigned uF, unsigned uFD, int iVar, int nVars, int fDir );
 /*=== mapperCutUtils.c ===============================================================*/
 extern Map_Cut_t *       Map_CutAlloc( Map_Man_t * p );
 extern void              Map_CutFree( Map_Man_t * p, Map_Cut_t * pCut );
@@ -383,17 +377,7 @@ extern Map_SuperLib_t *  Map_SuperLibCreate( Mio_Library_t * pGenlib, Vec_Str_t
 extern void              Map_SuperLibFree( Map_SuperLib_t * p );
 /*=== mapperMatch.c ===============================================================*/
 extern int               Map_MappingMatches( Map_Man_t * p );
-extern float             Map_MappingCombinePhases( Map_Man_t * p );
-extern void              Map_MatchClean( Map_Match_t * pMatch );
-extern int               Map_MatchCompare( Map_Man_t * pMan, Map_Match_t * pM1, Map_Match_t * pM2, int fDoingArea );
-/*=== mapperPower.c =============================================================*/
-extern float             Map_SwitchCutGetDerefed( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase );
-extern float             Map_SwitchCutRef( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase );
-extern float             Map_SwitchCutDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase );
-extern float             Map_MappingGetSwitching( Map_Man_t * pMan, Map_NodeVec_t * vMapping );
 /*=== mapperRefs.c =============================================================*/
-extern int               Map_NodeReadRefPhaseAct( Map_Node_t * pNode, int fPhase );
-extern float             Map_NodeReadRefPhaseEst( Map_Node_t * pNode, int fPhase );
 extern void              Map_MappingEstimateRefsInit( Map_Man_t * p );
 extern void              Map_MappingEstimateRefs( Map_Man_t * p );
 extern float             Map_CutGetAreaFlow( Map_Cut_t * pCut, int fPhase );
@@ -402,9 +386,12 @@ extern float             Map_CutGetAreaDerefed( Map_Cut_t * pCut, int fPhase );
 extern float             Map_CutRef( Map_Cut_t * pCut, int fPhase );
 extern float             Map_CutDeref( Map_Cut_t * pCut, int fPhase );
 extern void              Map_MappingSetRefs( Map_Man_t * pMan );
-extern float             Map_MappingGetArea( Map_Man_t * pMan, Map_NodeVec_t * vMapping );
-/*=== mapperShow.c =============================================================*/
-extern void              Map_MappingShow( Map_Man_t * pMan, char * pFileName );
+extern float             Map_MappingGetArea( Map_Man_t * pMan );
+/*=== mapperSwitch.c =============================================================*/
+extern float             Map_SwitchCutGetDerefed( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase );
+extern float             Map_SwitchCutRef( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase );
+extern float             Map_SwitchCutDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase );
+extern float             Map_MappingGetSwitching( Map_Man_t * pMan );
 /*=== mapperTree.c ===============================================================*/
 extern int               Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st__table * tExcludeGate );
 extern int               Map_LibraryReadFileTreeStr( Map_SuperLib_t * pLib, Mio_Library_t * pGenlib, Vec_Str_t * vStr, char * pFileName );
@@ -423,13 +410,8 @@ extern void              Map_SuperTableSortSupergates( Map_HashTable_t * p, int
 extern void              Map_SuperTableSortSupergatesByDelay( Map_HashTable_t * p, int nSupersMax );
 /*=== mapperTime.c =============================================================*/
 extern float             Map_TimeCutComputeArrival( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, float tWorstCaseLimit );
-extern void              Map_TimeCutComputeArrival_rec( Map_Cut_t * pCut, int fPhase );
 extern float             Map_TimeComputeArrivalMax( Map_Man_t * p );
 extern void              Map_TimeComputeRequiredGlobal( Map_Man_t * p );
-extern void              Map_TimeComputeRequired( Map_Man_t * p, float fRequired );
-extern float             Map_TimeNodeFanoutDelay( Map_Node_t * pNode, int fPhase );
-extern float             Map_TimeCutFanoutDelay( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase );
-extern float             Map_TimeMatchWithInverter( Map_Man_t * p, Map_Match_t * pMatch );
 /*=== mapperTruth.c ===============================================================*/
 extern void              Map_MappingTruths( Map_Man_t * pMan );
 extern int               Map_TruthsCutDontCare( Map_Man_t * pMan, Map_Cut_t * pCut, unsigned * uTruthDc );
@@ -437,11 +419,6 @@ extern int               Map_TruthCountOnes( unsigned * uTruth, int nLeaves );
 extern int               Map_TruthDetectTwoFirst( unsigned * uTruth, int nLeaves );
 /*=== mapperUtils.c ===============================================================*/
 extern Map_NodeVec_t *   Map_MappingDfs( Map_Man_t * pMan, int fCollectEquiv );
-extern Map_NodeVec_t *   Map_MappingDfsNodes( Map_Man_t * pMan, Map_Node_t ** ppNodes, int nNodes, int fEquiv );
-
-extern void              Map_MappingDfsMarked1_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, int fFirst );
-extern void              Map_MappingDfsMarked2_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, Map_NodeVec_t * vBoundary, int fFirst );
-
 extern int               Map_MappingCountLevels( Map_Man_t * pMan );
 extern void              Map_MappingUnmark( Map_Man_t * pMan );
 extern void              Map_MappingMark_rec( Map_Node_t * pNode );
@@ -464,6 +441,7 @@ extern void              Map_MappingReportChoices( Map_Man_t * pMan );
 /*=== mapperVec.c =============================================================*/
 extern Map_NodeVec_t *   Map_NodeVecAlloc( int nCap );
 extern void              Map_NodeVecFree( Map_NodeVec_t * p );
+extern Map_NodeVec_t *   Map_NodeVecDup( Map_NodeVec_t * p );
 extern Map_Node_t **     Map_NodeVecReadArray( Map_NodeVec_t * p );
 extern int               Map_NodeVecReadSize( Map_NodeVec_t * p );
 extern void              Map_NodeVecGrow( Map_NodeVec_t * p, int nCapMin );
diff --git a/src/map/mapper/mapperMatch.c b/src/map/mapper/mapperMatch.c
index ad559d6a..aa0d97a3 100644
--- a/src/map/mapper/mapperMatch.c
+++ b/src/map/mapper/mapperMatch.c
@@ -36,217 +36,93 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int  Map_MatchNodePhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase );
-static int  Map_MatchNodeCut( Map_Man_t * p, Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, float fWorstLimit );
-
-static void Map_MappingSetPiArrivalTimes( Map_Man_t * p );
-static void Map_NodeTryDroppingOnePhase( Map_Man_t * p, Map_Node_t * pNode );
-static void Map_NodeTransferArrivalTimes( Map_Man_t * p, Map_Node_t * pNode );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the best matches of the nodes.]
+  Synopsis    [Cleans the match.]
 
-  Description [Uses parameter p->fMappingMode to decide how to assign
-  the matches for both polarities of the node. While the matches are 
-  being assigned, one of them may turn out to be better than the other 
-  (in terms of delay, for example). In this case, the worse match can 
-  be permanently dropped, and the corresponding pointer set to NULL.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Map_MappingMatches( Map_Man_t * p )
+void Map_MatchClean( Map_Match_t * pMatch )
 {
-    ProgressBar * pProgress;
-    Map_Node_t * pNode;
-    int i;
-
-    assert( p->fMappingMode >= 0 && p->fMappingMode <= 4 );
-
-    // use the externally given PI arrival times
-    if ( p->fMappingMode == 0 )
-        Map_MappingSetPiArrivalTimes( p );
-
-    // estimate the fanouts
-    if ( p->fMappingMode == 0 )
-        Map_MappingEstimateRefsInit( p );
-    else if ( p->fMappingMode == 1 )
-        Map_MappingEstimateRefs( p );
-
-    // the PI cuts are matched in the cut computation package
-    // in the loop below we match the internal nodes
-    pProgress = Extra_ProgressBarStart( stdout, p->vAnds->nSize );
-    for ( i = 0; i < p->vAnds->nSize; i++ )
-    {
-        // skip primary inputs and secondary nodes if mapping with choices
-        pNode = p->vAnds->pArray[i];
-        if ( !Map_NodeIsAnd( pNode ) || pNode->pRepr )
-            continue;
-
-        // make sure that at least one non-trival cut is present
-        if ( pNode->pCuts->pNext == NULL )
-        {
-            Extra_ProgressBarStop( pProgress );
-            printf( "\nError: A node in the mapping graph does not have feasible cuts.\n" );
-            return 0;
-        }
-
-        // match negative phase
-        if ( !Map_MatchNodePhase( p, pNode, 0 ) )
-        {
-            Extra_ProgressBarStop( pProgress );
-            return 0;
-        }
-        // match positive phase
-        if ( !Map_MatchNodePhase( p, pNode, 1 ) )
-        {
-            Extra_ProgressBarStop( pProgress );
-            return 0;
-        }
-
-        // make sure that at least one phase is mapped
-        if ( pNode->pCutBest[0] == NULL && pNode->pCutBest[1] == NULL )
-        {
-            printf( "\nError: Could not match both phases of AIG node %d.\n", pNode->Num );
-            printf( "Please make sure that the supergate library has equivalents of AND2 or NAND2.\n" );
-            printf( "If such supergates exist in the library, report a bug.\n" );
-            Extra_ProgressBarStop( pProgress );
-            return 0;
-        }
-
-        // if both phases are assigned, check if one of them can be dropped
-        Map_NodeTryDroppingOnePhase( p, pNode );
-        // set the arrival times of the node using the best cuts
-        Map_NodeTransferArrivalTimes( p, pNode );
-
-        // update the progress bar
-        Extra_ProgressBarUpdate( pProgress, i, "Matches ..." );
-    }
-    Extra_ProgressBarStop( pProgress );
-    return 1;
+    memset( pMatch, 0, sizeof(Map_Match_t) );
+    pMatch->AreaFlow          = MAP_FLOAT_LARGE; // unassigned
+    pMatch->tArrive.Rise   = MAP_FLOAT_LARGE; // unassigned
+    pMatch->tArrive.Fall   = MAP_FLOAT_LARGE; // unassigned
+    pMatch->tArrive.Worst  = MAP_FLOAT_LARGE; // unassigned
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Find the matching of one polarity of the node.]
+  Synopsis    [Compares two matches.]
 
-  Description []
+  Description [Returns 1 if the second match is better. Otherwise returns 0.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Map_MatchNodePhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase )
+int Map_MatchCompare( Map_Man_t * pMan, Map_Match_t * pM1, Map_Match_t * pM2, int fDoingArea )
 {
-    Map_Match_t MatchBest, * pMatch;
-    Map_Cut_t * pCut, * pCutBest;
-    float Area1 = 0.0; // Suppress "might be used uninitialized
-    float Area2, fWorstLimit;
-
-    // skip the cuts that have been unassigned during area recovery
-    pCutBest = pNode->pCutBest[fPhase];
-    if ( p->fMappingMode != 0 && pCutBest == NULL )
-        return 1;
-
-    // recompute the arrival times of the current best match 
-    // because the arrival times of the fanins may have changed 
-    // as a result of remapping fanins in the topological order
-    if ( p->fMappingMode != 0 )
-    {
-        Map_TimeCutComputeArrival( pNode, pCutBest, fPhase, MAP_FLOAT_LARGE );
-        // make sure that the required times are met
-        assert( pCutBest->M[fPhase].tArrive.Rise < pNode->tRequired[fPhase].Rise + p->fEpsilon );
-        assert( pCutBest->M[fPhase].tArrive.Fall < pNode->tRequired[fPhase].Fall + p->fEpsilon );
-    }
-
-    // recompute the exact area of the current best match
-    // because the exact area of the fanins may have changed
-    // as a result of remapping fanins in the topological order
-    if ( p->fMappingMode == 2 || p->fMappingMode == 3 )
-    {
-        pMatch = pCutBest->M + fPhase;
-        if ( pNode->nRefAct[fPhase] > 0 || 
-            (pNode->pCutBest[!fPhase] == NULL && pNode->nRefAct[!fPhase] > 0) )
-            pMatch->AreaFlow = Area1 = Map_CutDeref( pCutBest, fPhase );
-        else
-            pMatch->AreaFlow = Area1 = Map_CutGetAreaDerefed( pCutBest, fPhase );
-    }
-    else if ( p->fMappingMode == 4 )
+    if ( !fDoingArea )
     {
-        pMatch = pCutBest->M + fPhase;
-        if ( pNode->nRefAct[fPhase] > 0 || 
-            (pNode->pCutBest[!fPhase] == NULL && pNode->nRefAct[!fPhase] > 0) )
-            pMatch->AreaFlow = Area1 = Map_SwitchCutDeref( pNode, pCutBest, fPhase );
-        else
-            pMatch->AreaFlow = Area1 = Map_SwitchCutGetDerefed( pNode, pCutBest, fPhase );
+        // compare the arrival times
+        if ( pM1->tArrive.Worst < pM2->tArrive.Worst - pMan->fEpsilon )
+            return 0;
+        if ( pM1->tArrive.Worst > pM2->tArrive.Worst + pMan->fEpsilon )
+            return 1;
+        // compare the areas or area flows
+        if ( pM1->AreaFlow < pM2->AreaFlow - pMan->fEpsilon )
+            return 0;
+        if ( pM1->AreaFlow > pM2->AreaFlow + pMan->fEpsilon )
+            return 1;
+        // compare the fanout limits
+        if ( pM1->pSuperBest->nFanLimit > pM2->pSuperBest->nFanLimit )
+            return 0;
+        if ( pM1->pSuperBest->nFanLimit < pM2->pSuperBest->nFanLimit )
+            return 1;
+        // compare the number of leaves
+        if ( pM1->pSuperBest->nFanins < pM2->pSuperBest->nFanins )
+            return 0;
+        if ( pM1->pSuperBest->nFanins > pM2->pSuperBest->nFanins )
+            return 1;
+        // otherwise prefer the old cut
+        return 0;
     }
-
-    // save the old mapping
-    if ( pCutBest )
-        MatchBest = pCutBest->M[fPhase];
     else
-        Map_MatchClean( &MatchBest );
- 
-    // select the new best cut
-    fWorstLimit = pNode->tRequired[fPhase].Worst;
-    for ( pCut = pNode->pCuts->pNext; pCut; pCut = pCut->pNext )
-    {
-        // limit gate sizes based on fanout count
-        if ( (pNode->nRefs > 3 && pCut->nLeaves > 2) || (pNode->nRefs > 1 && pCut->nLeaves > 3) )
-            continue;
-        pMatch = pCut->M + fPhase;
-        if ( pMatch->pSupers == NULL )
-            continue;
-
-        // find the matches for the cut
-        Map_MatchNodeCut( p, pNode, pCut, fPhase, fWorstLimit );
-        if ( pMatch->pSuperBest == NULL || pMatch->tArrive.Worst > fWorstLimit + p->fEpsilon )
-            continue;
-
-        // if the cut can be matched compare the matchings
-        if ( Map_MatchCompare( p, &MatchBest, pMatch, p->fMappingMode ) )
-        {
-            pCutBest  =  pCut;
-            MatchBest = *pMatch;
-            // if we are mapping for delay, the worst-case limit should be tightened
-            if ( p->fMappingMode == 0 )
-                fWorstLimit = MatchBest.tArrive.Worst;
-        }
-    }
-
-    if ( pCutBest == NULL )
-        return 1;
-
-    // set the new mapping
-    pNode->pCutBest[fPhase] = pCutBest;
-    pCutBest->M[fPhase]     = MatchBest;
-
-    // reference the new cut if it used
-    if ( p->fMappingMode >= 2 && 
-         (pNode->nRefAct[fPhase] > 0 || 
-         (pNode->pCutBest[!fPhase] == NULL && pNode->nRefAct[!fPhase] > 0)) )
     {
-        if ( p->fMappingMode == 2 || p->fMappingMode == 3 )
-            Area2 = Map_CutRef( pNode->pCutBest[fPhase], fPhase );
-        else if ( p->fMappingMode == 4 )
-            Area2 = Map_SwitchCutRef( pNode, pNode->pCutBest[fPhase], fPhase );
-        else 
-            assert( 0 );
-//        assert( Area2 < Area1 + p->fEpsilon );
+        // compare the areas or area flows
+        if ( pM1->AreaFlow < pM2->AreaFlow - pMan->fEpsilon )
+            return 0;
+        if ( pM1->AreaFlow > pM2->AreaFlow + pMan->fEpsilon )
+            return 1;
+        // compare the arrival times
+        if ( pM1->tArrive.Worst < pM2->tArrive.Worst - pMan->fEpsilon )
+            return 0;
+        if ( pM1->tArrive.Worst > pM2->tArrive.Worst + pMan->fEpsilon )
+            return 1;
+        // compare the fanout limits
+        if ( pM1->pSuperBest->nFanLimit > pM2->pSuperBest->nFanLimit )
+            return 0;
+        if ( pM1->pSuperBest->nFanLimit < pM2->pSuperBest->nFanLimit )
+            return 1;
+        // compare the number of leaves
+        if ( pM1->pSuperBest->nFanins < pM2->pSuperBest->nFanins )
+            return 0;
+        if ( pM1->pSuperBest->nFanins > pM2->pSuperBest->nFanins )
+            return 1;
+        // otherwise prefer the old cut
+        return 0;
     }
-
-    // make sure that the requited times are met
-    assert( MatchBest.tArrive.Rise < pNode->tRequired[fPhase].Rise + p->fEpsilon );
-    assert( MatchBest.tArrive.Fall < pNode->tRequired[fPhase].Fall + p->fEpsilon );
-    return 1;
 }
 
 /**Function*************************************************************
@@ -347,7 +223,7 @@ int Map_MatchNodeCut( Map_Man_t * p, Map_Node_t * pNode, Map_Cut_t * pCut, int f
 
 /**Function*************************************************************
 
-  Synopsis    [Cleans the match.]
+  Synopsis    [Find the matching of one polarity of the node.]
 
   Description []
                
@@ -356,78 +232,109 @@ int Map_MatchNodeCut( Map_Man_t * p, Map_Node_t * pNode, Map_Cut_t * pCut, int f
   SeeAlso     []
 
 ***********************************************************************/
-void Map_MatchClean( Map_Match_t * pMatch )
+int Map_MatchNodePhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase )
 {
-    memset( pMatch, 0, sizeof(Map_Match_t) );
-    pMatch->AreaFlow          = MAP_FLOAT_LARGE; // unassigned
-    pMatch->tArrive.Rise   = MAP_FLOAT_LARGE; // unassigned
-    pMatch->tArrive.Fall   = MAP_FLOAT_LARGE; // unassigned
-    pMatch->tArrive.Worst  = MAP_FLOAT_LARGE; // unassigned
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares two matches.]
+    Map_Match_t MatchBest, * pMatch;
+    Map_Cut_t * pCut, * pCutBest;
+    float Area1 = 0.0; // Suppress "might be used uninitialized
+    float Area2, fWorstLimit;
 
-  Description [Returns 1 if the second match is better. Otherwise returns 0.]
-               
-  SideEffects []
+    // skip the cuts that have been unassigned during area recovery
+    pCutBest = pNode->pCutBest[fPhase];
+    if ( p->fMappingMode != 0 && pCutBest == NULL )
+        return 1;
 
-  SeeAlso     []
+    // recompute the arrival times of the current best match 
+    // because the arrival times of the fanins may have changed 
+    // as a result of remapping fanins in the topological order
+    if ( p->fMappingMode != 0 )
+    {
+        Map_TimeCutComputeArrival( pNode, pCutBest, fPhase, MAP_FLOAT_LARGE );
+        // make sure that the required times are met
+        assert( pCutBest->M[fPhase].tArrive.Rise < pNode->tRequired[fPhase].Rise + p->fEpsilon );
+        assert( pCutBest->M[fPhase].tArrive.Fall < pNode->tRequired[fPhase].Fall + p->fEpsilon );
+    }
 
-***********************************************************************/
-int Map_MatchCompare( Map_Man_t * pMan, Map_Match_t * pM1, Map_Match_t * pM2, int fDoingArea )
-{
-    if ( !fDoingArea )
+    // recompute the exact area of the current best match
+    // because the exact area of the fanins may have changed
+    // as a result of remapping fanins in the topological order
+    if ( p->fMappingMode == 2 || p->fMappingMode == 3 )
     {
-        // compare the arrival times
-        if ( pM1->tArrive.Worst < pM2->tArrive.Worst - pMan->fEpsilon )
-            return 0;
-        if ( pM1->tArrive.Worst > pM2->tArrive.Worst + pMan->fEpsilon )
-            return 1;
-        // compare the areas or area flows
-        if ( pM1->AreaFlow < pM2->AreaFlow - pMan->fEpsilon )
-            return 0;
-        if ( pM1->AreaFlow > pM2->AreaFlow + pMan->fEpsilon )
-            return 1;
-        // compare the fanout limits
-        if ( pM1->pSuperBest->nFanLimit > pM2->pSuperBest->nFanLimit )
-            return 0;
-        if ( pM1->pSuperBest->nFanLimit < pM2->pSuperBest->nFanLimit )
-            return 1;
-        // compare the number of leaves
-        if ( pM1->pSuperBest->nFanins < pM2->pSuperBest->nFanins )
-            return 0;
-        if ( pM1->pSuperBest->nFanins > pM2->pSuperBest->nFanins )
-            return 1;
-        // otherwise prefer the old cut
-        return 0;
+        pMatch = pCutBest->M + fPhase;
+        if ( pNode->nRefAct[fPhase] > 0 || 
+            (pNode->pCutBest[!fPhase] == NULL && pNode->nRefAct[!fPhase] > 0) )
+            pMatch->AreaFlow = Area1 = Map_CutDeref( pCutBest, fPhase );
+        else
+            pMatch->AreaFlow = Area1 = Map_CutGetAreaDerefed( pCutBest, fPhase );
     }
+    else if ( p->fMappingMode == 4 )
+    {
+        pMatch = pCutBest->M + fPhase;
+        if ( pNode->nRefAct[fPhase] > 0 || 
+            (pNode->pCutBest[!fPhase] == NULL && pNode->nRefAct[!fPhase] > 0) )
+            pMatch->AreaFlow = Area1 = Map_SwitchCutDeref( pNode, pCutBest, fPhase );
+        else
+            pMatch->AreaFlow = Area1 = Map_SwitchCutGetDerefed( pNode, pCutBest, fPhase );
+    }
+
+    // save the old mapping
+    if ( pCutBest )
+        MatchBest = pCutBest->M[fPhase];
     else
+        Map_MatchClean( &MatchBest );
+ 
+    // select the new best cut
+    fWorstLimit = pNode->tRequired[fPhase].Worst;
+    for ( pCut = pNode->pCuts->pNext; pCut; pCut = pCut->pNext )
     {
-        // compare the areas or area flows
-        if ( pM1->AreaFlow < pM2->AreaFlow - pMan->fEpsilon )
-            return 0;
-        if ( pM1->AreaFlow > pM2->AreaFlow + pMan->fEpsilon )
-            return 1;
-        // compare the arrival times
-        if ( pM1->tArrive.Worst < pM2->tArrive.Worst - pMan->fEpsilon )
-            return 0;
-        if ( pM1->tArrive.Worst > pM2->tArrive.Worst + pMan->fEpsilon )
-            return 1;
-        // compare the fanout limits
-        if ( pM1->pSuperBest->nFanLimit > pM2->pSuperBest->nFanLimit )
-            return 0;
-        if ( pM1->pSuperBest->nFanLimit < pM2->pSuperBest->nFanLimit )
-            return 1;
-        // compare the number of leaves
-        if ( pM1->pSuperBest->nFanins < pM2->pSuperBest->nFanins )
-            return 0;
-        if ( pM1->pSuperBest->nFanins > pM2->pSuperBest->nFanins )
-            return 1;
-        // otherwise prefer the old cut
-        return 0;
+        // limit gate sizes based on fanout count
+        if ( (pNode->nRefs > 3 && pCut->nLeaves > 2) || (pNode->nRefs > 1 && pCut->nLeaves > 3) )
+            continue;
+        pMatch = pCut->M + fPhase;
+        if ( pMatch->pSupers == NULL )
+            continue;
+
+        // find the matches for the cut
+        Map_MatchNodeCut( p, pNode, pCut, fPhase, fWorstLimit );
+        if ( pMatch->pSuperBest == NULL || pMatch->tArrive.Worst > fWorstLimit + p->fEpsilon )
+            continue;
+
+        // if the cut can be matched compare the matchings
+        if ( Map_MatchCompare( p, &MatchBest, pMatch, p->fMappingMode ) )
+        {
+            pCutBest  =  pCut;
+            MatchBest = *pMatch;
+            // if we are mapping for delay, the worst-case limit should be tightened
+            if ( p->fMappingMode == 0 )
+                fWorstLimit = MatchBest.tArrive.Worst;
+        }
     }
+
+    if ( pCutBest == NULL )
+        return 1;
+
+    // set the new mapping
+    pNode->pCutBest[fPhase] = pCutBest;
+    pCutBest->M[fPhase]     = MatchBest;
+
+    // reference the new cut if it used
+    if ( p->fMappingMode >= 2 && 
+         (pNode->nRefAct[fPhase] > 0 || 
+         (pNode->pCutBest[!fPhase] == NULL && pNode->nRefAct[!fPhase] > 0)) )
+    {
+        if ( p->fMappingMode == 2 || p->fMappingMode == 3 )
+            Area2 = Map_CutRef( pNode->pCutBest[fPhase], fPhase );
+        else if ( p->fMappingMode == 4 )
+            Area2 = Map_SwitchCutRef( pNode, pNode->pCutBest[fPhase], fPhase );
+        else 
+            assert( 0 );
+//        assert( Area2 < Area1 + p->fEpsilon );
+    }
+
+    // make sure that the requited times are met
+    assert( MatchBest.tArrive.Rise < pNode->tRequired[fPhase].Rise + p->fEpsilon );
+    assert( MatchBest.tArrive.Fall < pNode->tRequired[fPhase].Fall + p->fEpsilon );
+    return 1;
 }
 
 /**Function*************************************************************
@@ -460,6 +367,25 @@ void Map_MappingSetPiArrivalTimes( Map_Man_t * p )
     }
 }
 
+/**function*************************************************************
+
+  synopsis    [Computes the exact area associated with the cut.]
+
+  description []
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+float Map_TimeMatchWithInverter( Map_Man_t * p, Map_Match_t * pMatch )
+{
+    Map_Time_t tArrInv;
+    tArrInv.Fall  = pMatch->tArrive.Rise + p->pSuperLib->tDelayInv.Fall;
+    tArrInv.Rise  = pMatch->tArrive.Fall + p->pSuperLib->tDelayInv.Rise;
+    tArrInv.Worst = MAP_MAX( tArrInv.Rise, tArrInv.Fall ); 
+    return tArrInv.Worst;
+}
 
 /**Function*************************************************************
 
@@ -609,6 +535,100 @@ void Map_NodeTransferArrivalTimes( Map_Man_t * p, Map_Node_t * pNode )
     assert( pNode->tArrival[1].Fall < pNode->tRequired[1].Fall + p->fEpsilon );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the best matches of the nodes.]
+
+  Description [Uses parameter p->fMappingMode to decide how to assign
+  the matches for both polarities of the node. While the matches are 
+  being assigned, one of them may turn out to be better than the other 
+  (in terms of delay, for example). In this case, the worse match can 
+  be permanently dropped, and the corresponding pointer set to NULL.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_MappingMatches( Map_Man_t * p )
+{
+    ProgressBar * pProgress;
+    Map_Node_t * pNode;
+    int i;
+
+    assert( p->fMappingMode >= 0 && p->fMappingMode <= 4 );
+
+    // use the externally given PI arrival times
+    if ( p->fMappingMode == 0 )
+        Map_MappingSetPiArrivalTimes( p );
+
+    // estimate the fanouts
+    if ( p->fMappingMode == 0 )
+        Map_MappingEstimateRefsInit( p );
+    else if ( p->fMappingMode == 1 )
+        Map_MappingEstimateRefs( p );
+
+    // the PI cuts are matched in the cut computation package
+    // in the loop below we match the internal nodes
+    pProgress = Extra_ProgressBarStart( stdout, p->vMapObjs->nSize );
+    for ( i = 0; i < p->vMapObjs->nSize; i++ )
+    {
+        pNode = p->vMapObjs->pArray[i];
+        if ( Map_NodeIsBuf(pNode) )
+        {
+            assert( pNode->p2 == NULL );
+            pNode->tArrival[0] = Map_Regular(pNode->p1)->tArrival[ Map_IsComplement(pNode->p1)];
+            pNode->tArrival[1] = Map_Regular(pNode->p1)->tArrival[!Map_IsComplement(pNode->p1)];
+            continue;
+        }
+
+        // skip primary inputs and secondary nodes if mapping with choices
+        if ( !Map_NodeIsAnd( pNode ) || pNode->pRepr )
+            continue;
+
+        // make sure that at least one non-trival cut is present
+        if ( pNode->pCuts->pNext == NULL )
+        {
+            Extra_ProgressBarStop( pProgress );
+            printf( "\nError: A node in the mapping graph does not have feasible cuts.\n" );
+            return 0;
+        }
+
+        // match negative phase
+        if ( !Map_MatchNodePhase( p, pNode, 0 ) )
+        {
+            Extra_ProgressBarStop( pProgress );
+            return 0;
+        }
+        // match positive phase
+        if ( !Map_MatchNodePhase( p, pNode, 1 ) )
+        {
+            Extra_ProgressBarStop( pProgress );
+            return 0;
+        }
+
+        // make sure that at least one phase is mapped
+        if ( pNode->pCutBest[0] == NULL && pNode->pCutBest[1] == NULL )
+        {
+            printf( "\nError: Could not match both phases of AIG node %d.\n", pNode->Num );
+            printf( "Please make sure that the supergate library has equivalents of AND2 or NAND2.\n" );
+            printf( "If such supergates exist in the library, report a bug.\n" );
+            Extra_ProgressBarStop( pProgress );
+            return 0;
+        }
+
+        // if both phases are assigned, check if one of them can be dropped
+        Map_NodeTryDroppingOnePhase( p, pNode );
+        // set the arrival times of the node using the best cuts
+        Map_NodeTransferArrivalTimes( p, pNode );
+
+        // update the progress bar
+        Extra_ProgressBarUpdate( pProgress, i, "Matches ..." );
+    }
+    Extra_ProgressBarStop( pProgress );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mapper/mapperRefs.c b/src/map/mapper/mapperRefs.c
index 9b0be068..6d6ff121 100644
--- a/src/map/mapper/mapperRefs.c
+++ b/src/map/mapper/mapperRefs.c
@@ -25,11 +25,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int   Map_NodeIncRefPhaseAct( Map_Node_t * pNode, int fPhase );
-static int   Map_NodeDecRefPhaseAct( Map_Node_t * pNode, int fPhase );
-static float Map_CutRefDeref( Map_Cut_t * pCut, int fPhase, int fReference );
-static void  Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode, Map_Node_t ** ppStore );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -132,9 +127,9 @@ void Map_MappingEstimateRefsInit( Map_Man_t * p )
 {
     Map_Node_t * pNode;
     int i;
-    for ( i = 0; i < p->vAnds->nSize; i++ )
+    for ( i = 0; i < p->vMapObjs->nSize; i++ )
     {
-        pNode = p->vAnds->pArray[i];
+        pNode = p->vMapObjs->pArray[i];
 //        pNode->nRefEst[0] = pNode->nRefEst[1] = ((float)pNode->nRefs)*(float)2.0;
         pNode->nRefEst[0] = pNode->nRefEst[1] = pNode->nRefEst[2] = ((float)pNode->nRefs);
     }
@@ -157,9 +152,9 @@ void Map_MappingEstimateRefs( Map_Man_t * p )
 {
     Map_Node_t * pNode;
     int i;
-    for ( i = 0; i < p->vAnds->nSize; i++ )
+    for ( i = 0; i < p->vMapObjs->nSize; i++ )
     {
-        pNode = p->vAnds->pArray[i];
+        pNode = p->vMapObjs->pArray[i];
 //        pNode->nRefEst[0] = (float)((2.0 * pNode->nRefEst[0] + 1.0 * pNode->nRefAct[0]) / 3.0);
 //        pNode->nRefEst[1] = (float)((2.0 * pNode->nRefEst[1] + 1.0 * pNode->nRefAct[1]) / 3.0);
 //        pNode->nRefEst[2] = (float)((2.0 * pNode->nRefEst[2] + 1.0 * pNode->nRefAct[2]) / 3.0);
@@ -169,10 +164,6 @@ void Map_MappingEstimateRefs( Map_Man_t * p )
     }
 }
 
-
-
-
-
 /**function*************************************************************
 
   synopsis    [Computes the area flow of the cut.]
@@ -223,79 +214,6 @@ float Map_CutGetAreaFlow( Map_Cut_t * pCut, int fPhase )
 }
 
 
-
-/**function*************************************************************
-
-  synopsis    [Computes the exact area associated with the cut.]
-
-  description [Assumes that the cut is referenced.]
-               
-  sideeffects []
-
-  seealso     []
-
-***********************************************************************/
-float Map_CutGetAreaRefed( Map_Cut_t * pCut, int fPhase )
-{
-    float aResult, aResult2;
-    aResult2 = Map_CutRefDeref( pCut, fPhase, 0 ); // dereference
-    aResult  = Map_CutRefDeref( pCut, fPhase, 1 ); // reference
-//    assert( aResult == aResult2 );
-    return aResult;
-}
-
-/**function*************************************************************
-
-  synopsis    [Computes the exact area associated with the cut.]
-
-  description []
-               
-  sideeffects []
-
-  seealso     []
-
-***********************************************************************/
-float Map_CutGetAreaDerefed( Map_Cut_t * pCut, int fPhase )
-{
-    float aResult, aResult2;
-    aResult2 = Map_CutRefDeref( pCut, fPhase, 1 ); // reference
-    aResult  = Map_CutRefDeref( pCut, fPhase, 0 ); // dereference
-//    assert( aResult == aResult2 );
-    return aResult;
-}
-
-/**function*************************************************************
-
-  synopsis    [References the cut.]
-
-  description []
-               
-  sideeffects []
-
-  seealso     []
-
-***********************************************************************/
-float Map_CutRef( Map_Cut_t * pCut, int fPhase )
-{
-    return Map_CutRefDeref( pCut, fPhase, 1 ); // reference
-}
-
-/**function*************************************************************
-
-  synopsis    [Dereferences the cut.]
-
-  description []
-               
-  sideeffects []
-
-  seealso     []
-
-***********************************************************************/
-float Map_CutDeref( Map_Cut_t * pCut, int fPhase )
-{
-    return Map_CutRefDeref( pCut, fPhase, 0 ); // dereference
-}
-
 /**function*************************************************************
 
   synopsis    [References or dereferences the cut.]
@@ -396,98 +314,115 @@ float Map_CutRefDeref( Map_Cut_t * pCut, int fPhase, int fReference )
     return aArea;
 }
 
+/**function*************************************************************
 
+  synopsis    [Computes the exact area associated with the cut.]
 
+  description [Assumes that the cut is referenced.]
+               
+  sideeffects []
 
-/**Function*************************************************************
+  seealso     []
 
-  Synopsis    [Computes actual reference counters.]
+***********************************************************************/
+float Map_CutGetAreaRefed( Map_Cut_t * pCut, int fPhase )
+{
+    float aResult, aResult2;
+    aResult2 = Map_CutRefDeref( pCut, fPhase, 0 ); // dereference
+    aResult  = Map_CutRefDeref( pCut, fPhase, 1 ); // reference
+//    assert( aResult == aResult2 );
+    return aResult;
+}
 
-  Description [Collects the nodes used in the mapping in array pMan->vMapping.
-  Nodes are collected in reverse topological order to facilitate the 
-  computation of required times.]
+/**function*************************************************************
+
+  synopsis    [Computes the exact area associated with the cut.]
+
+  description []
                
-  SideEffects []
+  sideeffects []
 
-  SeeAlso     []
+  seealso     []
 
 ***********************************************************************/
-void Map_MappingSetRefs( Map_Man_t * pMan )
+float Map_CutGetAreaDerefed( Map_Cut_t * pCut, int fPhase )
 {
-    Map_Node_t * pNode, ** ppStore;
-    int i, fPhase, LevelMax;
+    float aResult, aResult2;
+    aResult2 = Map_CutRefDeref( pCut, fPhase, 1 ); // reference
+    aResult  = Map_CutRefDeref( pCut, fPhase, 0 ); // dereference
+//    assert( aResult == aResult2 );
+    return aResult;
+}
 
-    // clean all references
-    for ( i = 0; i < pMan->vNodesAll->nSize; i++ )
-    {
-        pNode = pMan->vNodesAll->pArray[i];
-        pNode->nRefAct[0] = 0;
-        pNode->nRefAct[1] = 0;
-        pNode->nRefAct[2] = 0;
-    }
+/**function*************************************************************
 
-    // find the largest level of a node
-    LevelMax = 0;
-    for ( i = 0; i < pMan->nOutputs; i++ )
-        if ( LevelMax < (int)Map_Regular(pMan->pOutputs[i])->Level )
-            LevelMax = Map_Regular(pMan->pOutputs[i])->Level;
+  synopsis    [References the cut.]
 
-    // allocate place to store the nodes
-    ppStore = ABC_ALLOC( Map_Node_t *, LevelMax + 1 );
-    memset( ppStore, 0, sizeof(Map_Node_t *) * (LevelMax + 1) );
+  description []
+               
+  sideeffects []
 
-    // visit nodes reachable from POs in the DFS order through the best cuts
-    for ( i = 0; i < pMan->nOutputs; i++ )
-    {
-        pNode  = pMan->pOutputs[i];
-        fPhase = !Map_IsComplement(pNode);
-        if ( !Map_NodeIsConst(pNode) )
-            Map_MappingSetRefs_rec( pMan, pNode, ppStore );
-    }
+  seealso     []
 
-    // reconnect the nodes in reverse topological order
-    pMan->vMapping->nSize = 0;
-    for ( i = LevelMax; i >= 0; i-- )
-        for ( pNode = ppStore[i]; pNode; pNode = (Map_Node_t *)pNode->pData0 )
-            Map_NodeVecPush( pMan->vMapping, pNode );
-    ABC_FREE( ppStore );
+***********************************************************************/
+float Map_CutRef( Map_Cut_t * pCut, int fPhase )
+{
+    return Map_CutRefDeref( pCut, fPhase, 1 ); // reference
 }
 
+/**function*************************************************************
+
+  synopsis    [Dereferences the cut.]
+
+  description []
+               
+  sideeffects []
+
+  seealso     []
+
+***********************************************************************/
+float Map_CutDeref( Map_Cut_t * pCut, int fPhase )
+{
+    return Map_CutRefDeref( pCut, fPhase, 0 ); // dereference
+}
+
+
 /**Function*************************************************************
 
-  Synopsis    [Recursively computes the DFS ordering of the nodes.]
+  Synopsis    [Computes actual reference counters.]
 
-  Description []
+  Description [Collects the nodes used in the mapping in array pMan->vMapping.
+  Nodes are collected in reverse topological order to facilitate the 
+  computation of required times.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode, Map_Node_t ** ppStore )
+void Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode )
 {
     Map_Cut_t * pCut;
     Map_Node_t * pNodeR;
     unsigned uPhase;
     int i, fPhase, fInvPin;
-
     // get the regular node and its phase
     pNodeR = Map_Regular(pNode);
     fPhase = !Map_IsComplement(pNode);
-
-    // add the node to the list of all visited nodes
-    if ( pNodeR->nRefAct[2]++ == 0 )
-//        Map_NodeVecPush( pMan->vMapping, pNodeR );
-        pNodeR->pData0 = (char *)ppStore[pNodeR->Level], ppStore[pNodeR->Level] = pNodeR;
-
+    pNodeR->nRefAct[2]++;
     // quit if the node was already visited in this phase
     if ( pNodeR->nRefAct[fPhase]++ )
         return;
-
     // quit if this is a PI node
     if ( Map_NodeIsVar(pNodeR) )
         return;
-
+    // propagate through buffer
+    if ( Map_NodeIsBuf(pNodeR) )
+    {
+        Map_MappingSetRefs_rec( pMan, Map_NotCond(pNodeR->p1, Map_IsComplement(pNode)) );
+        return;
+    }
+    assert( Map_NodeIsAnd(pNode) );
     // get the cut implementing this or opposite polarity
     pCut = pNodeR->pCutBest[fPhase];
     if ( pCut == NULL )
@@ -495,13 +430,32 @@ void Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode, Map_Node_t **
         fPhase = !fPhase;
         pCut   = pNodeR->pCutBest[fPhase];
     }
-
     // visit the transitive fanin
     uPhase = pCut->M[fPhase].uPhaseBest;
     for ( i = 0; i < pCut->nLeaves; i++ )
     {
         fInvPin = ((uPhase & (1 << i)) > 0);
-        Map_MappingSetRefs_rec( pMan, Map_NotCond(pCut->ppLeaves[i], fInvPin), ppStore );
+        Map_MappingSetRefs_rec( pMan, Map_NotCond(pCut->ppLeaves[i], fInvPin) );
+    }
+}
+void Map_MappingSetRefs( Map_Man_t * pMan )
+{
+    Map_Node_t * pNode;
+    int i;
+    // clean all references
+    for ( i = 0; i < pMan->vMapObjs->nSize; i++ )
+    {
+        pNode = pMan->vMapObjs->pArray[i];
+        pNode->nRefAct[0] = 0;
+        pNode->nRefAct[1] = 0;
+        pNode->nRefAct[2] = 0;
+    }
+    // visit nodes reachable from POs in the DFS order through the best cuts
+    for ( i = 0; i < pMan->nOutputs; i++ )
+    {
+        pNode = pMan->pOutputs[i];
+        if ( !Map_NodeIsConst(pNode) )
+            Map_MappingSetRefs_rec( pMan, pNode );
     }
 }
 
@@ -517,15 +471,18 @@ void Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode, Map_Node_t **
   SeeAlso     []
 
 ***********************************************************************/
-float Map_MappingGetArea( Map_Man_t * pMan, Map_NodeVec_t * vMapping )
+float Map_MappingGetArea( Map_Man_t * pMan )
 {
     Map_Node_t * pNode;
-    float Area;
+    float Area = 0.0;
     int i;
-    Area = 0.0;
-    for ( i = 0; i < vMapping->nSize; i++ )
+    for ( i = 0; i < pMan->vMapObjs->nSize; i++ )
     {
-        pNode = vMapping->pArray[i];
+        pNode = pMan->vMapObjs->pArray[i];
+        if ( pNode->nRefAct[2] == 0 )
+            continue;
+        if ( Map_NodeIsBuf(pNode) )
+            continue;
         // at least one phase has the best cut assigned
         assert( pNode->pCutBest[0] != NULL || pNode->pCutBest[1] != NULL );
         // at least one phase is used in the mapping
diff --git a/src/map/mapper/mapperSwitch.c b/src/map/mapper/mapperSwitch.c
index 11e99d24..e85eccbb 100644
--- a/src/map/mapper/mapperSwitch.c
+++ b/src/map/mapper/mapperSwitch.c
@@ -184,15 +184,16 @@ float Map_SwitchCutRefDeref( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhase, i
   SeeAlso     []
 
 ***********************************************************************/
-float Map_MappingGetSwitching( Map_Man_t * pMan, Map_NodeVec_t * vMapping )
+float Map_MappingGetSwitching( Map_Man_t * pMan )
 {
     Map_Node_t * pNode;
-    float Switch;
+    float Switch = 0.0;
     int i;
-    Switch = 0.0;
-    for ( i = 0; i < vMapping->nSize; i++ )
+    for ( i = 0; i < pMan->vMapObjs->nSize; i++ )
     {
-        pNode = vMapping->pArray[i];
+        pNode = pMan->vMapObjs->pArray[i];
+        if ( pNode->nRefAct[2] == 0 )
+            continue;
         // at least one phase has the best cut assigned
         assert( pNode->pCutBest[0] != NULL || pNode->pCutBest[1] != NULL );
         // at least one phase is used in the mapping
diff --git a/src/map/mapper/mapperTime.c b/src/map/mapper/mapperTime.c
index ce909e24..6915116c 100644
--- a/src/map/mapper/mapperTime.c
+++ b/src/map/mapper/mapperTime.c
@@ -20,63 +20,40 @@
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void  Map_TimePropagateRequired( Map_Man_t * p, Map_NodeVec_t * vNodes );
-static void  Map_TimePropagateRequiredPhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase );
-static float Map_MatchComputeReqTimes( Map_Cut_t * pCut, int fPhase, Map_Time_t * ptArrRes );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/**function*************************************************************
-
-  synopsis    [Computes the exact area associated with the cut.]
-
-  description []
-               
-  sideeffects []
-
-  seealso     []
-
-***********************************************************************/
-float Map_TimeMatchWithInverter( Map_Man_t * p, Map_Match_t * pMatch )
-{
-    Map_Time_t tArrInv;
-    tArrInv.Fall  = pMatch->tArrive.Rise + p->pSuperLib->tDelayInv.Fall;
-    tArrInv.Rise  = pMatch->tArrive.Fall + p->pSuperLib->tDelayInv.Rise;
-    tArrInv.Worst = MAP_MAX( tArrInv.Rise, tArrInv.Fall ); 
-    return tArrInv.Worst;
-}
-
 /**Function*************************************************************
 
-  Synopsis    [Computes the arrival times of the cut recursively.]
+  Synopsis    [Computes the maximum arrival times.]
 
-  Description [When computing the arrival time for the previously unused 
-  cuts, their arrival time may be incorrect because their fanins have 
-  incorrect arrival time. This procedure is called to fix this problem.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Map_TimeCutComputeArrival_rec( Map_Cut_t * pCut, int fPhase )
+float Map_TimeComputeArrivalMax( Map_Man_t * p )
 {
-    int i, fPhaseLeaf;
-    for ( i = 0; i < pCut->nLeaves; i++ )
+    float tReqMax, tReq;
+    int i, fPhase;
+    // get the critical PO arrival time
+    tReqMax = -MAP_FLOAT_LARGE;
+    for ( i = 0; i < p->nOutputs; i++ )
     {
-        fPhaseLeaf = Map_CutGetLeafPhase( pCut, fPhase, i );
-        if ( pCut->ppLeaves[i]->nRefAct[fPhaseLeaf] > 0 )
+        if ( Map_NodeIsConst(p->pOutputs[i]) )
             continue;
-        Map_TimeCutComputeArrival_rec( pCut->ppLeaves[i]->pCutBest[fPhaseLeaf], fPhaseLeaf );
+        fPhase  = !Map_IsComplement(p->pOutputs[i]);
+        tReq    = Map_Regular(p->pOutputs[i])->tArrival[fPhase].Worst;
+        tReqMax = MAP_MAX( tReqMax, tReq );
     }
-    Map_TimeCutComputeArrival( NULL, pCut, fPhase, MAP_FLOAT_LARGE );
+    return tReqMax;
 }
 
 /**Function*************************************************************
@@ -160,217 +137,7 @@ float Map_TimeCutComputeArrival( Map_Node_t * pNode, Map_Cut_t * pCut, int fPhas
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the maximum arrival times.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float Map_TimeComputeArrivalMax( Map_Man_t * p )
-{
-    float tReqMax, tReq;
-    int i, fPhase;
-    // get the critical PO arrival time
-    tReqMax = -MAP_FLOAT_LARGE;
-    for ( i = 0; i < p->nOutputs; i++ )
-    {
-        if ( Map_NodeIsConst(p->pOutputs[i]) )
-            continue;
-        fPhase  = !Map_IsComplement(p->pOutputs[i]);
-        tReq    = Map_Regular(p->pOutputs[i])->tArrival[fPhase].Worst;
-        tReqMax = MAP_MAX( tReqMax, tReq );
-    }
-    return tReqMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the required times of all nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_TimeComputeRequiredGlobal( Map_Man_t * p )
-{
-    p->fRequiredGlo = Map_TimeComputeArrivalMax( p );
-    // update the required times according to the target
-    if ( p->DelayTarget != -1 )
-    {
-        if ( p->fRequiredGlo > p->DelayTarget + p->fEpsilon )
-        {
-            if ( p->fMappingMode == 1 )
-                printf( "Cannot meet the target required times (%4.2f). Continue anyway.\n", p->DelayTarget );
-        }
-        else if ( p->fRequiredGlo < p->DelayTarget - p->fEpsilon )
-        {
-            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;
-        }
-    }
-    Map_TimeComputeRequired( p, p->fRequiredGlo );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the required times of all nodes.]
-
-  Description [This procedure assumes that the nodes used in the mapping
-  are collected in p->vMapping.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_TimeComputeRequired( Map_Man_t * p, float fRequired )
-{
-    Map_Time_t * ptTime, * ptTimeA;
-    int fPhase, i;
-
-    // clean the required times
-    for ( i = 0; i < p->vAnds->nSize; i++ )
-    {
-        p->vAnds->pArray[i]->tRequired[0].Rise = MAP_FLOAT_LARGE;
-        p->vAnds->pArray[i]->tRequired[0].Fall = MAP_FLOAT_LARGE;
-        p->vAnds->pArray[i]->tRequired[0].Worst = MAP_FLOAT_LARGE;
-        p->vAnds->pArray[i]->tRequired[1].Rise = MAP_FLOAT_LARGE;
-        p->vAnds->pArray[i]->tRequired[1].Fall = MAP_FLOAT_LARGE;
-        p->vAnds->pArray[i]->tRequired[1].Worst = MAP_FLOAT_LARGE;
-    }
-
-    // set the required times for the POs
-    for ( i = 0; i < p->nOutputs; i++ )
-    {
-        fPhase  = !Map_IsComplement(p->pOutputs[i]);
-        ptTime  =  Map_Regular(p->pOutputs[i])->tRequired + fPhase;
-        ptTimeA =  Map_Regular(p->pOutputs[i])->tArrival + fPhase;
-
-        // if external required time can be achieved, use it
-        if ( p->pOutputRequireds && p->pOutputRequireds[i].Worst > 0 && ptTimeA->Worst <= p->pOutputRequireds[i].Worst )//&& p->pOutputRequireds[i].Worst <= fRequired )
-            ptTime->Rise = ptTime->Fall = ptTime->Worst = p->pOutputRequireds[i].Worst;
-        // if external required cannot be achieved, set the earliest possible arrival time
-        else if ( p->pOutputRequireds && p->pOutputRequireds[i].Worst > 0 && ptTimeA->Worst > p->pOutputRequireds[i].Worst )
-            ptTime->Rise = ptTime->Fall = ptTime->Worst = ptTimeA->Worst;
-        // otherwise, set the global required time
-        else
-            ptTime->Rise = ptTime->Fall = ptTime->Worst = fRequired;
-    }
-
-    // sorts the nodes in the decreasing order of levels
-    // this puts the nodes in reverse topological order
-//    Map_MappingSortByLevel( p, p->vMapping );
-    // the array is already sorted by construction in Map_MappingSetRefs()
-
-    Map_TimePropagateRequired( p, p->vMapping );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the required times of the given nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_TimePropagateRequired( Map_Man_t * p, Map_NodeVec_t * vNodes )
-{
-    Map_Node_t * pNode;
-    Map_Time_t tReqOutTest, * ptReqOutTest = &tReqOutTest;
-    Map_Time_t * ptReqIn, * ptReqOut;
-    int fPhase, k;
-
-    // go through the nodes in the reverse topological order
-    for ( k = 0; k < vNodes->nSize; k++ )
-    {
-        pNode = vNodes->pArray[k];
-
-        // this computation works for regular nodes only
-        assert( !Map_IsComplement(pNode) );
-        // at least one phase should be mapped
-        assert( pNode->pCutBest[0] != NULL || pNode->pCutBest[1] != NULL );
-        // the node should be used in the currently assigned mapping
-        assert( pNode->nRefAct[0] > 0 || pNode->nRefAct[1] > 0 );
-
-        // if one of the cuts is not given, project the required times from the other cut
-        if ( pNode->pCutBest[0] == NULL || pNode->pCutBest[1] == NULL )
-        {
-//            assert( 0 );
-            // get the missing phase 
-            fPhase = (pNode->pCutBest[1] == NULL); 
-            // check if the missing phase is needed in the mapping
-            if ( pNode->nRefAct[fPhase] > 0 )
-            {
-                // get the pointers to the required times of the missing phase
-                ptReqOut = pNode->tRequired +  fPhase;
-//                assert( ptReqOut->Fall < MAP_FLOAT_LARGE );
-                // get the pointers to the required times of the present phase
-                ptReqIn  = pNode->tRequired + !fPhase;
-                // propagate the required times from the missing phase to the present phase
-    //            tArrInv.Fall  = pMatch->tArrive.Rise + p->pSuperLib->tDelayInv.Fall;
-    //            tArrInv.Rise  = pMatch->tArrive.Fall + p->pSuperLib->tDelayInv.Rise;
-                ptReqIn->Fall = MAP_MIN( ptReqIn->Fall, ptReqOut->Rise - p->pSuperLib->tDelayInv.Rise );
-                ptReqIn->Rise = MAP_MIN( ptReqIn->Rise, ptReqOut->Fall - p->pSuperLib->tDelayInv.Fall );
-            }
-        }
-
-        // finalize the worst case computation
-        pNode->tRequired[0].Worst = MAP_MIN( pNode->tRequired[0].Fall, pNode->tRequired[0].Rise );
-        pNode->tRequired[1].Worst = MAP_MIN( pNode->tRequired[1].Fall, pNode->tRequired[1].Rise );
-
-        // skip the PIs
-        if ( !Map_NodeIsAnd(pNode) )
-            continue;
-
-        // propagate required times of different phases of the node
-        // the ordering of phases does not matter since they are mapped independently
-        if ( pNode->pCutBest[0] && pNode->tRequired[0].Worst < MAP_FLOAT_LARGE )
-            Map_TimePropagateRequiredPhase( p, pNode, 0 );
-        if ( pNode->pCutBest[1] && pNode->tRequired[1].Worst < MAP_FLOAT_LARGE )
-            Map_TimePropagateRequiredPhase( p, pNode, 1 );
-    }
-
-    // in the end, we verify the required times
-    // for this, we compute the arrival times of the outputs of each phase 
-    // of the supergates using the fanins' required times as the fanins' arrival times
-    // the resulting arrival time of the supergate should be less than the actual required time
-    for ( k = 0; k < vNodes->nSize; k++ )
-    {
-        pNode = vNodes->pArray[k];
-        if ( !Map_NodeIsAnd(pNode) )
-            continue;
-        // verify that the required times are propagated correctly
-//        if ( pNode->pCutBest[0] && (pNode->nRefAct[0] > 0 || pNode->pCutBest[1] == NULL) )
-        if ( pNode->pCutBest[0] && pNode->tRequired[0].Worst < MAP_FLOAT_LARGE/2 )
-        {
-            Map_MatchComputeReqTimes( pNode->pCutBest[0], 0, ptReqOutTest );
-//            assert( ptReqOutTest->Rise < pNode->tRequired[0].Rise + p->fEpsilon );
-//            assert( ptReqOutTest->Fall < pNode->tRequired[0].Fall + p->fEpsilon );
-        }
-//        if ( pNode->pCutBest[1] && (pNode->nRefAct[1] > 0 || pNode->pCutBest[0] == NULL) )
-        if ( pNode->pCutBest[1] && pNode->tRequired[1].Worst < MAP_FLOAT_LARGE/2 )
-        {
-            Map_MatchComputeReqTimes( pNode->pCutBest[1], 1, ptReqOutTest );
-//            assert( ptReqOutTest->Rise < pNode->tRequired[1].Rise + p->fEpsilon );
-//            assert( ptReqOutTest->Fall < pNode->tRequired[1].Fall + p->fEpsilon );
-        }
-    }
-
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the required times of the given nodes.]
+  Synopsis    []
 
   Description []
                
@@ -446,20 +213,6 @@ void Map_TimePropagateRequiredPhase( Map_Man_t * p, Map_Node_t * pNode, int fPha
     assert( pNode->tArrival[fPhase].Rise < ptReqOut->Rise + p->fEpsilon );
     assert( pNode->tArrival[fPhase].Fall < ptReqOut->Fall + p->fEpsilon );
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the arrival times of the cut.]
-
-  Description [Computes the arrival times of the cut if it is implemented using 
-  the given supergate with the given phase. Uses the constraint-type specification
-  of rise/fall arrival times.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 float Map_MatchComputeReqTimes( Map_Cut_t * pCut, int fPhase, Map_Time_t * ptArrRes )
 {
     Map_Time_t * ptArrIn;
@@ -518,6 +271,164 @@ float Map_MatchComputeReqTimes( Map_Cut_t * pCut, int fPhase, Map_Time_t * ptArr
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the required times of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_TimePropagateRequired( Map_Man_t * p )
+{
+    Map_Node_t * pNode;
+    Map_Time_t tReqOutTest, * ptReqOutTest = &tReqOutTest;
+    Map_Time_t * ptReqIn, * ptReqOut;
+    int fPhase, k;
+
+    // go through the nodes in the reverse topological order
+    for ( k = p->vMapObjs->nSize - 1; k >= 0; k-- )
+    {
+        pNode = p->vMapObjs->pArray[k];
+        if ( pNode->nRefAct[2] == 0 )
+            continue;
+
+        // propagate required times through the buffer
+        if ( Map_NodeIsBuf(pNode) )
+        {
+            assert( pNode->p2 == NULL );
+            Map_Regular(pNode->p1)->tRequired[ Map_IsComplement(pNode->p1)] = pNode->tRequired[0];
+            Map_Regular(pNode->p1)->tRequired[!Map_IsComplement(pNode->p1)] = pNode->tRequired[1];
+            continue;
+        }
+
+        // this computation works for regular nodes only
+        assert( !Map_IsComplement(pNode) );
+        // at least one phase should be mapped
+        assert( pNode->pCutBest[0] != NULL || pNode->pCutBest[1] != NULL );
+        // the node should be used in the currently assigned mapping
+        assert( pNode->nRefAct[0] > 0 || pNode->nRefAct[1] > 0 );
+
+        // if one of the cuts is not given, project the required times from the other cut
+        if ( pNode->pCutBest[0] == NULL || pNode->pCutBest[1] == NULL )
+        {
+//            assert( 0 );
+            // get the missing phase 
+            fPhase = (pNode->pCutBest[1] == NULL); 
+            // check if the missing phase is needed in the mapping
+            if ( pNode->nRefAct[fPhase] > 0 )
+            {
+                // get the pointers to the required times of the missing phase
+                ptReqOut = pNode->tRequired +  fPhase;
+//                assert( ptReqOut->Fall < MAP_FLOAT_LARGE );
+                // get the pointers to the required times of the present phase
+                ptReqIn  = pNode->tRequired + !fPhase;
+                // propagate the required times from the missing phase to the present phase
+    //            tArrInv.Fall  = pMatch->tArrive.Rise + p->pSuperLib->tDelayInv.Fall;
+    //            tArrInv.Rise  = pMatch->tArrive.Fall + p->pSuperLib->tDelayInv.Rise;
+                ptReqIn->Fall = MAP_MIN( ptReqIn->Fall, ptReqOut->Rise - p->pSuperLib->tDelayInv.Rise );
+                ptReqIn->Rise = MAP_MIN( ptReqIn->Rise, ptReqOut->Fall - p->pSuperLib->tDelayInv.Fall );
+            }
+        }
+
+        // finalize the worst case computation
+        pNode->tRequired[0].Worst = MAP_MIN( pNode->tRequired[0].Fall, pNode->tRequired[0].Rise );
+        pNode->tRequired[1].Worst = MAP_MIN( pNode->tRequired[1].Fall, pNode->tRequired[1].Rise );
+
+        // skip the PIs
+        if ( !Map_NodeIsAnd(pNode) )
+            continue;
+
+        // propagate required times of different phases of the node
+        // the ordering of phases does not matter since they are mapped independently
+        if ( pNode->pCutBest[0] && pNode->tRequired[0].Worst < MAP_FLOAT_LARGE )
+            Map_TimePropagateRequiredPhase( p, pNode, 0 );
+        if ( pNode->pCutBest[1] && pNode->tRequired[1].Worst < MAP_FLOAT_LARGE )
+            Map_TimePropagateRequiredPhase( p, pNode, 1 );
+    }
+
+    // in the end, we verify the required times
+    // for this, we compute the arrival times of the outputs of each phase 
+    // of the supergates using the fanins' required times as the fanins' arrival times
+    // the resulting arrival time of the supergate should be less than the actual required time
+    for ( k = p->vMapObjs->nSize - 1; k >= 0; k-- )
+    {
+        pNode = p->vMapObjs->pArray[k];
+        if ( pNode->nRefAct[2] == 0 )
+            continue;
+        if ( !Map_NodeIsAnd(pNode) )
+            continue;
+        // verify that the required times are propagated correctly
+//        if ( pNode->pCutBest[0] && (pNode->nRefAct[0] > 0 || pNode->pCutBest[1] == NULL) )
+        if ( pNode->pCutBest[0] && pNode->tRequired[0].Worst < MAP_FLOAT_LARGE/2 )
+        {
+            Map_MatchComputeReqTimes( pNode->pCutBest[0], 0, ptReqOutTest );
+//            assert( ptReqOutTest->Rise < pNode->tRequired[0].Rise + p->fEpsilon );
+//            assert( ptReqOutTest->Fall < pNode->tRequired[0].Fall + p->fEpsilon );
+        }
+//        if ( pNode->pCutBest[1] && (pNode->nRefAct[1] > 0 || pNode->pCutBest[0] == NULL) )
+        if ( pNode->pCutBest[1] && pNode->tRequired[1].Worst < MAP_FLOAT_LARGE/2 )
+        {
+            Map_MatchComputeReqTimes( pNode->pCutBest[1], 1, ptReqOutTest );
+//            assert( ptReqOutTest->Rise < pNode->tRequired[1].Rise + p->fEpsilon );
+//            assert( ptReqOutTest->Fall < pNode->tRequired[1].Fall + p->fEpsilon );
+        }
+    }
+}
+void Map_TimeComputeRequiredGlobal( Map_Man_t * p )
+{
+    Map_Time_t * ptTime, * ptTimeA;
+    int fPhase, i;
+    // update the required times according to the target
+    p->fRequiredGlo = Map_TimeComputeArrivalMax( p );
+    if ( p->DelayTarget != -1 )
+    {
+        if ( p->fRequiredGlo > p->DelayTarget + p->fEpsilon )
+        {
+            if ( p->fMappingMode == 1 )
+                printf( "Cannot meet the target required times (%4.2f). Continue anyway.\n", p->DelayTarget );
+        }
+        else if ( p->fRequiredGlo < p->DelayTarget - p->fEpsilon )
+        {
+            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;
+        }
+    }
+    // clean the required times
+    for ( i = 0; i < p->vMapObjs->nSize; i++ )
+    {
+        p->vMapObjs->pArray[i]->tRequired[0].Rise  = MAP_FLOAT_LARGE;
+        p->vMapObjs->pArray[i]->tRequired[0].Fall  = MAP_FLOAT_LARGE;
+        p->vMapObjs->pArray[i]->tRequired[0].Worst = MAP_FLOAT_LARGE;
+        p->vMapObjs->pArray[i]->tRequired[1].Rise  = MAP_FLOAT_LARGE;
+        p->vMapObjs->pArray[i]->tRequired[1].Fall  = MAP_FLOAT_LARGE;
+        p->vMapObjs->pArray[i]->tRequired[1].Worst = MAP_FLOAT_LARGE;
+    }
+    // set the required times for the POs
+    for ( i = 0; i < p->nOutputs; i++ )
+    {
+        fPhase  = !Map_IsComplement(p->pOutputs[i]);
+        ptTime  =  Map_Regular(p->pOutputs[i])->tRequired + fPhase;
+        ptTimeA =  Map_Regular(p->pOutputs[i])->tArrival + fPhase;
+
+        // if external required time can be achieved, use it
+        if ( p->pOutputRequireds && p->pOutputRequireds[i].Worst > 0 && ptTimeA->Worst <= p->pOutputRequireds[i].Worst )//&& p->pOutputRequireds[i].Worst <= p->fRequiredGlo )
+            ptTime->Rise = ptTime->Fall = ptTime->Worst = p->pOutputRequireds[i].Worst;
+        // if external required cannot be achieved, set the earliest possible arrival time
+        else if ( p->pOutputRequireds && p->pOutputRequireds[i].Worst > 0 && ptTimeA->Worst > p->pOutputRequireds[i].Worst )
+            ptTime->Rise = ptTime->Fall = ptTime->Worst = ptTimeA->Worst;
+        // otherwise, set the global required time
+        else
+            ptTime->Rise = ptTime->Fall = ptTime->Worst = p->fRequiredGlo;
+    }
+    // visit nodes in the reverse topological order
+    Map_TimePropagateRequired( p );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mapper/mapperTruth.c b/src/map/mapper/mapperTruth.c
index 377df9b4..8c88eedc 100644
--- a/src/map/mapper/mapperTruth.c
+++ b/src/map/mapper/mapperTruth.c
@@ -51,11 +51,11 @@ void Map_MappingTruths( Map_Man_t * pMan )
     Map_Cut_t * pCut;
     int nNodes, i;
     // compute the cuts for the POs
-    nNodes = pMan->vAnds->nSize;
+    nNodes = pMan->vMapObjs->nSize;
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
     for ( i = 0; i < nNodes; i++ )
     {
-        pNode = pMan->vAnds->pArray[i];
+        pNode = pMan->vMapObjs->pArray[i];
         if ( !Map_NodeIsAnd( pNode ) )
             continue;
         assert( pNode->pCuts );
diff --git a/src/map/mapper/mapperUtils.c b/src/map/mapper/mapperUtils.c
index fbee6f74..7ea60ec9 100644
--- a/src/map/mapper/mapperUtils.c
+++ b/src/map/mapper/mapperUtils.c
@@ -27,7 +27,6 @@ ABC_NAMESPACE_IMPL_START
 
 #define MAP_CO_LIST_SIZE 5
 
-static void  Map_MappingDfs_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, int fCollectEquiv );
 static int   Map_MappingCountLevels_rec( Map_Node_t * pNode );
 static float Map_MappingSetRefsAndArea_rec( Map_Man_t * pMan, Map_Node_t * pNode );
 static float Map_MappingSetRefsAndSwitch_rec( Map_Man_t * pMan, Map_Node_t * pNode );
@@ -37,41 +36,12 @@ static float Map_MappingArea_rec( Map_Man_t * pMan, Map_Node_t * pNode, Map_Node
 static int   Map_MappingCompareOutputDelay( Map_Node_t ** ppNode1, Map_Node_t ** ppNode2 );
 static void  Map_MappingFindLatest( Map_Man_t * p, int * pNodes, int nNodesMax );
 static unsigned Map_MappingExpandTruth_rec( unsigned uTruth, int nVars );
-static void Map_MappingGetChoiceLevels( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2, int * pMin, int * pMax );
-static float Map_MappingGetChoiceVolumes( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2 );
 static int Map_MappingCountUsedNodes( Map_Man_t * pMan, int fChoices );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the DFS ordering of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Map_NodeVec_t * Map_MappingDfs( Map_Man_t * pMan, int fCollectEquiv )
-{
-    Map_NodeVec_t * vNodes;
-    int i;
-    // perform the traversal
-    vNodes = Map_NodeVecAlloc( 100 );
-    for ( i = 0; i < pMan->nOutputs; i++ )
-        Map_MappingDfs_rec( Map_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv );
-    for ( i = 0; i < vNodes->nSize; i++ )
-        vNodes->pArray[i]->fMark0 = 0;
-//    for ( i = 0; i < pMan->nOutputs; i++ )
-//        Map_MappingUnmark_rec( Map_Regular(pMan->pOutputs[i]) );
-    return vNodes;
-}
-
 /**Function*************************************************************
 
   Synopsis    [Computes the DFS ordering of the nodes.]
@@ -83,30 +53,6 @@ Map_NodeVec_t * Map_MappingDfs( Map_Man_t * pMan, int fCollectEquiv )
   SeeAlso     []
 
 ***********************************************************************/
-Map_NodeVec_t * Map_MappingDfsNodes( Map_Man_t * pMan, Map_Node_t ** ppCuts, int nNodes, int fEquiv )
-{
-    Map_NodeVec_t * vNodes;
-    int i;
-    // perform the traversal
-    vNodes = Map_NodeVecAlloc( 200 );
-    for ( i = 0; i < nNodes; i++ )
-        Map_MappingDfs_rec( ppCuts[i], vNodes, fEquiv );
-    for ( i = 0; i < vNodes->nSize; i++ )
-        vNodes->pArray[i]->fMark0 = 0;
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes the DFS ordering of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 void Map_MappingDfs_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, int fCollectEquiv )
 {
     assert( !Map_IsComplement(pNode) );
@@ -128,144 +74,21 @@ void Map_MappingDfs_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, int fCollec
     // add the node to the list
     Map_NodeVecPush( vNodes, pNode );
 }
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes the DFS ordering of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_MappingDfsMarked1_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, int fFirst )
-{
-    assert( !Map_IsComplement(pNode) );
-    if ( pNode->fMark0 )
-        return;
-    // visit the transitive fanin
-    if ( Map_NodeIsAnd(pNode) )
-    {
-        Map_MappingDfsMarked1_rec( Map_Regular(pNode->p1), vNodes, 0 );
-        Map_MappingDfsMarked1_rec( Map_Regular(pNode->p2), vNodes, 0 );
-    }
-    // visit the equivalent nodes
-    if ( !fFirst && pNode->pNextE )
-        Map_MappingDfsMarked1_rec( pNode->pNextE, vNodes, 0 );
-    // make sure the node is not visited through the equivalent nodes
-    assert( pNode->fMark0 == 0 );
-    // mark the node as visited
-    pNode->fMark0 = 1;
-    // add the node to the list
-    Map_NodeVecPush( vNodes, pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes the DFS ordering of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_MappingDfsMarked2_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes, Map_NodeVec_t * vBoundary, int fFirst )
-{
-    assert( !Map_IsComplement(pNode) );
-    if ( pNode->fMark1 )
-        return;
-    if ( pNode->fMark0 || Map_NodeIsVar(pNode) )
-    {
-        pNode->fMark1 = 1;
-        Map_NodeVecPush(vBoundary, pNode);
-        return;
-    }
-    // visit the transitive fanin
-    if ( Map_NodeIsAnd(pNode) )
-    {
-        Map_MappingDfsMarked2_rec( Map_Regular(pNode->p1), vNodes, vBoundary, 0 );
-        Map_MappingDfsMarked2_rec( Map_Regular(pNode->p2), vNodes, vBoundary, 0 );
-    }
-    // visit the equivalent nodes
-    if ( !fFirst && pNode->pNextE )
-        Map_MappingDfsMarked2_rec( pNode->pNextE, vNodes, vBoundary, 0 );
-    // make sure the node is not visited through the equivalent nodes
-    assert( pNode->fMark1 == 0 );
-    // mark the node as visited
-    pNode->fMark1 = 1;
-    // add the node to the list
-    Map_NodeVecPush( vNodes, pNode );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes the DFS ordering of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_MappingDfsMarked3_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes )
-{
-    assert( !Map_IsComplement(pNode) );
-    if ( pNode->fMark0 )
-        return;
-    // visit the transitive fanin
-    if ( Map_NodeIsAnd(pNode) )
-    {
-        Map_MappingDfsMarked3_rec( Map_Regular(pNode->p1), vNodes );
-        Map_MappingDfsMarked3_rec( Map_Regular(pNode->p2), vNodes );
-    }
-    // make sure the node is not visited through the equivalent nodes
-    assert( pNode->fMark0 == 0 );
-    // mark the node as visited
-    pNode->fMark0 = 1;
-    // add the node to the list
-    Map_NodeVecPush( vNodes, pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes the DFS ordering of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_MappingDfsMarked4_rec( Map_Node_t * pNode, Map_NodeVec_t * vNodes )
+Map_NodeVec_t * Map_MappingDfs( Map_Man_t * pMan, int fCollectEquiv )
 {
-    assert( !Map_IsComplement(pNode) );
-    if ( pNode->fMark1 )
-        return;
-    // visit the transitive fanin
-    if ( Map_NodeIsAnd(pNode) )
-    {
-        Map_MappingDfsMarked4_rec( Map_Regular(pNode->p1), vNodes );
-        Map_MappingDfsMarked4_rec( Map_Regular(pNode->p2), vNodes );
-    }
-    // make sure the node is not visited through the equivalent nodes
-    assert( pNode->fMark1 == 0 );
-    // mark the node as visited
-    pNode->fMark1 = 1;
-    // add the node to the list
-    Map_NodeVecPush( vNodes, pNode );
+    Map_NodeVec_t * vNodes;
+    int i;
+    // perform the traversal
+    vNodes = Map_NodeVecAlloc( 100 );
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        Map_MappingDfs_rec( Map_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv );
+    for ( i = 0; i < vNodes->nSize; i++ )
+        vNodes->pArray[i]->fMark0 = 0;
+//    for ( i = 0; i < pMan->nOutputs; i++ )
+//        Map_MappingUnmark_rec( Map_Regular(pMan->pOutputs[i]) );
+    return vNodes;
 }
 
-
-
 /**Function*************************************************************
 
   Synopsis    [Computes the number of logic levels not counting PIs/POs.]
@@ -829,8 +652,8 @@ int Map_MappingCountDoubles( Map_Man_t * pMan, Map_NodeVec_t * vNodes )
 void Map_ManCleanData( Map_Man_t * p )
 {
     int i;
-    for ( i = 0; i < p->vNodesAll->nSize; i++ )
-        p->vNodesAll->pArray[i]->pData0 = p->vNodesAll->pArray[i]->pData1 = 0;
+    for ( i = 0; i < p->vMapObjs->nSize; i++ )
+        p->vMapObjs->pArray[i]->pData0 = p->vMapObjs->pArray[i]->pData1 = 0;
 }
 
 /**Function*************************************************************
@@ -892,10 +715,10 @@ float Map_MappingComputeDelayWithFanouts( Map_Man_t * p )
     Map_Node_t * pNode;
     float Result;
     int i;
-    for ( i = 0; i < p->vAnds->nSize; i++ )
+    for ( i = 0; i < p->vMapObjs->nSize; i++ )
     {
         // skip primary inputs
-        pNode = p->vAnds->pArray[i];
+        pNode = p->vMapObjs->pArray[i];
         if ( !Map_NodeIsAnd( pNode ) )
             continue;
         // skip a secondary node
@@ -1031,9 +854,9 @@ void Map_MappingReportChoices( Map_Man_t * pMan )
 
     // report statistics about choices
     nChoiceNodes = nChoices = 0;
-    for ( i = 0; i < pMan->vAnds->nSize; i++ )
+    for ( i = 0; i < pMan->vMapObjs->nSize; i++ )
     {
-        pNode = pMan->vAnds->pArray[i];
+        pNode = pMan->vMapObjs->pArray[i];
         if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
         { // this is a choice node = the primary node that has equivalent nodes
             nChoiceNodes++;
@@ -1056,89 +879,6 @@ void Map_MappingReportChoices( Map_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-void Map_MappingGetChoiceLevels( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2, int * pMin, int * pMax )
-{
-    Map_NodeVec_t * vNodes;
-    Map_NodeVec_t * vBoundary;
-    Map_Node_t * pNode;
-    int i, Min, Max;
-
-    vNodes    = Map_NodeVecAlloc( 100 );
-    vBoundary = Map_NodeVecAlloc( 100 );
-    Map_MappingDfsMarked1_rec( p1, vNodes, 1 );
-    Map_MappingDfsMarked2_rec( p2, vNodes, vBoundary, 1 );
-    // clean the marks
-    Min =  100000;
-    Max = -100000;
-    for ( i = 0; i < vBoundary->nSize; i++ )
-    {
-        pNode = vBoundary->pArray[i];
-        if ( Min > (int)pNode->Level )
-            Min = pNode->Level;
-        if ( Max < (int)pNode->Level )
-            Max = pNode->Level;
-    }
-    Map_NodeVecFree( vBoundary );
-    for ( i = 0; i < vNodes->nSize; i++ )
-    {
-        pNode = vNodes->pArray[i];
-        pNode->fMark0 = pNode->fMark1 = 0;
-    }
-    Map_NodeVecFree( vNodes );
-    *pMin = Min;
-    *pMax = Max;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float Map_MappingGetChoiceVolumes( Map_Man_t * pMan, Map_Node_t * p1, Map_Node_t * p2 )
-{
-    Map_NodeVec_t * vNodes;
-    Map_Node_t * pNode;
-    int i, nVolumeTotal, nVolumeUnique;
-
-    vNodes    = Map_NodeVecAlloc( 100 );
-    Map_MappingDfsMarked3_rec( p1, vNodes );
-    Map_MappingDfsMarked4_rec( p2, vNodes );
-    // clean the marks
-    nVolumeTotal = nVolumeUnique = 0;
-    for ( i = 0; i < vNodes->nSize; i++ )
-    {
-        pNode = vNodes->pArray[i];
-        if ( !Map_NodeIsAnd(pNode) )
-            continue;
-        nVolumeTotal++;
-        if ( pNode->fMark0 ^ pNode->fMark1 )
-            nVolumeUnique++;
-        pNode->fMark0 = pNode->fMark1 = 0;
-    }
-    Map_NodeVecFree( vNodes );
-//    return ((float)nVolumeUnique)/nVolumeTotal;
-    return (float)nVolumeUnique;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the maximum and minimum levels of the choice nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Map_MappingCountUsedNodes( Map_Man_t * pMan, int fChoices )
 {
     Map_NodeVec_t * vNodes;
diff --git a/src/map/mapper/mapperVec.c b/src/map/mapper/mapperVec.c
index dd87e752..8316072a 100644
--- a/src/map/mapper/mapperVec.c
+++ b/src/map/mapper/mapperVec.c
@@ -67,6 +67,8 @@ Map_NodeVec_t * Map_NodeVecAlloc( int nCap )
 ***********************************************************************/
 void Map_NodeVecFree( Map_NodeVec_t * p )
 {
+    if ( p == NULL )
+        return;
     ABC_FREE( p->pArray );
     ABC_FREE( p );
 }
@@ -82,6 +84,25 @@ void Map_NodeVecFree( Map_NodeVec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Map_NodeVec_t * Map_NodeVecDup( Map_NodeVec_t * p )
+{
+    Map_NodeVec_t * pNew = Map_NodeVecAlloc( p->nSize );
+    memcpy( pNew->pArray, p->pArray, sizeof(int) * p->nSize );
+    pNew->nSize = p->nSize;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Map_Node_t ** Map_NodeVecReadArray( Map_NodeVec_t * p )
 {
     return p->pArray;