Version abc50827

31 files changed, 1160 insertions, 585 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                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index a12fbce4..d5b0330f 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -674,7 +674,7 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
         if ( uCanons[uTruth] )
         {
             assert( uTruth > uCanons[uTruth] );
-            uMap[uTruth] = uMap[uCanons[uTruth]];
+            uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]];
             continue;
         }
         uMap[uTruth] = nClasses++;
diff --git a/src/misc/vec/vecFan.h b/src/misc/vec/vecFan.h
index 8698a1b7..08d1d734 100644
--- a/src/misc/vec/vecFan.h
+++ b/src/misc/vec/vecFan.h
@@ -47,8 +47,8 @@ struct Abc_Fan_t_ // 1 word
 typedef struct Vec_Fan_t_       Vec_Fan_t;
 struct Vec_Fan_t_ 
 {
-    int              nSize;
     int              nCap;
+    int              nSize;
     Abc_Fan_t *      pArray;
 };
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 919b7e5a..793dd567 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -39,8 +39,8 @@
 typedef struct Vec_Int_t_       Vec_Int_t;
 struct Vec_Int_t_ 
 {
-    int              nSize;
     int              nCap;
+    int              nSize;
     int *            pArray;
 };
 
@@ -322,9 +322,31 @@ static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Entry )
 {
     int i;
     Vec_IntGrow( p, nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = Entry;
     p->nSize = nSize;
-    for ( i = 0; i < p->nSize; i++ )
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
+{
+    int i;
+    if ( p->nSize >= nSize )
+        return;
+    Vec_IntGrow( p, nSize );
+    for ( i = p->nSize; i < nSize; i++ )
         p->pArray[i] = Entry;
+    p->nSize = nSize;
 }
 
 /**Function*************************************************************
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index ed78c8c2..1d3e0633 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -39,8 +39,8 @@
 typedef struct Vec_Ptr_t_       Vec_Ptr_t;
 struct Vec_Ptr_t_ 
 {
-    int              nSize;
     int              nCap;
+    int              nSize;
     void **          pArray;
 };
 
@@ -323,9 +323,31 @@ static inline void Vec_PtrFill( Vec_Ptr_t * p, int nSize, void * Entry )
 {
     int i;
     Vec_PtrGrow( p, nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = Entry;
     p->nSize = nSize;
-    for ( i = 0; i < p->nSize; i++ )
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
+{
+    int i;
+    if ( p->nSize >= nSize )
+        return;
+    Vec_PtrGrow( p, nSize );
+    for ( i = p->nSize; i < nSize; i++ )
         p->pArray[i] = Entry;
+    p->nSize = nSize;
 }
 
 /**Function*************************************************************
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 2a9dc7a0..4b8e6a1c 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -39,8 +39,8 @@
 typedef struct Vec_Str_t_       Vec_Str_t;
 struct Vec_Str_t_ 
 {
-    int              nSize;
     int              nCap;
+    int              nSize;
     char *           pArray;
 };
 
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index 4ee62080..bb911bfe 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -39,9 +39,9 @@
 typedef struct Vec_Vec_t_       Vec_Vec_t;
 struct Vec_Vec_t_ 
 {
-    int         nSize;
-    int         nCap;
-    void **     pArray;
+    int              nCap;
+    int              nSize;
+    void **          pArray;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -55,6 +55,8 @@ struct Vec_Vec_t_
     for ( i = LevelStart; (i < Vec_PtrSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
 #define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop )                 \
     for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelReverse( vGlob, vVec, i )                                          \
+    for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i-- )
 
 // iteratores through entries
 #define Vec_VecForEachEntry( vGlob, pEntry, i, k )                                            \
@@ -96,6 +98,28 @@ static inline Vec_Vec_t * Vec_VecAlloc( int nCap )
 
 /**Function*************************************************************
 
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Vec_t * Vec_VecStart( int nSize )
+{
+    Vec_Vec_t * p;
+    int i;
+    p = Vec_VecAlloc( nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = Vec_PtrAlloc( 0 );
+    p->nSize = nSize;
+    return p;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index 0b4c4535..f3a0f743 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -99,6 +99,7 @@ extern void             Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t *
 extern void             Cut_NodeFreeCuts( Cut_Man_t * p, int Node );
 extern void             Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node );
 extern void             Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node );
+extern void             Cut_CutPrint( Cut_Cut_t * pCut );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index da54a188..fe5080b4 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -70,6 +70,7 @@ struct Cut_ManStruct_t_
     int                nCutsPeak;
     int                nCutsTriv;
     int                nCutsNode;
+    int                nNodes;
     // runtime
     int                timeMerge;
     int                timeUnion;
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index a96f8173..4ad3a66a 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -141,8 +141,9 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     printf( "Peak cuts         = %8d.\n", p->nCutsPeak );
     printf( "Total allocated   = %8d.\n", p->nCutsAlloc );
     printf( "Total deallocated = %8d.\n", p->nCutsDealloc );
-    printf( "The cut size      = %3d bytes.\n", p->EntrySize );
-    printf( "Peak memory       = %.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
+    printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsCur-p->nCutsTriv))/p->nNodes );
+    printf( "The cut size      = %8d bytes.\n", p->EntrySize );
+    printf( "Peak memory       = %8.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
     PRT( "Merge ", p->timeMerge );
     PRT( "Union ", p->timeUnion );
     PRT( "Hash  ", Cut_TableReadTime(p->tTable) );
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 6ce3b983..8d16ac8a 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -65,6 +65,8 @@ static void               Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
 ***********************************************************************/
 Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
 {
+    if ( Node >= p->vCuts->nSize )
+        return NULL;
     return Vec_PtrEntry( p->vCuts, Node );
 }
 
@@ -209,6 +211,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
     }
 finish :
     // set the list at the node
+    Vec_PtrFillExtra( p->vCuts, Node + 1, NULL );
     assert( Cut_NodeReadCuts(p, Node) == NULL );
     pList0 = Cut_ListFinish( &SuperList );
     Cut_NodeWriteCuts( p, Node, pList0 );
@@ -227,6 +230,7 @@ clk = clock();
     if ( p->pParams->fFilter )
         Cut_CutFilter( p, pList0 );
 p->timeFilter += clock() - clk;
+    p->nNodes++;
     return pList0;
 }
 
@@ -387,6 +391,7 @@ clk = clock();
     if ( p->pParams->fFilter )
         Cut_CutFilter( p, pList );
 p->timeFilter += clock() - clk;
+    p->nNodes -= vNodes->nSize - 1;
     return pList;
 }
 
@@ -498,7 +503,7 @@ void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
 void Cut_CutPrint( Cut_Cut_t * pCut )
 {
     int i;
-    assert( pCut->nLeaves > 1 );
+    assert( pCut->nLeaves > 0 );
     printf( "%d : {", pCut->nLeaves );
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
         printf( " %d", pCut->pLeaves[i] );
diff --git a/src/opt/rwr/module.make b/src/opt/rwr/module.make
index fc72630f..077a3c01 100644
--- a/src/opt/rwr/module.make
+++ b/src/opt/rwr/module.make
@@ -1,4 +1,4 @@
-SRC +=  src/opt/rwr/rwrCut.c \
+SRC +=  src/opt/rwr/rwrDec.c \
     src/opt/rwr/rwrEva.c \
     src/opt/rwr/rwrExp.c \
     src/opt/rwr/rwrLib.c \
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 5d190745..6e127b27 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "abc.h"
+#include "cut.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -39,7 +40,6 @@
 
 typedef struct Rwr_Man_t_   Rwr_Man_t;
 typedef struct Rwr_Node_t_  Rwr_Node_t;
-typedef struct Rwr_Cut_t_   Rwr_Cut_t;
 
 struct Rwr_Man_t_
 {
@@ -50,7 +50,7 @@ struct Rwr_Man_t_
     char *             pPerms;           // canonical permutations
     unsigned char *    pMap;             // mapping of functions into class numbers
     char *             pPractical;       // practical NPN classes
-    unsigned short **  puPerms43;        // four-var permutations for three var functions
+    char **            pPerms4;          // four-var permutations
     // node space
     Vec_Ptr_t *        vForest;          // all the nodes
     Rwr_Node_t **      pTable;           // the hash table of nodes by their canonical form
@@ -61,19 +61,26 @@ struct Rwr_Man_t_
     int                nConsidered;      // the number of nodes considered
     int                nAdded;           // the number of nodes added to lists
     int                nClasses;         // the number of NN classes
-    // intermediate data
-    Vec_Int_t *        vFanNums;         // the number of fanouts of each node (used to free cuts)
-    Vec_Int_t *        vReqTimes;        // the required times for each node (used for delay-driven evalution)
     // the result of resynthesis
+    int                fCompl;           // indicates if the output of FF should be complemented
     Vec_Int_t *        vForm;            // the decomposition tree (temporary)
-    Vec_Int_t *        vLevNums;         // the array of levels (temporary)
     Vec_Ptr_t *        vFanins;          // the fanins array (temporary)
-    int                nGainMax;
+    Vec_Ptr_t *        vFaninsCur;       // the fanins array (temporary)
+    Vec_Int_t *        vLevNums;         // the array of levels (temporary)
+    // node statistics
+    int                nNodesConsidered;
+    int                nNodesRewritten;
+    int                nNodesGained;
+    int                nScores[222];
+    int                nCutsGood;
+    int                nCutsBad;
+    int                nSubgraphs;
     // runtime statistics
-    int                time1;
-    int                time2;
-    int                time3;
-    int                time4;
+    int                timeStart;
+    int                timeCut;
+    int                timeRes;
+    int                timeEval;
+    int                timeTotal;
 };
 
 struct Rwr_Node_t_ // 24 bytes
@@ -90,18 +97,6 @@ struct Rwr_Node_t_ // 24 bytes
     Rwr_Node_t *       pNext;            // next in the table
 };
 
-struct Rwr_Cut_t_ // 24 bytes
-{
-    unsigned           nLeaves : 3;      // the number of leaves
-    unsigned           fTime  :  1;      // set to 1 if meets the required times
-    unsigned           fGain  :  1;      // set to 1 if does not increase nodes
-    unsigned           Volume : 11;      // the gain in the number of nodes
-    unsigned           uTruth : 16;      // the truth table
-    Abc_Obj_t *        ppLeaves[4];      // the leaves
-    Rwr_Cut_t *        pNext;            // the next cut in the list
-};
-
-
 // manipulation of complemented attributes
 static inline bool         Rwr_IsComplement( Rwr_Node_t * p )    { return (bool)(((unsigned)p) & 01);           }
 static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p )         { return (Rwr_Node_t *)((unsigned)(p) & ~01);  }
@@ -116,12 +111,10 @@ static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_N
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== rwrCut.c ========================================================*/
-extern void              Rwr_NtkStartCuts( Rwr_Man_t * p, Abc_Ntk_t * pNtk );
-extern void              Rwr_NodeComputeCuts( Rwr_Man_t * p, Abc_Obj_t * pNode );
-/*=== rwrEva.c ========================================================*/
-extern int               Rwr_NodeRewrite( Rwr_Man_t * p, Abc_Obj_t * pNode );
+/*=== rwrDec.c ========================================================*/
 extern void              Rwr_ManPreprocess( Rwr_Man_t * p );
+/*=== rwrEva.c ========================================================*/
+extern int               Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros );
 /*=== rwrLib.c ========================================================*/
 extern void              Rwr_ManPrecompute( Rwr_Man_t * p );
 extern Rwr_Node_t *      Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute );
@@ -131,14 +124,18 @@ extern void              Rwr_ManIncTravId( Rwr_Man_t * p );
 /*=== rwrMan.c ========================================================*/
 extern Rwr_Man_t *       Rwr_ManStart( bool fPrecompute );
 extern void              Rwr_ManStop( Rwr_Man_t * p );
+extern void              Rwr_ManPrintStats( Rwr_Man_t * p );
 extern void              Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *       Rwr_ManReadFanins( Rwr_Man_t * p );
 extern Vec_Int_t *       Rwr_ManReadDecs( Rwr_Man_t * p );
+extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
+extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
+extern void              Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time );
 /*=== rwrPrint.c ========================================================*/
 extern void              Rwr_ManPrint( Rwr_Man_t * p );
 /*=== rwrUtil.c ========================================================*/
 extern void              Rwr_ManWriteToArray( Rwr_Man_t * p );
-extern void              Rwr_ManLoadFromArray( Rwr_Man_t * p );
+extern void              Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose );
 extern void              Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName );
 extern void              Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName );
 extern Vec_Int_t *       Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk );
diff --git a/src/opt/rwr/rwrCut.c b/src/opt/rwr/rwrCut.c
deleted file mode 100644
index be512963..00000000
--- a/src/opt/rwr/rwrCut.c
+++ /dev/null
@@ -1,254 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [rwrCut.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [DAG-aware AIG rewriting package.]
-
-  Synopsis    [Cut computation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: rwrCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "rwr.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Rwr_Cut_t * Rwr_CutAlloc( Rwr_Man_t * p );
-static Rwr_Cut_t * Rwr_CutCreateTriv( Rwr_Man_t * p, Abc_Obj_t * pNode );
-static Rwr_Cut_t * Rwr_CutsMerge( Rwr_Man_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes cuts for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Rwr_NtkStartCuts( Rwr_Man_t * p, Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    int i;
-    // set the trivial cuts
-    Abc_NtkCleanCopy( pNtk );
-    Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)Rwr_CutCreateTriv( p, pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes cuts for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Rwr_NodeComputeCuts( Rwr_Man_t * p, Abc_Obj_t * pNode )
-{
-    Rwr_Cut_t * pCuts0, * pCuts1, * pTemp0, * pTemp1, * pCut;
-    Rwr_Cut_t * pList = NULL, ** ppPlace = &pList; // linked list of cuts
-    assert( Abc_ObjIsNode(pNode) );
-    if ( Abc_NodeIsConst(pNode) )
-        return;
-    // create the elementary cut
-    pCut = Rwr_CutCreateTriv( p, pNode );
-    // add it to the linked list
-    *ppPlace = pCut;  ppPlace  = &pCut->pNext;
-    // create cuts by merging pairwise
-    pCuts0 = (Rwr_Cut_t *)Abc_ObjFanin0(pNode)->pCopy;
-    pCuts1 = (Rwr_Cut_t *)Abc_ObjFanin1(pNode)->pCopy;
-    assert( pCuts0 && pCuts1 );
-    for ( pTemp0 = pCuts0; pTemp0; pTemp0 = pTemp0->pNext )
-    for ( pTemp1 = pCuts1; pTemp1; pTemp1 = pTemp1->pNext )
-    {
-        pCut = Rwr_CutsMerge( p, pTemp0, pTemp1, Abc_ObjFaninC0(pNode), Abc_ObjFaninC1(pNode) );
-        if ( pCut == NULL )
-            continue;
-        // add it to the linked list
-        *ppPlace = pCut;  ppPlace  = &pCut->pNext;
-    }
-    // set the linked list
-    pNode->pCopy = (Abc_Obj_t *)pList;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Rwr_Cut_t * Rwr_CutsMerge( Rwr_Man_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 )
-{
-    Abc_Obj_t * ppNodes[4], * pNodeTemp;
-    Rwr_Cut_t * pCut;
-    unsigned uPhase, uTruth0, uTruth1;
-    int i, k, min, nTotal;
-
-    // solve the most typical case: both cuts are four input
-    if ( pCut0->nLeaves == 4 && pCut1->nLeaves == 4 )
-    {
-        for ( i = 0; i < 4; i++ )
-            if ( pCut0->ppLeaves[i] != pCut1->ppLeaves[i] )
-                return NULL;
-        // create the cut
-        pCut = Rwr_CutAlloc( p );
-        pCut->nLeaves = 4;
-        for ( i = 0; i < 4; i++ )
-            pCut->ppLeaves[i] = pCut0->ppLeaves[i];
-        pCut->uTruth = (fCompl0? ~pCut0->uTruth : pCut0->uTruth) & (fCompl1? ~pCut1->uTruth : pCut1->uTruth) & 0xFFFF;
-        return pCut;
-    }
-
-    // create the set of new nodes
-    // count the number of unique entries in pCut1
-    nTotal = pCut0->nLeaves;
-    for ( i = 0; i < (int)pCut1->nLeaves; i++ )
-    {
-        // try to find this entry among the leaves of pCut0
-        for ( k = 0; k < (int)pCut0->nLeaves; k++ )
-            if ( pCut1->ppLeaves[i] == pCut0->ppLeaves[k] )
-                break;
-        if ( k < (int)pCut0->nLeaves ) // found
-            continue;
-        // we found a new entry to add
-        if ( nTotal == 4 )
-            return NULL;
-        ppNodes[nTotal++] = pCut1->ppLeaves[i];
-    }
-    // we know that the feasible cut exists
-
-    // add the starting entries
-    for ( k = 0; k < (int)pCut0->nLeaves; k++ )
-        ppNodes[k] = pCut0->ppLeaves[k];
-
-    // selection-sort the entries
-    for ( i = 0; i < nTotal - 1; i++ )
-    {
-        min = i;
-        for ( k = i+1; k < nTotal; k++ )
-            if ( ppNodes[k]->Id < ppNodes[min]->Id )
-                min = k;
-        pNodeTemp    = ppNodes[i];
-        ppNodes[i]   = ppNodes[min];
-        ppNodes[min] = pNodeTemp;
-    }
-
-    // find the mapping from the old nodes to the new
-    if ( pCut0->nLeaves == 4 )
-        uTruth0 = pCut0->uTruth;
-    else
-    {
-        uPhase = 0;
-        for ( i = 0; i < (int)pCut0->nLeaves; i++ )
-        {
-            for ( k = 0; k < nTotal; k++ )
-                if ( pCut0->ppLeaves[i] == ppNodes[k] )
-                    break;
-            uPhase |= (1 << k);
-        }
-        assert( uPhase < 16 );
-        assert( pCut0->uTruth < 256 );
-        uTruth0 = p->puPerms43[pCut0->uTruth][uPhase];
-    }
-
-    // find the mapping from the old nodes to the new
-    if ( pCut1->nLeaves == 4 )
-        uTruth1 = pCut1->uTruth;
-    else
-    {
-        uPhase = 0;
-        for ( i = 0; i < (int)pCut1->nLeaves; i++ )
-        {
-            for ( k = 0; k < nTotal; k++ )
-                if ( pCut1->ppLeaves[i] == ppNodes[k] )
-                    break;
-            uPhase |= (1 << k);
-        }
-        assert( uPhase < 16 );
-        assert( pCut1->uTruth < 256 );
-        uTruth1 = p->puPerms43[pCut1->uTruth][uPhase];
-    }
-
-    // create the cut
-    pCut = Rwr_CutAlloc( p );
-    pCut->nLeaves = nTotal;
-    for ( i = 0; i < nTotal; i++ )
-        pCut->ppLeaves[i] = ppNodes[i];
-    pCut->uTruth = (fCompl0? ~uTruth0 : uTruth0) & (fCompl1? ~uTruth1 : uTruth1) & 0xFFFF;
-    return pCut;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Rwr_Cut_t * Rwr_CutAlloc( Rwr_Man_t * p )
-{
-    Rwr_Cut_t * pCut;
-    pCut = (Rwr_Cut_t *)Extra_MmFixedEntryFetch( p->pMmNode );
-    memset( pCut, 0, sizeof(Rwr_Cut_t) );
-    return pCut;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Start the cut computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Rwr_Cut_t * Rwr_CutCreateTriv( Rwr_Man_t * p, Abc_Obj_t * pNode )
-{
-    Rwr_Cut_t * pCut;
-    pCut = Rwr_CutAlloc( p );
-    pCut->nLeaves = 1;
-    pCut->ppLeaves[0] = pNode;
-    pCut->uTruth = 0xAAAA;
-    return pCut;
-}
-
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
new file mode 100644
index 00000000..9cfc9659
--- /dev/null
+++ b/src/opt/rwr/rwrDec.c
@@ -0,0 +1,231 @@
+/**CFile****************************************************************
+
+  FileName    [rwrDec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    [Evaluation and decomposition procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrDec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+#include "ft.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode );
+static int         Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm );
+static void        Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruth );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Preprocesses computed library of subgraphs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManPreprocess( Rwr_Man_t * p )
+{
+    Rwr_Node_t * pNode;
+    int i, k;
+    // put the nodes into the structure
+    p->vClasses = Vec_VecStart( 222 );
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        if ( p->pTable[i] == NULL )
+            continue;
+        // consider all implementations of this function
+        for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
+        {
+            assert( pNode->uTruth == p->pTable[i]->uTruth );
+            assert( p->pMap[pNode->uTruth] >= 0 && p->pMap[pNode->uTruth] < 222 );
+            Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
+        }
+    }
+    // compute decomposition forms for each node
+    Vec_VecForEachEntry( p->vClasses, pNode, i, k )
+        pNode->pNext = (Rwr_Node_t *)Rwr_NodePreprocess( p, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Preprocesses subgraphs rooted at this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
+{
+    Vec_Int_t * vForm;
+    int i, Root;
+    // consider constant
+    if ( pNode->uTruth == 0 )
+        return Ft_FactorConst( 0 );
+    // consider the case of elementary var
+    if ( pNode->uTruth == 0x00FF )
+        return Ft_FactorVar( 3, 4, 1 );
+    // start the factored form
+    vForm = Vec_IntAlloc( 10 );
+    for ( i = 0; i < 4; i++ )
+        Vec_IntPush( vForm, 0 );
+    // collect the nodes
+    Rwr_ManIncTravId( p );
+    Root = Rwr_TravCollect_rec( p, pNode, vForm );
+    if ( Root & 1 )
+        Ft_FactorComplement( vForm );
+    // verify the factored form
+    Rwr_FactorVerify( vForm, pNode->uTruth );
+    return vForm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm )
+{
+    Ft_Node_t Node, NodeA, NodeB;
+    int Node0, Node1;
+    // elementary variable
+    if ( pNode->fUsed )
+        return ((pNode->Id - 1) << 1); 
+    // previously visited node
+    if ( pNode->TravId == p->nTravIds )
+        return pNode->Volume;
+    pNode->TravId = p->nTravIds;
+    // solve for children
+    Node0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), vForm );
+    Node1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), vForm );
+    // create the decomposition node(s)
+    if ( pNode->fExor )
+    {
+        assert( !Rwr_IsComplement(pNode->p0) );
+        assert( !Rwr_IsComplement(pNode->p1) );
+        NodeA.fIntern = 1;
+        NodeA.fConst  = 0;
+        NodeA.fCompl  = 0;
+        NodeA.fCompl0 = !(Node0 & 1);
+        NodeA.fCompl1 =  (Node1 & 1);
+        NodeA.iFanin0 = (Node0 >> 1);
+        NodeA.iFanin1 = (Node1 >> 1);
+        Vec_IntPush( vForm, Ft_Node2Int(NodeA) );
+
+        NodeB.fIntern = 1;
+        NodeB.fConst  = 0;
+        NodeB.fCompl  = 0;
+        NodeB.fCompl0 =  (Node0 & 1);
+        NodeB.fCompl1 = !(Node1 & 1);
+        NodeB.iFanin0 = (Node0 >> 1);
+        NodeB.iFanin1 = (Node1 >> 1);
+        Vec_IntPush( vForm, Ft_Node2Int(NodeB) );
+
+        Node.fIntern = 1;
+        Node.fConst  = 0;
+        Node.fCompl  = 0;
+        Node.fCompl0 = 1;
+        Node.fCompl1 = 1;
+        Node.iFanin0 = vForm->nSize - 2;
+        Node.iFanin1 = vForm->nSize - 1;
+        Vec_IntPush( vForm, Ft_Node2Int(Node) );
+    }
+    else
+    {
+        Node.fIntern = 1;
+        Node.fConst  = 0;
+        Node.fCompl  = 0;
+        Node.fCompl0 = Rwr_IsComplement(pNode->p0) ^ (Node0 & 1);
+        Node.fCompl1 = Rwr_IsComplement(pNode->p1) ^ (Node1 & 1);
+        Node.iFanin0 = (Node0 >> 1);
+        Node.iFanin1 = (Node1 >> 1);
+        Vec_IntPush( vForm, Ft_Node2Int(Node) );
+    }
+    // save the number of this node
+    pNode->Volume = ((vForm->nSize - 1) << 1) | pNode->fExor;
+    return pNode->Volume;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruthGold )
+{
+    Ft_Node_t * pFtNode;
+    Vec_Int_t * vTruths;
+    unsigned uTruth, uTruth0, uTruth1;
+    int i;
+
+    vTruths = Vec_IntAlloc( vForm->nSize );
+    Vec_IntPush( vTruths, 0xAAAA );
+    Vec_IntPush( vTruths, 0xCCCC );
+    Vec_IntPush( vTruths, 0xF0F0 );
+    Vec_IntPush( vTruths, 0xFF00 );
+
+    assert( Ft_FactorGetNumVars( vForm ) == 4 );
+    for ( i = 4; i < vForm->nSize; i++ )
+    {
+        pFtNode = Ft_NodeRead( vForm, i );
+        // make sure there are no elementary variables
+        assert( pFtNode->iFanin0 != pFtNode->iFanin1 );
+
+        uTruth0 = vTruths->pArray[pFtNode->iFanin0];
+        uTruth0 = pFtNode->fCompl0? ~uTruth0 : uTruth0;
+
+        uTruth1 = vTruths->pArray[pFtNode->iFanin1];
+        uTruth1 = pFtNode->fCompl1? ~uTruth1 : uTruth1;
+
+        uTruth = uTruth0 & uTruth1;
+        Vec_IntPush( vTruths, uTruth );
+    }
+    // complement if necessary
+    if ( pFtNode->fCompl )
+        uTruth = ~uTruth;
+    uTruth &= 0xFFFF;
+    if ( uTruth != uTruthGold )
+        printf( "Verification failed\n" );
+    Vec_IntFree( vTruths );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index b486785f..735232af 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -25,7 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Rwr_Cut_t * pCut, int NodeMax, int LevelMax );
+static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -49,37 +49,101 @@ static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Rwr_Cut_t
   SeeAlso     []
 
 ***********************************************************************/
-int Rwr_NodeRewrite( Rwr_Man_t * p, Abc_Obj_t * pNode )
+int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros )
 {
+    int fVeryVerbose = 0;
     Vec_Int_t * vForm;
-    Rwr_Cut_t * pCut;
+    Cut_Cut_t * pCut;
+    Abc_Obj_t * pFanin;
+    unsigned uPhase, uTruthBest;
+    char * pPerm;
     int Required, nNodesSaved;
-    int i, BestGain = -1;
-    // compute the cuts for this node
-    Rwr_NodeComputeCuts( p, pNode );
+    int i, GainCur, GainBest = -1;
+    int clk;
+
+    p->nNodesConsidered++;
     // get the required times
-    Required = Vec_IntEntry( p->vReqTimes, pNode->Id );
-    // label MFFC with current ID
-    nNodesSaved = Abc_NodeMffcLabel( pNode );
+    Required = Abc_NodeReadRequiredLevel( pNode );
+    // get the node's cuts
+clk = clock();
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode );
+    assert( pCut != NULL );
+p->timeCut += clock() - clk;
+
     // go through the cuts
-    for ( pCut = (Rwr_Cut_t *)pNode->pCopy, pCut = pCut->pNext; pCut; pCut = pCut->pNext )
+clk = clock();
+    for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
     {
+        // consider only 4-input cuts
+        if ( pCut->nLeaves < 4 )
+            continue;
+        // get the fanin permutation
+        pPerm = p->pPerms4[ p->pPerms[pCut->uTruth] ];
+        uPhase = p->pPhases[pCut->uTruth];
+        // collect fanins with the corresponding permutation/phase
+        Vec_PtrClear( p->vFaninsCur );
+        Vec_PtrFill( p->vFaninsCur, (int)pCut->nLeaves, 0 );
+        for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        {
+            pFanin = Abc_NtkObj( pNode->pNtk, pCut->pLeaves[pPerm[i]] );
+            if ( pFanin == NULL )
+                break;
+            pFanin = Abc_ObjNotCond(pFanin, ((uPhase & (1<<i)) > 0) );
+            Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
+        }
+        if ( i != (int)pCut->nLeaves )
+        {
+            p->nCutsBad++;
+            continue;
+        }
+        p->nCutsGood++;
+
+        // mark the fanin boundary 
+        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+            Abc_ObjRegular(pFanin)->vFanouts.nSize++;
+        // label MFFC with current ID
+        Abc_NtkIncrementTravId( pNode->pNtk );
+        nNodesSaved = Abc_NodeMffcLabel( pNode );
+        // unmark the fanin boundary
+        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+            Abc_ObjRegular(pFanin)->vFanouts.nSize--;
+
         // evaluate the cut
-        vForm = Rwr_CutEvaluate( p, pNode, pCut, nNodesSaved, Required );
-        // check if the cut is better than the currently best one
-        if ( vForm != NULL && BestGain < (int)pCut->Volume )
+        vForm = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur );
+
+        // check if the cut is better than the current best one
+        if ( vForm != NULL && GainBest < GainCur )
         {
-            assert( pCut->Volume >= 0 );
-            BestGain  = pCut->Volume;
             // save this form
-            p->vForm = vForm;
-            // collect fanins
+            GainBest  = GainCur;
+            p->vForm  = vForm;
+            p->fCompl = ((uPhase & (1<<4)) > 0);
+            uTruthBest = pCut->uTruth;
+            // collect fanins in the
             Vec_PtrClear( p->vFanins );
-            for ( i = 0; i < (int)pCut->nLeaves; i++ )
-                Vec_PtrPush( p->vFanins, pCut->ppLeaves[i] );
+            Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+                Vec_PtrPush( p->vFanins, pFanin );
         }
     }
-    return BestGain;
+p->timeRes += clock() - clk;
+
+    if ( GainBest == -1 || GainBest == 0 && !fUseZeros )
+        return GainBest;
+
+    p->nScores[p->pMap[uTruthBest]]++;
+    p->nNodesRewritten++;
+    p->nNodesGained += GainBest;
+
+    // report the progress
+    if ( fVeryVerbose )
+    {
+        printf( "Node %6s :   ", Abc_ObjName(pNode) );
+        printf( "Fanins = %d. ", p->vFanins->nSize );
+        printf( "Cone = %2d.  ", p->vForm->nSize - 4 );
+        printf( "GAIN = %2d.  ", GainBest );
+        printf( "\n" );
+    }
+    return GainBest;
 }
 
 /**Function*************************************************************
@@ -93,161 +157,39 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Rwr_Cut_t * pCut, int NodeMax, int LevelMax )
+Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest )
 {
-    Vec_Ptr_t Vector = {0,0,0}, * vFanins = &Vector;
     Vec_Ptr_t * vSubgraphs;
     Vec_Int_t * vFormBest;
     Rwr_Node_t * pNode;
-    int GainCur, GainBest = -1, i;
+    int nNodesAdded, GainBest = -1, i;
+    int clk = clock();
     // find the matching class of subgraphs
     vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[pCut->uTruth] );
+    p->nSubgraphs += vSubgraphs->nSize;
     // determine the best subgraph
     Vec_PtrForEachEntry( vSubgraphs, pNode, i )
     {
-        // create the fanin array
-        vFanins->nSize  = pCut->nLeaves;
-        vFanins->pArray = pCut->ppLeaves;
         // detect how many unlabeled nodes will be reused
-        GainCur = Abc_NodeStrashDecCount( pRoot->pNtk->pManFunc,  pRoot, vFanins, (Vec_Int_t *)pNode->pNext, 
-            p->vLevNums, NodeMax, LevelMax );
-        if ( GainBest < GainCur )
+        nNodesAdded = Abc_NodeStrashDecCount( pRoot->pNtk->pManFunc, pRoot, vFaninsCur, 
+            (Vec_Int_t *)pNode->pNext, p->vLevNums, nNodesSaved, LevelMax );
+        if ( nNodesAdded == -1 )
+            continue;
+        assert( nNodesSaved >= nNodesAdded );
+        // count the gain at this node
+        if ( GainBest < nNodesSaved - nNodesAdded )
         {
-            GainBest  = GainCur;
+            GainBest  = nNodesSaved - nNodesAdded;
             vFormBest = (Vec_Int_t *)pNode->pNext;
         }
     }
+p->timeEval += clock() - clk;
     if ( GainBest == -1 )
         return NULL;
-    pCut->Volume = GainBest;
+    *pGainBest = GainBest;
     return vFormBest;
 }
 
-
-/**Function*************************************************************
-
-  Synopsis    [Adds one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm )
-{
-    Ft_Node_t Node, NodeA, NodeB;
-    int Node0, Node1;
-    // elementary variable
-    if ( pNode->fUsed )
-        return ((pNode->Id - 1) << 1); 
-    // previously visited node
-    if ( pNode->TravId == p->nTravIds )
-        return pNode->Volume;
-    pNode->TravId = p->nTravIds;
-    // solve for children
-    Node0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), vForm );
-    Node1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), vForm );
-    // create the decomposition node(s)
-    if ( pNode->fExor )
-    {
-        assert( !Rwr_IsComplement(pNode->p0) );
-        assert( !Rwr_IsComplement(pNode->p1) );
-        NodeA.fIntern = 1;
-        NodeA.fConst  = 0;
-        NodeA.fCompl  = 0;
-        NodeA.fCompl0 = !(Node0 & 1);
-        NodeA.fCompl1 =  (Node1 & 1);
-        NodeA.iFanin0 = (Node0 >> 1);
-        NodeA.iFanin1 = (Node1 >> 1);
-        Vec_IntPush( vForm, Ft_Node2Int(NodeA) );
-
-        NodeB.fIntern = 1;
-        NodeB.fConst  = 0;
-        NodeB.fCompl  = 0;
-        NodeB.fCompl0 =  (Node0 & 1);
-        NodeB.fCompl1 = !(Node1 & 1);
-        NodeB.iFanin0 = (Node0 >> 1);
-        NodeB.iFanin1 = (Node1 >> 1);
-        Vec_IntPush( vForm, Ft_Node2Int(NodeB) );
-
-        Node.fIntern = 1;
-        Node.fConst  = 0;
-        Node.fCompl  = 0;
-        Node.fCompl0 = 1;
-        Node.fCompl1 = 1;
-        Node.iFanin0 = vForm->nSize - 2;
-        Node.iFanin1 = vForm->nSize - 1;
-        Vec_IntPush( vForm, Ft_Node2Int(Node) );
-    }
-    else
-    {
-        Node.fIntern = 1;
-        Node.fConst  = 0;
-        Node.fCompl  = 0;
-        Node.fCompl0 = Rwr_IsComplement(pNode->p0) ^ (Node0 & 1);
-        Node.fCompl1 = Rwr_IsComplement(pNode->p1) ^ (Node1 & 1);
-        Node.iFanin0 = (Node0 >> 1);
-        Node.iFanin1 = (Node1 >> 1);
-        Vec_IntPush( vForm, Ft_Node2Int(Node) );
-    }
-    // save the number of this node
-    pNode->Volume = ((vForm->nSize - 1) << 1) | pNode->fExor;
-    return pNode->Volume;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Preprocesses subgraphs rooted at this node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
-{
-    Vec_Int_t * vForm;
-    int i, Root;
-    vForm = Vec_IntAlloc( 10 );
-    for ( i = 0; i < 5; i++ )
-        Vec_IntPush( vForm, 0 );
-    // collect the nodes
-    Rwr_ManIncTravId( p );
-    Root = Rwr_TravCollect_rec( p, pNode, vForm );
-    if ( Root & 1 )
-        Ft_FactorComplement( vForm );
-    pNode->pNext = (Rwr_Node_t *)vForm;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Preprocesses computed library of subgraphs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Rwr_ManPreprocess( Rwr_Man_t * p )
-{
-    Rwr_Node_t * pNode;
-    int i, k;
-    // put the nodes into the structure
-    p->vClasses = Vec_VecAlloc( 222 );
-    for ( i = 0; i < p->nFuncs; i++ )
-        for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
-            Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
-    // compute decomposition forms for each node
-    Vec_VecForEachEntry( p->vClasses, pNode, i, k )
-        Rwr_NodePreprocess( p, pNode );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index ead86b4e..71db4b20 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -49,14 +49,13 @@ Rwr_Man_t * Rwr_ManStart( bool fPrecompute )
     // canonical forms, phases, perms
 clk = clock();
     Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
-PRT( "NPN classes precomputation time", clock() - clk ); 
+//PRT( "NPN classes precomputation time", clock() - clk ); 
     // initialize practical NPN classes
     p->pPractical  = Rwr_ManGetPractical( p );
     // create the table
     p->pTable = ALLOC( Rwr_Node_t *, p->nFuncs );
     memset( p->pTable, 0, sizeof(Rwr_Node_t *) * p->nFuncs );
     // create the elementary nodes
-    assert( sizeof(Rwr_Node_t) == sizeof(Rwr_Cut_t) );
     p->pMmNode  = Extra_MmFixedStart( sizeof(Rwr_Node_t) );
     p->vForest  = Vec_PtrAlloc( 100 );
     Rwr_ManAddVar( p, 0x0000, fPrecompute ); // constant 0
@@ -66,10 +65,11 @@ PRT( "NPN classes precomputation time", clock() - clk );
     Rwr_ManAddVar( p, 0xFF00, fPrecompute ); // var D
     p->nClasses = 5;
     // other stuff
-    p->nTravIds = 1;
-    p->puPerms43 = Extra_TruthPerm43();
-    p->vLevNums  = Vec_IntAlloc( 50 );
-    p->vFanins   = Vec_PtrAlloc( 50 );
+    p->nTravIds   = 1;
+    p->pPerms4    = Extra_Permutations( 4 );
+    p->vLevNums   = Vec_IntAlloc( 50 );
+    p->vFanins    = Vec_PtrAlloc( 50 );
+    p->vFaninsCur = Vec_PtrAlloc( 50 );
     if ( fPrecompute )
     {   // precompute subgraphs
         Rwr_ManPrecompute( p );
@@ -78,11 +78,11 @@ PRT( "NPN classes precomputation time", clock() - clk );
     }
     else
     {   // load saved subgraphs
-        Rwr_ManLoadFromArray( p );
-//        Rwr_ManPrint( p );
+        Rwr_ManLoadFromArray( p, 0 );
+        Rwr_ManPrint( p );
         Rwr_ManPreprocess( p );
-        return NULL;
     }
+p->timeStart = clock() - clk;
     return p;
 }
 
@@ -106,16 +106,15 @@ void Rwr_ManStop( Rwr_Man_t * p )
         Vec_VecForEachEntry( p->vClasses, pNode, i, k )
             Vec_IntFree( (Vec_Int_t *)pNode->pNext );
     }
-    if ( p->vFanNums )  Vec_IntFree( p->vFanNums );
-    if ( p->vReqTimes ) Vec_IntFree( p->vReqTimes );
     if ( p->vClasses )  Vec_VecFree( p->vClasses );
     Vec_PtrFree( p->vForest );
     Vec_IntFree( p->vLevNums );
     Vec_PtrFree( p->vFanins );
+    Vec_PtrFree( p->vFaninsCur );
     Extra_MmFixedStop( p->pMmNode, 0 );
     free( p->pTable );
     free( p->pPractical );
-    free( p->puPerms43 );
+    free( p->pPerms4 );
     free( p->puCanons );
     free( p->pPhases );
     free( p->pPerms );
@@ -125,6 +124,46 @@ void Rwr_ManStop( Rwr_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManPrintStats( Rwr_Man_t * p )
+{
+    int i, Counter = 0;
+    for ( i = 0; i < 222; i++ )
+        Counter += (p->nScores[i] > 0);
+
+    printf( "Rewriting statistics:\n" );
+    printf( "Total cuts tries  = %8d.\n", p->nCutsGood );
+    printf( "Bad cuts found    = %8d.\n", p->nCutsBad );
+    printf( "Total subgraphs   = %8d.\n", p->nSubgraphs );
+    printf( "Used NPN classes  = %8d.\n", Counter );
+    printf( "Nodes considered  = %8d.\n", p->nNodesConsidered );
+    printf( "Nodes rewritten   = %8d.\n", p->nNodesRewritten );
+    printf( "Calculated gain   = %8d.\n", p->nNodesGained     );
+    PRT( "Start       ", p->timeStart );
+    PRT( "Cuts        ", p->timeCut );
+    PRT( "Resynthesis ", p->timeRes );
+    PRT( "    Eval    ", p->timeEval );
+    PRT( "TOTAL       ", p->timeTotal );
+
+/*
+    printf( "The scores are : " );
+    for ( i = 0; i < 222; i++ )
+        if ( p->nScores[i] > 0 )
+            printf( "%d=%d ", i, p->nScores[i] );
+    printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
   Synopsis    [Assigns elementary cuts to the PIs.]
 
   Description []
@@ -137,11 +176,11 @@ void Rwr_ManStop( Rwr_Man_t * p )
 void Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk )
 {
     // save the fanout counters for all internal nodes
-    p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
+//    p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
     // precompute the required times for all internal nodes
-    p->vReqTimes = Abc_NtkGetRequiredLevels( pNtk );
+//    p->vReqTimes = Abc_NtkGetRequiredLevels( pNtk );
     // start the cut computation
-    Rwr_NtkStartCuts( p, pNtk );
+//    Rwr_NtkStartCuts( p, pNtk );
 }
 
 /**Function*************************************************************
@@ -176,6 +215,54 @@ Vec_Int_t * Rwr_ManReadDecs( Rwr_Man_t * p )
     return p->vForm;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_ManReadCompl( Rwr_Man_t * p )
+{
+    return p->fCompl;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time )
+{
+    p->timeCut += Time;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time )
+{
+    p->timeTotal += Time;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/opt/rwr/rwrPrint.c b/src/opt/rwr/rwrPrint.c
index 7c0bc212..30c99f00 100644
--- a/src/opt/rwr/rwrPrint.c
+++ b/src/opt/rwr/rwrPrint.c
@@ -209,17 +209,17 @@ void Rwr_ManPrint( Rwr_Man_t * p )
     FILE * pFile;
     Rwr_Node_t * pNode;
     unsigned uTruth;
-    int Counter, Volume, nFuncs, i;
+    int Limit, Counter, Volume, nFuncs, i;
     pFile = fopen( "graph_lib.txt", "w" );
     Counter = 0;
-    nFuncs = (1 << 16);
-    for ( i = 0; i < nFuncs; i++ )
+    Limit = (1 << 16);
+    for ( i = 0; i < Limit; i++ )
     {
         if ( p->pTable[i] == NULL )
             continue;
         if ( i != p->puCanons[i] )
             continue;
-        fprintf( pFile, "\nClass %3d  ", Counter++ );
+        fprintf( pFile, "\nClass %3d.  Func %6d.  ", p->pMap[i], Counter++ );
         Rwr_GetBushVolume( p, i, &Volume, &nFuncs );
         fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume );
         uTruth = i;
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index 30b0cf69..dedd86fe 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -87,7 +87,7 @@ void Rwr_ManWriteToArray( Rwr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManLoadFromArray( Rwr_Man_t * p )
+void Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose )
 {
     unsigned short * pArray = s_RwtAigSubgraphs;
     Rwr_Node_t * p0, * p1;
@@ -119,8 +119,11 @@ void Rwr_ManLoadFromArray( Rwr_Man_t * p )
         Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor );
     }
     nEntries = i - 1;
-    printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
-    printf( "The number of nodes loaded = %d.  ", nEntries );  PRT( "Loading", clock() - clk );
+    if ( fVerbose )
+    {
+        printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
+        printf( "The number of nodes loaded = %d.  ", nEntries );  PRT( "Loading", clock() - clk );
+    }
 }
 
 
diff --git a/src/sop/ft/ft.h b/src/sop/ft/ft.h
index cea7d935..da162e99 100644
--- a/src/sop/ft/ft.h
+++ b/src/sop/ft/ft.h
@@ -95,6 +95,8 @@ extern Vec_Int_t *        Ft_Factor( char * pSop );
 extern int                Ft_FactorGetNumNodes( Vec_Int_t * vForm );
 extern int                Ft_FactorGetNumVars( Vec_Int_t * vForm );
 extern void               Ft_FactorComplement( Vec_Int_t * vForm );
+extern Vec_Int_t *        Ft_FactorConst( int fConst1 );
+extern Vec_Int_t *        Ft_FactorVar( int iVar, int nVars, int fCompl );
 /*=== ftPrint.c =====================================================*/
 extern void               Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * pNameOut );
 
diff --git a/src/sop/ft/ftFactor.c b/src/sop/ft/ftFactor.c
index 1654973f..d25d0653 100644
--- a/src/sop/ft/ftFactor.c
+++ b/src/sop/ft/ftFactor.c
@@ -39,7 +39,6 @@ static Ft_Node_t *       Ft_FactorTrivialCubeCascade( Vec_Int_t * vForm, Mvc_Cov
 static Ft_Node_t *       Ft_FactorNodeCreate( Vec_Int_t * vForm, int Type, Ft_Node_t * pNode1, Ft_Node_t * pNode2 );
 static Ft_Node_t *       Ft_FactorLeafCreate( Vec_Int_t * vForm, int iLit );
 static void              Ft_FactorFinalize( Vec_Int_t * vForm, Ft_Node_t * pNode, int nVars );
-static Vec_Int_t *       Ft_FactorConst( int fConst1 );
 
 // temporary procedures that work with the covers
 static Mvc_Cover_t *     Ft_ConvertSopToMvc( char * pSop );
@@ -320,6 +319,8 @@ Ft_Node_t * Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, i
         return ppNodes[0];
 
     // split the nodes into two parts
+//    nNodes1 = nNodes/2;
+//    nNodes2 = nNodes - nNodes1;
     nNodes2 = nNodes/2;
     nNodes1 = nNodes - nNodes2;
 
@@ -613,6 +614,32 @@ Vec_Int_t * Ft_FactorConst( int fConst1 )
     return vForm;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates a constant 0 or 1 factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ft_FactorVar( int iVar, int nVars, int fCompl )
+{
+    Vec_Int_t * vForm;
+    Ft_Node_t * pNode;
+    // create the elementary variable node
+    vForm = Vec_IntAlloc( nVars + 1 );
+    Vec_IntFill( vForm, nVars + 1, 0 );
+    pNode = Ft_NodeReadLast( vForm );
+    pNode->iFanin0 = iVar;
+    pNode->iFanin1 = iVar;
+    pNode->fIntern = 1;
+    pNode->fCompl  = fCompl;
+    return vForm;
+}
+