Version abc50818

8 files changed, 533 insertions, 339 deletions

diff --git a/src/opt/rwr/module.make b/src/opt/rwr/module.make
new file mode 100644
index 00000000..e97eb33e
--- /dev/null
+++ b/src/opt/rwr/module.make
@@ -0,0 +1,6 @@
+SRC +=  rwrCut.c \
+    rwrEva.c \
+    rwrExp.c \
+    rwrLib.c \
+    rwrMan.c \
+    rwrUtil.c
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 19fc34c4..96810c25 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -37,40 +37,18 @@
  
 #define RWR_LIMIT  1048576/4  // ((1 << 20) 
 
+typedef struct Rwr_Man_t_   Rwr_Man_t;
 typedef struct Rwr_Node_t_  Rwr_Node_t;
-struct Rwr_Node_t_ // 24 bytes
-{
-    int                Id;               // ID 
-    int                TravId;           // traversal ID
-    unsigned           uTruth : 16;      // truth table
-    unsigned           Volume :  8;      // volume
-    unsigned           Level  :  5;      // level
-    unsigned           fMark  :  1;      // mark
-    unsigned           fUsed  :  1;      // mark
-    unsigned           fExor  :  1;      // mark
-    Rwr_Node_t *       p0;               // first child
-    Rwr_Node_t *       p1;               // second child
-    Rwr_Node_t *       pNext;            // next in the table
-};
+typedef struct Rwr_Cut_t_   Rwr_Cut_t;
 
-typedef struct Rwr_Cut_t_  Rwr_Cut_t;
-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
-};
-
-struct Abc_ManRwr_t_
+struct Rwr_Man_t_
 {
     // internal lookups
     int                nFuncs;           // the number of four var functions
     unsigned short *   puCanons;         // canonical forms
-    char *             puPhases;         // canonical phases
+    char *             pPhases;          // canonical phases
+    char *             pPerms;           // canonical permutations
+    unsigned char *    pMap;             // mapping of functions into class numbers
     char *             pPractical;       // practical classes
     unsigned short     puPerms[256][16]; // permutations for three var functions
     // node space
@@ -88,6 +66,7 @@ struct Abc_ManRwr_t_
     Vec_Int_t *        vForm;            // the decomposition tree (temporary)
     Vec_Ptr_t *        vFanins;          // the fanins array (temporary)
     Vec_Ptr_t *        vTfo;             // the TFO node array (temporary)
+    Vec_Ptr_t *        vTfoFor;          // the TFO node array (temporary)
     Vec_Vec_t *        vLevels;          // the levelized structure (temporary)
     int                nGainMax;
     // runtime statistics
@@ -97,6 +76,33 @@ struct Abc_ManRwr_t_
     int                time4;
 };
 
+struct Rwr_Node_t_ // 24 bytes
+{
+    int                Id;               // ID 
+    int                TravId;           // traversal ID
+    unsigned           uTruth : 16;      // truth table
+    unsigned           Volume :  8;      // volume
+    unsigned           Level  :  5;      // level
+    unsigned           fMark  :  1;      // mark
+    unsigned           fUsed  :  1;      // mark
+    unsigned           fExor  :  1;      // mark
+    Rwr_Node_t *       p0;               // first child
+    Rwr_Node_t *       p1;               // second child
+    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);  }
@@ -111,17 +117,27 @@ static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_N
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== rwrLib.c ==========================================================*/
-extern void                Rwr_ManPrecompute( Abc_ManRwr_t * p );
-extern void                Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName );
-extern void                Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName );
-extern void                Rwr_ManPrint( Abc_ManRwr_t * p );
-extern Rwr_Node_t *        Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth );
-/*=== rwrMan.c ==========================================================*/
-extern unsigned short      Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase );
-/*=== rwrUtil.c ==========================================================*/
-extern Vec_Int_t *         Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk );
-extern Vec_Int_t *         Rwt_NtkRequiredLevels( Abc_Ntk_t * pNtk );
+/*=== 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 );
+/*=== rwrLib.c ========================================================*/
+extern void              Rwr_ManPrecompute( Rwr_Man_t * p );
+extern void              Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName );
+extern void              Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName );
+extern void              Rwr_ManPrintFirst( Rwr_Man_t * p );
+extern void              Rwr_ManPrintNext( Rwr_Man_t * p );
+extern Rwr_Node_t *      Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, char * pFileName  );
+/*=== rwrMan.c ========================================================*/
+extern Rwr_Man_t *       Rwr_ManStart( char * pFileName );
+extern void              Rwr_ManStop( 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 unsigned short    Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase );
+/*=== rwrUtil.c ========================================================*/
+extern Vec_Int_t *       Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/rwr/rwrCut.c b/src/opt/rwr/rwrCut.c
index 88ea3cdb..c8560114 100644
--- a/src/opt/rwr/rwrCut.c
+++ b/src/opt/rwr/rwrCut.c
@@ -24,9 +24,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p );
-static Rwr_Cut_t * Rwr_CutCreateTriv( Abc_ManRwr_t * p, Abc_Obj_t * pNode );
-static Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 );
+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                           ///
@@ -34,7 +34,7 @@ static Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t
 
 /**Function*************************************************************
 
-  Synopsis    [Assigns elementary cuts to the PIs.]
+  Synopsis    [Computes cuts for one node.]
 
   Description []
                
@@ -43,7 +43,7 @@ static Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk )
+void Rwr_NtkStartCuts( Rwr_Man_t * p, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i;
@@ -51,10 +51,6 @@ void Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk )
     Abc_NtkCleanCopy( pNtk );
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Rwr_CutCreateTriv( p, pNode );
-    // precompute the required times for all internal nodes
-    p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
-    // save the fanout counters for all internal nodes
-    p->vReqTimes = Rwt_NtkRequiredLevels( pNtk );
 }
 
 /**Function*************************************************************
@@ -68,7 +64,7 @@ void Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeRwrComputeCuts( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+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
@@ -107,7 +103,7 @@ void Abc_NodeRwrComputeCuts( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 )
+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;
@@ -219,7 +215,7 @@ Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut
   SeeAlso     []
 
 ***********************************************************************/
-Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p )
+Rwr_Cut_t * Rwr_CutAlloc( Rwr_Man_t * p )
 {
     Rwr_Cut_t * pCut;
     pCut = (Rwr_Cut_t *)Extra_MmFixedEntryFetch( p->pMmNode );
@@ -238,7 +234,7 @@ Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Rwr_Cut_t * Rwr_CutCreateTriv( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+Rwr_Cut_t * Rwr_CutCreateTriv( Rwr_Man_t * p, Abc_Obj_t * pNode )
 {
     Rwr_Cut_t * pCut;
     pCut = Rwr_CutAlloc( p );
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index ecf03f4f..50e773f8 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -24,8 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut );
-static void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vForm );
+static void Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pNode, Rwr_Cut_t * pCut );
+static void Rwr_CutDecompose( Rwr_Man_t * p, Abc_Obj_t * pNode, Rwr_Cut_t * pCut, Vec_Int_t * vForm );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -49,13 +49,16 @@ static void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vF
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+int Rwr_NodeRewrite( Rwr_Man_t * p, Abc_Obj_t * pNode )
 {
     Vec_Ptr_t Vector = {0,0,0}, * vFanins = &Vector;
     Rwr_Cut_t * pCut, * pCutBest;
     int BestGain = -1;
     int i, Required = Vec_IntEntry( p->vReqTimes, pNode->Id );
 
+    // compute the cuts of the node
+    Rwr_NodeComputeCuts( p, pNode );
+
     // go through the cuts
     for ( pCut = (Rwr_Cut_t *)pNode->pCopy, pCut = pCut->pNext; pCut; pCut = pCut->pNext )
     {
@@ -64,7 +67,7 @@ int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
         vFanins->pArray = pCut->ppLeaves;
         Abc_NodeCollectTfoCands( pNode->pNtk, pNode, vFanins, Required, p->vLevels, p->vTfo );
         // evaluate the cut
-        Rwr_CutEvaluate( p, pCut );
+        Rwr_CutEvaluate( p, pNode, pCut );
         // check if the cut is the best
         if ( pCut->fTime && pCut->fGain )
         {
@@ -83,14 +86,14 @@ int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
     // collect the TFO again
     Abc_NodeCollectTfoCands( pNode->pNtk, pNode, p->vFanins, Required, p->vLevels, p->vTfo );
     // perform the decomposition
-    Rwr_CutDecompose( p, pCutBest, p->vForm );
+    Rwr_CutDecompose( p, pNode, pCutBest, p->vForm );
     // the best fanins are in p->vFanins, the result of decomposition is in p->vForm
     return BestGain;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Evaluates one cut.]
+  Synopsis    [Evaluates the cut.]
 
   Description []
                
@@ -99,13 +102,46 @@ int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut )
+void Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Rwr_Cut_t * pCut )
 {
+    Abc_Obj_t * pNode, * pFanin0, * pFanin1;
+    Rwr_Node_t * pNodeFor;
+    int i;
+    // mark forest PIs corresponding to cut leaves
+    Vec_PtrClear( p->vTfoFor );
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        pNodeFor = p->vForest->pArray[i];
+        Vec_PtrPush( p->vTfoFor, pNodeFor );
+        pCut->ppLeaves[i]->pData = pNodeFor;
+        pNodeFor->fMark = 1;
+    }
+    // detect forest nodes corresponding to TFO
+    Vec_PtrForEachEntry( p->vTfo, pNode, i )
+    {
+        pFanin0 = Abc_ObjFanin0(pNode);
+        if ( pFanin0->pData == NULL )
+            continue;
+        pFanin1 = Abc_ObjFanin1(pNode);
+        if ( pFanin1->pData == NULL )
+            continue;
+
+    }
+
+    // find the best implementation of the root
+
+    // assign costs
+
+    // clean the nodes
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        pCut->ppLeaves[i]->pData = NULL;
+    Vec_PtrForEachEntry( p->vTfo, pNode, i )
+        pNode->pData = NULL;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Evaluates one cut.]
+  Synopsis    [Decomposes the cut.]
 
   Description []
                
@@ -114,12 +150,10 @@ void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vForm )
+void Rwr_CutDecompose( Rwr_Man_t * p, Abc_Obj_t * pRoot, Rwr_Cut_t * pCut, Vec_Int_t * vForm )
 {
-}
-
-
 
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c
index 37eabf5b..a5c355a9 100644
--- a/src/opt/rwr/rwrExp.c
+++ b/src/opt/rwr/rwrExp.c
@@ -24,8 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Abc_ManRwrExp_t_ Abc_ManRwrExp_t;
-struct Abc_ManRwrExp_t_
+typedef struct Rwr_Man4_t_ Rwr_Man4_t;
+struct Rwr_Man4_t_
 {
     // internal lookups
     int                nFuncs;           // the number of four-var functions
@@ -35,13 +35,21 @@ struct Abc_ManRwrExp_t_
     int                nClasses;         // the number of NN classes
 };
 
-static Abc_ManRwrExp_t * s_pManRwrExp = NULL;
+typedef struct Rwr_Man5_t_ Rwr_Man5_t;
+struct Rwr_Man5_t_
+{
+    // internal lookups
+    stmm_table *       tTableNN;         // the NN canonical forms
+    stmm_table *       tTableNPN;        // the NPN canonical forms
+};
+
+static Rwr_Man4_t * s_pManRwrExp4 = NULL;
+static Rwr_Man5_t * s_pManRwrExp5 = NULL;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
   Synopsis    [Collects stats about 4-var functions appearing in netlists.]
@@ -53,43 +61,19 @@ static Abc_ManRwrExp_t * s_pManRwrExp = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManExploreStart()
+void Rwt_Man4ExploreStart()
 {
-    Abc_ManRwrExp_t * p;
-    unsigned uTruth;
-    int i, k, nClasses;
-    int clk = clock();
-
-    p = ALLOC( Abc_ManRwrExp_t, 1 );
-    memset( p, 0, sizeof(Abc_ManRwrExp_t) );
+    Rwr_Man4_t * p;
+    p = ALLOC( Rwr_Man4_t, 1 );
+    memset( p, 0, sizeof(Rwr_Man4_t) );
     // canonical forms
     p->nFuncs    = (1<<16);
-    p->puCanons  = ALLOC( unsigned short, p->nFuncs );
-    memset( p->puCanons, 0, sizeof(unsigned short) * p->nFuncs );
+    // canonical forms, phases, perms
+    Extra_Truth4VarNPN( &p->puCanons, NULL, NULL );
     // counters
     p->pnCounts  = ALLOC( int, p->nFuncs );
     memset( p->pnCounts, 0, sizeof(int) * p->nFuncs );
-
-    // initialize the canonical forms
-    nClasses = 1;
-    for ( i = 1; i < p->nFuncs-1; i++ )
-    {
-        if ( p->puCanons[i] )
-            continue;
-        nClasses++;
-        for ( k = 0; k < 32; k++ )
-        {
-            uTruth = Rwr_FunctionPhase( (unsigned)i, (unsigned)k );
-            if ( p->puCanons[uTruth] == 0 )
-                p->puCanons[uTruth] = (unsigned short)i;
-            else
-                assert( p->puCanons[uTruth] == (unsigned short)i );
-        }
-    }
-    // set info for constant 1
-    p->puCanons[p->nFuncs-1] = 0;
-    printf( "The number of NN-canonical forms = %d.\n", nClasses );
-    s_pManRwrExp = p;
+    s_pManRwrExp4 = p;
 }
 
 /**Function*************************************************************
@@ -103,10 +87,10 @@ void Rwt_ManExploreStart()
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManExploreCount( unsigned uTruth )
+void Rwt_Man4ExploreCount( unsigned uTruth )
 {
     assert( uTruth < (1<<16) );
-    s_pManRwrExp->pnCounts[ s_pManRwrExp->puCanons[uTruth] ]++;    
+    s_pManRwrExp4->pnCounts[ s_pManRwrExp4->puCanons[uTruth] ]++;    
 }
 
 /**Function*************************************************************
@@ -120,7 +104,7 @@ void Rwt_ManExploreCount( unsigned uTruth )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManExplorePrint()
+void Rwt_Man4ExplorePrint()
 {
     FILE * pFile;
     int i, CountMax, CountWrite, nCuts, nClasses;
@@ -129,12 +113,12 @@ void Rwt_ManExplorePrint()
     // find the max number of occurences
     nCuts = nClasses = 0;
     CountMax = 0;
-    for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
+    for ( i = 0; i < s_pManRwrExp4->nFuncs; i++ )
     {
-        if ( CountMax < s_pManRwrExp->pnCounts[i] )
-            CountMax = s_pManRwrExp->pnCounts[i];
-        nCuts += s_pManRwrExp->pnCounts[i];
-        if ( s_pManRwrExp->pnCounts[i] > 0 )
+        if ( CountMax < s_pManRwrExp4->pnCounts[i] )
+            CountMax = s_pManRwrExp4->pnCounts[i];
+        nCuts += s_pManRwrExp4->pnCounts[i];
+        if ( s_pManRwrExp4->pnCounts[i] > 0 )
             nClasses++;
     }
     printf( "Number of cuts considered       = %8d.\n", nCuts );
@@ -143,10 +127,10 @@ void Rwt_ManExplorePrint()
     pDistrib = ALLOC( int, CountMax + 1 );
     pReprs   = ALLOC( int, CountMax + 1 );
     memset( pDistrib, 0, sizeof(int)*(CountMax + 1) );
-    for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
+    for ( i = 0; i < s_pManRwrExp4->nFuncs; i++ )
     {
-        pDistrib[ s_pManRwrExp->pnCounts[i] ]++;
-        pReprs[ s_pManRwrExp->pnCounts[i] ] = i;
+        pDistrib[ s_pManRwrExp4->pnCounts[i] ]++;
+        pReprs[ s_pManRwrExp4->pnCounts[i] ] = i;
     }
 
     printf( "Occurence = %6d.  Num classes = %4d.  \n", 0, 2288-nClasses );
@@ -161,17 +145,187 @@ void Rwt_ManExplorePrint()
     free( pReprs );
     // write into a file all classes above limit (5)
     CountWrite = 0;
-    pFile = fopen( "nnclass_stats.txt", "w" );
-    for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
-        if ( s_pManRwrExp->pnCounts[i] > 5 )
+    pFile = fopen( "npnclass_stats4.txt", "w" );
+    for ( i = 0; i < s_pManRwrExp4->nFuncs; i++ )
+        if ( s_pManRwrExp4->pnCounts[i] > 0 )
         {
-            fprintf( pFile, "%d ", i );
+            Extra_PrintHex( pFile, i, 4 );
+            fprintf( pFile, " %10d\n", s_pManRwrExp4->pnCounts[i] );
+//            fprintf( pFile, "%d ", i );
             CountWrite++;
         }
     fclose( pFile );
-    printf( "%d classes written into file \"%s\".\n", CountWrite, "nnclass_stats.txt" );
+    printf( "%d classes written into file \"%s\".\n", CountWrite, "npnclass_stats4.txt" );
 }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects stats about 4-var functions appearing in netlists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwt_Man5ExploreStart()
+{
+    Rwr_Man5_t * p;
+    p = ALLOC( Rwr_Man5_t, 1 );
+    memset( p, 0, sizeof(Rwr_Man5_t) );
+    p->tTableNN  = stmm_init_table( st_numcmp, st_numhash );
+    p->tTableNPN = stmm_init_table( st_numcmp, st_numhash );
+    s_pManRwrExp5 = p;
+
+//Extra_PrintHex( stdout, Extra_TruthCanonNPN( 0x0000FFFF, 5 ), 5 );
+//printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects stats about 4-var functions appearing in netlists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwt_Man5ExploreCount( unsigned uTruth )
+{
+    int * pCounter;
+    if ( !stmm_find_or_add( s_pManRwrExp5->tTableNN, (char *)uTruth, (char***)&pCounter ) )
+        *pCounter = 0;
+    (*pCounter)++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects stats about 4-var functions appearing in netlists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwt_Man5ExplorePrint()
+{
+    FILE * pFile;
+    stmm_generator * gen;
+    int i, CountMax, nCuts, Counter;
+    int * pDistrib;
+    unsigned * pReprs;
+    unsigned uTruth, uTruthC;
+    int clk = clock();
+    Vec_Int_t * vClassesNN, * vClassesNPN;
+
+    // find the max number of occurences
+    nCuts = 0;
+    CountMax = 0;
+    stmm_foreach_item( s_pManRwrExp5->tTableNN, gen, (char **)&uTruth, (char **)&Counter )
+    {
+        nCuts += Counter;
+        if ( CountMax < Counter )
+            CountMax = Counter;
+    }
+    printf( "Number of cuts considered       = %8d.\n", nCuts );
+    printf( "Classes occurring at least once = %8d.\n", stmm_count(s_pManRwrExp5->tTableNN) );
+    printf( "The largest number of occurence = %8d.\n", CountMax );
+
+    // print the distribution of classes
+    pDistrib = ALLOC( int, CountMax + 1 );
+    pReprs   = ALLOC( unsigned, CountMax + 1 );
+    memset( pDistrib, 0, sizeof(int)*(CountMax + 1) );
+    stmm_foreach_item( s_pManRwrExp5->tTableNN, gen, (char **)&uTruth, (char **)&Counter )
+    {
+        assert( Counter <= CountMax );
+        pDistrib[ Counter ]++;
+        pReprs[ Counter ] = uTruth;
+    }
+
+    for ( i = 1; i <= CountMax; i++ )
+        if ( pDistrib[i] )
+        {
+            printf( "Occurence = %6d.  Num classes = %4d.  Repr = ", i, pDistrib[i] );
+            Extra_PrintBinary( stdout, pReprs + i, 32 ); 
+            printf( "\n" );
+        }
+    free( pDistrib );
+    free( pReprs );
+
+
+    // put them into an array
+    vClassesNN = Vec_IntAlloc( stmm_count(s_pManRwrExp5->tTableNN) );
+    stmm_foreach_item( s_pManRwrExp5->tTableNN, gen, (char **)&uTruth, NULL )
+        Vec_IntPush( vClassesNN, (int)uTruth );
+    Vec_IntSortUnsigned( vClassesNN );
+
+    // write into a file all classes
+    pFile = fopen( "nnclass_stats5.txt", "w" );
+    Vec_IntForEachEntry( vClassesNN, uTruth, i )
+    {
+        if ( !stmm_lookup( s_pManRwrExp5->tTableNN, (char *)uTruth, (char **)&Counter ) )
+        {
+            assert( 0 );
+        }
+        Extra_PrintHex( pFile, uTruth, 5 );
+        fprintf( pFile, " %10d\n", Counter );
+    }
+    fclose( pFile );
+    printf( "%d classes written into file \"%s\".\n", vClassesNN->nSize, "nnclass_stats5.txt" );
+
+
+clk = clock();
+    // how many NPN classes exist?
+    Vec_IntForEachEntry( vClassesNN, uTruth, i )
+    {
+        int * pCounter;
+        uTruthC = Extra_TruthCanonNPN( uTruth, 5 );
+        if ( !stmm_find_or_add( s_pManRwrExp5->tTableNPN, (char *)uTruthC, (char***)&pCounter ) )
+            *pCounter = 0;
+        if ( !stmm_lookup( s_pManRwrExp5->tTableNN, (char *)uTruth, (char **)&Counter ) )
+        {
+            assert( 0 );
+        }
+        (*pCounter) += Counter;
+    }
+    printf( "The numbe of NPN classes = %d.\n", stmm_count(s_pManRwrExp5->tTableNPN) );
+PRT( "Computing NPN classes", clock() - clk );
+
+    // put them into an array
+    vClassesNPN = Vec_IntAlloc( stmm_count(s_pManRwrExp5->tTableNPN) );
+    stmm_foreach_item( s_pManRwrExp5->tTableNPN, gen, (char **)&uTruth, NULL )
+        Vec_IntPush( vClassesNPN, (int)uTruth );
+    Vec_IntSortUnsigned( vClassesNPN );
+
+    // write into a file all classes
+    pFile = fopen( "npnclass_stats5.txt", "w" );
+    Vec_IntForEachEntry( vClassesNPN, uTruth, i )
+    {
+        if ( !stmm_lookup( s_pManRwrExp5->tTableNPN, (char *)uTruth, (char **)&Counter ) )
+        {
+            assert( 0 );
+        }
+        Extra_PrintHex( pFile, uTruth, 5 );
+        fprintf( pFile, " %10d\n", Counter );
+    }
+    fclose( pFile );
+    printf( "%d classes written into file \"%s\".\n", vClassesNPN->nSize, "npnclass_stats5.txt" );
+
+
+    // can they be uniquely characterized?
+
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c
index 91604244..a283e38f 100644
--- a/src/opt/rwr/rwrLib.c
+++ b/src/opt/rwr/rwrLib.c
@@ -24,14 +24,15 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Rwr_Node_t *        Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
-static Rwr_Node_t *        Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
-static int                 Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 );
+static Rwr_Node_t *        Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
+static Rwr_Node_t *        Rwr_ManAddNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
+static int                 Rwr_ManNodeVolume( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 );
 
-static void                Rwr_ManIncTravId_int( Abc_ManRwr_t * p );
-static inline void         Rwr_ManIncTravId( Abc_ManRwr_t * p )     { if ( p->nTravIds++ == 0x8FFFFFFF ) Rwr_ManIncTravId_int( p ); }
+static void                Rwr_ManIncTravId_int( Rwr_Man_t * p );
+static inline void         Rwr_ManIncTravId( Rwr_Man_t * p )     { if ( p->nTravIds++ == 0x8FFFFFFF ) Rwr_ManIncTravId_int( p ); }
 
-static void                Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode );
+static void                Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode );
+static void                Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -48,7 +49,7 @@ static void                Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNod
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManPrecompute( Abc_ManRwr_t * p )
+void Rwr_ManPrecompute( Rwr_Man_t * p )
 {
     Rwr_Node_t * p0, * p1;
     int i, k, Level, Volume;
@@ -80,7 +81,7 @@ void Rwr_ManPrecompute( Abc_ManRwr_t * p )
         // compute the level and volume of the new nodes
         Level  = 1 + ABC_MAX( p0->Level, p1->Level );
         Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
-        // try four different nodes
+        // try four different AND nodes
         Rwr_ManTryNode( p,         p0 ,         p1 , 0, Level, Volume );
         Rwr_ManTryNode( p, Rwr_Not(p0),         p1 , 0, Level, Volume );
         Rwr_ManTryNode( p,         p0 , Rwr_Not(p1), 0, Level, Volume );
@@ -136,7 +137,7 @@ save :
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName )
+void Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName )
 {
     FILE * pFile;
     Rwr_Node_t * pNode;
@@ -173,7 +174,7 @@ void Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName )
+void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName )
 {
     FILE * pFile;
     Rwr_Node_t * p0, * p1;
@@ -227,7 +228,7 @@ void Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManIncTravId_int( Abc_ManRwr_t * p )
+void Rwr_ManIncTravId_int( Rwr_Man_t * p )
 {
     Rwr_Node_t * pNode;
     int i;
@@ -247,7 +248,7 @@ void Rwr_ManIncTravId_int( Abc_ManRwr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode )
+void Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode )
 {
     if ( pNode->fUsed || pNode->TravId == p->nTravIds )
         return;
@@ -268,7 +269,7 @@ void Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_Trav_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume )
+void Rwr_Trav_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, int * pVolume )
 {
     if ( pNode->fMark || pNode->TravId == p->nTravIds )
         return;
@@ -291,7 +292,7 @@ void Rwr_Trav_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_Trav2_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume )
+void Rwr_Trav2_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, int * pVolume )
 {
     if ( pNode->fMark || pNode->TravId == p->nTravIds )
         return;
@@ -312,7 +313,7 @@ void Rwr_Trav2_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume )
   SeeAlso     []
 
 ***********************************************************************/
-int Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
+int Rwr_ManNodeVolume( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
 {
     int Volume = 0;
     Rwr_ManIncTravId( p );
@@ -332,10 +333,10 @@ int Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
   SeeAlso     []
 
 ***********************************************************************/
-Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
+Rwr_Node_t * Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
 {
     Rwr_Node_t * pOld, * pNew, ** ppPlace;
-    unsigned uTruth, uCanon;
+    unsigned uTruth;
     // compute truth table, level, volume
     p->nConsidered++;
     if ( fExor )
@@ -346,12 +347,11 @@ Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1,
     else
         uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
                  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
-    uCanon = p->puCanons[uTruth];
     // skip non-practical classes
-    if ( Level > 2 && p->pPractical[uCanon] == 0 )
+    if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] )
         return NULL;
     // enumerate through the nodes with the same canonical form
-    ppPlace = p->pTable + uCanon;
+    ppPlace = p->pTable + uTruth;
     for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
     {
         if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
@@ -361,8 +361,19 @@ Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1,
 //        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
 //            return NULL;
     }
-//    if ( fExor )
-//        printf( "Adding EXOR of %d and %d.\n", p0->Id, p1->Id );
+    // enumerate through the nodes with the opposite polarity
+    for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext )
+    {
+        if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
+            return NULL;
+        if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
+            return NULL;
+//        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
+//            return NULL;
+    }
+    // count the classes
+    if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth )
+        p->nClasses++;
     // create the new node
     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
     pNew->Id     = p->vForest->nSize;
@@ -378,8 +389,6 @@ Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1,
     pNew->pNext  = NULL;
     Vec_PtrPush( p->vForest, pNew );
     *ppPlace     = pNew;
-    if ( p->pTable[uCanon] == pNew )
-        p->nClasses++;
     return pNew;
 }
 
@@ -394,10 +403,10 @@ Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1,
   SeeAlso     []
 
 ***********************************************************************/
-Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
+Rwr_Node_t * Rwr_ManAddNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
 {
-    Rwr_Node_t * pOld, * pNew;
-    unsigned uTruth, uCanon;
+    Rwr_Node_t * pNew;
+    unsigned uTruth;
     // compute truth table, leve, volume
     p->nConsidered++;
     if ( fExor )
@@ -405,10 +414,6 @@ Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1,
     else
         uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
                  (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
-    uCanon = p->puCanons[uTruth];
-    // skip non-practical classes
-//    if ( p->pPractical[uCanon] == 0 )
-//        return NULL;
     // create the new node
     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
     pNew->Id     = p->vForest->nSize;
@@ -424,16 +429,14 @@ Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1,
     pNew->pNext  = NULL;
     Vec_PtrPush( p->vForest, pNew );
     // do not add if the node is not essential
-    if ( uTruth != uCanon )
+    if ( uTruth != p->puCanons[uTruth] )
         return pNew;
 
     // add to the list
     p->nAdded++;
-    pOld = p->pTable[uCanon];
-    if ( pOld == NULL )
+    if ( p->pTable[p->pMap[uTruth]] == NULL )
         p->nClasses++;
-    pNew->pNext = pOld;
-    p->pTable[uCanon] = pNew;
+    Rwr_ListAddToTail( p->pTable + p->pMap[uTruth], pNew );
     return pNew;
 }
 
@@ -448,7 +451,7 @@ Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1,
   SeeAlso     []
 
 ***********************************************************************/
-Rwr_Node_t * Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth )
+Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, char * pFileName )
 {
     Rwr_Node_t * pNew;
     pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
@@ -461,16 +464,40 @@ Rwr_Node_t * Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth )
     pNew->fUsed  = 1;
     pNew->fExor  = 0;
     pNew->p0     = NULL;
-    pNew->p1     = NULL;    pNew->pNext  = NULL;
+    pNew->p1     = NULL;    
+    pNew->pNext  = NULL;
     Vec_PtrPush( p->vForest, pNew );
-    assert( p->pTable[p->puCanons[uTruth]] == NULL );
-    p->pTable[p->puCanons[uTruth]] = pNew;
+    if ( pFileName == NULL )
+        Rwr_ListAddToTail( p->pTable + uTruth, pNew );
+//    else
+//        Rwr_ListAddToTail( p->pTable + p->pMap[uTruth], pNew );
     return pNew;
 }
 
 
 /**Function*************************************************************
 
+  Synopsis    [Adds the node to the end of the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode )
+{
+    Rwr_Node_t * pTemp;
+    // find the last one
+    for ( pTemp = *ppList; pTemp; pTemp = pTemp->pNext )
+        ppList = &pTemp->pNext;
+    // attach at the end
+    *ppList = pNode;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints one rwr node.]
 
   Description []
@@ -567,16 +594,17 @@ void Rwr_NodePrint_rec( FILE * pFile, Rwr_Node_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_NodePrint( FILE * pFile, Abc_ManRwr_t * p, Rwr_Node_t * pNode )
+void Rwr_NodePrint( FILE * pFile, Rwr_Man_t * p, Rwr_Node_t * pNode )
 {
     unsigned uTruth;
-    fprintf( pFile, "%5d :", pNode->Id );
-    fprintf( pFile, " tt=", pNode->Id );
+    fprintf( pFile, "%5d : ", pNode->Id );
+    Extra_PrintHex( pFile, pNode->uTruth, 4 );
+    fprintf( pFile, " tt=" );
     uTruth = pNode->uTruth;
     Extra_PrintBinary( pFile, &uTruth, 16 );
-    fprintf( pFile, " cn=", pNode->Id );
-    uTruth = p->puCanons[pNode->uTruth];
-    Extra_PrintBinary( pFile, &uTruth, 16 );
+//    fprintf( pFile, " cn=", pNode->Id );
+//    uTruth = p->puCanons[pNode->uTruth];
+//    Extra_PrintBinary( pFile, &uTruth, 16 );
     fprintf( pFile, " lev=%d", pNode->Level );
     fprintf( pFile, " vol=%d", pNode->Volume );
     fprintf( pFile, "  " );
@@ -595,45 +623,84 @@ void Rwr_NodePrint( FILE * pFile, Abc_ManRwr_t * p, Rwr_Node_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManPrint( Abc_ManRwr_t * p )
+void Rwr_ManPrintFirst( Rwr_Man_t * p )
 {
-/*
+    FILE * pFile;
     Rwr_Node_t * pNode;
     unsigned uTruth;
-    int Limit = 4;
+    int nFuncs;
+    int Counter;
     int i;
 
-    for ( i = 0; i < p->nFuncs; i++ )
+    pFile = fopen( "graph_lib.txt", "w" );
+
+    Counter = 0;
+    nFuncs = (1 << 16);
+    for ( i = 0; i < nFuncs; i++ )
     {
         if ( p->pTable[i] == NULL )
             continue;
-        if ( Limit-- == 0 )
-            break;
-        printf( "\nClass " );
+        if ( i != p->puCanons[i] )
+            continue;
+
+        fprintf( pFile, "\nClass %3d  ", Counter++ );
+
+        // count the volume of the bush
+        {
+            int Volume = 0;
+            int nFuncs = 0;
+            Rwr_ManIncTravId( p );
+            for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
+            {
+                if ( pNode->uTruth != p->puCanons[pNode->uTruth] )
+                    continue;
+                nFuncs++;
+                Rwr_Trav2_rec( p, pNode, &Volume );
+            }
+            fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume );
+        }
+
         uTruth = i;
-        Extra_PrintBinary( stdout, &uTruth, 16 );
-        printf( "\n" );
+        Extra_PrintBinary( pFile, &uTruth, 16 );
+        fprintf( pFile, "\n" );
+
         for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
             if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
-                Rwr_NodePrint( p, pNode );
+                Rwr_NodePrint( pFile, p, pNode );
     }
-*/
+
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one rwr node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManPrintNext( Rwr_Man_t * p )
+{
     FILE * pFile;
     Rwr_Node_t * pNode;
     unsigned uTruth;
-    int Limit = 4;
+    int nFuncs;
     int Counter;
     int i;
 
-    pFile = fopen( "graph_lib.txt", "w" );
+    pFile = fopen( "graph_lib2.txt", "w" );
 
     Counter = 0;
-    for ( i = 0; i < p->nFuncs; i++ )
+    nFuncs = (1 << 16);
+    for ( i = 0; i < 222; i++ )
     {
         if ( p->pTable[i] == NULL )
             continue;
-//        if ( Limit-- == 0 )
-//            break;
+
         fprintf( pFile, "\nClass %3d  ", Counter++ );
 
         // count the volume of the bush
@@ -642,15 +709,16 @@ void Rwr_ManPrint( Abc_ManRwr_t * p )
             int nFuncs = 0;
             Rwr_ManIncTravId( p );
             for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
-                if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
-                {
-                    nFuncs++;
-                    Rwr_Trav2_rec( p, pNode, &Volume );
-                }
+            {
+                if ( pNode->uTruth != p->puCanons[pNode->uTruth] )
+                    continue;
+                nFuncs++;
+                Rwr_Trav2_rec( p, pNode, &Volume );
+            }
             fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume );
         }
 
-        uTruth = i;
+        uTruth = p->pTable[i]->uTruth;
         Extra_PrintBinary( pFile, &uTruth, 16 );
         fprintf( pFile, "\n" );
 
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 46752696..3d40f79e 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -6,7 +6,7 @@
 
   PackageName [DAG-aware AIG rewriting package.]
 
-  Synopsis    []
+  Synopsis    [Rewriting manager.]
 
   Author      [Alan Mishchenko]
   
@@ -24,51 +24,26 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// the following information was derived by computing all 4-input cuts of IWLS, MCNC, and ISCAS benchmarks
-#define RWR_NUM_CLASSES  775
+// the following practical NPN classes of 4-variable functions were computed
+// by considering all 4-input cuts appearing in IWLS, MCNC, and ISCAS benchmarks
+#define RWR_NUM_CLASSES  135
 static int s_PracticalClasses[RWR_NUM_CLASSES] = {
-    0, 1, 3, 5, 6, 7, 15, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 51, 53, 54, 55, 60, 61, 63, 85, 86, 
-    87, 90, 91, 95, 102, 103, 105, 107, 111, 119, 123, 125, 126, 127, 255, 257, 258, 259, 260, 261, 262, 263, 264, 265, 
-    266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 281, 282, 284, 286, 287, 288, 289, 290, 291, 293, 297, 
-    298, 299, 300, 302, 303, 304, 305, 306, 307, 308, 310, 311, 312, 313, 315, 316, 317, 319, 320, 321, 323, 324, 325, 329, 
-    332, 334, 335, 336, 337, 338, 340, 341, 342, 343, 345, 347, 349, 351, 352, 357, 358, 359, 361, 367, 368, 369, 371, 
-    373, 375, 379, 381, 383, 384, 385, 386, 388, 389, 392, 393, 395, 397, 399, 400, 404, 408, 409, 416, 417, 419, 420, 
-    421, 424, 425, 426, 427, 431, 433, 443, 448, 449, 451, 453, 456, 457, 459, 460, 461, 462, 463, 465, 476, 477, 480, 
-    481, 483, 489, 492, 493, 494, 495, 496, 497, 499, 500, 501, 506, 507, 508, 509, 510, 771, 773, 774, 775, 780, 781, 
-    783, 785, 786, 787, 788, 790, 791, 792, 796, 797, 799, 816, 817, 819, 820, 821, 834, 835, 836, 837, 838, 839, 840, 
-    844, 847, 848, 849, 850, 851, 852, 853, 854, 855, 856, 859, 860, 861, 863, 864, 867, 870, 871, 876, 878, 880, 883, 
-    884, 885, 887, 967, 973, 975, 979, 984, 988, 989, 990, 1009, 1011, 1012, 1013, 1020, 1285, 1286, 1287, 1290, 1291, 
-    1295, 1297, 1298, 1300, 1301, 1303, 1307, 1308, 1309, 1311, 1314, 1316, 1317, 1318, 1319, 1322, 1325, 1327, 1329, 
-    1330, 1331, 1332, 1333, 1334, 1335, 1336, 1338, 1340, 1341, 1360, 1361, 1363, 1365, 1367, 1380, 1381, 1382, 1383, 
-    1390, 1392, 1395, 1397, 1399, 1440, 1445, 1447, 1450, 1451, 1455, 1458, 1461, 1463, 1467, 1525, 1530, 1542, 1543, 
-    1545, 1547, 1551, 1553, 1554, 1558, 1559, 1561, 1567, 1569, 1570, 1572, 1574, 1576, 1587, 1588, 1590, 1591, 1596, 
-    1618, 1620, 1621, 1623, 1624, 1632, 1638, 1641, 1647, 1654, 1655, 1680, 1686, 1687, 1689, 1695, 1718, 1776, 1782, 
-    1785, 1799, 1803, 1805, 1806, 1807, 1811, 1813, 1815, 1823, 1826, 1831, 1843, 1844, 1847, 1859, 1860, 1863, 1875, 
-    1877, 1879, 1895, 1902, 1904, 1911, 1912, 1927, 1928, 1933, 1935, 1945, 1956, 1957, 1959, 1962, 1964, 1965, 1975, 
-    1979, 1987, 1991, 1995, 1996, 2000, 2002, 2007, 2013, 2023, 2032, 2040, 3855, 3857, 3859, 3861, 3864, 3866, 3867, 
-    3868, 3869, 3870, 3891, 3892, 3893, 3900, 3921, 3925, 3942, 3945, 3956, 3960, 4080, 4369, 4370, 4371, 4372, 4373, 
-    4374, 4375, 4376, 4377, 4378, 4379, 4380, 4381, 4382, 4386, 4387, 4388, 4389, 4391, 4392, 4394, 4396, 4403, 4405, 
-    4408, 4409, 4411, 4420, 4421, 4422, 4423, 4424, 4426, 4428, 4437, 4439, 4445, 4488, 4494, 4505, 4507, 4509, 4522, 
-    4524, 4525, 4526, 4539, 4540, 4542, 4556, 4557, 4573, 4574, 4590, 4626, 4627, 4629, 4630, 4631, 4632, 4634, 4638, 
-    4641, 4643, 4648, 4659, 4680, 4695, 4698, 4702, 4713, 4731, 4740, 4758, 4766, 4773, 4791, 4812, 4830, 4845, 4883, 
-    4885, 4887, 4888, 4891, 4892, 4899, 4903, 4913, 4914, 4915, 4934, 4940, 4945, 4947, 4949, 4951, 4972, 5005, 5011, 
-    5017, 5019, 5029, 5043, 5049, 5058, 5059, 5060, 5068, 5075, 5079, 5083, 5084, 5100, 5140, 5141, 5142, 5143, 5148, 
-    5160, 5171, 5174, 5180, 5182, 5185, 5186, 5187, 5189, 5205, 5207, 5214, 5238, 5245, 5246, 5250, 5270, 5278, 5290, 
-    5310, 5315, 5335, 5355, 5397, 5399, 5401, 5402, 5405, 5413, 5414, 5415, 5418, 5427, 5429, 5445, 5457, 5460, 5461, 
-    5463, 5469, 5482, 5522, 5525, 5533, 5540, 5546, 5557, 5565, 5571, 5580, 5589, 5593, 5605, 5610, 5654, 5673, 5692, 
-    5698, 5729, 5734, 5782, 5790, 5796, 5814, 5826, 5846, 5911, 5931, 5965, 6001, 6066, 6120, 6168, 6174, 6180, 6206, 
-    6210, 6229, 6234, 6270, 6273, 6279, 6363, 6375, 6425, 6427, 6438, 6446, 6451, 6457, 6478, 6482, 6485, 6489, 6502, 
-    6545, 6553, 6564, 6570, 6594, 6617, 6630, 6682, 6683, 6685, 6686, 6693, 6709, 6741, 6746, 6817, 6821, 6826, 6833, 
-    6849, 6885, 6939, 6940, 6951, 6963, 6969, 6990, 6997, 7065, 7077, 7089, 7140, 7196, 7212, 7219, 7220, 7228, 7230, 
-    7251, 7324, 7356, 7361, 7363, 7372, 7377, 7395, 7453, 7470, 7475, 7495, 7509, 7513, 7526, 7619, 7633, 7650, 7710, 
-    7725, 7731, 7740, 7755, 7770, 7800, 7815, 7830, 7845, 7860, 7890, 7905, 13107, 13109, 13110, 13116, 13141, 13146, 
-    13161, 13164, 13621, 13622, 13626, 13651, 13653, 13658, 13669, 13670, 13763, 13765, 13770, 13878, 13881, 13884, 
-    13910, 13923, 13926, 13932, 13971, 13974, 13980, 14022, 14025, 15420, 15445, 15450, 15462, 15465, 15555, 21845, 
-    21846, 21850, 21865, 21866, 21930, 22102, 22105, 22106, 22117, 22118, 22122, 22165, 22166, 22169, 22170, 22181, 
-    22182, 22185, 23130, 23142, 23145, 23205, 26214, 26217, 26985, 27030 
+    0x0000, 0x0001, 0x0003, 0x0006, 0x0007, 0x000f, 0x0016, 0x0017, 0x0018, 0x0019, 0x001b, 
+    0x001e, 0x001f, 0x003c, 0x003d, 0x003f, 0x0069, 0x006b, 0x006f, 0x007e, 0x007f, 0x00ff, 
+    0x0116, 0x0118, 0x0119, 0x011a, 0x011b, 0x011e, 0x011f, 0x012c, 0x012d, 0x012f, 0x013c, 
+    0x013d, 0x013e, 0x013f, 0x0168, 0x0169, 0x016f, 0x017f, 0x0180, 0x0181, 0x0182, 0x0183, 
+    0x0186, 0x0189, 0x018b, 0x018f, 0x0198, 0x0199, 0x019b, 0x01a8, 0x01a9, 0x01aa, 0x01ab, 
+    0x01ac, 0x01ad, 0x01ae, 0x01af, 0x01bf, 0x01e9, 0x01ea, 0x01eb, 0x01ee, 0x01ef, 0x01fe, 
+    0x033c, 0x033d, 0x033f, 0x0356, 0x0357, 0x0358, 0x0359, 0x035a, 0x035b, 0x035f, 0x0368, 
+    0x0369, 0x036c, 0x036e, 0x037d, 0x03c0, 0x03c1, 0x03c3, 0x03c7, 0x03cf, 0x03d4, 0x03d5, 
+    0x03d7, 0x03d8, 0x03d9, 0x03dc, 0x03dd, 0x03de, 0x03fc, 0x0660, 0x0661, 0x0666, 0x0669, 
+    0x066f, 0x0676, 0x067e, 0x0690, 0x0696, 0x0697, 0x069f, 0x06b1, 0x06b6, 0x06f0, 0x06f2, 
+    0x06f6, 0x06f9, 0x0776, 0x0778, 0x07b0, 0x07b1, 0x07b4, 0x07bc, 0x07f0, 0x07f2, 0x07f8, 
+    0x0ff0, 0x1683, 0x1696, 0x1698, 0x169e, 0x16e9, 0x178e, 0x17e8, 0x18e7, 0x19e6, 0x1be4, 
+    0x1ee1, 0x3cc3, 0x6996 
 };
 
-static unsigned short      Rwr_FunctionPerm( unsigned uTruth, int Phase );
+static unsigned short  Rwr_FunctionPerm( unsigned uTruth, int Phase );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -85,77 +60,64 @@ static unsigned short      Rwr_FunctionPerm( unsigned uTruth, int Phase );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_ManRwr_t * Abc_NtkManRwrStart( char * pFileName )
+Rwr_Man_t * Rwr_ManStart( char * pFileName )
 {
-    Abc_ManRwr_t * p;
-    unsigned uTruth;
+    Rwr_Man_t * p;
     int i, k, nClasses;
     int clk = clock();
+    int TableSize;
 
-    p = ALLOC( Abc_ManRwr_t, 1 );
-    memset( p, 0, sizeof(Abc_ManRwr_t) );
-    // canonical forms
+    p = ALLOC( Rwr_Man_t, 1 );
+    memset( p, 0, sizeof(Rwr_Man_t) );
     p->nFuncs    = (1<<16);
-    p->puCanons  = ALLOC( unsigned short, p->nFuncs );
-    memset( p->puCanons, 0, sizeof(unsigned short) * p->nFuncs );
-    // permutations
-    p->puPhases  = ALLOC( char, p->nFuncs );
-    memset( p->puPhases, 0, sizeof(char) * p->nFuncs );
-    // hash table
-    p->pTable  = ALLOC( Rwr_Node_t *, p->nFuncs );
-    memset( p->pTable, 0, sizeof(Rwr_Node_t *) * p->nFuncs );
-    // practical classes
+    // create the table
+    TableSize = pFileName? 222: (1<<16);
+    p->pTable = ALLOC( Rwr_Node_t *, TableSize );
+    memset( p->pTable, 0, sizeof(Rwr_Node_t *) * TableSize );
+    // canonical forms, phases, perms
+    Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms );
+    // initialize practical classes
     p->pPractical  = ALLOC( char, p->nFuncs );
     memset( p->pPractical, 0, sizeof(char) * p->nFuncs );
-    // other stuff
-    p->vForest  = Vec_PtrAlloc( 100 );
-    p->vForm    = Vec_IntAlloc( 50 );
-    p->vFanins  = Vec_PtrAlloc( 50 );
-    p->vTfo     = Vec_PtrAlloc( 50 );
-    p->vLevels  = Vec_VecAlloc( 50 );
-    p->pMmNode  = Extra_MmFixedStart( sizeof(Rwr_Node_t) );
-    p->nTravIds = 1;
-    assert( sizeof(Rwr_Node_t) == sizeof(Rwr_Cut_t) );
-
-    // initialize the canonical forms
-    nClasses = 1;
-    for ( i = 1; i < p->nFuncs-1; i++ )
+    for ( i = 0; i < RWR_NUM_CLASSES; i++ )
+        p->pPractical[ s_PracticalClasses[i] ] = 1;
+    // set the mapping of classes
+    nClasses = 0;
+    p->pMap = ALLOC( unsigned char, p->nFuncs );
+    for ( i = 0; i < p->nFuncs; i++ )
     {
-        if ( p->puCanons[i] )
-            continue;
-        nClasses++;
-        for ( k = 0; k < 32; k++ )
+        if ( i != p->puCanons[i] )
         {
-            uTruth = Rwr_FunctionPhase( (unsigned)i, (unsigned)k );
-            if ( p->puCanons[uTruth] == 0 )
-            {
-                p->puCanons[uTruth] = (unsigned short)i;
-                p->puPhases[uTruth] = (char)k;
-            }
-            else
-                assert( p->puCanons[uTruth] == (unsigned short)i );
+            assert( i > p->puCanons[i] );
+            p->pMap[i] = p->pMap[p->puCanons[i]];
+            continue;
         }
+        p->pMap[i] = nClasses++;
     }
-    // set info for constant 1
-    p->puCanons[p->nFuncs-1] = 0;
-    p->puPhases[p->nFuncs-1] = 16;
-    printf( "The number of NN-canonical forms = %d.\n", nClasses );
+    printf( "The number of NPN-canonical forms = %d.\n", nClasses );
 
     // initialize permutations
     for ( i = 0; i < 256; i++ )
         for ( k = 0; k < 16; k++ )
             p->puPerms[i][k] = Rwr_FunctionPerm( i, k );
 
-    // initialize practical classes
-    for ( i = 0; i < RWR_NUM_CLASSES; i++ )
-        p->pPractical[ s_PracticalClasses[i] ] = 1;
+    // other stuff
+    p->nTravIds = 1;
+    p->vForest  = Vec_PtrAlloc( 100 );
+    p->vForm    = Vec_IntAlloc( 50 );
+    p->vFanins  = Vec_PtrAlloc( 50 );
+    p->vTfo     = Vec_PtrAlloc( 50 );
+    p->vTfoFor  = Vec_PtrAlloc( 50 );
+    p->vLevels  = Vec_VecAlloc( 50 );
+    p->pMmNode  = Extra_MmFixedStart( sizeof(Rwr_Node_t) );
+    assert( sizeof(Rwr_Node_t) == sizeof(Rwr_Cut_t) );
 
     // initialize forest
-    Rwr_ManAddVar( p, 0xFFFF ); // constant 1
-    Rwr_ManAddVar( p, 0xAAAA ); // var A
-    Rwr_ManAddVar( p, 0xCCCC ); // var B
-    Rwr_ManAddVar( p, 0xF0F0 ); // var C
-    Rwr_ManAddVar( p, 0xFF00 ); // var D
+    Rwr_ManAddVar( p, 0x0000, pFileName ); // constant 0
+    Rwr_ManAddVar( p, 0xAAAA, pFileName ); // var A
+    Rwr_ManAddVar( p, 0xCCCC, pFileName ); // var B
+    Rwr_ManAddVar( p, 0xF0F0, pFileName ); // var C
+    Rwr_ManAddVar( p, 0xFF00, pFileName ); // var D
     p->nClasses = 5;
 PRT( "Manager startup time", clock() - clk ); 
 
@@ -164,12 +126,13 @@ PRT( "Manager startup time", clock() - clk );
     {   // precompute
         Rwr_ManPrecompute( p );
         Rwr_ManWriteToFile( p, "data.aaa" );
+        Rwr_ManPrintFirst( p );
     }
     else
     {   // load previously saved nodes
         Rwr_ManLoadFromFile( p, pFileName );
+        Rwr_ManPrintNext( p );
     }
-    Rwr_ManPrint( p );
     return p;
 }
 
@@ -184,26 +147,29 @@ PRT( "Manager startup time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkManRwrStop( Abc_ManRwr_t * p )
+void Rwr_ManStop( Rwr_Man_t * p )
 {
     if ( p->vFanNums )  Vec_IntFree( p->vFanNums );
     if ( p->vReqTimes ) Vec_IntFree( p->vReqTimes );
     Vec_IntFree( p->vForm );
     Vec_PtrFree( p->vFanins );
+    Vec_PtrFree( p->vTfoFor );
     Vec_PtrFree( p->vTfo );
     Vec_VecFree( p->vLevels );
     Vec_PtrFree( p->vForest );
     Extra_MmFixedStop( p->pMmNode,   0 );
     free( p->pPractical );
     free( p->puCanons );
-    free( p->puPhases );
+    free( p->pPhases );
+    free( p->pPerms );
+    free( p->pMap );
     free( p->pTable );
     free( p );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Stops the resynthesis manager.]
+  Synopsis    [Assigns elementary cuts to the PIs.]
 
   Description []
                
@@ -212,9 +178,14 @@ void Abc_NtkManRwrStop( Abc_ManRwr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Abc_NtkManRwrDecs( Abc_ManRwr_t * p )
+void Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk )
 {
-    return p->vForm;
+    // save the fanout counters for all internal nodes
+    p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
+    // precompute the required times for all internal nodes
+    p->vReqTimes = Abc_NtkGetRequiredLevels( pNtk );
+    // start the cut computation
+    Rwr_NtkStartCuts( p, pNtk );
 }
 
 /**Function*************************************************************
@@ -228,14 +199,14 @@ Vec_Int_t * Abc_NtkManRwrDecs( Abc_ManRwr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkManRwrFanins( Abc_ManRwr_t * p )
+Vec_Ptr_t * Rwr_ManReadFanins( Rwr_Man_t * p )
 {
     return p->vFanins;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes a phase of the 4-var function.]
+  Synopsis    [Stops the resynthesis manager.]
 
   Description []
                
@@ -244,17 +215,9 @@ Vec_Ptr_t * Abc_NtkManRwrFanins( Abc_ManRwr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned short Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase )
+Vec_Int_t * Rwr_ManReadDecs( Rwr_Man_t * p )
 {
-    static unsigned uMasks0[4] = { 0x5555, 0x3333, 0x0F0F, 0x00FF };
-    static unsigned uMasks1[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
-    int v, Shift;
-    for ( v = 0, Shift = 1; v < 4; v++, Shift <<= 1 )
-        if ( uPhase & Shift )
-            uTruth = (((uTruth & uMasks0[v]) << Shift) | ((uTruth & uMasks1[v]) >> Shift));
-    if ( uPhase & 16 )
-        uTruth = ~uTruth & 0xFFFF;
-    return uTruth;
+    return p->vForm;
 }
 
 /**Function*************************************************************
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index ae8665ef..96d89db5 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -52,49 +52,6 @@ Vec_Int_t * Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk )
     return vFanNums;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Creates the array of required times.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Rwt_NtkRequiredLevels( 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 );
-    // 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 );
-    }
-    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;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////