Version abc80130

9 files changed, 48 insertions, 669 deletions

diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index f24f9535..6d1a6c06 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -21,10 +21,6 @@
 #ifndef __RWR_H__
 #define __RWR_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -53,7 +49,6 @@ 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
@@ -68,17 +63,14 @@ 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;
@@ -88,8 +80,6 @@ struct Rwr_Man_t_
     int                timeCut;
     int                timeRes;
     int                timeEval;
-    int                timeMffc;
-    int                timeUpdate;
     int                timeTotal;
 };
 
@@ -97,9 +87,6 @@ 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
@@ -111,13 +98,13 @@ struct Rwr_Node_t_ // 24 bytes
 };
 
 // manipulation of complemented attributes
-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));  }
+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));  }
 
 ////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
+///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
@@ -127,9 +114,7 @@ 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 fUpdateLevel, int fUseZeros, int fPlaceEnable );
-extern void              Rwr_ScoresClean( Rwr_Man_t * p );
-extern void              Rwr_ScoresReport( Rwr_Man_t * p );
+extern int               Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros );
 /*=== rwrLib.c ========================================================*/
 extern void              Rwr_ManPrecompute( Rwr_Man_t * p );
 extern Rwr_Node_t *      Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute );
@@ -140,12 +125,9 @@ 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 );
@@ -157,13 +139,9 @@ 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 ef7af34f..d072879d 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -49,8 +49,6 @@ 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++ )
     {
@@ -62,7 +60,6 @@ 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
@@ -135,7 +132,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, 0 );
+        eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1 );
     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 396a659c..c934dfd8 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -25,13 +25,10 @@
 ///                        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, 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 );
+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 );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -52,35 +49,27 @@ static int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves );
   SeeAlso     []
 
 ***********************************************************************/
-int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable )
+int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros )
 {
     int fVeryVerbose = 0;
     Dec_Graph_t * pGraph;
-    Cut_Cut_t * pCut;//, * pTemp;
+    Cut_Cut_t * pCut;
     Abc_Obj_t * pFanin;
-    unsigned uPhase, uTruthBest, uTruth;
+    unsigned uPhase, uTruthBest;
     char * pPerm;
-    int Required, nNodesSaved, nNodesSaveCur;
+    int Required, nNodesSaved;
     int i, GainCur, GainBest = -1;
-    int clk, clk2;//, Counter;
+    int clk, clk2;
 
     p->nNodesConsidered++;
     // get the required times
-    Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
-
+    Required = Abc_NodeReadRequiredLevel( pNode );
     // get the node's cuts
 clk = clock();
-    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0, 0 );
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode );
     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 )
@@ -88,12 +77,9 @@ clk = clock();
         // consider only 4-input cuts
         if ( pCut->nLeaves < 4 )
             continue;
-//            Cut_CutPrint( pCut, 0 ), printf( "\n" );
-
         // get the fanin permutation
-        uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
-        pPerm = p->pPerms4[ p->pPerms[uTruth] ];
-        uPhase = p->pPhases[uTruth];
+        pPerm = p->pPerms4[ p->pPerms[pCut->uTruth] ];
+        uPhase = p->pPhases[pCut->uTruth];
         // collect fanins with the corresponding permutation/phase
         Vec_PtrClear( p->vFaninsCur );
         Vec_PtrFill( p->vFaninsCur, (int)pCut->nLeaves, 0 );
@@ -112,48 +98,29 @@ 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_NodeMffcLabelAig( pNode );
+        nNodesSaved = Abc_NodeMffcLabel( 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, fPlaceEnable );
+        pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur );
 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 = 0xFFFF & *Cut_CutReadTruth(pCut);
+            uTruthBest = pCut->uTruth;
             // collect fanins in the
             Vec_PtrClear( p->vFanins );
             Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
@@ -164,69 +131,22 @@ 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 && GainBest > 0 )
+    if ( fVeryVerbose )
     {
         printf( "Node %6s :   ", Abc_ObjName(pNode) );
         printf( "Fanins = %d. ", p->vFanins->nSize );
-        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( "Cone = %2d.  ", Dec_GraphNodeNum(p->pGraph) );
+        printf( "GAIN = %2d.  ", GainBest );
         printf( "\n" );
     }
     return GainBest;
@@ -243,22 +163,17 @@ 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, int fPlaceEnable )
+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 )
 {
-    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
-    uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
-    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
+    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[pCut->uTruth] );
     p->nSubgraphs += vSubgraphs->nSize;
     // determine the best subgraph
     GainBest = -1;
-    CostBest = ABC_INFINITY;
     Vec_PtrForEachEntry( vSubgraphs, pNode, i )
     {
         // get the current graph
@@ -271,58 +186,11 @@ Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCu
         if ( nNodesAdded == -1 )
             continue;
         assert( 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
-*/
+        // count the gain at this node
+        if ( GainBest < nNodesSaved - nNodesAdded )
         {
-            // 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;
-                }
-            }
+            GainBest   = nNodesSaved - nNodesAdded;
+            pGraphBest = pGraphCur;
         }
     }
     if ( GainBest == -1 )
@@ -331,257 +199,6 @@ 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 2d00bb1c..e93a2611 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c
index 1cdf350e..fbcb8916 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 87a080c7..a21dd520 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**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();
+    pManDec   = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
     p->puCanons = pManDec->puCanons; 
     p->pPhases  = pManDec->pPhases; 
     p->pPerms   = pManDec->pPerms; 
@@ -75,7 +75,6 @@ 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 );
@@ -113,13 +112,11 @@ 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 );
-    FREE( p->pMapInv );
+    Extra_MmFixedStop( p->pMmNode, 0 );
     free( p->pTable );
     free( p->pPractical );
     free( p->pPerms4 );
@@ -150,50 +147,20 @@ 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( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
+    printf( "Calculated gain   = %8d.\n", p->nNodesGained     );
     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:\n" );
+    printf( "The scores are : " );
     for ( i = 0; i < 222; i++ )
         if ( p->nScores[i] > 0 )
-        {
-            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( "%d=%d ", i, p->nScores[i] );
     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*************************************************************
@@ -223,22 +190,6 @@ 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;
@@ -271,22 +222,6 @@ 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 82ad2a90..30c99f00 100644
--- a/src/opt/rwr/rwrPrint.c
+++ b/src/opt/rwr/rwrPrint.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
  
 /**Function*************************************************************
@@ -79,33 +79,6 @@ 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 []
@@ -246,9 +219,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, "Roots = %3d. Vol = %3d. Sum = %3d.  ", nFuncs, Volume, Rwr_GetBushSumOfVolumes(p, i) );
+        fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume );
         uTruth = i;
         Extra_PrintBinary( pFile, &uTruth, 16 );
         fprintf( pFile, "\n" );
diff --git a/src/opt/rwr/rwrTemp.c b/src/opt/rwr/rwrTemp.c
deleted file mode 100644
index 3ffbd408..00000000
--- a/src/opt/rwr/rwrTemp.c
+++ /dev/null
@@ -1,121 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [rwrCut.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [DAG-aware AIG rewriting package.]
-
-  Synopsis    [Cut computation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: rwrCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "rwr.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static 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 b2add2bf..65b2bd6f 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -34,7 +34,7 @@ static unsigned short s_RwtAigSubgraphs[];
 #endif
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************