Version abc50827

11 files changed, 573 insertions, 109 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index 7d9f9725..c2b739b5 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -848,7 +848,7 @@ usage:
 int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp;
     int c;
     int fDuplicate;
 
@@ -878,14 +878,25 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+
+    // get the new network
+    if ( Abc_NtkIsAig(pNtk) )
     {
-        fprintf( pErr, "Cannot balance a network that is not an AIG.\n" );
-        return 1;
+        pNtkRes = Abc_NtkBalance( pNtk, fDuplicate );
+    }
+    else
+    {
+        pNtkTemp = Abc_NtkStrash( pNtk, 0 );
+        if ( pNtkTemp == NULL )
+        {
+            fprintf( pErr, "Strashing before balancing has failed.\n" );
+            return 1;
+        }
+        pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate );
+        Abc_NtkDelete( pNtkTemp );
     }
 
-    // get the new network
-    pNtkRes = Abc_NtkBalance( pNtk, fDuplicate );
+    // check if balancing worked
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Balancing has failed.\n" );
@@ -897,7 +908,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: balance [-dh]\n" );
-    fprintf( pErr, "\t        transforms an AIG into a well-balanced AIG\n" );
+    fprintf( pErr, "\t        transforms the current network into a well-balanced AIG\n" );
     fprintf( pErr, "\t-d    : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
@@ -1327,27 +1338,32 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    bool fVerbose;
     bool fPrecompute;
+    bool fUseZeros;
+    bool fVerbose;
     // external functions
     extern void   Rwr_Precompute();
-    extern int    Abc_NtkRewrite( Abc_Ntk_t * pNtk );
+    extern int    Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose    = 0;
     fPrecompute = 0;
+    fUseZeros   = 0;
+    fVerbose    = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "zvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "xzvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'z':
+        case 'x':
             fPrecompute ^= 1;
             break;
+        case 'z':
+            fUseZeros ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -1381,7 +1397,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkRewrite( pNtk ) )
+    if ( !Abc_NtkRewrite( pNtk, fUseZeros, fVerbose ) )
     {
         fprintf( pErr, "Rewriting has failed.\n" );
         return 1;
@@ -1389,8 +1405,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: rewrite [-vh]\n" );
+    fprintf( pErr, "usage: rewrite [-zvh]\n" );
     fprintf( pErr, "\t         performs technology-independent rewriting of the AIG\n" );
+    fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -1428,7 +1445,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     nConeSizeMax = 16;
     fUseZeros    =  0;
     fUseDcs      =  0;
-    fVerbose     =  1;
+    fVerbose     =  0;
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "NCzdvh" ) ) != EOF )
     {
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index ff1252c1..200d2501 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -144,8 +144,13 @@ struct Abc_Ntk_t_
     int              nPos;          // the number of primary outputs
     // the functionality manager 
     void *           pManFunc;      // AIG manager, BDD manager, or memory manager for SOPs
-    // the timing manager
+    // the timing manager (for mapped networks)
     Abc_ManTime_t *  pManTime;      // stores arrival/required times for all nodes
+    // the cut manager (for AIGs)
+    void *           pManCut;       // stores information about the cuts computed for the nodes
+    // level information (for AIGs)
+    int              LevelMax;      // maximum number of levels
+    Vec_Int_t *      vLevelsR;       // level in the reverse topological order 
     // the external don't-care if given
     Abc_Ntk_t *      pExdc;         // the EXDC network
     // miscellaneous data members
@@ -423,6 +428,11 @@ extern Abc_Obj_t *        Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFani
 extern Abc_Obj_t *        Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
 extern Abc_Obj_t *        Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
 extern Abc_Obj_t *        Abc_NodeClone( Abc_Obj_t * pNode );
+/*=== abcCut.c ==========================================================*/
+extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj );
+extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj );
+extern void *             Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
+extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
 /*=== abcDfs.c ==========================================================*/
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
@@ -572,7 +582,11 @@ extern void               Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
 extern float *            Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk );
 extern Abc_Time_t *       Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk );
 extern float              Abc_NtkDelayTrace( Abc_Ntk_t * pNtk );
-extern Vec_Int_t *        Abc_NtkGetRequiredLevels( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
+extern void               Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
+extern int                Abc_NodeReadReverseLevel( Abc_Obj_t * pObj );
+extern int                Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj );
 /*=== abcTravId.c ==========================================================*/
 extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
 extern void               Abc_NodeSetTravId( Abc_Obj_t * pObj, int TravId );
@@ -609,6 +623,7 @@ extern void               Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames );
 extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
 extern void               Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb );
 extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
+extern Vec_Int_t *        Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 883c544f..d42fdac0 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -58,6 +58,7 @@ struct Abc_Aig_t_
     Vec_Ptr_t *       vStackReplaceOld;  // the nodes to be replaced
     Vec_Ptr_t *       vStackReplaceNew;  // the nodes to be used for replacement
     Vec_Vec_t *       vLevels;           // the nodes to be updated
+    Vec_Vec_t *       vLevelsR;          // the nodes to be updated
 };
 
 // iterators through the entries in the linked lists of nodes
@@ -85,6 +86,9 @@ static void        Abc_AigResize( Abc_Aig_t * pMan );
 static void        Abc_AigReplace_int( Abc_Aig_t * pMan );
 static void        Abc_AigDelete_int( Abc_Aig_t * pMan );
 static void        Abc_AigUpdateLevel_int( Abc_Aig_t * pMan );
+static void        Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan );
+static void        Abc_AigRemoveFromLevelStructure( Vec_Vec_t * vStruct, Abc_Obj_t * pNode );
+static void        Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -116,6 +120,7 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
     pMan->vStackReplaceOld = Vec_PtrAlloc( 100 );
     pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
     pMan->vLevels          = Vec_VecAlloc( 100 );
+    pMan->vLevelsR         = Vec_VecAlloc( 100 );
     // save the current network
     pMan->pNtkAig = pNtkAig;
     // allocate constant nodes
@@ -199,6 +204,7 @@ void Abc_AigFree( Abc_Aig_t * pMan )
     assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
     // free the table
     Vec_VecFree( pMan->vLevels );
+    Vec_VecFree( pMan->vLevelsR );
     Vec_PtrFree( pMan->vStackDelete );
     Vec_PtrFree( pMan->vStackReplaceOld );
     Vec_PtrFree( pMan->vStackReplaceNew );
@@ -381,6 +387,9 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     pAnd->pNext      = pMan->pBins[Key];
     pMan->pBins[Key] = pAnd;
     pMan->nEntries++;
+    // create the cuts if defined
+//    if ( pAnd->pNtk->pManCut )
+//        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
     return pAnd;
 }
 
@@ -399,6 +408,7 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
 {
     Abc_Obj_t * pTemp;
     unsigned Key;
+    assert( !Abc_ObjIsComplement(pAnd) );
     // order the arguments
     if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
         pTemp = p0, p0 = p1, p1 = pTemp;
@@ -412,6 +422,9 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
     Key = Abc_HashKey2( p0, p1, pMan->nBins );
     pAnd->pNext      = pMan->pBins[Key];
     pMan->pBins[Key] = pAnd;
+    // create the cuts if defined
+//    if ( pAnd->pNtk->pManCut )
+//        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
     return pAnd;
 }
 
@@ -494,6 +507,9 @@ void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis )
     }
     assert( pAnd == pThis );
     pMan->nEntries--;
+    // delete the cuts if defined
+    if ( pThis->pNtk->pManCut )
+        Abc_NodeFreeCuts( pThis->pNtk->pManCut, pThis );
 }
 
 /**Function*************************************************************
@@ -644,9 +660,8 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
     Vec_PtrPush( pMan->vStackReplaceNew, pNew );
     while ( Vec_PtrSize(pMan->vStackReplaceOld) )
         Abc_AigReplace_int( pMan );
-//    while ( Vec_PtrSize(pMan->vStackDelete) )
-//        Abc_AigDelete_int( pMan );
     Abc_AigUpdateLevel_int( pMan );
+    Abc_AigUpdateLevelR_int( pMan );
 }
 
 /**Function*************************************************************
@@ -705,8 +720,14 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         Abc_ObjRemoveFanins( pFanout );
         // recreate the old fanout with new fanins and add it to the table
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
-        // schedule the updated fanout for updating level
+        // schedule the updated fanout for updating direct level
+        assert( pFanout->fMarkA == 0 );
+        pFanout->fMarkA = 1;
         Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
+        // schedule the updated fanout for updating reverse level
+        assert( pFanout->fMarkB == 0 );
+        pFanout->fMarkB = 1;
+        Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
         // the fanout has changed, update EXOR status of its fanouts
         Abc_ObjForEachFanout( pFanout, pFanoutFanout, v )
             if ( Abc_NodeIsAigAnd(pFanoutFanout) )
@@ -764,15 +785,47 @@ void Abc_AigDelete_int( Abc_Aig_t * pMan )
 
     // collect the MFFC
     vNodes = Abc_NodeMffcCollect( pRoot );
+
+    // if reverse levels are specified, schedule fanins of MFFC for updating
+    // currently, we do not do it because we do not know the correct level of the fanins
+    // also, it is unlikely that this will make a difference since we are
+    // processing the network forward while at this point fanins are left behind...
+/*
+    if ( pObj->pNtk->vLevelsR )
+        Vec_PtrForEachEntry( vNodes, pObj, k )
+        {
+            Abc_Obj_t * pFanin;
+            if ( Abc_ObjIsCi(pObj) )
+                continue;
+            pFanin = Abc_ObjFanin0(pObj);
+            if ( pFanin->fMarkB == 0 )
+            {
+                pFanin->fMarkB = 1;
+                Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanin), pFanin );
+            }
+            pFanin = Abc_ObjFanin1(pObj);
+            if ( pFanin->fMarkB == 0 )
+            {
+                pFanin->fMarkB = 1;
+                Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanin), pFanin );
+            }
+        }
+*/
+
+    // delete the nodes in MFFC
     Vec_PtrForEachEntry( vNodes, pObj, k )
     {
         if ( Abc_ObjIsCi(pObj) )
             continue;
-        assert( pObj->fMarkA == 0 );
+        assert( Abc_ObjFanoutNum(pObj) == 0 );
         // remove the node from the table
         Abc_AigAndDelete( pMan, pObj );
+        // if the node is in the level structure, remove it
+        if ( pObj->fMarkA )
+            Abc_AigRemoveFromLevelStructure( pMan->vLevels, pObj );
+        if ( pObj->fMarkB )
+            Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pObj );
         // remove the node from the network
-//printf( "Removing " );  Abc_AigPrintNode( pObj );
         Abc_NtkDeleteObj( pObj );
     }
     Vec_PtrFree( vNodes );
@@ -782,7 +835,11 @@ void Abc_AigDelete_int( Abc_Aig_t * pMan )
 
   Synopsis    [Updates the level of the node after it has changed.]
 
-  Description []
+  Description [This procedure is based on the observation that
+  after the node's level has changed, the fanouts levels can change too, 
+  but the new fanout levels are always larger than the node's level.
+  As a result, we can accumulate the nodes to be updated in the queue
+  and process them in the increasing order of levels.]
                
   SideEffects []
 
@@ -793,8 +850,7 @@ void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
 {
     Abc_Obj_t * pNode, * pFanout;
     Vec_Ptr_t * vVec;
-    unsigned LevelNew;
-    int i, k, v;
+    int LevelNew, i, k, v;
 
     // go through the nodes and update the level of their fanouts
     Vec_VecForEachLevel( pMan->vLevels, vVec, i )
@@ -803,10 +859,12 @@ void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
             continue;
         Vec_PtrForEachEntry( vVec, pNode, k )
         {
-//            assert( Abc_ObjIsNode(pNode) );
-            // for some reason, deleted nodes are encountered here!!!
-            if ( !Abc_ObjIsNode(pNode) )
+            if ( pNode == NULL )
                 continue;
+            assert( Abc_ObjIsNode(pNode) );
+            // clean the mark
+            assert( pNode->fMarkA == 1 );
+            pNode->fMarkA = 0;
             // iterate through the fanouts
             Abc_ObjForEachFanout( pNode, pFanout, v )
             {
@@ -814,11 +872,17 @@ void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
                     continue;
                 // get the new level of this fanout
                 LevelNew = 1 + ABC_MAX( Abc_ObjFanin0(pFanout)->Level, Abc_ObjFanin1(pFanout)->Level );
-                if ( pFanout->Level == LevelNew ) // no change
+                assert( LevelNew > i );
+                if ( (int)pFanout->Level == LevelNew ) // no change
                     continue;
+                // if the fanout is present in the data structure, pull it out
+                if ( pFanout->fMarkA )
+                    Abc_AigRemoveFromLevelStructure( pMan->vLevels, pFanout );
                 // update the fanout level
                 pFanout->Level = LevelNew;
-                // add the fanout to be updated
+                // add the fanout to the data structure to update its fanouts
+                assert( pFanout->fMarkA == 0 );
+                pFanout->fMarkA = 1;
                 Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
             }
         }
@@ -826,7 +890,122 @@ void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Updates the level of the node after it has changed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t * pNode, * pFanin, * pFanout;
+    Vec_Ptr_t * vVec;
+    int LevelNew, i, k, v, j;
+
+    // go through the nodes and update the level of their fanouts
+    Vec_VecForEachLevel( pMan->vLevelsR, vVec, i )
+    {
+        if ( Vec_PtrSize(vVec) == 0 )
+            continue;
+        Vec_PtrForEachEntry( vVec, pNode, k )
+        {
+            if ( pNode == NULL )
+                continue;
+            assert( Abc_ObjIsNode(pNode) );
+            // clean the mark
+            assert( pNode->fMarkB == 1 );
+            pNode->fMarkB = 0;
+            // iterate through the fanins
+            Abc_ObjForEachFanin( pNode, pFanin, v )
+            {
+                if ( Abc_ObjIsCi(pFanin) )
+                    continue;
+                // get the new reverse level of this fanin
+                LevelNew = 0;
+                Abc_ObjForEachFanout( pFanin, pFanout, j )
+                    if ( LevelNew < Abc_NodeReadReverseLevel(pFanout) )
+                        LevelNew = Abc_NodeReadReverseLevel(pFanout);
+                LevelNew += 1;
+                assert( LevelNew > i );
+                if ( Abc_NodeReadReverseLevel(pFanin) == LevelNew ) // no change
+                    continue;
+                // if the fanin is present in the data structure, pull it out
+                if ( pFanin->fMarkB )
+                    Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin );
+                // update the reverse level
+                Abc_NodeSetReverseLevel( pFanin, LevelNew );
+                // add the fanin to the data structure to update its fanins
+                assert( pFanin->fMarkB == 0 );
+                pFanin->fMarkB = 1;
+                Vec_VecPush( pMan->vLevelsR, LevelNew, pFanin );
+            }
+        }
+        Vec_PtrClear( vVec );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the node from the level structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigRemoveFromLevelStructure( Vec_Vec_t * vStruct, Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vVecTemp;
+    Abc_Obj_t * pTemp;
+    int m;
+    assert( pNode->fMarkA );
+    vVecTemp = Vec_VecEntry( vStruct, pNode->Level );
+    Vec_PtrForEachEntry( vVecTemp, pTemp, m )
+    {
+        if ( pTemp != pNode )
+            continue;
+        Vec_PtrWriteEntry( vVecTemp, m, NULL );
+        break;
+    }
+    assert( m < Vec_PtrSize(vVecTemp) ); // found
+    pNode->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the node from the level structure.]
 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vVecTemp;
+    Abc_Obj_t * pTemp;
+    int m;
+    assert( pNode->fMarkB );
+    vVecTemp = Vec_VecEntry( vStruct, Abc_NodeReadReverseLevel(pNode) );
+    Vec_PtrForEachEntry( vVecTemp, pTemp, m )
+    {
+        if ( pTemp != pNode )
+            continue;
+        Vec_PtrWriteEntry( vVecTemp, m, NULL );
+        break;
+    }
+    assert( m < Vec_PtrSize(vVecTemp) ); // found
+    pNode->fMarkB = 0;
+}
 
 
 
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index ead24663..ee77cd02 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -404,6 +404,11 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                 printf( " duplicated fanin %s.\n", Abc_ObjName(Abc_ObjFanin(pObj,k)) );
             }
+
+    // save time: do not check large fanout lists
+    if ( pObj->vFanouts.nSize > 20 )
+        return Value;
+
     // make sure fanouts are not duplicated
     for ( i = 0; i < pObj->vFanouts.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanouts.nSize; k++ )
diff --git a/src/base/abc/abcCut.c b/src/base/abc/abcCut.c
index 424d7561..b7d83af0 100644
--- a/src/base/abc/abcCut.c
+++ b/src/base/abc/abcCut.c
@@ -24,8 +24,6 @@
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
-static Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -78,8 +76,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
         if ( Abc_NodeIsConst(pObj) )
             continue;
         // compute the cuts to the internal node
-        Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
-            Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );  
+        Abc_NodeGetCuts( p, pObj );  
         // add cuts due to choices
         if ( Abc_NodeIsAigChoice(pObj) )
         {
@@ -118,7 +115,7 @@ PRT( "Total", clock() - clk );
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the array of fanout counters.]
+  Synopsis    [Computes the cuts for the network.]
 
   Description []
                
@@ -127,27 +124,63 @@ PRT( "Total", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk )
+void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj )
 {
-    Vec_Int_t * vFanNums;
-    Abc_Obj_t * pObj;//, * pFanout;
-    int i;//, k, nFanouts;
-    vFanNums = Vec_IntAlloc( 0 );
-    Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 );
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) )
-        {
-            Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) );
-/*
-            // get the number of non-CO fanouts
-            nFanouts = 0;
-            Abc_ObjForEachFanout( pObj, pFanout, k )
-                if ( !Abc_ObjIsCo(pFanout) )
-                    nFanouts++;
-            Vec_IntWriteEntry( vFanNums, i, nFanouts );
-*/
-        }
-    return vFanNums;
+    void * pList;
+    if ( pList = Abc_NodeReadCuts( p, pObj ) )
+        return pList;
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj) );
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj) );
+    return Abc_NodeGetCuts( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj )
+{
+    return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj )
+{
+    return Cut_NodeReadCuts( p, pObj->Id );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj )
+{
+    Cut_NodeFreeCuts( p, pObj->Id );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c
index 2667cba5..95454668 100644
--- a/src/base/abc/abcRefactor.c
+++ b/src/base/abc/abcRefactor.c
@@ -34,7 +34,7 @@ struct Abc_ManRef_t_
     int              fVerbose;          // the verbosity flag
     // internal data structures
     DdManager *      dd;                // the BDD manager
-    Vec_Int_t *      vReqTimes;         // required times for each node
+//    Vec_Int_t *      vReqTimes;         // required times for each node
     Vec_Str_t *      vCube;             // temporary
     Vec_Int_t *      vForm;             // temporary
     Vec_Int_t *      vLevNums;          // temporary
@@ -51,6 +51,7 @@ struct Abc_ManRef_t_
     int              timeDcs;
     int              timeSop;
     int              timeFact;
+    int              timeEval;
     int              timeRes;
     int              timeNtk;
     int              timeTotal;
@@ -98,7 +99,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax );
     pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
     pManRef->vLeaves   = Abc_NtkManCutReadLeaves( pManCut );
-    pManRef->vReqTimes = Abc_NtkGetRequiredLevels( pNtk );
+    Abc_NtkStartReverseLevels( pNtk );
 
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
@@ -137,6 +138,7 @@ pManRef->timeTotal = clock() - clkStart;
     // delete the managers
     Abc_NtkManCutStop( pManCut );
     Abc_NtkManRefStop( pManRef );
+    Abc_NtkStopReverseLevels( pNtk );
     // check
     if ( fCheck && !Abc_NtkCheck( pNtk ) )
     {
@@ -165,10 +167,13 @@ Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * v
     DdNode * bNodeFunc, * bNodeDc, * bNodeOn, * bNodeOnDc;
     char * pSop;
     int nBddNodes, nFtNodes, nNodesSaved, nNodesAdded;
-    int i, clk;
+    int i, Required, clk;
 
     p->nNodesConsidered++;
 
+    // get the required level of this node
+    Required = Abc_NodeReadRequiredLevel( pNode );
+
     // get the function of the cut
 clk = clock();
     bNodeFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pNode, vFanins, p->vVisited );  Cudd_Ref( bNodeFunc );
@@ -186,7 +191,7 @@ clk = clock();
 
         nMints = (1 << vFanins->nSize);
         nMintsDc = (int)Cudd_CountMinterm( p->dd, bNodeDc, vFanins->nSize );
-        printf( "Percentage of minterms = %5.2f.\n", 100.0 * nMintsDc / nMints );
+//        printf( "Percentage of minterms = %5.2f.\n", 100.0 * nMintsDc / nMints );
 
         // get the ISF
         bNodeOn   = Cudd_bddAnd( p->dd, bNodeFunc, Cudd_Not(bNodeDc) );   Cudd_Ref( bNodeOn );
@@ -204,13 +209,16 @@ p->timeDcs += clock() - clk;
     // always accept the case of constant node
     if ( Cudd_IsConstant(bNodeFunc) )
     {
-        p->nNodesGained += Abc_NodeMffcSize( pNode );
+        p->nLastGain = Abc_NodeMffcSize( pNode );
+        p->nNodesGained += p->nLastGain;
         p->nNodesRefactored++;
-        // get the costant node
-        pFanin = Abc_ObjNotCond( Abc_AigConst1(pNode->pNtk->pManFunc), Cudd_IsComplement(bNodeFunc) );
-        Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pFanin );
+        // get the constant node
+//        pFanin = Abc_ObjNotCond( Abc_AigConst1(pNode->pNtk->pManFunc), Cudd_IsComplement(bNodeFunc) );
+//        Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pFanin );
+//        Cudd_RecursiveDeref( p->dd, bNodeFunc );
+//printf( "Gain = %d.\n", p->nLastGain );
         Cudd_RecursiveDeref( p->dd, bNodeFunc );
-        return NULL;
+        return Ft_FactorConst( !Cudd_IsComplement(bNodeFunc) );
     }
 
     // get the SOP of the cut
@@ -241,8 +249,10 @@ p->timeFact += clock() - clk;
         pFanin->vFanouts.nSize--;
 
     // detect how many new nodes will be added (while taking into account reused nodes)
+clk = clock();
     nNodesAdded = Abc_NodeStrashDecCount( pNode->pNtk->pManFunc, pNode, vFanins, vForm, 
-        p->vLevNums, nNodesSaved, Vec_IntEntry( p->vReqTimes, pNode->Id ) );
+        p->vLevNums, nNodesSaved, Required );
+p->timeEval += clock() - clk;
     // quit if there is no improvement
     if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !fUseZeros )
     {
@@ -316,7 +326,7 @@ Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUse
 void Abc_NtkManRefStop( Abc_ManRef_t * p )
 {
     Extra_StopManager( p->dd );
-    Vec_IntFree( p->vReqTimes );
+//    Vec_IntFree( p->vReqTimes );
     Vec_PtrFree( p->vVisited );
     Vec_IntFree( p->vLevNums );
     Vec_StrFree( p->vCube    );
@@ -337,15 +347,16 @@ void Abc_NtkManRefStop( Abc_ManRef_t * p )
 void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
 {
     printf( "Refactoring statistics:\n" );
-    printf( "Nodes considered  = %6d.\n", p->nNodesConsidered );
-    printf( "Nodes refactored  = %6d.\n", p->nNodesRefactored );
-    printf( "Calculated gain   = %6d.\n", p->nNodesGained     );
+    printf( "Nodes considered  = %8d.\n", p->nNodesConsidered );
+    printf( "Nodes refactored  = %8d.\n", p->nNodesRefactored );
+    printf( "Calculated gain   = %8d.\n", p->nNodesGained     );
     PRT( "Cuts       ", p->timeCut );
     PRT( "Resynthesis", p->timeRes );
     PRT( "    BDD    ", p->timeBdd );
     PRT( "    DCs    ", p->timeDcs );
     PRT( "    SOP    ", p->timeSop );
     PRT( "    FF     ", p->timeFact );
+    PRT( "    Eval   ", p->timeEval );
     PRT( "AIG update ", p->timeNtk );
     PRT( "TOTAL      ", p->timeTotal );
 }
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index ea7aeff4..1a8f7966 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -124,10 +124,7 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t
     int Counter;
     // label visited nodes
     if ( fLabel )
-    {
         Abc_NodeSetTravIdCurrent( pNode );
-//printf( "Labeling " );  Abc_AigPrintNode( pNode );
-    }
     // collect visited nodes
     if ( vNodes )
         Vec_PtrPush( vNodes, pNode );
diff --git a/src/base/abc/abcRewrite.c b/src/base/abc/abcRewrite.c
index 0cd56349..0b573bac 100644
--- a/src/base/abc/abcRewrite.c
+++ b/src/base/abc/abcRewrite.c
@@ -20,11 +20,15 @@
 
 #include "abc.h"
 #include "rwr.h"
+#include "ft.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop );
+static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -40,20 +44,28 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRewrite( Abc_Ntk_t * pNtk )
+int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
 {
     int fCheck = 1;
+    int fDrop = 0;
     ProgressBar * pProgress;
-    Rwr_Man_t * p;
+    Cut_Man_t * pManCut;
+    Rwr_Man_t * pManRwr;
     Abc_Obj_t * pNode;
     int i, nNodes, nGain;
+    int clk, clkStart = clock();
 
     assert( Abc_NtkIsAig(pNtk) );
     // start the rewriting manager
-    p = Rwr_ManStart( 0 );
-    if ( p == NULL )
+    pManRwr = Rwr_ManStart( 0 );
+    if ( pManRwr == NULL )
         return 0;
-    Rwr_ManPrepareNetwork( p, pNtk );
+    Abc_NtkStartReverseLevels( pNtk );
+    // start the cut manager
+clk = clock();
+    pManCut = Abc_NtkStartCutManForRewrite( pNtk, fDrop );
+Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
+    pNtk->pManCut = pManCut;
 
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
@@ -68,12 +80,28 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk )
         if ( Abc_NodeIsConst(pNode) )
             continue;
         // for each cut, try to resynthesize it
-        if ( (nGain = Rwr_NodeRewrite( p, pNode )) >= 0 )
-            Abc_NodeUpdate( pNode, Rwr_ManReadFanins(p), Rwr_ManReadDecs(p), nGain );
+        nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros );
+        if ( nGain > 0 || nGain == 0 && fUseZeros )
+        {
+            Vec_Int_t * vForm   = Rwr_ManReadDecs(pManRwr);
+            Vec_Ptr_t * vFanins = Rwr_ManReadFanins(pManRwr);
+            int fCompl          = Rwr_ManReadCompl(pManRwr);
+            // complement the FF if needed
+            if ( fCompl ) Ft_FactorComplement( vForm );
+            Abc_NodeUpdate( pNode, vFanins, vForm, nGain );
+            if ( fCompl ) Ft_FactorComplement( vForm );
+        }
     }
     Extra_ProgressBarStop( pProgress );
-    // delete the manager
-    Rwr_ManStop( p );
+Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
+    // print stats
+    if ( fVerbose )
+        Rwr_ManPrintStats( pManRwr );
+    // delete the managers
+    Rwr_ManStop( pManRwr );
+    Cut_ManStop( pManCut );
+    pNtk->pManCut = NULL;
+    Abc_NtkStopReverseLevels( pNtk );
     // check
     if ( fCheck && !Abc_NtkCheck( pNtk ) )
     {
@@ -84,6 +112,70 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut manager for rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk, int fDrop )
+{
+    static Cut_Params_t Params, * pParams = &Params;
+    Cut_Man_t * pManCut;
+    Abc_Obj_t * pObj;
+    int i;
+    // start the cut manager
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = 4;     // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
+    pParams->fTruth    = 1;     // compute truth tables
+    pParams->fHash     = 1;     // hash cuts to detect unique
+    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fSeq      = 0;     // compute sequential cuts
+    pParams->fDrop     = fDrop; // drop cuts on the fly
+    pParams->fVerbose  = 0;     // the verbosiness flag
+    pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
+    pManCut = Cut_ManStart( pParams );
+    if ( pParams->fDrop )
+        Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) );
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_NodeSetTriv( pManCut, pObj->Id );
+    return pManCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the cuts at the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodePrintCuts( Abc_Obj_t * pNode )
+{
+    Cut_Cut_t * pCut;
+    unsigned uTruth;
+    printf( "\nNode %s\n", Abc_ObjName(pNode) );
+    for ( pCut = (Cut_Cut_t *)pNode->pCopy; pCut; pCut = pCut->pNext )
+    {
+        uTruth = pCut->uTruth;
+        Extra_PrintBinary( stdout, &uTruth, 16 ); 
+        printf( "   " );
+        Cut_CutPrint( pCut );   
+        printf( "\n" );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index 1c4134d0..961e6c5f 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -318,12 +318,12 @@ Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t
     nVars = Ft_FactorGetNumVars( vForm );
     assert( nVars >= 0 );
     assert( vForm->nSize > nVars );
-    assert( nVars == vFanins->nSize );
 
     // check for constant function
     pFtNode = Ft_NodeRead( vForm, 0 );
     if ( pFtNode->fConst )
         return Abc_ObjNotCond( Abc_AigConst1(pMan), pFtNode->fCompl );
+    assert( nVars == vFanins->nSize );
 
     // compute the function of other nodes
     for ( i = nVars; i < vForm->nSize; i++ )
@@ -365,17 +365,17 @@ int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFa
     nVars = Ft_FactorGetNumVars( vForm );
     assert( nVars >= 0 );
     assert( vForm->nSize > nVars );
-    assert( nVars == vFanins->nSize ); // set the fanin number to nVars???
 
     // check for constant function
     pFtNode = Ft_NodeRead( vForm, 0 );
     if ( pFtNode->fConst )
         return 0;
+    assert( nVars == vFanins->nSize ); 
 
     // set the levels
     Vec_IntClear( vLevels );
     Vec_PtrForEachEntry( vFanins, pAnd, i )
-        Vec_IntPush( vLevels, pAnd->Level );
+        Vec_IntPush( vLevels, Abc_ObjRegular(pAnd)->Level );
 
     // compute the function of other nodes
     Counter = 0;
@@ -422,9 +422,17 @@ int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFa
         }
 
         // count the number of new levels
-        if ( pAnd && Abc_ObjRegular(pAnd) == Abc_AigConst1(pMan) )
-            LevelNew = 0;
-        else
+        LevelNew = -1;
+        if ( pAnd )
+        {
+            if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pMan) )
+                LevelNew = 0;
+            else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd0) )
+                LevelNew = (int)Abc_ObjRegular(pAnd0)->Level;
+            else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) )
+                LevelNew = (int)Abc_ObjRegular(pAnd1)->Level;
+        }
+        if ( LevelNew == -1 )
             LevelNew = 1 + ABC_MAX( Vec_IntEntry(vLevels, pFtNode->iFanin0), Vec_IntEntry(vLevels, pFtNode->iFanin1) );
 
 //        assert( pAnd == NULL || LevelNew == LevelOld );
@@ -433,7 +441,11 @@ int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFa
             LevelOld = (int)Abc_ObjRegular(pAnd)->Level;
             if ( LevelNew != LevelOld ) 
             {
-               int x = 0;
+                int x = 0;
+                Abc_Obj_t * pFanin0, * pFanin1;
+                pFanin0 = Abc_ObjFanin0( Abc_ObjRegular(pAnd) );
+                pFanin1 = Abc_ObjFanin1( Abc_ObjRegular(pAnd) );
+                x = 0;
             }
         }
 
diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c
index 10f8ae98..9d71ace5 100644
--- a/src/base/abc/abcTiming.c
+++ b/src/base/abc/abcTiming.c
@@ -626,47 +626,126 @@ void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode )
     pTimeOut->Worst = ABC_MAX( pTimeOut->Rise, pTimeOut->Fall );
 }
 
+
+
+
 /**Function*************************************************************
 
-  Synopsis    [Creates the array of required times.]
+  Synopsis    [Prepares the AIG for the comptuation of required levels.]
 
-  Description []
+  Description [This procedure should be called before the required times
+  are used. It starts internal data structures, which records the level 
+  from the COs of the AIG nodes in reverse topologogical order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Abc_NtkGetRequiredLevels( Abc_Ntk_t * pNtk )
+void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
 {
-    Vec_Int_t * vReqTimes;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj, * pFanout;
-    int i, k, nLevelsMax, nLevelsCur;
-    // start the required times
-    vReqTimes = Vec_IntAlloc( 0 );
-    Vec_IntFill( vReqTimes, Abc_NtkObjNumMax(pNtk), ABC_INFINITY );
+    int i, k, nLevelsCur;
+    assert( Abc_NtkIsAig(pNtk) );
+    // remember the maximum number of direct levels
+    pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
+    // start the reverse levels
+    pNtk->vLevelsR = Vec_IntAlloc( 0 );
+    Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 );
     // compute levels in reverse topological order
-    Abc_NtkForEachCo( pNtk, pObj, i )
-        Vec_IntWriteEntry( vReqTimes, pObj->Id, 0 );
     vNodes = Abc_NtkDfsReverse( pNtk );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         nLevelsCur = 0;
         Abc_ObjForEachFanout( pObj, pFanout, k )
-            if ( nLevelsCur < Vec_IntEntry(vReqTimes, pFanout->Id) )
-                nLevelsCur = Vec_IntEntry(vReqTimes, pFanout->Id);
-        Vec_IntWriteEntry( vReqTimes, pObj->Id, nLevelsCur + 1 );
+            if ( nLevelsCur < Vec_IntEntry(pNtk->vLevelsR, pFanout->Id) )
+                nLevelsCur = Vec_IntEntry(pNtk->vLevelsR, pFanout->Id);
+        Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, nLevelsCur + 1 );
     }
     Vec_PtrFree( vNodes );
-    // convert levels into required times: RetTime = NumLevels + 1 - Level
-    nLevelsMax = Abc_AigGetLevelNum(pNtk) + 1;
-    Abc_NtkForEachNode( pNtk, pObj, i )
-        Vec_IntWriteEntry( vReqTimes, pObj->Id, nLevelsMax - Vec_IntEntry(vReqTimes, pObj->Id) );
-//    Abc_NtkForEachNode( pNtk, pObj, i )
-//        printf( "(%d,%d)", pObj->Level, Vec_IntEntry(vReqTimes, pObj->Id) );
-//    printf( "\n" );
-    return vReqTimes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the data structures used to compute required levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk )
+{
+    assert( pNtk->vLevelsR );
+    Vec_IntFree( pNtk->vLevelsR );
+    pNtk->vLevelsR = NULL;
+    pNtk->LevelMax = 0;
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the reverse level of the node.]
+
+  Description [The reverse level is the level of the node in reverse
+  topological order, starting from the COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( Abc_NtkIsAig(pNtk) );
+    assert( pNtk->vLevelsR );
+    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
+    Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the reverse level of the node.]
+
+  Description [The reverse level is the level of the node in reverse
+  topological order, starting from the COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( Abc_NtkIsAig(pNtk) );
+    assert( pNtk->vLevelsR );
+    Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
+    return Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns required level of the node.]
+
+  Description [Converts the reverse levels of the node into its required 
+  level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    assert( Abc_NtkIsAig(pNtk) );
+    assert( pNtk->vLevelsR );
+    return pNtk->LevelMax + 1 - Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index d62cec11..87d57947 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1021,6 +1021,30 @@ void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
     pNtk->tObj2Name = tObj2NameNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates the array of fanout counters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vFanNums;
+    Abc_Obj_t * pObj;
+    int i;
+    vFanNums = Vec_IntAlloc( 0 );
+    Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) )
+            Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) );
+    return vFanNums;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////