Version abc50819

20 files changed, 412 insertions, 894 deletions

diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h
index 62a93a75..9dad1670 100644
--- a/src/map/fpga/fpga.h
+++ b/src/map/fpga/fpga.h
@@ -80,10 +80,7 @@ extern void            Fpga_ManSetTimeToNet( Fpga_Man_t * p, int Time );
 extern void            Fpga_ManSetTimeTotal( Fpga_Man_t * p, int Time );
 extern void            Fpga_ManSetOutputNames( Fpga_Man_t * p, char ** ppNames );
 extern void            Fpga_ManSetInputArrivals( Fpga_Man_t * p, float * pArrivals );
-extern void            Fpga_ManSetTree( Fpga_Man_t * p, int fTree );
-extern void            Fpga_ManSetPower( Fpga_Man_t * p, int fPower );
 extern void            Fpga_ManSetAreaRecovery( Fpga_Man_t * p, int fAreaRecovery );
-extern void            Fpga_ManSetResyn( Fpga_Man_t * p, int fResynthesis );
 extern void            Fpga_ManSetDelayLimit( Fpga_Man_t * p, float DelayLimit );
 extern void            Fpga_ManSetAreaLimit( Fpga_Man_t * p, float AreaLimit );
 extern void            Fpga_ManSetTimeLimit( Fpga_Man_t * p, float TimeLimit );
@@ -95,7 +92,6 @@ extern void            Fpga_ManSetChoiceNodeNum( Fpga_Man_t * p, int nChoiceNode
 extern void            Fpga_ManSetChoiceNum( Fpga_Man_t * p, int nChoices );
 extern void            Fpga_ManSetVerbose( Fpga_Man_t * p, int fVerbose );
 extern void            Fpga_ManSetLatchNum( Fpga_Man_t * p, int nLatches );
-extern void            Fpga_ManSetSequential( Fpga_Man_t * p, int fSequential );
 extern void            Fpga_ManSetName( Fpga_Man_t * p, char * pFileName );
 
 extern int             Fpga_LibReadLutMax( Fpga_LutLib_t * pLib );
diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c
index 457c2384..b181e997 100644
--- a/src/map/fpga/fpgaCore.c
+++ b/src/map/fpga/fpgaCore.c
@@ -17,18 +17,12 @@
 ***********************************************************************/
 
 #include "fpgaInt.h"
-//#include "res.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int   Fpga_MappingPostProcess( Fpga_Man_t * p );
-
-extern void  Fpga_Experiment( Fpga_Man_t * p );
-extern void Fpga_MappingCutsSeq( Fpga_Man_t * p );
-extern void Fpga_MappingLValues( Fpga_Man_t * pMan, int fVerbose );
-
+static int  Fpga_MappingPostProcess( Fpga_Man_t * p );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -51,35 +45,18 @@ extern void Fpga_MappingLValues( Fpga_Man_t * pMan, int fVerbose );
 ***********************************************************************/
 int Fpga_Mapping( Fpga_Man_t * p )
 {
-    int clk;
+    int clk, clkTotal = clock();
 
     // collect the nodes reachable from POs in the DFS order (including the choices)
     p->vAnds = Fpga_MappingDfs( p, 1 );
     Fpga_ManReportChoices( p ); // recomputes levels
     Fpga_MappingSetChoiceLevels( p );
 
-    if ( p->fSequential )
-    {
-//        Fpga_MappingCutsSeq( p );
-        Fpga_MappingCuts( p );
-//clk = clock();
-//        Fpga_MappingLValues( p, p->fVerbose );
-//PRT( "Time", clock() - clk );
-        return 0;
-    }
-
     // compute the cuts of nodes in the DFS order
     clk = clock();
     Fpga_MappingCuts( p );
     p->timeCuts = clock() - clk;
 
-//    Fpga_MappingSortByLevel( p, p->vAnds, 1 );
-
-    // derive the truth tables 
-    clk = clock();
-//    Fpga_MappingTruths( p );
-    p->timeTruth = clock() - clk;
-
     // match the truth tables to the supergates
     clk = clock();
     if ( !Fpga_MappingMatches( p, 1 ) )
@@ -94,10 +71,7 @@ int Fpga_Mapping( Fpga_Man_t * p )
             return 0;
         p->timeRecover = clock() - clk;
     }
-
-    // perform resynthesis
-//    if ( p->fResynthesis )
-//        Res_Resynthesize( p, p->DelayLimit, p->AreaLimit, p->TimeLimit, 1 );
+PRT( "Total mapping time", clock() - clkTotal );
 
     // print the AI-graph used for mapping
     //Fpga_ManShow( p, "test" );
@@ -124,128 +98,59 @@ int Fpga_Mapping( Fpga_Man_t * p )
 int Fpga_MappingPostProcess( Fpga_Man_t * p )
 {
     float aAreaTotalPrev, aAreaTotalCur, aAreaTotalCur2;
-    float aSwitchTotalPrev, aSwitchTotalCur;
     int Iter, clk;
 
-
+    // compute area, set references, and collect nodes used in the mapping
+    aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
 if ( p->fVerbose )
 {
-printf( "Iteration %dD :  Area = %11.1f  ", 0, Fpga_MappingArea( p ) );
+printf( "Iteration %dD :  Area = %11.1f  ", 0, aAreaTotalCur );
 PRT( "Time", p->timeMatch );
 }
 
-
-//    Fpga_MappingExplore( p );
-//    p->fAreaGlo = Fpga_MappingArea( p );
-//    return;
-
-
-//    aAreaTotalCur = FPGA_FLOAT_LARGE;
-    aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
-
     Iter = 1;
     do {
 clk = clock();
         // save the previous area flow
         aAreaTotalPrev = aAreaTotalCur;
-
         // compute the required times and the fanouts
         Fpga_TimeComputeRequiredGlobal( p );
         // remap topologically
         Fpga_MappingMatches( p, 0 );
         // get the resulting area
-        aAreaTotalCur = Fpga_MappingArea( p );
+//        aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
+        aAreaTotalCur = Fpga_MappingAreaTrav( p );
+        // note that here we do not update the reference counter
+        // for some reason, this works better on benchmarks
 if ( p->fVerbose )
 {
 printf( "Iteration %dF :  Area = %11.1f  ", Iter++, aAreaTotalCur );
 PRT( "Time", clock() - clk );
 }
-        if ( p->fPower )
-            aSwitchTotalCur = Fpga_MappingPrintSwitching( p );
         // quit if this iteration reduced area flow by less than 1%
     } while ( aAreaTotalPrev > 1.02 * aAreaTotalCur );
 
-
-//    Fpga_MappingExplore( p );
-//    p->fAreaGlo = Fpga_MappingArea( p );
-//    return;
-
-
-/*
-    // compute the area of each cut
-    aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
-    // compute the required times and the fanouts
-    Fpga_TimeComputeRequiredGlobal( p );
-    // perform experiment
-    Fpga_Experiment( p );
-*/
-
-
-    // compute the area of each cut
-    aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
-    aAreaTotalCur2 = Fpga_MappingComputeCutAreas( p );
+    // update reference counters
+    aAreaTotalCur2 = Fpga_MappingSetRefsAndArea( p );
     assert( aAreaTotalCur == aAreaTotalCur2 );
 
-
-//    aAreaTotalCur = FPGA_FLOAT_LARGE;
-//    Iter = 1;
     do {
 clk = clock();
         // save the previous area flow
         aAreaTotalPrev = aAreaTotalCur;
-
         // compute the required times and the fanouts
         Fpga_TimeComputeRequiredGlobal( p );
         // remap topologically
         Fpga_MappingMatchesArea( p );
         // get the resulting area
-        aAreaTotalCur = Fpga_MappingArea( p );
+        aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
 if ( p->fVerbose )
 {
 printf( "Iteration %dA :  Area = %11.1f  ", Iter++, aAreaTotalCur );
 PRT( "Time", clock() - clk );
 }
-        if ( p->fPower )
-        {
-            aSwitchTotalPrev = aSwitchTotalCur;
-            aSwitchTotalCur  = Fpga_MappingPrintSwitching( p );
-        }
         // quit if this iteration reduced area flow by less than 1%
     } while ( aAreaTotalPrev > 1.02 * aAreaTotalCur );
-
-
-    if ( p->fPower )
-    {
-        do {
-clk = clock();
-            // save the previous area flow
-            aAreaTotalPrev = aAreaTotalCur;
-
-            // compute the required times and the fanouts
-            Fpga_TimeComputeRequiredGlobal( p );
-            // remap topologically
-            Fpga_MappingMatchesSwitch( p );
-            // get the resulting area
-            aAreaTotalCur = Fpga_MappingArea( p );
-if ( p->fVerbose )
-{
-printf( "Iteration %dS :  Area = %11.1f  ", Iter++, aAreaTotalCur );
-PRT( "Time", clock() - clk );
-}
-            aSwitchTotalPrev = aSwitchTotalCur;
-            aSwitchTotalCur  = Fpga_MappingPrintSwitching( p );
-            // quit if this iteration reduced area flow by less than 1%
-        } while ( aSwitchTotalPrev > 1.01 * aSwitchTotalCur );
-    }
-
-/*
-    // compute the area of each cut
-    aAreaTotalCur = Fpga_MappingSetRefsAndArea( p );
-    // compute the required times and the fanouts
-    Fpga_TimeComputeRequiredGlobal( p );
-    // perform experiment
-    Fpga_Experiment( p );
-*/
     p->fAreaGlo = aAreaTotalCur;
     return 1;
 }
diff --git a/src/map/fpga/fpgaCreate.c b/src/map/fpga/fpgaCreate.c
index 1e654ded..f3abbedb 100644
--- a/src/map/fpga/fpgaCreate.c
+++ b/src/map/fpga/fpgaCreate.c
@@ -58,10 +58,7 @@ void            Fpga_ManSetTimeToNet( Fpga_Man_t * p, int Time )          { p->t
 void            Fpga_ManSetTimeTotal( Fpga_Man_t * p, int Time )          { p->timeTotal = Time;  }
 void            Fpga_ManSetOutputNames( Fpga_Man_t * p, char ** ppNames ) { p->ppOutputNames = ppNames; }
 void            Fpga_ManSetInputArrivals( Fpga_Man_t * p, float * pArrivals ) { p->pInputArrivals = pArrivals; }
-void            Fpga_ManSetTree( Fpga_Man_t * p, int fTree )              { p->fTree = fTree;           }
-void            Fpga_ManSetPower( Fpga_Man_t * p, int fPower )              { p->fPower = fPower;           }
 void            Fpga_ManSetAreaRecovery( Fpga_Man_t * p, int fAreaRecovery ) { p->fAreaRecovery = fAreaRecovery;}
-void            Fpga_ManSetResyn( Fpga_Man_t * p, int fResynthesis )         { p->fResynthesis = fResynthesis;  }
 void            Fpga_ManSetDelayLimit( Fpga_Man_t * p, float DelayLimit )    { p->DelayLimit   = DelayLimit;    }
 void            Fpga_ManSetAreaLimit( Fpga_Man_t * p, float AreaLimit )      { p->AreaLimit    = AreaLimit;     }
 void            Fpga_ManSetTimeLimit( Fpga_Man_t * p, float TimeLimit )      { p->TimeLimit    = TimeLimit;     }
@@ -69,7 +66,6 @@ void            Fpga_ManSetChoiceNodeNum( Fpga_Man_t * p, int nChoiceNodes ) { p
 void            Fpga_ManSetChoiceNum( Fpga_Man_t * p, int nChoices )         { p->nChoices = nChoices;          }   
 void            Fpga_ManSetVerbose( Fpga_Man_t * p, int fVerbose )           { p->fVerbose = fVerbose;          }   
 void            Fpga_ManSetLatchNum( Fpga_Man_t * p, int nLatches )          { p->nLatches = nLatches;          }   
-void            Fpga_ManSetSequential( Fpga_Man_t * p, int fSequential )     { p->fSequential = fSequential;    }   
 void            Fpga_ManSetName( Fpga_Man_t * p, char * pFileName )          { p->pFileName = pFileName;        }   
 
 /**Function*************************************************************
@@ -170,8 +166,6 @@ Fpga_Man_t * Fpga_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->nVarsMax  = p->pLutLib->LutMax;
     p->fVerbose  = fVerbose;
     p->fAreaRecovery = 1;
-    p->fTree     = 0;
-    p->fRefCount = 1;
     p->fEpsilon  = (float)0.001;
 
     Fpga_TableCreate( p );
@@ -181,13 +175,14 @@ Fpga_Man_t * Fpga_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->mmCuts   = Extra_MmFixedStart( sizeof(Fpga_Cut_t) );
 
     assert( p->nVarsMax > 0 );
-    Fpga_MappingSetupTruthTables( p->uTruths );
+//    Fpga_MappingSetupTruthTables( p->uTruths );
 
     // make sure the constant node will get index -1
     p->nNodes = -1;
     // create the constant node
     p->pConst1 = Fpga_NodeCreate( p, NULL, NULL );
-    p->vNodesAll = Fpga_NodeVecAlloc( 100 );
+    p->vNodesAll = Fpga_NodeVecAlloc( 1000 );
+    p->vMapping = Fpga_NodeVecAlloc( 1000 );
 
     // create the PI nodes
     p->nInputs = nInputs;
@@ -216,27 +211,23 @@ Fpga_Man_t * Fpga_ManCreate( int nInputs, int nOutputs, int fVerbose )
 void Fpga_ManFree( Fpga_Man_t * p )
 {
 //    Fpga_ManStats( p );
-
 //    int i;
 //    for ( i = 0; i < p->vNodesAll->nSize; i++ )
 //        Fpga_NodeVecFree( p->vNodesAll->pArray[i]->vFanouts );
 //    Fpga_NodeVecFree( p->pConst1->vFanouts );
+    if ( p->vMapping )
+        Fpga_NodeVecFree( p->vMapping );
     if ( p->vAnds )    
         Fpga_NodeVecFree( p->vAnds );
     if ( p->vNodesAll )    
         Fpga_NodeVecFree( p->vNodesAll );
     Extra_MmFixedStop( p->mmNodes, 0 );
     Extra_MmFixedStop( p->mmCuts, 0 );
+    FREE( p->ppOutputNames );
     FREE( p->pInputArrivals );
     FREE( p->pInputs );
     FREE( p->pOutputs );
     FREE( p->pBins );
-    FREE( p->ppOutputNames );
-    if ( p->pSimInfo )
-    {
-    FREE( p->pSimInfo[0] );
-    FREE( p->pSimInfo );
-    }
     FREE( p );
 }
 
@@ -316,19 +307,18 @@ Fpga_Node_t * Fpga_NodeCreate( Fpga_Man_t * p, Fpga_Node_t * p1, Fpga_Node_t * p
     // set the level of this node
     if ( p1 ) 
     {
+#ifdef FPGA_ALLOCATE_FANOUT
         // create the fanout info
         Fpga_NodeAddFaninFanout( Fpga_Regular(p1), pNode );
         Fpga_NodeAddFaninFanout( Fpga_Regular(p2), pNode );
+#endif
         // compute the level
         pNode->Level = 1 + FPGA_MAX(Fpga_Regular(p1)->Level, Fpga_Regular(p2)->Level);
         pNode->fInv  = Fpga_NodeIsSimComplement(p1) & Fpga_NodeIsSimComplement(p2);
     }
-    // reference the inputs (will be used to compute the number of fanouts)
-    if ( p->fRefCount )
-    {
-        if ( p1 ) Fpga_NodeRef(p1);
-        if ( p2 ) Fpga_NodeRef(p2);
-    }
+    // reference the inputs 
+    if ( p1 ) Fpga_NodeRef(p1);
+    if ( p2 ) Fpga_NodeRef(p2);
     return pNode;
 }
 
diff --git a/src/map/fpga/fpgaCut.c b/src/map/fpga/fpgaCut.c
index 27079953..5b5fbe69 100644
--- a/src/map/fpga/fpgaCut.c
+++ b/src/map/fpga/fpgaCut.c
@@ -206,8 +206,9 @@ Fpga_Cut_t * Fpga_CutCompute( Fpga_Man_t * p, Fpga_CutTable_t * pTable, Fpga_Nod
     Fpga_Node_t * pTemp;
     Fpga_Cut_t * pList, * pList1, * pList2;
     Fpga_Cut_t * pCut;
-    int fPivot1 = p->fTree && (Fpga_NodeReadRef(pNode->p1)>2);
-    int fPivot2 = p->fTree && (Fpga_NodeReadRef(pNode->p2)>2);
+    int fTree = 0;
+    int fPivot1 = fTree && (Fpga_NodeReadRef(pNode->p1)>2);
+    int fPivot2 = fTree && (Fpga_NodeReadRef(pNode->p2)>2);
 
     // if the cuts are computed return them
     if ( pNode->pCuts )
diff --git a/src/map/fpga/fpgaFanout.c b/src/map/fpga/fpgaFanout.c
index 50809f65..0a34ff43 100644
--- a/src/map/fpga/fpgaFanout.c
+++ b/src/map/fpga/fpgaFanout.c
@@ -18,6 +18,8 @@
 
 #include "fpgaInt.h"
 
+#ifdef MAP_ALLOCATE_FANOUT
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -26,7 +28,6 @@
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
   Synopsis    [Add the fanout to the node.]
@@ -136,4 +137,5 @@ int Fpga_NodeGetFanoutNum( Fpga_Node_t * pNode )
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif
 
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index 63308d53..95203378 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -35,6 +35,9 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
  
+// uncomment to have fanouts represented in the mapping graph
+//#define FPGA_ALLOCATE_FANOUT  1
+
 ////////////////////////////////////////////////////////////////////////
 ///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
@@ -104,10 +107,11 @@ struct Fpga_ManStruct_t_
     Fpga_Node_t **      pOutputs;      // the array of outputs
     int                 nOutputs;      // the number of outputs
     int                 nNodes;        // the total number of nodes
-    Fpga_Node_t *       pConst1;       // the constant 1 node
-    Fpga_NodeVec_t *    vAnds;         // the array of pointer to nodes by number
-    Fpga_NodeVec_t *    vNodesAll;     // the array of pointer to nodes by number
     int                 nLatches;      // the number of latches in the circuit
+    Fpga_Node_t *       pConst1;       // the constant 1 node
+    Fpga_NodeVec_t *    vNodesAll;     // the nodes by number
+    Fpga_NodeVec_t *    vAnds;         // the nodes reachable from COs
+    Fpga_NodeVec_t *    vMapping;      // the nodes used in the current mapping
 
     // info about the original circuit
     char *              pFileName;     // the file name
@@ -116,12 +120,12 @@ struct Fpga_ManStruct_t_
 
     // mapping parameters
     int                 nVarsMax;      // the max number of variables
-    int                 fTree;         // the flag to enable tree mapping
-    int                 fPower;        // the flag to enable power optimization
+//    int                 fTree;         // the flag to enable tree mapping
+//    int                 fPower;        // the flag to enable power optimization
     int                 fAreaRecovery; // the flag to use area flow as the first parameter
     int                 fVerbose;      // the verbosiness flag
-    int                 fRefCount;     // enables reference counting
-    int                 fSequential;   // use sequential mapping
+//    int                 fRefCount;     // enables reference counting
+//    int                 fSequential;   // use sequential mapping
     int                 nTravIds;
 
     // support of choice nodes
@@ -133,16 +137,12 @@ struct Fpga_ManStruct_t_
  
     // the supergate library
     Fpga_LutLib_t *     pLutLib;       // the current LUT library
-    unsigned            uTruths[6][2]; // the elementary truth tables
+//    unsigned            uTruths[6][2]; // the elementary truth tables
 
     // the memory managers
     Extra_MmFixed_t *   mmNodes;       // the memory manager for nodes
     Extra_MmFixed_t *   mmCuts;        // the memory manager for cuts
 
-    // simulation info from the FRAIG manager
-    int                 nSimRounds;    // the number of words in the simulation info
-    unsigned **         pSimInfo;      // the simulation info for each PI
-
     // resynthesis parameters
     int                 fResynthesis;  // the resynthesis flag
     float               fRequiredGlo;  // the global required times
@@ -203,12 +203,14 @@ struct Fpga_NodeStruct_t_
     Fpga_Node_t *       p2;            // the second child
     Fpga_Node_t *       pNextE;        // the next functionally equivalent node
     Fpga_Node_t *       pRepr;         // the representative of the functionally equivalent class
-//    Fpga_NodeVec_t *    vFanouts;      // the array of fanouts of the node
 
+#ifdef FPGA_ALLOCATE_FANOUT
     // representation of node's fanouts
     Fpga_Node_t *       pFanPivot;     // the first fanout of this node
     Fpga_Node_t *       pFanFanin1;    // the next fanout of p1
     Fpga_Node_t *       pFanFanin2;    // the next fanout of p2
+//    Fpga_NodeVec_t *    vFanouts;      // the array of fanouts of the gate
+#endif
 
     // the delay information
     float               tRequired;     // the best area flow 
@@ -335,8 +337,6 @@ extern void              Fpga_TimeComputeRequiredGlobal( Fpga_Man_t * p );
 extern void              Fpga_TimeComputeRequired( Fpga_Man_t * p, float fRequired );
 extern void              Fpga_TimePropagateRequired( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes );
 extern void              Fpga_TimePropagateArrival( Fpga_Man_t * p );
-/*=== fpgaTruth.c ===============================================================*/
-extern void              Fpga_MappingTruths( Fpga_Man_t * pMan );
 /*=== fpgaVec.c =============================================================*/
 extern Fpga_NodeVec_t *  Fpga_NodeVecAlloc( int nCap );
 extern void              Fpga_NodeVecFree( Fpga_NodeVec_t * p );
@@ -359,23 +359,11 @@ extern void              Fpga_NodeVecReverse( Fpga_NodeVec_t * vNodes );
 /*=== fpgaUtils.c ===============================================================*/
 extern Fpga_NodeVec_t *  Fpga_MappingDfs( Fpga_Man_t * pMan, int fCollectEquiv );
 extern Fpga_NodeVec_t *  Fpga_MappingDfsNodes( Fpga_Man_t * pMan, Fpga_Node_t ** ppNodes, int nNodes, int fEquiv );
-extern Fpga_NodeVec_t *  Fpga_MappingDfsCutsNode( Fpga_Man_t * pMan, Fpga_Node_t * pNode );
-//extern Sat_IntVec_t *    Fpga_MappingDfsNodesSat( Fpga_Man_t * pMan, Fpga_Node_t ** ppNodes, int nNodes );
-extern Fpga_NodeVec_t *  Fpga_MappingDfsCuts( Fpga_Man_t * pMan );
 extern int               Fpga_CountLevels( Fpga_Man_t * pMan );
-extern int               Fpga_CountLevelsNodes( Fpga_Man_t * pMan, Fpga_Node_t ** ppRoots, int nRoots );
-extern void              Fpga_MappingMarkUsed( Fpga_Man_t * pMan );
 extern float             Fpga_MappingGetAreaFlow( Fpga_Man_t * p );
 extern float             Fpga_MappingArea( Fpga_Man_t * pMan );
-extern float             Fpga_MappingComputeCutAreas( Fpga_Man_t * pMan );
+extern float             Fpga_MappingAreaTrav( Fpga_Man_t * pMan );
 extern float             Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan );
-extern Fpga_NodeVec_t *  Fpga_MappingCollectRefed( Fpga_Man_t * pMan );
-extern int               Fpga_MappingCountLevels( Fpga_Man_t * pMan );
-extern void              Fpga_MappingUnmark( Fpga_Man_t * pMan );
-extern void              Fpga_MappingUnmark_rec( Fpga_Node_t * pNode );
-extern void              Fpga_MappingMark_rec( Fpga_Node_t * pNode );
-extern void              Fpga_MappedMark_rec( Fpga_Node_t * pNode );
-extern void              Fpga_MappedUnmark_rec( Fpga_Node_t * pNode );
 extern void              Fpga_MappingPrintOutputArrivals( Fpga_Man_t * p );
 extern void              Fpga_MappingSetupTruthTables( unsigned uTruths[][2] );
 extern void              Fpga_MappingSetupMask( unsigned uMask[], int nVarsMax );
@@ -383,7 +371,7 @@ extern void              Fpga_MappingSortByLevel( Fpga_Man_t * pMan, Fpga_NodeVe
 extern Fpga_NodeVec_t *  Fpga_DfsLim( Fpga_Man_t * pMan, Fpga_Node_t * pNode, int nLevels );
 extern Fpga_NodeVec_t *  Fpga_MappingLevelize( Fpga_Man_t * pMan, Fpga_NodeVec_t * vNodes );
 extern float             Fpga_MappingPrintSwitching( Fpga_Man_t * pMan );
-extern int               Fpga_GetMaxLevel( Fpga_Man_t * pMan );
+extern int               Fpga_MappingMaxLevel( Fpga_Man_t * pMan );
 extern void              Fpga_ManReportChoices( Fpga_Man_t * pMan );
 extern void              Fpga_MappingSetChoiceLevels( Fpga_Man_t * pMan );
 
diff --git a/src/map/fpga/fpgaMatch.c b/src/map/fpga/fpgaMatch.c
index 599662f7..63ee682d 100644
--- a/src/map/fpga/fpgaMatch.c
+++ b/src/map/fpga/fpgaMatch.c
@@ -777,59 +777,6 @@ float Fpga_FindBestNode( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes, Fpga_Node_t **
     return Gain;
 }
 
-/**function*************************************************************
-
-  synopsis    [Performs area minimization using a heuristic algorithm.]
-
-  description []
-               
-  sideeffects []
-
-  seealso     []
-
-***********************************************************************/
-void Fpga_MappingExplore( Fpga_Man_t * p )
-{
-    Fpga_Cut_t * pCutBest;
-    Fpga_Node_t * pNodeBest;
-    Fpga_NodeVec_t * vNodes;
-    float Area, Gain, CutArea1, CutArea2;
-    int i;
-
-    // compute the arrival times
-    Fpga_TimePropagateArrival( p );
-    p->fRequiredGlo = Fpga_TimeComputeArrivalMax( p );
-    Fpga_TimeComputeRequired( p, p->fRequiredGlo );
-
-    // assign the refs
-    Area = Fpga_MappingSetRefsAndArea( p );
-    // collect the nodes
-    vNodes = Fpga_MappingCollectRefed( p );
-    // find the best node to update
-    for ( i = 0; Gain = Fpga_FindBestNode(p, vNodes, &pNodeBest, &pCutBest); i++ )
-    {
-        // update the node
-        assert( pNodeBest->pCutBest != pCutBest );
-        // deref the current cut
-        CutArea1 = Fpga_CutDeref( p, pNodeBest, pNodeBest->pCutBest, 0 );
-        // ref the new cut
-        CutArea2 = Fpga_CutRef( p, pNodeBest, pCutBest, 0 );
-        assert( CutArea1 - CutArea2 == Gain );
-        printf( "Iteration %2d: Gain = %5.2f.\n", i, Gain );
-        // update the node
-        pNodeBest->pCutBest = pCutBest;
-        // collect new nodes
-        Fpga_NodeVecFree( vNodes );
-        vNodes = Fpga_MappingCollectRefed( p );
-        // compute the arrival and required times
-        Fpga_TimePropagateArrival( p );
-        Fpga_TimeComputeRequired( p, p->fRequiredGlo );
-    }
-
-
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/fpga/fpgaTime.c b/src/map/fpga/fpgaTime.c
index 066ae215..6cbe16f9 100644
--- a/src/map/fpga/fpgaTime.c
+++ b/src/map/fpga/fpgaTime.c
@@ -128,21 +128,15 @@ void Fpga_TimeComputeRequiredGlobal( Fpga_Man_t * p )
 ***********************************************************************/
 void Fpga_TimeComputeRequired( Fpga_Man_t * p, float fRequired )
 {
-    Fpga_NodeVec_t * vNodes;
     int i;
-
     // clean the required times and the fanout counts for all nodes
     for ( i = 0; i < p->vAnds->nSize; i++ )
         p->vAnds->pArray[i]->tRequired = FPGA_FLOAT_LARGE;
-
     // set the required times for the POs
     for ( i = 0; i < p->nOutputs; i++ )
         Fpga_Regular(p->pOutputs[i])->tRequired = fRequired;
-
     // collect nodes reachable from POs in the DFS order through the best cuts
-    vNodes = Fpga_MappingDfsCuts( p );
-    Fpga_TimePropagateRequired( p, vNodes );
-    Fpga_NodeVecFree( vNodes );
+    Fpga_TimePropagateRequired( p, p->vMapping );
 }
 
 /**Function*************************************************************
@@ -163,7 +157,9 @@ void Fpga_TimePropagateRequired( Fpga_Man_t * p, Fpga_NodeVec_t * vNodes )
     int i, k;
 
     // sorts the nodes in the decreasing order of levels
-    Fpga_MappingSortByLevel( p, vNodes, 0 );
+//    Fpga_MappingSortByLevel( p, vNodes, 0 );
+    // the nodes area already sorted in Fpga_MappingSetRefsAndArea()
+
     // go through the nodes in the reverse topological order
     for ( k = 0; k < vNodes->nSize; k++ )
     {
diff --git a/src/map/fpga/fpgaUtils.c b/src/map/fpga/fpgaUtils.c
index fc67d52b..bf334afa 100644
--- a/src/map/fpga/fpgaUtils.c
+++ b/src/map/fpga/fpgaUtils.c
@@ -24,15 +24,10 @@
 
 static void  Fpga_MappingDfs_rec( Fpga_Node_t * pNode, Fpga_NodeVec_t * vNodes, int fCollectEquiv );
 static void  Fpga_MappingDfsCuts_rec( Fpga_Node_t * pNode, Fpga_NodeVec_t * vNodes );
-static float Fpga_MappingArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_NodeVec_t * vNodes );
-static int   Fpga_MappingCountLevels_rec( Fpga_Node_t * pNode );
-static void  Fpga_MappingMarkUsed_rec( Fpga_Node_t * pNode );
 static int   Fpga_MappingCompareOutputDelay( int * pOut1, int * pOut2 );
-static float Fpga_MappingSetRefsAndArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode );
-static Fpga_Man_t * s_pMan = NULL;
-
 static void  Fpga_DfsLim_rec( Fpga_Node_t * pNode, int Level, Fpga_NodeVec_t * vNodes );
-static int Fpga_CollectNodeTfo_rec( Fpga_Node_t * pNode, Fpga_Node_t * pPivot, Fpga_NodeVec_t * vVisited, Fpga_NodeVec_t * vTfo );
+static int   Fpga_CollectNodeTfo_rec( Fpga_Node_t * pNode, Fpga_Node_t * pPivot, Fpga_NodeVec_t * vVisited, Fpga_NodeVec_t * vTfo );
+static Fpga_Man_t * s_pMan = NULL;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -131,184 +126,6 @@ Fpga_NodeVec_t * Fpga_MappingDfsNodes( Fpga_Man_t * pMan, Fpga_Node_t ** ppNodes
     return vNodes;
 }
 
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fpga_CountLevels( Fpga_Man_t * pMan )
-{
-    int i, LevelsMax, LevelsCur;
-    // perform the traversal
-    LevelsMax = -1;
-    for ( i = 0; i < pMan->nOutputs; i++ )
-    {
-        LevelsCur = Fpga_Regular(pMan->pOutputs[i])->Level;
-        if ( LevelsMax < LevelsCur )
-            LevelsMax = LevelsCur;
-    }
-    return LevelsMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fpga_CountLevelsNodes( Fpga_Man_t * pMan, Fpga_Node_t ** ppRoots, int nRoots )
-{
-    int i, LevelsMax, LevelsCur;
-    // perform the traversal
-    LevelsMax = -1;
-    for ( i = 0; i < nRoots; i++ )
-    {
-        LevelsCur = Fpga_Regular(ppRoots[i])->Level;
-        if ( LevelsMax < LevelsCur )
-            LevelsMax = LevelsCur;
-    }
-    return LevelsMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the DFS ordering of the nodes visible in current mapping.]
-
-  Description [The node is visible if it appears as a root of one of the best
-  cuts (that is cuts selected for the current mapping).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fpga_NodeVec_t * Fpga_MappingDfsCuts( Fpga_Man_t * pMan )
-{
-    Fpga_NodeVec_t * vNodes;
-    int i;
-    // perform the traversal
-    vNodes = Fpga_NodeVecAlloc( 100 );
-    for ( i = 0; i < pMan->nOutputs; i++ )
-        Fpga_MappingDfsCuts_rec( Fpga_Regular(pMan->pOutputs[i]), vNodes );
-    for ( i = 0; i < vNodes->nSize; i++ )
-        vNodes->pArray[i]->fMark0 = 0;
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the DFS ordering of the nodes visible in current mapping.]
-
-  Description [The node is visible if it appears as a root of one of the best
-  cuts (that is cuts selected for the current mapping).]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fpga_NodeVec_t * Fpga_MappingDfsCutsNode( Fpga_Man_t * pMan, Fpga_Node_t * pNode )
-{
-    Fpga_NodeVec_t * vNodes;
-    int i;
-    // perform the traversal
-    vNodes = Fpga_NodeVecAlloc( 100 );
-    Fpga_MappingDfsCuts_rec( pNode, vNodes );
-    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 Fpga_MappingDfsCuts_rec( Fpga_Node_t * pNode, Fpga_NodeVec_t * vNodes )
-{
-    int i;
-    assert( !Fpga_IsComplement(pNode) );
-    if ( !Fpga_NodeIsAnd(pNode) )
-        return;
-    if ( pNode->fMark0 )
-        return;
-    assert( pNode->pCutBest != NULL );
-    // visit the transitive fanin of the selected cut
-    for ( i = 0; i < pNode->pCutBest->nLeaves; i++ )
-        Fpga_MappingDfsCuts_rec( pNode->pCutBest->ppLeaves[i], vNodes );
-    // make sure the node is not visited through the fanin nodes
-    assert( pNode->fMark0 == 0 );
-    // mark the node as visited
-    pNode->fMark0 = 1;
-    // add the node to the list
-    Fpga_NodeVecPush( vNodes, pNode );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Marks the nodes used in the mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fpga_MappingMarkUsed( Fpga_Man_t * pMan )
-{
-    int i;
-    for ( i = 0; i < pMan->nOutputs; i++ )
-        Fpga_MappingMarkUsed_rec( Fpga_Regular(pMan->pOutputs[i]) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fpga_MappingMarkUsed_rec( Fpga_Node_t * pNode )
-{
-    int i;
-    assert( !Fpga_IsComplement(pNode) );
-    if ( pNode->fUsed )
-        return;
-    pNode->fUsed = 1;
-    if ( !Fpga_NodeIsAnd(pNode) )
-        return;
-    assert( pNode->pCutBest != NULL );
-    // visit the transitive fanin of the selected cut
-    for ( i = 0; i < pNode->pCutBest->nLeaves; i++ )
-        Fpga_MappingMarkUsed_rec( pNode->pCutBest->ppLeaves[i] );
-}
-
-
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -346,22 +163,16 @@ float Fpga_MappingGetAreaFlow( Fpga_Man_t * p )
 ***********************************************************************/
 float Fpga_MappingArea( Fpga_Man_t * pMan )
 {
-    Fpga_NodeVec_t * vNodes;
+    Fpga_Node_t * pNode;
     float aTotal;
     int i;
     // perform the traversal
     aTotal = 0;
-    vNodes = Fpga_NodeVecAlloc( 100 );
-    for ( i = 0; i < pMan->nOutputs; i++ )
+    for ( i = 0; i < pMan->vMapping->nSize; i++ )
     {
-        aTotal += Fpga_MappingArea_rec( pMan, Fpga_Regular(pMan->pOutputs[i]), vNodes );
-        // add the area for single-input nodes (if any) at the POs
-//        if ( Fpga_NodeIsVar(pMan->pOutputs[i]) || Fpga_IsComplement(pMan->pOutputs[i]) )
-//            aTotal += pMan->pLutLib->pLutAreas[1];
+        pNode = pMan->vMapping->pArray[i];
+        aTotal += pMan->pLutLib->pLutAreas[pNode->pCutBest->nLeaves];
     }
-    for ( i = 0; i < vNodes->nSize; i++ )
-        vNodes->pArray[i]->fMark0 = 0;
-    Fpga_NodeVecFree( vNodes );
     return aTotal;
 }
 
@@ -401,10 +212,9 @@ float Fpga_MappingArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_NodeVec
     return aArea;
 }
 
-
 /**Function*************************************************************
 
-  Synopsis    [Sets the correct reference counts for the mapping.]
+  Synopsis    [Computes the area of the current mapping.]
 
   Description []
                
@@ -413,55 +223,22 @@ float Fpga_MappingArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_NodeVec
   SeeAlso     []
 
 ***********************************************************************/
-float Fpga_MappingComputeCutAreas( Fpga_Man_t * pMan )
+float Fpga_MappingAreaTrav( Fpga_Man_t * pMan )
 {
     Fpga_NodeVec_t * vNodes;
-    Fpga_Node_t * pNode;
-    float Area = 0;
+    float aTotal;
     int i;
-    // collect nodes reachable from POs in the DFS order through the best cuts
-    vNodes = Fpga_MappingDfsCuts( pMan );
+    // perform the traversal
+    aTotal = 0;
+    vNodes = Fpga_NodeVecAlloc( 100 );
+    for ( i = 0; i < pMan->nOutputs; i++ )
+        aTotal += Fpga_MappingArea_rec( pMan, Fpga_Regular(pMan->pOutputs[i]), vNodes );
     for ( i = 0; i < vNodes->nSize; i++ )
-    {
-        pNode = vNodes->pArray[i];
-        pNode->pCutBest->aFlow = Fpga_CutGetAreaRefed( pMan, pNode->pCutBest );
-        Area += pMan->pLutLib->pLutAreas[pNode->pCutBest->nLeaves];
-    }
+        vNodes->pArray[i]->fMark0 = 0;
     Fpga_NodeVecFree( vNodes );
-    return Area;
+    return aTotal;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Sets the correct reference counts for the mapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-float Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan )
-{
-    Fpga_Node_t * pNode;
-    float aArea;
-    int i;
-    // clean all references
-    for ( i = 0; i < pMan->vNodesAll->nSize; i++ )
-        pMan->vNodesAll->pArray[i]->nRefs = 0;
-    // collect nodes reachable from POs in the DFS order through the best cuts
-    aArea = 0;
-    for ( i = 0; i < pMan->nOutputs; i++ )
-    {
-        pNode = Fpga_Regular(pMan->pOutputs[i]);
-        if ( pNode == pMan->pConst1 )
-            continue;
-        aArea += Fpga_MappingSetRefsAndArea_rec( pMan, pNode );
-        pNode->nRefs++;
-    }
-    return aArea;
-}
 
 /**Function*************************************************************
 
@@ -474,7 +251,7 @@ float Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-float Fpga_MappingSetRefsAndArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode )
+float Fpga_MappingSetRefsAndArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode, Fpga_Node_t ** ppStore )
 {
     float aArea;
     int i;
@@ -484,217 +261,63 @@ float Fpga_MappingSetRefsAndArea_rec( Fpga_Man_t * pMan, Fpga_Node_t * pNode )
     if ( !Fpga_NodeIsAnd(pNode) )
         return 0;
     assert( pNode->pCutBest != NULL );
+    // store the node in the structure by level
+    pNode->pData0 = (char *)ppStore[pNode->Level]; 
+    ppStore[pNode->Level] = pNode;
     // visit the transitive fanin of the selected cut
     aArea = pMan->pLutLib->pLutAreas[pNode->pCutBest->nLeaves];
     for ( i = 0; i < pNode->pCutBest->nLeaves; i++ )
-        aArea += Fpga_MappingSetRefsAndArea_rec( pMan, pNode->pCutBest->ppLeaves[i] );
+        aArea += Fpga_MappingSetRefsAndArea_rec( pMan, pNode->pCutBest->ppLeaves[i], ppStore );
     return aArea;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collect the referenced nodes.]
+  Synopsis    [Sets the correct reference counts for the mapping.]
 
-  Description []
+  Description [Collects the nodes in reverse topological order
+  and places in them in array pMan->vMapping.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Fpga_NodeVec_t * Fpga_MappingCollectRefed( Fpga_Man_t * pMan )
+float Fpga_MappingSetRefsAndArea( Fpga_Man_t * pMan )
 {
-    Fpga_NodeVec_t * vNodes;
-    int i;
-    vNodes = Fpga_NodeVecAlloc( 100 );
-    for ( i = 0; i < pMan->vNodesAll->nSize; i++ )
-    {
-        if ( Fpga_NodeIsVar(pMan->vNodesAll->pArray[i]) )
-            continue;
-        if ( pMan->vNodesAll->pArray[i]->nRefs )
-            Fpga_NodeVecPush( vNodes, pMan->vNodesAll->pArray[i] );
-    }
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+    Fpga_Node_t * pNode, ** ppStore;
+    float aArea;
+    int i, LevelMax;
 
-  Description []
-               
-  SideEffects [Note that this procedure will reassign the levels assigned
-  originally by NodeCreate() because it counts the number of levels with 
-  choices differently!]
+    // clean all references
+    for ( i = 0; i < pMan->vNodesAll->nSize; i++ )
+        pMan->vNodesAll->pArray[i]->nRefs = 0;
 
-  SeeAlso     []
+    // allocate place to store the nodes
+    LevelMax = Fpga_MappingMaxLevel( pMan );
+    ppStore = ALLOC( Fpga_Node_t *, LevelMax + 1 );
+    memset( ppStore, 0, sizeof(Fpga_Node_t *) * (LevelMax + 1) );
 
-***********************************************************************/
-int Fpga_MappingCountLevels( Fpga_Man_t * pMan )
-{
-    int i, LevelsMax, LevelsCur;
-    // perform the traversal
-    LevelsMax = -1;
-    for ( i = 0; i < pMan->nOutputs; i++ )
-    {
-        LevelsCur = Fpga_MappingCountLevels_rec( Fpga_Regular(pMan->pOutputs[i]) );
-        if ( LevelsMax < LevelsCur )
-            LevelsMax = LevelsCur;
-    }
+    // collect nodes reachable from POs in the DFS order through the best cuts
+    aArea = 0;
     for ( i = 0; i < pMan->nOutputs; i++ )
-        Fpga_MappingUnmark_rec( Fpga_Regular(pMan->pOutputs[i]) );
-    return LevelsMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes the number of logic levels.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fpga_MappingCountLevels_rec( Fpga_Node_t * pNode )
-{
-    int Level1, Level2;
-    assert( !Fpga_IsComplement(pNode) );
-    if ( !Fpga_NodeIsAnd(pNode) )
     {
-        pNode->Level = 0;
-        return 0;
+        pNode = Fpga_Regular(pMan->pOutputs[i]);
+        if ( pNode == pMan->pConst1 )
+            continue;
+        aArea += Fpga_MappingSetRefsAndArea_rec( pMan, pNode, ppStore );
+        pNode->nRefs++;
     }
-    if ( pNode->fMark0 )
-        return pNode->Level;
-    pNode->fMark0 = 1;
-    // visit the transitive fanin
-    Level1 = Fpga_MappingCountLevels_rec( Fpga_Regular(pNode->p1) );
-    Level2 = Fpga_MappingCountLevels_rec( Fpga_Regular(pNode->p2) );
-    // set the number of levels
-    pNode->Level = 1 + ((Level1>Level2)? Level1: Level2);
-    return pNode->Level;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Unmarks the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fpga_MappingUnmark( Fpga_Man_t * pMan )
-{
-    int i;
-    for ( i = 0; i < pMan->nOutputs; i++ )
-        Fpga_MappingUnmark_rec( Fpga_Regular(pMan->pOutputs[i]) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively unmarks the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fpga_MappingUnmark_rec( Fpga_Node_t * pNode )
-{
-    assert( !Fpga_IsComplement(pNode) );
-    if ( pNode->fMark0 == 0 )
-        return;
-    pNode->fMark0 = 0;
-    if ( !Fpga_NodeIsAnd(pNode) )
-        return;
-    Fpga_MappingUnmark_rec( Fpga_Regular(pNode->p1) );
-    Fpga_MappingUnmark_rec( Fpga_Regular(pNode->p2) );
-    // visit the equivalent nodes
-    if ( pNode->pNextE )
-        Fpga_MappingUnmark_rec( pNode->pNextE );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively unmarks the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fpga_MappingMark_rec( Fpga_Node_t * pNode )
-{
-    assert( !Fpga_IsComplement(pNode) );
-    if ( pNode->fMark0 == 1 )
-        return;
-    pNode->fMark0 = 1;
-    if ( !Fpga_NodeIsAnd(pNode) )
-        return;
-    Fpga_MappingMark_rec( Fpga_Regular(pNode->p1) );
-    Fpga_MappingMark_rec( Fpga_Regular(pNode->p2) );
-}
-
-/**Function*************************************************************
 
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fpga_MappedMark_rec( Fpga_Node_t * pNode )
-{
-    int i;
-    assert( !Fpga_IsComplement(pNode) );
-    if ( pNode->fMark0 == 1 )
-        return;
-    pNode->fMark0 = 1;
-    if ( !Fpga_NodeIsAnd(pNode) )
-        return;
-    assert( pNode->pCutBest != NULL );
-    // visit the transitive fanin of the selected cut
-    for ( i = 0; i < pNode->pCutBest->nLeaves; i++ )
-        Fpga_MappedMark_rec( pNode->pCutBest->ppLeaves[i] );
+    // reconnect the nodes in reverse topological order
+    pMan->vMapping->nSize = 0;
+    for ( i = LevelMax; i > 0; i-- )
+        for ( pNode = ppStore[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 )
+            Fpga_NodeVecPush( pMan->vMapping, pNode );
+    free( ppStore );
+    return aArea;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Recursively unmarks the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fpga_MappedUnmark_rec( Fpga_Node_t * pNode )
-{
-    int i;
-    assert( !Fpga_IsComplement(pNode) );
-    if ( pNode->fMark0 == 0 )
-        return;
-    pNode->fMark0 = 0;
-    if ( !Fpga_NodeIsAnd(pNode) )
-        return;
-    assert( pNode->pCutBest != NULL );
-    // visit the transitive fanin of the selected cut
-    for ( i = 0; i < pNode->pCutBest->nLeaves; i++ )
-        Fpga_MappedUnmark_rec( pNode->pCutBest->ppLeaves[i] );
-}
 
 /**Function*************************************************************
 
@@ -710,7 +333,7 @@ void Fpga_MappedUnmark_rec( Fpga_Node_t * pNode )
 void Fpga_MappingPrintOutputArrivals( Fpga_Man_t * p )
 {
     Fpga_Node_t * pNode;
-    int fCompl, Limit, i;
+    int fCompl, Limit, MaxNameSize, i;
     int * pSorted;
 
     // sort outputs by arrival time
@@ -723,15 +346,21 @@ void Fpga_MappingPrintOutputArrivals( Fpga_Man_t * p )
     assert( Fpga_MappingCompareOutputDelay( pSorted, pSorted + p->nOutputs - 1 ) <= 0 );
     s_pMan = NULL;
 
-    // print the latest outputs
+    // determine max size of the node's name
+    MaxNameSize = 0;
     Limit = (p->nOutputs > 5)? 5 : p->nOutputs;
     for ( i = 0; i < Limit; i++ )
+        if ( MaxNameSize < (int)strlen(p->ppOutputNames[pSorted[i]]) )
+            MaxNameSize = strlen(p->ppOutputNames[pSorted[i]]);
+
+    // print the latest outputs
+    for ( i = 0; i < Limit; i++ )
     {
         // get the i-th latest output
         pNode  = Fpga_Regular(p->pOutputs[pSorted[i]]);
         fCompl = Fpga_IsComplement(p->pOutputs[pSorted[i]]);
         // print out the best arrival time
-        printf( "Output  %20s : ", p->ppOutputNames[pSorted[i]] );
+        printf( "Output  %-*s : ", MaxNameSize + 3, p->ppOutputNames[pSorted[i]] );
         printf( "Delay = %8.2f  ",     (double)pNode->pCutBest->tArrival );
         if ( fCompl )
             printf( "NEG" );
@@ -1169,7 +798,7 @@ float Fpga_MappingPrintSwitching( Fpga_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fpga_GetMaxLevel( Fpga_Man_t * pMan )
+int Fpga_MappingMaxLevel( Fpga_Man_t * pMan )
 {
     int nLevelMax, i;
     nLevelMax = 0;
@@ -1269,11 +898,11 @@ void Fpga_ManReportChoices( Fpga_Man_t * pMan )
     int i, LevelMax1, LevelMax2;
 
     // report the number of levels
-    LevelMax1 = Fpga_GetMaxLevel( pMan );
+    LevelMax1 = Fpga_MappingMaxLevel( pMan );
     pMan->nTravIds++;
     for ( i = 0; i < pMan->nOutputs; i++ )
         Fpga_MappingUpdateLevel_rec( pMan, Fpga_Regular(pMan->pOutputs[i]), 0 );
-    LevelMax2 = Fpga_GetMaxLevel( pMan );
+    LevelMax2 = Fpga_MappingMaxLevel( pMan );
 
     // report statistics about choices
     nChoiceNodes = nChoices = 0;
diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h
index 9ef8ee17..1322cdfa 100644
--- a/src/map/mapper/mapper.h
+++ b/src/map/mapper/mapper.h
@@ -152,8 +152,8 @@ extern void            Map_NodeSetChoice( Map_Man_t * pMan, Map_Node_t * pNodeOl
 
 /*=== resmCanon.c =============================================================*/
 extern int             Map_CanonComputeSlow( unsigned uTruths[][2], int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char * puPhases, unsigned uTruthRes[] );
+extern int             Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char * puPhases, unsigned uTruthRes[] );
 /*=== mapperCut.c =============================================================*/
-extern void            Map_MappingCreatePiCuts( Map_Man_t * p );
 extern Map_Cut_t *     Map_CutAlloc( Map_Man_t * p );
 /*=== mapperCutUtils.c =============================================================*/
 extern void            Map_CutCreateFromNode( Map_Man_t * p, Map_Super_t * pSuper, int iRoot, unsigned uPhaseRoot, 
diff --git a/src/map/mapper/mapperCanon.c b/src/map/mapper/mapperCanon.c
index c5186c7e..4937fd0e 100644
--- a/src/map/mapper/mapperCanon.c
+++ b/src/map/mapper/mapperCanon.c
@@ -154,6 +154,95 @@ void Map_CanonComputePhase6( unsigned uTruths[][2], int nVars, unsigned uTruth[]
         }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the N-canonical form of the Boolean function.]
+
+  Description [The N-canonical form is defined as the truth table with 
+  the minimum integer value. This function exhaustively enumerates 
+  through the complete set of 2^N phase assignments.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char * puPhases, unsigned uTruthRes[] )
+{
+    unsigned uTruth0, uTruth1;
+    unsigned uCanon0, uCanon1, uCanonBest;
+    int i, Limit;
+
+    if ( nVarsMax != 5 || nVarsReal < 5 )
+        return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes );
+
+    assert( nVarsMax == 5 );
+    uTruth0 = uTruth[0] & 0xFFFF;
+    uTruth1 = (uTruth[0] >> 16);
+    if ( uTruth1 == 0 )
+    {
+        uTruthRes[0] = p->uCanons[uTruth0];
+        uTruthRes[1] = uTruthRes[0];
+        Limit = (p->pCounters[uTruth0] > 4)? 4 : p->pCounters[uTruth0];
+        for ( i = 0; i < Limit; i++ )
+            puPhases[i] = p->uPhases[uTruth0][i];
+        return Limit;
+    }
+    else if ( uTruth0 == 0 )
+    {
+        uTruthRes[0] = p->uCanons[uTruth1];
+        uTruthRes[1] = uTruthRes[0];
+        Limit = (p->pCounters[uTruth1] > 4)? 4 : p->pCounters[uTruth1];
+        for ( i = 0; i < Limit; i++ )
+        {
+            puPhases[i] = p->uPhases[uTruth1][i];
+            puPhases[i] |= (1 << 4);
+        }
+        return Limit;
+    }
+    uCanon0 = p->uCanons[uTruth0];
+    uCanon1 = p->uCanons[uTruth1];
+    if ( uCanon0 && uCanon1 && uCanon0 > uCanon1 ) // using nCanon1 as the main one
+    {
+        assert( p->pCounters[uTruth1] > 0 );
+        uCanonBest = 0xFFFF;
+        for ( i = 0; i < p->pCounters[uTruth1]; i++ )
+        {
+            uCanon0 = Extra_TruthPolarize( uTruth0, p->uPhases[uTruth1][i], 4 );
+            if ( uCanonBest > uCanon0 )
+                uCanonBest = uCanon0;
+        }
+        uTruthRes[0] = (uCanon1 << 16) | uCanonBest;
+        uTruthRes[1] = uTruthRes[0];
+        Limit = (p->pCounters[uTruth1] > 4)? 4 : p->pCounters[uTruth1];
+        for ( i = 0; i < Limit; i++ )
+            puPhases[i] = p->uPhases[uTruth1][i];
+        return Limit;
+    }
+    else if ( uCanon0 && uCanon1 && uCanon0 < uCanon1 )
+    {
+        assert( p->pCounters[uTruth0] > 0 );
+        uCanonBest = 0xFFFF;
+        for ( i = 0; i < p->pCounters[uTruth0]; i++ )
+        {
+            uCanon1 = Extra_TruthPolarize( uTruth1, p->uPhases[uTruth0][i], 4 );
+            if ( uCanonBest > uCanon1 )
+                uCanonBest = uCanon1;
+        }
+        uTruthRes[0] = (uCanon0 << 16) | uCanonBest;
+        uTruthRes[1] = uTruthRes[0];
+        Limit = (p->pCounters[uTruth0] > 4)? 4 : p->pCounters[uTruth0];
+        for ( i = 0; i < Limit; i++ )
+        {
+            puPhases[i]  = p->uPhases[uTruth0][i];
+            puPhases[i] |= (1 << 4);
+        }
+        return Limit;
+    }
+    else
+        return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c
index 0014d48f..16cbfd5c 100644
--- a/src/map/mapper/mapperCore.c
+++ b/src/map/mapper/mapperCore.c
@@ -69,6 +69,7 @@ int Map_Mapping( Map_Man_t * p )
     Map_MappingTruths( p );
     p->timeTruth = clock() - clk;
     //////////////////////////////////////////////////////////////////////
+//PRT( "Truths", clock() - clk );
 
     //////////////////////////////////////////////////////////////////////
     // compute the minimum-delay mapping
diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c
index eb938847..dc056f34 100644
--- a/src/map/mapper/mapperCreate.c
+++ b/src/map/mapper/mapperCreate.c
@@ -196,6 +196,9 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->fEpsilon  = (float)0.001;
     assert( p->nVarsMax > 0 );
 
+    if ( p->nVarsMax == 5 )
+        Extra_Truth4VarN( &p->uCanons, &p->uPhases, &p->pCounters, 16 );
+
     // start various data structures
     Map_TableCreate( p );
     Map_MappingSetupTruthTables( p->uTruths );
@@ -211,8 +214,6 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->vNodesAll  = Map_NodeVecAlloc( 100 );
     p->vNodesTemp = Map_NodeVecAlloc( 100 );
     p->vMapping   = Map_NodeVecAlloc( 100 );
-    p->vInside    = Map_NodeVecAlloc( 100 );
-    p->vFanins    = Map_NodeVecAlloc( 100 );
     p->vVisited   = Map_NodeVecAlloc( 100 );
 
     // create the PI nodes
@@ -245,10 +246,6 @@ void Map_ManFree( Map_Man_t * p )
 //    for ( i = 0; i < p->vNodesAll->nSize; i++ )
 //        Map_NodeVecFree( p->vNodesAll->pArray[i]->vFanouts );
 //    Map_NodeVecFree( p->pConst1->vFanouts );
-    if ( p->vInside )    
-        Map_NodeVecFree( p->vInside );
-    if ( p->vFanins )    
-        Map_NodeVecFree( p->vFanins );
     if ( p->vAnds )    
         Map_NodeVecFree( p->vAnds );
     if ( p->vNodesAll )    
@@ -259,6 +256,9 @@ void Map_ManFree( Map_Man_t * p )
         Map_NodeVecFree( p->vMapping );
     if ( p->vVisited )    
         Map_NodeVecFree( p->vVisited );
+    if ( p->uCanons )   free( p->uCanons );
+    if ( p->uPhases )   free( p->uPhases );
+    if ( p->pCounters ) free( p->pCounters );
     Extra_MmFixedStop( p->mmNodes, 0 );
     Extra_MmFixedStop( p->mmCuts, 0 );
     FREE( p->pInputArrivals );
@@ -266,8 +266,6 @@ void Map_ManFree( Map_Man_t * p )
     FREE( p->pOutputs );
     FREE( p->pBins );
     FREE( p->ppOutputNames );
-    if ( p->pSimInfo ) FREE( p->pSimInfo[0] );
-    FREE( p->pSimInfo );
     FREE( p );
 }
 
@@ -357,9 +355,11 @@ Map_Node_t * Map_NodeCreate( Map_Man_t * p, Map_Node_t * p1, Map_Node_t * p2 )
     // set the level of this node
     if ( p1 ) 
     {
+#ifdef MAP_ALLOCATE_FANOUT
         // create the fanout info
         Map_NodeAddFaninFanout( Map_Regular(p1), pNode );
         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);
     }
diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c
index 1f3c8074..0c3a0910 100644
--- a/src/map/mapper/mapperCut.c
+++ b/src/map/mapper/mapperCut.c
@@ -65,6 +65,7 @@ static Map_Cut_t *      Map_CutSortCuts( Map_Man_t * pMan, Map_CutTable_t * p, M
 static int              Map_CutList2Array( Map_Cut_t ** pArray, Map_Cut_t * pList );
 static Map_Cut_t *      Map_CutArray2List( Map_Cut_t ** pArray, int nCuts );
 
+static unsigned         Map_CutComputeTruth( Map_Man_t * p, Map_Cut_t * pCut, Map_Cut_t * pTemp0, Map_Cut_t * pTemp1, int fComp0, int fComp1 );
 
 // iterator through all the cuts of the list
 #define Map_ListForEachCut( pList, pCut )                 \
@@ -78,7 +79,6 @@ static Map_Cut_t *      Map_CutArray2List( Map_Cut_t ** pArray, int nCuts );
           pCut = pCut2,                                   \
           pCut2 = pCut? pCut->pNext: NULL )
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -114,6 +114,7 @@ void Map_MappingCuts( Map_Man_t * p )
     Map_Node_t * pNode;
     Map_Cut_t * pCut;
     int nCuts, nNodes, i;
+    int clk = clock();
     // set the elementary cuts for the PI variables
     assert( p->nVarsMax > 1 && p->nVarsMax < 7 );
     for ( i = 0; i < p->nInputs; i++ )
@@ -121,10 +122,10 @@ void Map_MappingCuts( Map_Man_t * p )
         pCut = Map_CutAlloc( p );
         pCut->nLeaves = 1;
         pCut->ppLeaves[0] = p->pInputs[i];
-//        pCut->fLevel = (float)pCut->ppLeaves[0]->Level;
         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;
     }
@@ -148,8 +149,9 @@ void Map_MappingCuts( Map_Man_t * p )
     if ( p->fVerbose )
     {
         nCuts = Map_MappingCountAllCuts(p);
-        printf( "Nodes = %6d. Total %d-feasible cuts = %d. Cuts per node = %.1f.\n", 
+        printf( "Nodes = %6d. Total %d-feasible cuts = %d. Per node = %.1f. ", 
                p->nNodes, p->nVarsMax, nCuts, ((float)nCuts)/p->nNodes );
+        PRT( "Time", clock() - clk );
     }
 
     // print the cuts for the first primary output
@@ -158,48 +160,6 @@ void Map_MappingCuts( Map_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs technology mapping for variable-size-LUTs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Map_MappingCreatePiCuts( Map_Man_t * p )
-{
-    Map_Cut_t * pCut;
-    int i;
-
-    // set the elementary cuts for the PI variables
-    for ( i = 0; i < p->nInputs; i++ )
-    {
-        pCut = Map_CutAlloc( p );
-        pCut->nLeaves = 1;
-        pCut->ppLeaves[0] = p->pInputs[i];
-//        pCut->fLevel = (float)pCut->ppLeaves[0]->Level;
-        p->pInputs[i]->pCuts   = pCut;
-        p->pInputs[i]->pCutBest[1] = pCut;
-        p->pInputs[i]->pCutBest[0] = pCut;
-        // set the input arrival times
-//        p->pInputs[i]->pCut[1]->tArrival = p->pInputArrivals[i];
-
-        // set the input arrival times
-        pCut = p->pInputs[i]->pCutBest[1];
-        pCut->M[1].tArrive = p->pInputArrivals[i];
-        pCut->M[1].tArrive.Worst = MAP_MAX( pCut->M[1].tArrive.Rise, pCut->M[1].tArrive.Fall );
-        // set the arrival times of the negative phases of the PI nodes
-        pCut = p->pInputs[i]->pCutBest[0];
-        pCut->M[0].tArrive.Rise = p->pInputArrivals[i].Fall + p->pSuperLib->tDelayInv.Rise;
-        pCut->M[0].tArrive.Fall = p->pInputArrivals[i].Rise + p->pSuperLib->tDelayInv.Fall;
-        pCut->M[0].tArrive.Worst = MAP_MAX( pCut->M[0].tArrive.Rise, pCut->M[0].tArrive.Fall );
-
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes the cuts for one node.]
 
   Description []
@@ -242,7 +202,7 @@ Map_Cut_t * Map_CutCompute( Map_Man_t * p, Map_CutTable_t * pTable, Map_Node_t *
     pCut = Map_CutAlloc( p );
     pCut->nLeaves = 1;
     pCut->ppLeaves[0] = pNode;
-//    pCut->fLevel = (float)pCut->ppLeaves[0]->Level;
+    pCut->uTruth = 0xAAAAAAAA;
     // append (it is important that the elementary cut is appended first)
     pCut->pNext = pList;
     // set at the node
@@ -392,6 +352,8 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             // add data to the cut
             pCut->pOne = Map_CutNotCond( pTemp1, fComp1 );
             pCut->pTwo = Map_CutNotCond( pTemp2, fComp2 );
+//            if ( p->nVarsMax == 5 )
+//            pCut->uTruth = Map_CutComputeTruth( p, pCut, pTemp1, pTemp2, fComp1, fComp2 );
             // add it to the corresponding list
             pCut->pNext = pLists[pCut->nLeaves];
             pLists[pCut->nLeaves] = pCut;
@@ -424,6 +386,8 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             // add data to the cut
             pCut->pOne = Map_CutNotCond( pTemp1, fComp1 );
             pCut->pTwo = Map_CutNotCond( pTemp2, fComp2 );
+//            if ( p->nVarsMax == 5 )
+//            pCut->uTruth = Map_CutComputeTruth( p, pCut, pTemp1, pTemp2, fComp1, fComp2 );
             // add it to the corresponding list
             pCut->pNext = pLists[pCut->nLeaves];
             pLists[pCut->nLeaves] = pCut;
@@ -459,6 +423,8 @@ Map_Cut_t * Map_CutMergeLists( Map_Man_t * p, Map_CutTable_t * pTable,
             // add data to the cut
             pCut->pOne = Map_CutNotCond( pTemp1, fComp1 );
             pCut->pTwo = Map_CutNotCond( pTemp2, fComp2 );
+//            if ( p->nVarsMax == 5 )
+//            pCut->uTruth = Map_CutComputeTruth( p, pCut, pTemp1, pTemp2, fComp1, fComp2 );
             // add it to the corresponding list
             pCut->pNext = pLists[pCut->nLeaves];
             pLists[pCut->nLeaves] = pCut;
@@ -725,12 +691,26 @@ 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;
     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++;
+*/
+                }
+//    printf( "Total cuts = %6d. 55 = %6d. 5x = %6d. 4x = %6d. 3x = %6d.\n", nCuts, nCuts55, nCuts5x, nCuts4x, nCuts3x );
     return nCuts;
 }
 
@@ -926,7 +906,6 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
     Map_Cut_t * pCut;
     int Place, i;
 //    int clk;
-
     // check the cut
     Place = Map_CutTableLookup( p, ppNodes, nNodes );
     if ( Place == -1 )
@@ -937,13 +916,8 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
     pCut = Map_CutAlloc( pMan );
 //pMan->time1 += clock() - clk;
     pCut->nLeaves = nNodes;
-//    pCut->fLevel = 0;
     for ( i = 0; i < nNodes; i++ )
-    {
         pCut->ppLeaves[i] = ppNodes[i];
-//        pCut->fLevel += ppNodes[i]->Level;
-    }
-//    pCut->fLevel /= nNodes;
     // add the cut to the table
     assert( p->pBins[Place] == NULL );
     p->pBins[Place] = pCut;
@@ -994,12 +968,6 @@ int Map_CutSortCutsCompare( Map_Cut_t ** pC1, Map_Cut_t ** pC2 )
         return -1;
     if ( (*pC1)->nLeaves > (*pC2)->nLeaves )
         return 1;
-/*
-    if ( (*pC1)->fLevel < (*pC2)->fLevel )
-        return -1;
-    if ( (*pC1)->fLevel > (*pC2)->fLevel )
-        return 1;
-*/
     return 0;
 }
 
@@ -1081,7 +1049,6 @@ Map_Cut_t * Map_CutArray2List( Map_Cut_t ** pArray, int nCuts )
         // connect these lists
         *ppListNew = pArray[i];
         ppListNew  = &pArray[i]->pNext;
-//printf( " %d(%.2f)", pArray[i]->nLeaves, pArray[i]->fLevel );
     }
 //printf( "\n" );
 
@@ -1090,6 +1057,103 @@ Map_Cut_t * Map_CutArray2List( Map_Cut_t ** pArray, int nCuts )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of the 5-input cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Map_CutComputeTruth( Map_Man_t * p, Map_Cut_t * pCut, Map_Cut_t * pTemp0, Map_Cut_t * pTemp1, int fComp0, int fComp1 )
+{
+    static unsigned ** pPerms53 = NULL;
+    static unsigned ** pPerms54 = NULL;
+
+    unsigned uPhase, uTruth, uTruth0, uTruth1;
+    int i, k;
+
+    if ( pPerms53 == NULL )
+    {
+        pPerms53 = (unsigned **)Extra_TruthPerm53();
+        pPerms54 = (unsigned **)Extra_TruthPerm54();
+    }
+
+    // find the mapping from the old nodes to the new
+    if ( pTemp0->nLeaves == pCut->nLeaves )
+        uTruth0 = pTemp0->uTruth;
+    else
+    {
+        assert( pTemp0->nLeaves < pCut->nLeaves );
+        uPhase = 0;
+        for ( i = 0; i < (int)pTemp0->nLeaves; i++ )
+        {
+            for ( k = 0; k < pCut->nLeaves; k++ )
+                if ( pTemp0->ppLeaves[i] == pCut->ppLeaves[k] )
+                    break;
+            uPhase |= (1 << k);
+        }
+        assert( uPhase < 32 );
+        if ( pTemp0->nLeaves == 4 )
+        {
+            if ( uPhase == 31-16 ) // 01111
+                uTruth0 = pTemp0->uTruth;
+            else if ( uPhase == 31-8 ) // 10111
+                uTruth0 = pPerms54[pTemp0->uTruth & 0xFFFF][0];
+            else if ( uPhase == 31-4 ) // 11011
+                uTruth0 = pPerms54[pTemp0->uTruth & 0xFFFF][1];
+            else if ( uPhase == 31-2 ) // 11101
+                uTruth0 = pPerms54[pTemp0->uTruth & 0xFFFF][2];
+            else if ( uPhase == 31-1 ) // 11110
+                uTruth0 = pPerms54[pTemp0->uTruth & 0xFFFF][3];
+            else
+                assert( 0 );
+        }
+        else
+            uTruth0 = pPerms53[pTemp0->uTruth & 0xFF][uPhase];
+    }
+    uTruth0 = fComp0? ~uTruth0: uTruth0;
+
+    // find the mapping from the old nodes to the new
+    if ( pTemp1->nLeaves == pCut->nLeaves )
+        uTruth1 = pTemp1->uTruth;
+    else
+    {
+        assert( pTemp1->nLeaves < pCut->nLeaves );
+        uPhase = 0;
+        for ( i = 0; i < (int)pTemp1->nLeaves; i++ )
+        {
+            for ( k = 0; k < pCut->nLeaves; k++ )
+                if ( pTemp1->ppLeaves[i] == pCut->ppLeaves[k] )
+                    break;
+            uPhase |= (1 << k);
+        }
+        assert( uPhase < 32 );
+        if ( pTemp1->nLeaves == 4 )
+        {
+            if ( uPhase == 31-16 ) // 01111
+                uTruth1 = pTemp1->uTruth;
+            else if ( uPhase == 31-8 ) // 10111
+                uTruth1 = pPerms54[pTemp1->uTruth & 0xFFFF][0];
+            else if ( uPhase == 31-4 ) // 11011
+                uTruth1 = pPerms54[pTemp1->uTruth & 0xFFFF][1];
+            else if ( uPhase == 31-2 ) // 11101
+                uTruth1 = pPerms54[pTemp1->uTruth & 0xFFFF][2];
+            else if ( uPhase == 31-1 ) // 11110
+                uTruth1 = pPerms54[pTemp1->uTruth & 0xFFFF][3];
+            else
+                assert( 0 );
+        }
+        else
+            uTruth1 = pPerms53[pTemp1->uTruth & 0xFF][uPhase];
+    }
+    uTruth1 = fComp1? ~uTruth1: uTruth1;
+    uTruth  = uTruth0 & uTruth1;
+    return uTruth;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/map/mapper/mapperFanout.c b/src/map/mapper/mapperFanout.c
index 7bd92ed9..aca29918 100644
--- a/src/map/mapper/mapperFanout.c
+++ b/src/map/mapper/mapperFanout.c
@@ -18,6 +18,8 @@
 
 #include "mapperInt.h"
 
+#ifdef MAP_ALLOCATE_FANOUT
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -26,7 +28,6 @@
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
   Synopsis    [Add the fanout to the node.]
@@ -136,4 +137,5 @@ int Map_NodeGetFanoutNum( Map_Node_t * pNode )
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif
 
diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h
index d4262abb..7d63a804 100644
--- a/src/map/mapper/mapperInt.h
+++ b/src/map/mapper/mapperInt.h
@@ -36,7 +36,10 @@
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
- 
+
+// uncomment to have fanouts represented in the mapping graph
+//#define MAP_ALLOCATE_FANOUT  1
+
 ////////////////////////////////////////////////////////////////////////
 ///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
@@ -123,18 +126,15 @@ struct Map_ManStruct_t_
     int                 nCountsBest[32];// the counter of minterms
     Map_NodeVec_t *     vVisited;      // the visited cuts during cut computation
 
-    // simulation info from the FRAIG manager
-    int                 nSimRounds;    // the number of words in the simulation info
-    unsigned **         pSimInfo;      // the simulation info for each PI
-
-    // don't-care computation
-    Map_NodeVec_t *     vInside;       // the array of nodes for SDC computation
-    Map_NodeVec_t *     vFanins;       // the array of nodes for SDC computation
-
     // the memory managers
     Extra_MmFixed_t *   mmNodes;       // the memory manager for nodes
     Extra_MmFixed_t *   mmCuts;        // the memory manager for cuts
 
+    // precomputed N-canonical forms
+    unsigned short *    uCanons;       // N-canonical forms
+    char **             uPhases;       // N-canonical phases
+    char *              pCounters;     // counters of phases
+
     // various statistical variables
     int                 nChoiceNodes;  // the number of choice nodes
     int                 nChoices;      // the number of all choices
@@ -211,27 +211,25 @@ struct Map_NodeStruct_t_
     int                 nRefAct[3];    // estimated fanout for current covering phase, neg and pos and sum
     float               nRefEst[3];    // actual fanout for previous covering phase, neg and pos and sum
 
-    // the successors of this node     
+    // connectivity
     Map_Node_t *        p1;            // the first child
     Map_Node_t *        p2;            // the second child
     Map_Node_t *        pNextE;        // the next functionally equivalent node
     Map_Node_t *        pRepr;         // the representative of the functionally equivalent class
-//    Map_NodeVec_t *     vFanouts;      // the array of fanouts of the node
 
+#ifdef MAP_ALLOCATE_FANOUT
     // representation of node's fanouts
     Map_Node_t *        pFanPivot;     // the first fanout of this node
     Map_Node_t *        pFanFanin1;    // the next fanout of p1
     Map_Node_t *        pFanFanin2;    // the next fanout of p2
-
-    unsigned *          pSims;         // the simulation info
-    float               SwitchProb;    // the switching probability
+//    Map_NodeVec_t *     vFanouts;      // the array of fanouts of the gate
+#endif
 
     // the delay information
     Map_Time_t          tArrival[2];   // the best arrival time of the neg (0) and pos (1) phases
     Map_Time_t          tRequired[2];  // the required time of the neg (0) and pos (1) phases
 
     // misc information  
-    Map_Cut_t *         pCutOld[2];    // the old mapping for neg and pos phase
     Map_Cut_t *         pCutBest[2];   // the best mapping for neg and pos phase
     Map_Cut_t *         pCuts;         // mapping choices for the node (elementary comes first)
     char *              pData0;        // temporary storage for the corresponding network node
@@ -259,6 +257,7 @@ struct Map_CutStruct_t_
     Map_Cut_t *         pOne;          // the father of this cut
     Map_Cut_t *         pTwo;          // the mother of this cut
     Map_Node_t *        ppLeaves[6];   // the leaves of this cut
+    unsigned            uTruth;        // truth table for five-input cuts
     char                nLeaves;       // the number of leaves
     char                nVolume;       // the volume of this cut
     char                fMark;         // the mark to denote visited cut
diff --git a/src/map/mapper/mapperRefs.c b/src/map/mapper/mapperRefs.c
index 334e98c7..e74bab9a 100644
--- a/src/map/mapper/mapperRefs.c
+++ b/src/map/mapper/mapperRefs.c
@@ -25,7 +25,7 @@
 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 );
+static void  Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode, Map_Node_t ** ppStore );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -401,8 +401,9 @@ float Map_CutRefDeref( Map_Cut_t * pCut, int fPhase, int fReference )
 
   Synopsis    [Computes actual reference counters.]
 
-  Description [Stores all the nodes used in the mapping in the array pMan->vMapping.
-  The nodes are stored in the random order.]
+  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 []
 
@@ -411,8 +412,9 @@ float Map_CutRefDeref( Map_Cut_t * pCut, int fPhase, int fReference )
 ***********************************************************************/
 void Map_MappingSetRefs( Map_Man_t * pMan )
 {
-    Map_Node_t * pNode;
-    int i, fPhase;
+    Map_Node_t * pNode, ** ppStore;
+    int i, fPhase, LevelMax;
+
     // clean all references
     for ( i = 0; i < pMan->vNodesAll->nSize; i++ )
     {
@@ -421,18 +423,32 @@ void Map_MappingSetRefs( Map_Man_t * pMan )
         pNode->nRefAct[1] = 0;
         pNode->nRefAct[2] = 0;
     }
+
+    // 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;
+
+    // allocate place to store the nodes
+    ppStore = ALLOC( Map_Node_t *, LevelMax + 1 );
+    memset( ppStore, 0, sizeof(Map_Node_t *) * (LevelMax + 1) );
+
     // visit nodes reachable from POs in the DFS order through the best cuts
-    pMan->vMapping->nSize = 0;
     for ( i = 0; i < pMan->nOutputs; i++ )
     {
         pNode  = pMan->pOutputs[i];
         fPhase = !Map_IsComplement(pNode);
         if ( !Map_NodeIsConst(pNode) )
-            Map_MappingSetRefs_rec( pMan, pNode );
-        // reference count the PO node
-//        Map_Regular(pNode)->nRefAct[fPhase]++;
-//        Map_Regular(pNode)->nRefAct[2]++;
+            Map_MappingSetRefs_rec( pMan, pNode, ppStore );
     }
+
+    // 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 );
+    free( ppStore );
 }
 
 /**Function*************************************************************
@@ -446,7 +462,7 @@ void Map_MappingSetRefs( Map_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-void Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode )
+void Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode, Map_Node_t ** ppStore )
 {
     Map_Cut_t * pCut;
     Map_Node_t * pNodeR;
@@ -459,7 +475,8 @@ void Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode )
 
     // add the node to the list of all visited nodes
     if ( pNodeR->nRefAct[2]++ == 0 )
-        Map_NodeVecPush( pMan->vMapping, pNodeR );
+//        Map_NodeVecPush( pMan->vMapping, pNodeR );
+        pNodeR->pData0 = (char *)ppStore[pNodeR->Level], ppStore[pNodeR->Level] = pNodeR;
 
     // quit if the node was already visited in this phase
     if ( pNodeR->nRefAct[fPhase]++ )
@@ -482,7 +499,7 @@ void Map_MappingSetRefs_rec( Map_Man_t * pMan, Map_Node_t * pNode )
     for ( i = 0; i < pCut->nLeaves; i++ )
     {
         fInvPin = ((uPhase & (1 << i)) > 0);
-        Map_MappingSetRefs_rec( pMan, Map_NotCond(pCut->ppLeaves[i], fInvPin) );
+        Map_MappingSetRefs_rec( pMan, Map_NotCond(pCut->ppLeaves[i], fInvPin), ppStore );
     }
 }
 
diff --git a/src/map/mapper/mapperTime.c b/src/map/mapper/mapperTime.c
index 0ff88b0e..f1cafae7 100644
--- a/src/map/mapper/mapperTime.c
+++ b/src/map/mapper/mapperTime.c
@@ -252,7 +252,9 @@ void Map_TimeComputeRequired( Map_Man_t * p, float fRequired )
 
     // sorts the nodes in the decreasing order of levels
     // this puts the nodes in reverse topological order
-    Map_MappingSortByLevel( p, p->vMapping );
+//    Map_MappingSortByLevel( p, p->vMapping );
+    // the array is already sorted by construction in Map_MappingSetRefs()
+
     Map_TimePropagateRequired( p, p->vMapping );
 }
 
diff --git a/src/map/mapper/mapperTruth.c b/src/map/mapper/mapperTruth.c
index 97e64920..54fc0391 100644
--- a/src/map/mapper/mapperTruth.c
+++ b/src/map/mapper/mapperTruth.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static void Map_TruthsCut( Map_Man_t * pMan, Map_Cut_t * pCut );
-static void Map_TruthsCutOne( Map_Man_t * p, Map_Cut_t * pCut, unsigned uTruth[] );
+extern void Map_TruthsCutOne( Map_Man_t * p, Map_Cut_t * pCut, unsigned uTruth[] );
 static void Map_CutsCollect_rec( Map_Cut_t * pCut, Map_NodeVec_t * vVisited );
 
 ////////////////////////////////////////////////////////////////////////
@@ -90,18 +90,30 @@ void Map_MappingTruths( Map_Man_t * pMan )
 ***********************************************************************/
 void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
 {
-    unsigned uTruth[2], uCanon[2];
 //    unsigned uCanon1, uCanon2;
+    unsigned uTruth[2], uCanon[2];
     unsigned char uPhases[16];
+    int fUseFast = 1;
 
     // generally speaking, 1-input cut can be matched into a wire!
     if ( pCut->nLeaves == 1 )
         return;
+/*
+    if ( p->nVarsMax == 5 )
+    {
+        uTruth[0] = pCut->uTruth;
+        uTruth[1] = pCut->uTruth;
+    }
+    else
+*/
     Map_TruthsCutOne( p, pCut, uTruth );
 
 
     // compute the canonical form for the positive phase
-    Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
+    if ( fUseFast )
+        Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
+    else
+        Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
     pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
     pCut->M[1].uPhase  = uPhases[0];
     p->nCanons++;
@@ -111,13 +123,15 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
     // compute the canonical form for the negative phase
     uTruth[0] = ~uTruth[0];
     uTruth[1] = ~uTruth[1];
-    Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
+    if ( fUseFast )
+        Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
+    else
+        Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
     pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
     pCut->M[0].uPhase  = uPhases[0];
     p->nCanons++;
 
 //uCanon2 = uCanon[0] & 0xFFFF;
-
 //assert( p->nVarsMax == 4 );
 //Rwt_Man4ExploreCount( uCanon1 < uCanon2 ? uCanon1 : uCanon2 );
 
diff --git a/src/map/mapper/mapperUtils.c b/src/map/mapper/mapperUtils.c
index f8fd1a4c..78885729 100644
--- a/src/map/mapper/mapperUtils.c
+++ b/src/map/mapper/mapperUtils.c
@@ -405,7 +405,7 @@ void Map_MappingPrintOutputArrivals( Map_Man_t * p )
     Map_Time_t * pTimes;
     Map_Node_t * pNode;
     int fPhase, Limit, i;
-    int nOutputs;
+    int nOutputs, MaxNameSize;
     int * pSorted;
 
     // sort outputs by arrival time
@@ -423,16 +423,22 @@ void Map_MappingPrintOutputArrivals( Map_Man_t * p )
     assert( Map_MappingCompareOutputDelay( pSorted, pSorted + nOutputs - 1 ) <= 0 );
     s_pMan = NULL;
 
-    // print the latest outputs
+    // determine max size of the node's name
+    MaxNameSize = 0;
     Limit = (nOutputs > 5)? 5 : nOutputs;
     for ( i = 0; i < Limit; i++ )
+        if ( MaxNameSize < (int)strlen(p->ppOutputNames[pSorted[i]]) )
+            MaxNameSize = strlen(p->ppOutputNames[pSorted[i]]);
+
+    // print the latest outputs
+    for ( i = 0; i < Limit; i++ )
     {
         // get the i-th latest output
         pNode  = Map_Regular(p->pOutputs[pSorted[i]]);
         fPhase =!Map_IsComplement(p->pOutputs[pSorted[i]]);
         pTimes = pNode->tArrival + fPhase;
         // print out the best arrival time
-        printf( "Out  %20s : ", p->ppOutputNames[pSorted[i]] );
+        printf( "Output  %-*s : ", MaxNameSize + 3, p->ppOutputNames[pSorted[i]] );
         printf( "Delay = (%5.2f, %5.2f)  ", (double)pTimes->Rise, (double)pTimes->Fall );
         printf( "%s", fPhase? "POS" : "NEG" );
         printf( "\n" );
@@ -1013,136 +1019,6 @@ void Map_MappingReportChoices( Map_Man_t * pMan )
     printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
 }
 
-/*
-void Map_MappingReportChoices( Map_Man_t * pMan )
-{
-    Map_Node_t * pNode, * pTemp;
-    int nChoiceNodes, nChoices;
-    int i, LevelMax1, LevelMax2;
-    int DiffMaxTotal, DiffMinTotal, Min, Max;
-    int CounterByMin[300]={0}, CounterByMax[300]={0};
-
-    // report the number of levels
-    LevelMax1 = Map_MappingGetMaxLevel( pMan );
-    pMan->nTravIds++;
-    for ( i = 0; i < pMan->nOutputs; i++ )
-//        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 0 );
-        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 1 );
-    LevelMax2 = Map_MappingGetMaxLevel( pMan );
-
-    // report statistics about choices
-    nChoiceNodes = nChoices = 0;
-    DiffMaxTotal = DiffMinTotal = 0;
-    for ( i = 0; i < pMan->vAnds->nSize; i++ )
-    {
-        pNode = pMan->vAnds->pArray[i];
-        if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
-        { // this is a choice node = the primary node that has equivalent nodes
-            nChoiceNodes++;
-            for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
-                nChoices++;
-            // call to compare the levels
-            Map_MappingGetChoiceLevels( pMan, pNode, pNode->pNextE, &Min, &Max );
-            assert( Min < (int)pNode->Level );
-            assert( Max < (int)pNode->Level );
-            DiffMinTotal += pNode->Level - Max;
-            DiffMaxTotal += pNode->Level - Min;
-
-            CounterByMin[pNode->Level - Max]++;
-            CounterByMax[pNode->Level - Min]++;
-
-        }
-    }
-    printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
-    printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
-    printf( "Choice depth:  Minimum = %4.2f. Maximum = %4.2f.\n", 
-        ((float)DiffMinTotal)/nChoiceNodes, ((float)DiffMaxTotal)/nChoiceNodes );
-
-    {
-    FILE * pTable;
-    pTable = fopen( "statsc.txt", "a+" );
-    fprintf( pTable, "%6d ", pMan->vAnds->nSize );
-    fprintf( pTable, "%5d ", LevelMax2 );
-    fprintf( pTable, "%5d ", nChoiceNodes );
-    fprintf( pTable, "%5d ", nChoices );
-    fprintf( pTable, "%5.2f ", ((float)DiffMinTotal)/nChoiceNodes );
-    fprintf( pTable, "%5.2f ", ((float)DiffMaxTotal)/nChoiceNodes );
-//    fprintf( pTable, "%4.2f\n", (float)(Time)/(float)(CLOCKS_PER_SEC) );
-    fprintf( pTable, "\n" );
-    fclose( pTable );
-    }
-
-
-    printf( "Distribution by min/max levels:\n" );
-    for ( i = 0; i < LevelMax2; i++ )
-        printf( "%3d :  %5d  %5d\n", i, CounterByMin[i], CounterByMax[i] );
-    printf( "\n" );
-}
-*/
-
-/*
-void Map_MappingReportChoices( Map_Man_t * pMan )
-{
-    Map_Node_t * pNode, * pTemp;
-    int nChoiceNodes, nChoices;
-    int i, LevelMax1, LevelMax2;
-    int CounterByVol[1000]={0};
-    float VolumeAve, Volume;
-
-    // report the number of levels
-    LevelMax1 = Map_MappingGetMaxLevel( pMan );
-    pMan->nTravIds++;
-    for ( i = 0; i < pMan->nOutputs; i++ )
-        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 0 );
-//        Map_MappingUpdateLevel_rec( pMan, Map_Regular(pMan->pOutputs[i]), 1 );
-    LevelMax2 = Map_MappingGetMaxLevel( pMan );
-
-    // report statistics about choices
-    nChoiceNodes = nChoices = 0;
-    VolumeAve = 0.0;
-    for ( i = 0; i < pMan->vAnds->nSize; i++ )
-    {
-        pNode = pMan->vAnds->pArray[i];
-        if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
-        { // this is a choice node = the primary node that has equivalent nodes
-            nChoiceNodes++;
-            for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
-                nChoices++;
-            Volume = Map_MappingGetChoiceVolumes( pMan, pNode, pNode->pNextE );
-            VolumeAve += Volume;
-            assert( Volume < 1000 );
-            CounterByVol[(int)Volume]++;
-        }
-    }
-    printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
-    printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
-    printf( "Average volume = %5.4f.\n", VolumeAve/nChoiceNodes );
-*/
-/*
-    {
-    FILE * pTable;
-    pTable = fopen( "statsv.txt", "a+" );
-    fprintf( pTable, "%6d ", Map_MappingCountUsedNodes(pMan,1) );
-    fprintf( pTable, "%6d ", Map_MappingCountUsedNodes(pMan,0) );
-    fprintf( pTable, "%5d ", LevelMax1 );
-    fprintf( pTable, "   " );
-    fprintf( pTable, "%5d ", nChoiceNodes );
-    fprintf( pTable, "%5d ", nChoices );
-    fprintf( pTable, "   " );
-    fprintf( pTable, "%5.4f ", VolumeAve/nChoiceNodes );
-    fprintf( pTable, "\n" );
-    fclose( pTable );
-    }
-    printf( "Distribution by volume:\n" );
-    for ( i = 0; i < 1000; i++ )
-        if ( CounterByVol[i] > 0 )
-        printf( "%3d :  %5d\n", i, CounterByVol[i] );
-    printf( "\n" );
-*/
-/*
-}
-*/
-
 /**Function*************************************************************
 
   Synopsis    [Computes the maximum and minimum levels of the choice nodes.]