New MFS package.

4 files changed, 22 insertions, 10 deletions

diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 7e34e1c3..0d144f9b 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -220,6 +220,7 @@ p->timeInt += clock() - clk;
 
     if ( fOnlyRemove )
         return 0;
+//    return 0;
 
     if ( fVeryVerbose )
     {
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index acdee9c1..e9721ec7 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -71,6 +71,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
 ***********************************************************************/
 void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
 {
+    p->timeOther = p->timeTotal - p->timeWin - p->timeDiv - p->timeCnf - p->timeSat;
     printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
         Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
 
@@ -88,6 +89,7 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
     ABC_PRTP( "Div", p->timeDiv  ,  p->timeTotal );
     ABC_PRTP( "Cnf", p->timeCnf  ,  p->timeTotal );
     ABC_PRTP( "Sat", p->timeSat  ,  p->timeTotal );
+    ABC_PRTP( "Oth", p->timeOther,  p->timeTotal );
     ABC_PRTP( "ALL", p->timeTotal,  p->timeTotal );
 }
 
@@ -145,6 +147,8 @@ p->timeSat += clock() - clk;
         goto finish;
     if ( fRemoveOnly || Vec_IntSize(p->vDivs) == 0 )
         return 0;
+//    return 0;
+
     if ( fVeryVerbose )
     {
         for ( i = 0; i < 9; i++ )
@@ -209,10 +213,10 @@ finish:
 int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
+    p->nNodesTried++;
     // prepare SAT solver
     if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) )
         return 0;
-    p->nNodesTried++;
     Sfm_NtkWindowToSolver( p );
     Sfm_NtkPrepareDivisors( p, iNode );
     // try replacing area critical fanins
@@ -271,7 +275,8 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
             continue;
         if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
             continue;
-        Counter += Sfm_NodeResub( p, i );
+        while ( Sfm_NodeResub(p, i) )
+            Counter++;
     }
     p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
     p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins);
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 03d03111..5c41e9f0 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -116,6 +116,7 @@ struct Sfm_Ntk_t_
     clock_t           timeDiv;
     clock_t           timeCnf;
     clock_t           timeSat;
+    clock_t           timeOther;
     clock_t           timeTotal;
 };
 
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 54cf924d..887bf0f7 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -182,11 +182,12 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
 void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
 {
     int i, iFanout;
+    if ( Sfm_ObjFanoutNum(p, iNode) > p->pPars->nFanoutMax )
+        return;
     Sfm_ObjForEachFanout( p, iNode, iFanout, i )
     {
-        // skip TFI nodes, PO nodes, and nodes with high fanout or nodes with high logic level
+        // skip TFI nodes, PO nodes, or nodes with high logic level
         if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || 
-            Sfm_ObjFanoutNum(p, iFanout) >= p->pPars->nFanoutMax ||
             (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
             continue;
         // handle single-input nodes
@@ -216,20 +217,22 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
   SeeAlso     []
 
 ***********************************************************************/
-void Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode )
+int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, int nWinSizeMax )
 {
     int i, iFanin;
     if ( Sfm_ObjIsTravIdCurrent( p, iNode ) )
-        return;
+        return 0;
     Sfm_ObjSetTravIdCurrent( p, iNode );
     if ( Sfm_ObjIsPi( p, iNode ) )
     {
         Vec_IntPush( p->vLeaves, iNode );
-        return;
+        return 0;
     }
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
-        Sfm_NtkCollectTfi_rec( p, iFanin );
+        if ( Sfm_NtkCollectTfi_rec( p, iFanin, nWinSizeMax ) )
+            return 1;
     Vec_IntPush( p->vNodes, iNode );
+    return nWinSizeMax && (Vec_IntSize(p->vNodes) > nWinSizeMax);
 }
 int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
 {
@@ -243,9 +246,11 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     Vec_IntClear( p->vTfo );    // roots
     // collect transitive fanin
     Sfm_NtkIncrementTravId( p );
-    Sfm_NtkCollectTfi_rec( p, iNode );
-    if ( Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) > p->pPars->nWinSizeMax )
+    if ( Sfm_NtkCollectTfi_rec( p, iNode, p->pPars->nWinSizeMax ) )
+    {
+        p->timeWin += clock() - clk;
         return 0;
+    }
     // collect TFO (currently use only one level of TFO)
     if ( Sfm_NtkCheckFanouts(p, iNode) )
     {