Version abc80130_2

9 files changed, 669 insertions, 48 deletions

diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 6d1a6c06..f24f9535 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -21,6 +21,10 @@
 #ifndef __RWR_H__
 #define __RWR_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -49,6 +53,7 @@ struct Rwr_Man_t_
     char *             pPhases;          // canonical phases
     char *             pPerms;           // canonical permutations
     unsigned char *    pMap;             // mapping of functions into class numbers
+    unsigned short *   pMapInv;          // mapping of classes into functions
     char *             pPractical;       // practical NPN classes
     char **            pPerms4;          // four-var permutations
     // node space
@@ -63,14 +68,17 @@ struct Rwr_Man_t_
     int                nClasses;         // the number of NN classes
     // the result of resynthesis
     int                fCompl;           // indicates if the output of FF should be complemented
-    void *             pGraph;            // the decomposition tree (temporary)
+    void *             pGraph;           // the decomposition tree (temporary)
     Vec_Ptr_t *        vFanins;          // the fanins array (temporary)
     Vec_Ptr_t *        vFaninsCur;       // the fanins array (temporary)
     Vec_Int_t *        vLevNums;         // the array of levels (temporary)
+    Vec_Ptr_t *        vNodesTemp;       // the nodes in MFFC (temporary)
     // node statistics
     int                nNodesConsidered;
     int                nNodesRewritten;
     int                nNodesGained;
+    int                nNodesBeg;
+    int                nNodesEnd;
     int                nScores[222];
     int                nCutsGood;
     int                nCutsBad;
@@ -80,6 +88,8 @@ struct Rwr_Man_t_
     int                timeCut;
     int                timeRes;
     int                timeEval;
+    int                timeMffc;
+    int                timeUpdate;
     int                timeTotal;
 };
 
@@ -87,6 +97,9 @@ struct Rwr_Node_t_ // 24 bytes
 {
     int                Id;               // ID 
     int                TravId;           // traversal ID
+    short              nScore;
+    short              nGain;
+    short              nAdded;
     unsigned           uTruth : 16;      // truth table
     unsigned           Volume :  8;      // volume
     unsigned           Level  :  6;      // level
@@ -98,13 +111,13 @@ struct Rwr_Node_t_ // 24 bytes
 };
 
 // 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);  }
-static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p )             { return (Rwr_Node_t *)((unsigned)(p) ^  01);  }
-static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_Node_t *)((unsigned)(p) ^ (c));  }
+static inline bool         Rwr_IsComplement( Rwr_Node_t * p )    { return (bool)(((unsigned long)p) & 01);           }
+static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p )         { return (Rwr_Node_t *)((unsigned long)(p) & ~01);  }
+static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p )             { return (Rwr_Node_t *)((unsigned long)(p) ^  01);  }
+static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_Node_t *)((unsigned long)(p) ^ (c));  }
 
 ////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFITIONS                             ///
+///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
@@ -114,7 +127,9 @@ static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_N
 /*=== 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 );
+extern int               Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable );
+extern void              Rwr_ScoresClean( Rwr_Man_t * p );
+extern void              Rwr_ScoresReport( Rwr_Man_t * p );
 /*=== rwrLib.c ========================================================*/
 extern void              Rwr_ManPrecompute( Rwr_Man_t * p );
 extern Rwr_Node_t *      Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute );
@@ -125,9 +140,12 @@ extern void              Rwr_ManIncTravId( Rwr_Man_t * p );
 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_ManPrintStatsFile( Rwr_Man_t * p );
 extern void *            Rwr_ManReadDecs( Rwr_Man_t * p );
+extern Vec_Ptr_t *       Rwr_ManReadLeaves( 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_ManAddTimeUpdate( 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 );
@@ -139,9 +157,13 @@ extern void              Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName );
 extern void              Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode );
 extern char *            Rwr_ManGetPractical( Rwr_Man_t * p );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
index d072879d..ef7af34f 100644
--- a/src/opt/rwr/rwrDec.c
+++ b/src/opt/rwr/rwrDec.c
@@ -29,7 +29,7 @@ static Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode );
 static Dec_Edge_t    Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -49,6 +49,8 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
     Rwr_Node_t * pNode;
     int i, k;
     // put the nodes into the structure
+    p->pMapInv  = ALLOC( unsigned short, 222 );
+    memset( p->pMapInv, 0, sizeof(unsigned short) * 222 );
     p->vClasses = Vec_VecStart( 222 );
     for ( i = 0; i < p->nFuncs; i++ )
     {
@@ -60,6 +62,7 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
             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 );
+            p->pMapInv[ p->pMap[pNode->uTruth] ] = p->puCanons[pNode->uTruth];
         }
     }
     // compute decomposition forms for each node and verify them
@@ -132,7 +135,7 @@ Dec_Edge_t Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t *
         eNode1.fCompl = !eNode1.fCompl;
     // create the decomposition node(s)
     if ( pNode->fExor )
-        eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1 );
+        eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1, 0 );
     else
         eNode = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
     // save the result
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index c934dfd8..396a659c 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -25,10 +25,13 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Dec_Graph_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 );
+static Dec_Graph_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, int fPlaceEnable );
+static int Rwr_CutIsBoolean( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves );
+static int Rwr_CutCountNumNodes( Abc_Obj_t * pObj, Cut_Cut_t * pCut );
+static int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -49,27 +52,35 @@ static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_
   SeeAlso     []
 
 ***********************************************************************/
-int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros )
+int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable )
 {
     int fVeryVerbose = 0;
     Dec_Graph_t * pGraph;
-    Cut_Cut_t * pCut;
+    Cut_Cut_t * pCut;//, * pTemp;
     Abc_Obj_t * pFanin;
-    unsigned uPhase, uTruthBest;
+    unsigned uPhase, uTruthBest, uTruth;
     char * pPerm;
-    int Required, nNodesSaved;
+    int Required, nNodesSaved, nNodesSaveCur;
     int i, GainCur, GainBest = -1;
-    int clk, clk2;
+    int clk, clk2;//, Counter;
 
     p->nNodesConsidered++;
     // get the required times
-    Required = Abc_NodeReadRequiredLevel( pNode );
+    Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
+
     // get the node's cuts
 clk = clock();
-    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode );
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0, 0 );
     assert( pCut != NULL );
 p->timeCut += clock() - clk;
 
+//printf( " %d", Rwr_CutCountNumNodes(pNode, pCut) );
+/*
+    Counter = 0;
+    for ( pTemp = pCut->pNext; pTemp; pTemp = pTemp->pNext )
+        Counter++;
+    printf( "%d ", Counter );
+*/
     // go through the cuts
 clk = clock();
     for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
@@ -77,9 +88,12 @@ clk = clock();
         // consider only 4-input cuts
         if ( pCut->nLeaves < 4 )
             continue;
+//            Cut_CutPrint( pCut, 0 ), printf( "\n" );
+
         // get the fanin permutation
-        pPerm = p->pPerms4[ p->pPerms[pCut->uTruth] ];
-        uPhase = p->pPhases[pCut->uTruth];
+        uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
+        pPerm = p->pPerms4[ p->pPerms[uTruth] ];
+        uPhase = p->pPhases[uTruth];
         // collect fanins with the corresponding permutation/phase
         Vec_PtrClear( p->vFaninsCur );
         Vec_PtrFill( p->vFaninsCur, (int)pCut->nLeaves, 0 );
@@ -98,29 +112,48 @@ clk = clock();
         }
         p->nCutsGood++;
 
+        {
+            int Counter = 0;
+            Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+                if ( Abc_ObjFanoutNum(Abc_ObjRegular(pFanin)) == 1 )
+                    Counter++;
+            if ( Counter > 2 )
+                continue;
+        }
+
+clk2 = clock();
+/*
+        printf( "Considering: (" );
+        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+            printf( "%d ", Abc_ObjFanoutNum(Abc_ObjRegular(pFanin)) );
+        printf( ")\n" );
+*/
         // 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 );
+        nNodesSaved = Abc_NodeMffcLabelAig( pNode );
         // unmark the fanin boundary
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize--;
+p->timeMffc += clock() - clk2;
 
         // evaluate the cut
 clk2 = clock();
-        pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur );
+        pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, fPlaceEnable );
 p->timeEval += clock() - clk2;
 
         // check if the cut is better than the current best one
         if ( pGraph != NULL && GainBest < GainCur )
         {
             // save this form
+            nNodesSaveCur = nNodesSaved;
             GainBest  = GainCur;
             p->pGraph  = pGraph;
             p->fCompl = ((uPhase & (1<<4)) > 0);
-            uTruthBest = pCut->uTruth;
+            uTruthBest = 0xFFFF & *Cut_CutReadTruth(pCut);
             // collect fanins in the
             Vec_PtrClear( p->vFanins );
             Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
@@ -131,22 +164,69 @@ p->timeRes += clock() - clk;
 
     if ( GainBest == -1 )
         return -1;
+/*
+    if ( GainBest > 0 )
+    {
+        printf( "Class %d  ", p->pMap[uTruthBest] );
+        printf( "Gain = %d. Node %d : ", GainBest, pNode->Id );
+        Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+            printf( "%d ", Abc_ObjRegular(pFanin)->Id );
+        Dec_GraphPrint( stdout, p->pGraph, NULL, NULL );
+        printf( "\n" );
+    }
+*/
+
+//    printf( "%d", nNodesSaveCur - GainBest );
+/*
+    if ( GainBest > 0 )
+    {
+        if ( Rwr_CutIsBoolean( pNode, p->vFanins ) )
+            printf( "b" );
+        else
+        {
+            printf( "Node %d : ", pNode->Id );
+            Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+                printf( "%d ", Abc_ObjRegular(pFanin)->Id );
+            printf( "a" );
+        }
+    }
+*/
+/*
+    if ( GainBest > 0 )
+        if ( p->fCompl )
+            printf( "c" );
+        else
+            printf( "." );
+*/
 
     // copy the leaves
     Vec_PtrForEachEntry( p->vFanins, pFanin, i )
         Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
+/*
+    printf( "(" );
+    Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+        printf( " %d", Abc_ObjRegular(pFanin)->vFanouts.nSize - 1 );
+    printf( " )  " );
+*/
+//    printf( "%d ", Rwr_NodeGetDepth_rec( pNode, p->vFanins ) );
 
     p->nScores[p->pMap[uTruthBest]]++;
-    p->nNodesRewritten++;
     p->nNodesGained += GainBest;
+    if ( fUseZeros || GainBest > 0 )
+    {
+        p->nNodesRewritten++;
+    }
 
     // report the progress
-    if ( fVeryVerbose )
+    if ( fVeryVerbose && GainBest > 0 )
     {
         printf( "Node %6s :   ", Abc_ObjName(pNode) );
         printf( "Fanins = %d. ", p->vFanins->nSize );
-        printf( "Cone = %2d.  ", Dec_GraphNodeNum(p->pGraph) );
-        printf( "GAIN = %2d.  ", GainBest );
+        printf( "Save = %d.  ", nNodesSaveCur );
+        printf( "Add = %d.  ",  nNodesSaveCur-GainBest );
+        printf( "GAIN = %d.  ", GainBest );
+        printf( "Cone = %d.  ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
+        printf( "Class = %d.  ", p->pMap[uTruthBest] );
         printf( "\n" );
     }
     return GainBest;
@@ -163,17 +243,22 @@ p->timeRes += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Dec_Graph_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 )
+Dec_Graph_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, int fPlaceEnable )
 {
+    extern int            Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
     Vec_Ptr_t * vSubgraphs;
     Dec_Graph_t * pGraphBest, * pGraphCur;
     Rwr_Node_t * pNode, * pFanin;
     int nNodesAdded, GainBest, i, k;
+    unsigned uTruth;
+    float CostBest;//, CostCur;
     // find the matching class of subgraphs
-    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[pCut->uTruth] );
+    uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
+    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
     p->nSubgraphs += vSubgraphs->nSize;
     // determine the best subgraph
     GainBest = -1;
+    CostBest = ABC_INFINITY;
     Vec_PtrForEachEntry( vSubgraphs, pNode, i )
     {
         // get the current graph
@@ -186,11 +271,58 @@ Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCu
         if ( nNodesAdded == -1 )
             continue;
         assert( nNodesSaved >= nNodesAdded );
-        // count the gain at this node
-        if ( GainBest < nNodesSaved - nNodesAdded )
+/*
+        // evaluate the cut
+        if ( fPlaceEnable )
+        {
+            extern float Abc_PlaceEvaluateCut( Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins );
+
+            float Alpha = 0.5; // ???
+            float PlaceCost;
+
+            // get the placement cost of the cut
+            PlaceCost = Abc_PlaceEvaluateCut( pRoot, vFaninsCur );
+
+            // get the weigted cost of the cut
+            CostCur = nNodesSaved - nNodesAdded + Alpha * PlaceCost;
+
+            // do not allow uphill moves
+            if ( nNodesSaved - nNodesAdded < 0 )
+                continue;
+
+            // decide what cut to use
+            if ( CostBest > CostCur )
+            {
+                GainBest   = nNodesSaved - nNodesAdded; // pure node cost
+                CostBest   = CostCur;                   // cost with placement
+                pGraphBest = pGraphCur;                 // subgraph to be used for rewriting
+
+                // score the graph
+                if ( nNodesSaved - nNodesAdded > 0 )
+                {
+                    pNode->nScore++;
+                    pNode->nGain += GainBest;
+                    pNode->nAdded += nNodesAdded;
+                }
+            }
+        }
+        else
+*/
         {
-            GainBest   = nNodesSaved - nNodesAdded;
-            pGraphBest = pGraphCur;
+            // count the gain at this node
+            if ( GainBest < nNodesSaved - nNodesAdded )
+            {
+                GainBest   = nNodesSaved - nNodesAdded;
+                pGraphBest = pGraphCur;
+
+                // score the graph
+                if ( nNodesSaved - nNodesAdded > 0 )
+                {
+                    pNode->nScore++;
+                    pNode->nGain += GainBest;
+                    pNode->nAdded += nNodesAdded;
+                }
+            }
         }
     }
     if ( GainBest == -1 )
@@ -199,6 +331,257 @@ Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCu
     return pGraphBest;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks the type of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_CutIsBoolean_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves, int fMarkA )
+{
+    if ( Vec_PtrFind(vLeaves, pObj) >= 0 || Vec_PtrFind(vLeaves, Abc_ObjNot(pObj)) >= 0 )
+    {
+        if ( fMarkA )
+            pObj->fMarkA = 1;
+        else
+            pObj->fMarkB = 1;
+        return;
+    }
+    assert( !Abc_ObjIsCi(pObj) );
+    Rwr_CutIsBoolean_rec( Abc_ObjFanin0(pObj), vLeaves, fMarkA );
+    Rwr_CutIsBoolean_rec( Abc_ObjFanin1(pObj), vLeaves, fMarkA );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the type of the cut.]
+
+  Description [Returns 1(0) if the cut is Boolean (algebraic).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_CutIsBoolean( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pTemp;
+    int i, RetValue;
+    Vec_PtrForEachEntry( vLeaves, pTemp, i )
+    {
+        pTemp = Abc_ObjRegular(pTemp);
+        assert( !pTemp->fMarkA && !pTemp->fMarkB );
+    }
+    Rwr_CutIsBoolean_rec( Abc_ObjFanin0(pObj), vLeaves, 1 );
+    Rwr_CutIsBoolean_rec( Abc_ObjFanin1(pObj), vLeaves, 0 );
+    RetValue = 0;
+    Vec_PtrForEachEntry( vLeaves, pTemp, i )
+    {
+        pTemp = Abc_ObjRegular(pTemp);
+        RetValue |= pTemp->fMarkA && pTemp->fMarkB;
+        pTemp->fMarkA = pTemp->fMarkB = 0;
+    }
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Count the nodes in the cut space of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_CutCountNumNodes_rec( Abc_Obj_t * pObj, Cut_Cut_t * pCut, Vec_Ptr_t * vNodes )
+{
+    int i;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        if ( pCut->pLeaves[i] == pObj->Id )
+        {
+            // check if the node is collected
+            if ( pObj->fMarkC == 0 )
+            {
+                pObj->fMarkC = 1;
+                Vec_PtrPush( vNodes, pObj );
+            }
+            return;
+        }
+    assert( Abc_ObjIsNode(pObj) );
+    // check if the node is collected
+    if ( pObj->fMarkC == 0 )
+    {
+        pObj->fMarkC = 1;
+        Vec_PtrPush( vNodes, pObj );
+    }
+    // traverse the fanins
+    Rwr_CutCountNumNodes_rec( Abc_ObjFanin0(pObj), pCut, vNodes );
+    Rwr_CutCountNumNodes_rec( Abc_ObjFanin1(pObj), pCut, vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the nodes in the cut space of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_CutCountNumNodes( Abc_Obj_t * pObj, Cut_Cut_t * pCut )
+{
+    Vec_Ptr_t * vNodes;
+    int i, Counter;
+    // collect all nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
+        Rwr_CutCountNumNodes_rec( pObj, pCut, vNodes );
+    // clean all nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->fMarkC = 0;
+    // delete and return
+    Counter = Vec_PtrSize(vNodes);
+    Vec_PtrFree( vNodes );
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns depth of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pLeaf;
+    int i, Depth0, Depth1;
+    if ( Abc_ObjIsCi(pObj) )
+        return 0;
+    Vec_PtrForEachEntry( vLeaves, pLeaf, i )
+        if ( pObj == Abc_ObjRegular(pLeaf) )
+            return 0;
+    Depth0 = Rwr_NodeGetDepth_rec( Abc_ObjFanin0(pObj), vLeaves );
+    Depth1 = Rwr_NodeGetDepth_rec( Abc_ObjFanin1(pObj), vLeaves );
+    return 1 + ABC_MAX( Depth0, Depth1 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ScoresClean( Rwr_Man_t * p )
+{
+    Vec_Ptr_t * vSubgraphs;
+    Rwr_Node_t * pNode;
+    int i, k;
+    for ( i = 0; i < p->vClasses->nSize; i++ )
+    {
+        vSubgraphs = Vec_VecEntry( p->vClasses, i );
+        Vec_PtrForEachEntry( vSubgraphs, pNode, k )
+            pNode->nScore = pNode->nGain = pNode->nAdded = 0;
+    }
+}
+
+static int Gains[222];
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_ScoresCompare( int * pNum1, int * pNum2 )
+{
+    if ( Gains[*pNum1] > Gains[*pNum2] )
+        return -1;
+    if ( Gains[*pNum1] < Gains[*pNum2] )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ScoresReport( Rwr_Man_t * p )
+{
+    extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
+    int Perm[222];
+    Vec_Ptr_t * vSubgraphs;
+    Rwr_Node_t * pNode;
+    int i, iNew, k;
+    unsigned uTruth;
+    // collect total gains
+    assert( p->vClasses->nSize == 222 );
+    for ( i = 0; i < p->vClasses->nSize; i++ )
+    {
+        Perm[i] = i;
+        Gains[i] = 0;
+        vSubgraphs = Vec_VecEntry( p->vClasses, i );
+        Vec_PtrForEachEntry( vSubgraphs, pNode, k )
+            Gains[i] += pNode->nGain;
+    }
+    // sort the gains
+    qsort( Perm, 222, sizeof(int), (int (*)(const void *, const void *))Rwr_ScoresCompare );
+
+    // print classes
+    for ( i = 0; i < p->vClasses->nSize; i++ )
+    {
+        iNew = Perm[i];
+        if ( Gains[iNew] == 0 )
+            break;
+        vSubgraphs = Vec_VecEntry( p->vClasses, iNew );
+        printf( "CLASS %3d: Subgr = %3d. Total gain = %6d.  ", iNew, Vec_PtrSize(vSubgraphs), Gains[iNew] );
+        uTruth = (unsigned)p->pMapInv[iNew];
+        Extra_PrintBinary( stdout, &uTruth, 16 );
+        printf( "  " );
+        Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[iNew] | ((unsigned)p->pMapInv[iNew] << 16) );
+        Vec_PtrForEachEntry( vSubgraphs, pNode, k )
+        {
+            if ( pNode->nScore == 0 )
+                continue;
+            printf( "    %2d: S=%5d. A=%5d. G=%6d. ", k, pNode->nScore, pNode->nAdded, pNode->nGain );
+            Dec_GraphPrint( stdout, (Dec_Graph_t *)pNode->pNext, NULL, NULL );
+        }
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c
index e93a2611..2d00bb1c 100644
--- a/src/opt/rwr/rwrExp.c
+++ b/src/opt/rwr/rwrExp.c
@@ -47,7 +47,7 @@ static Rwr_Man4_t * s_pManRwrExp4 = NULL;
 static Rwr_Man5_t * s_pManRwrExp5 = NULL;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c
index fbcb8916..1cdf350e 100644
--- a/src/opt/rwr/rwrLib.c
+++ b/src/opt/rwr/rwrLib.c
@@ -28,7 +28,7 @@ static Rwr_Node_t *        Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_N
 static void                Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index a21dd520..87a080c7 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -50,7 +50,7 @@ clk = clock();
     p = ALLOC( Rwr_Man_t, 1 );
     memset( p, 0, sizeof(Rwr_Man_t) );
     p->nFuncs = (1<<16);
-    pManDec   = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    pManDec   = Abc_FrameReadManDec();
     p->puCanons = pManDec->puCanons; 
     p->pPhases  = pManDec->pPhases; 
     p->pPerms   = pManDec->pPerms; 
@@ -75,6 +75,7 @@ clk = clock();
     p->vLevNums   = Vec_IntAlloc( 50 );
     p->vFanins    = Vec_PtrAlloc( 50 );
     p->vFaninsCur = Vec_PtrAlloc( 50 );
+    p->vNodesTemp = Vec_PtrAlloc( 50 );
     if ( fPrecompute )
     {   // precompute subgraphs
         Rwr_ManPrecompute( p );
@@ -112,11 +113,13 @@ void Rwr_ManStop( Rwr_Man_t * p )
             Dec_GraphFree( (Dec_Graph_t *)pNode->pNext );
     }
     if ( p->vClasses )  Vec_VecFree( p->vClasses );
+    Vec_PtrFree( p->vNodesTemp );
     Vec_PtrFree( p->vForest );
     Vec_IntFree( p->vLevNums );
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vFaninsCur );
-    Extra_MmFixedStop( p->pMmNode, 0 );
+    Extra_MmFixedStop( p->pMmNode );
+    FREE( p->pMapInv );
     free( p->pTable );
     free( p->pPractical );
     free( p->pPerms4 );
@@ -147,20 +150,50 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
     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     );
+    printf( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
     PRT( "Start       ", p->timeStart );
     PRT( "Cuts        ", p->timeCut );
     PRT( "Resynthesis ", p->timeRes );
+    PRT( "    Mffc    ", p->timeMffc );
     PRT( "    Eval    ", p->timeEval );
+    PRT( "Update      ", p->timeUpdate );
     PRT( "TOTAL       ", p->timeTotal );
 
 /*
-    printf( "The scores are : " );
+    printf( "The scores are:\n" );
     for ( i = 0; i < 222; i++ )
         if ( p->nScores[i] > 0 )
-            printf( "%d=%d ", i, p->nScores[i] );
-    printf( "\n" );
+        {
+            extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
+            printf( "%3d = %8d  canon = %5d  ", i, p->nScores[i], p->pMapInv[i] );
+            Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[i] | ((unsigned)p->pMapInv[i] << 16) );
+        }
 */
+    printf( "\n" );
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManPrintStatsFile( Rwr_Man_t * p )
+{
+    FILE * pTable;
+    pTable = fopen( "stats.txt", "a+" );
+    fprintf( pTable, "%d ", p->nCutsGood );
+    fprintf( pTable, "%d ", p->nSubgraphs );
+    fprintf( pTable, "%d ", p->nNodesRewritten );
+    fprintf( pTable, "%d", p->nNodesGained );
+    fprintf( pTable, "\n" );
+    fclose( pTable );
 }
 
 /**Function*************************************************************
@@ -190,6 +223,22 @@ void * Rwr_ManReadDecs( Rwr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Ptr_t * Rwr_ManReadLeaves( Rwr_Man_t * p )
+{
+    return p->vFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Rwr_ManReadCompl( Rwr_Man_t * p )
 {
     return p->fCompl;
@@ -222,6 +271,22 @@ void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time )
   SeeAlso     []
 
 ***********************************************************************/
+void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time )
+{
+    p->timeUpdate += Time;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time )
 {
     p->timeTotal += Time;
diff --git a/src/opt/rwr/rwrPrint.c b/src/opt/rwr/rwrPrint.c
index 30c99f00..82ad2a90 100644
--- a/src/opt/rwr/rwrPrint.c
+++ b/src/opt/rwr/rwrPrint.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
  
 /**Function*************************************************************
@@ -79,6 +79,33 @@ void Rwr_GetBushVolume( Rwr_Man_t * p, int Entry, int * pVolume, int * pnFuncs )
 
 /**Function*************************************************************
 
+  Synopsis    [Adds the node to the end of the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_GetBushSumOfVolumes( Rwr_Man_t * p, int Entry )
+{
+    Rwr_Node_t * pNode;
+    int Volume, VolumeTotal = 0;
+    for ( pNode = p->pTable[Entry]; pNode; pNode = pNode->pNext )
+    {
+        if ( pNode->uTruth != p->puCanons[pNode->uTruth] )
+            continue;
+        Volume = 0;
+        Rwr_ManIncTravId( p );
+        Rwr_Trav2_rec( p, pNode, &Volume );
+        VolumeTotal += Volume;
+    }
+    return VolumeTotal;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints one rwr node.]
 
   Description []
@@ -219,9 +246,9 @@ void Rwr_ManPrint( Rwr_Man_t * p )
             continue;
         if ( i != p->puCanons[i] )
             continue;
-        fprintf( pFile, "\nClass %3d.  Func %6d.  ", p->pMap[i], 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 );
+        fprintf( pFile, "Roots = %3d. Vol = %3d. Sum = %3d.  ", nFuncs, Volume, Rwr_GetBushSumOfVolumes(p, i) );
         uTruth = i;
         Extra_PrintBinary( pFile, &uTruth, 16 );
         fprintf( pFile, "\n" );
diff --git a/src/opt/rwr/rwrTemp.c b/src/opt/rwr/rwrTemp.c
new file mode 100644
index 00000000..3ffbd408
--- /dev/null
+++ b/src/opt/rwr/rwrTemp.c
@@ -0,0 +1,121 @@
+/**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 int pTruths[13719];
+static int pFreqs[13719];
+static int pPerm[13719];
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_TempCompare( int * pNum1, int * pNum2 )
+{
+    int Freq1 = pFreqs[*pNum1];
+    int Freq2 = pFreqs[*pNum2];
+    if ( Freq1 < Freq2 )
+        return 1;
+    if ( Freq1 > Freq2 )
+        return -1;
+    return 0; 
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_Temp()
+{
+    char Buffer[32];
+    int nFuncs = 13719;
+    int nEntries = 100;
+    unsigned uTruth;
+    int i, k;
+    FILE * pFile;
+
+    pFile = fopen( "nnclass_stats5.txt", "r" );
+    for ( i = 0; i < 13719; i++ )
+    {
+        fscanf( pFile, "%s%d", Buffer, &pFreqs[i] );
+        Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
+        pTruths[i] = uTruth;
+    }
+    fclose( pFile );
+
+    for ( i = 0; i < 13719; i++ )
+        pPerm[i] = i;
+
+    qsort( (void *)pPerm, 13719, sizeof(int), 
+            (int (*)(const void *, const void *)) Rwr_TempCompare );
+
+
+    pFile = fopen( "5npn_100.blif", "w" );
+    fprintf( pFile, "# Most frequent NPN classes of 5 vars.\n" );
+    fprintf( pFile, ".model 5npn\n" );
+    fprintf( pFile, ".inputs a b c d e\n" );
+    fprintf( pFile, ".outputs" );
+    for ( i = 0; i < nEntries; i++ )
+        fprintf( pFile, " %02d", i );
+    fprintf( pFile, "\n" );
+
+    for ( i = 0; i < nEntries; i++ )
+    {
+        fprintf( pFile, ".names a b c d e %02d\n", i );
+        uTruth = pTruths[pPerm[i]];
+        for ( k = 0; k < 32; k++ )
+            if ( uTruth & (1 << k) )
+            {
+                Extra_PrintBinary( pFile, &k, 5 );
+                fprintf( pFile, " 1\n" );
+            }
+    }
+    fprintf( pFile, ".end\n" );
+    fclose( pFile );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index 65b2bd6f..b2add2bf 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -34,7 +34,7 @@ static unsigned short s_RwtAigSubgraphs[];
 #endif
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************