Version abc50827

12 files changed, 479 insertions, 465 deletions

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 );
+    }
 }