Version abc50908

5 files changed, 66 insertions, 8 deletions

diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 6d1a6c06..1467ce7a 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -49,6 +49,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,10 +64,11 @@ 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;
@@ -80,6 +82,8 @@ struct Rwr_Man_t_
     int                timeCut;
     int                timeRes;
     int                timeEval;
+    int                timeMffc;
+    int                timeUpdate;
     int                timeTotal;
 };
 
@@ -114,7 +118,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 fUseZeros );
+extern int               Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, 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 );
@@ -128,6 +132,7 @@ extern void              Rwr_ManPrintStats( Rwr_Man_t * p );
 extern void *            Rwr_ManReadDecs( Rwr_Man_t * p );
 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
 extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
+extern void              Rwr_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 );
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
index d072879d..a7f55a90 100644
--- a/src/opt/rwr/rwrDec.c
+++ b/src/opt/rwr/rwrDec.c
@@ -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
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index c934dfd8..8a00cec8 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -49,7 +49,7 @@ 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 fVeryVerbose = 0;
     Dec_Graph_t * pGraph;
@@ -63,7 +63,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
 
     p->nNodesConsidered++;
     // get the required times
-    Required = Abc_NodeReadRequiredLevel( pNode );
+    Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
     // get the node's cuts
 clk = clock();
     pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode );
@@ -98,6 +98,7 @@ clk = clock();
         }
         p->nCutsGood++;
 
+clk2 = clock();
         // mark the fanin boundary 
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize++;
@@ -107,6 +108,7 @@ clk = clock();
         // unmark the fanin boundary
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize--;
+p->timeMffc += clock() - clk2;
 
         // evaluate the cut
 clk2 = clock();
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index a21dd520..bfeaa273 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -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 );
+    FREE( p->pMapInv );
     free( p->pTable );
     free( p->pPractical );
     free( p->pPerms4 );
@@ -151,14 +154,16 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
     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( "%3d = %8d  canon = %5d\n", i, p->nScores[i], p->pMapInv[i] );
     printf( "\n" );
 */
 }
@@ -222,6 +227,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..9011ce56 100644
--- a/src/opt/rwr/rwrPrint.c
+++ b/src/opt/rwr/rwrPrint.c
@@ -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" );