New MFS package.

5 files changed, 24 insertions, 32 deletions

diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 9916b582..8292e617 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -50,6 +50,7 @@ struct Mfs_Par_t_
     int           nWinSizeMax;   // the maximum size of the window
     int           nGrowthLevel;  // the maximum allowed growth in level
     int           nBTLimit;      // the maximum number of conflicts in one SAT run
+    int           fRrOnly;       // perform redundance removal
     int           fResub;        // performs resubstitution
     int           fArea;         // performs optimization for area
     int           fMoreEffort;   // performs high-affort minimization
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 9e50333f..22a28e22 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -54,6 +54,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
     pPars->nWinSizeMax  =  300;
     pPars->nGrowthLevel =    0;
     pPars->nBTLimit     = 5000;
+    pPars->fRrOnly      =    0;
     pPars->fResub       =    1;
     pPars->fArea        =    0;
     pPars->fMoreEffort  =    0;
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 44346997..23a59833 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -101,6 +101,10 @@ struct Mfs_Man_t_
     int                 nCares;    // the number of care minterms
     unsigned            uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)];  // the computed care-set
     // performance statistics
+    int                 nTryRemoves; // number of fanin removals
+    int                 nTryResubs;  // number of resubstitutions
+    int                 nRemoves;    // number of fanin removals
+    int                 nResubs;     // number of resubstitutions
     int                 nNodesTried;
     int                 nNodesResub;
     int                 nMintsCare;
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index caa82e68..3ed6436f 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -112,43 +112,26 @@ void Mfs_ManPrint( Mfs_Man_t * p )
 {
     if ( p->pPars->fResub )
     {
-/*
-        printf( "Reduction in nodes = %5d. (%.2f %%) ", 
-            p->nTotalNodesBeg-p->nTotalNodesEnd, 
-            100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
-        printf( "Reduction in edges = %5d. (%.2f %%) ", 
-            p->nTotalEdgesBeg-p->nTotalEdgesEnd, 
-            100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
-        printf( "\n" );
-        printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", 
+        printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
             Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
-        if ( p->pPars->fSwapEdge )
-            printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
-                p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
-        else
-            Abc_NtkMfsPrintResubStats( p );
-//        printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
-*/
-        printf( "@@@-------  Node( %4d, %4.2f%% ),  ",
-            p->nTotalNodesBeg-p->nTotalNodesEnd,
-            100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
-        printf( "Edge( %4d, %4.2f%% ),  ",
-            p->nTotalEdgesBeg-p->nTotalEdgesEnd,
-            100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
+
+        printf( "Attempts :   " );
+        printf( "Remove %6d out of %6d (%6.2f %%)   ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
+        printf( "Resub  %6d out of %6d (%6.2f %%)   ", p->nResubs,  p->nTryResubs,  100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs)  );
+        printf( "\n" );
+
+        printf( "Reduction:   " );
+        printf( "Nodes  %6d out of %6d (%6.2f %%)   ", p->nTotalNodesBeg-p->nTotalNodesEnd, p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) );
+        printf( "Edges  %6d out of %6d (%6.2f %%)   ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) );
+        printf( "\n" );
+
         if (p->pPars->fPower)
-            printf( "Power( %5.2f, %4.2f%%) ",
+            printf( "Power( %5.2f, %4.2f%%) \n",
                  p->TotalSwitchingBeg - p->TotalSwitchingEnd,
                  100.0*(p->TotalSwitchingBeg-p->TotalSwitchingEnd)/p->TotalSwitchingBeg );
-        printf( "\n" );
-//#if 0
-        printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
-            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
-//#endif
         if ( p->pPars->fSwapEdge )
             printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n",
                 p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
-        else
-            Abc_NtkMfsPrintResubStats( p );
 //        printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
     }
     else
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 0d144f9b..0ecd0f67 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -172,6 +172,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
+    p->nTryRemoves++;
 
     // clean simulation info
     Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
@@ -215,13 +216,14 @@ clk = clock();
         // update the network
         Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
 p->timeInt += clock() - clk;
+        p->nRemoves++;
         return 1;
     }
 
-    if ( fOnlyRemove )
+    if ( fOnlyRemove || p->pPars->fRrOnly )
         return 0;
-//    return 0;
 
+    p->nTryResubs++;
     if ( fVeryVerbose )
     {
         for ( i = 0; i < 9; i++ )
@@ -292,6 +294,7 @@ clk = clock();
             Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
             Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
 p->timeInt += clock() - clk;
+            p->nResubs++;
             return 1;
         }
         if ( p->nCexes >= p->pPars->nDivMax )