New MFS package.

4 files changed, 32 insertions, 57 deletions

diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 55947a14..af2cb836 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -118,7 +118,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
     // report init stats
     if ( p->pPars->fVeryVerbose )
         printf( "%5d : Lev =%3d. Leaf =%3d.  Node =%3d.  Div=%3d.  Fanin =%4d (%d/%d). MFFC = %d\n", 
-            iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), 
+            iNode, Sfm_ObjLevel(p, iNode), 0, Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), 
             Sfm_ObjFanin(p, iNode, f), f, Sfm_ObjFaninNum(p, iNode), Sfm_ObjMffcSize(p, Sfm_ObjFanin(p, iNode, f)) );
     // clean simulation info
     p->nCexes = 0;
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 8ba875c1..60648b44 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -77,10 +77,7 @@ struct Sfm_Ntk_t_
     int               nTravIds2;   // traversal IDs
     // window
     int               iPivotNode;  // window pivot
-    Vec_Int_t *       vLeaves;     // leaves 
-    Vec_Int_t *       vLeaves2;    // leaves 
     Vec_Int_t *       vNodes;      // internal
-    Vec_Int_t *       vNodes2;     // internal
     Vec_Int_t *       vDivs;       // divisors
     Vec_Int_t *       vRoots;      // roots
     Vec_Int_t *       vTfo;        // TFO (excluding iNode)
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 86c8390d..e66e6e8e 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -163,10 +163,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
 }
 void Sfm_NtkPrepare( Sfm_Ntk_t * p )
 {
-    p->vLeaves   = Vec_IntAlloc( 1000 );
-    p->vLeaves2  = Vec_IntAlloc( 1000 );
     p->vNodes    = Vec_IntAlloc( 1000 );
-    p->vNodes2   = Vec_IntAlloc( 1000 );
     p->vDivs     = Vec_IntAlloc( 100 );
     p->vRoots    = Vec_IntAlloc( 1000 );
     p->vTfo      = Vec_IntAlloc( 1000 );
@@ -198,10 +195,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
     Vec_WecFree( p->vCnfs );
     Vec_IntFree( p->vCover );
     // other data
-    Vec_IntFreeP( &p->vLeaves );
-    Vec_IntFreeP( &p->vLeaves2 );
     Vec_IntFreeP( &p->vNodes );
-    Vec_IntFreeP( &p->vNodes2 );
     Vec_IntFreeP( &p->vDivs  );
     Vec_IntFreeP( &p->vRoots );
     Vec_IntFreeP( &p->vTfo   );
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 29b9d8e1..db6bd0ea 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -266,41 +266,34 @@ static inline int Sfm_ObjIsUseful( Sfm_Ntk_t * p, int iNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
+int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes )
 {
     int i, iFanin;
     if ( Sfm_ObjIsTravIdCurrent( p, iNode ) )
         return 0;
     Sfm_ObjSetTravIdCurrent( p, iNode );
-    if ( Sfm_ObjIsPi( p, iNode ) )
-    {
-        Vec_IntPush( vLeaves, iNode );
-        return 0;
-    }
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
-        if ( Sfm_NtkCollectTfi_rec( p, iFanin, vLeaves, vNodes ) )
+        if ( Sfm_NtkCollectTfi_rec( p, iFanin, vNodes ) )
             return 1;
     Vec_IntPush( vNodes, iNode );
     return p->pPars->nWinSizeMax && (Vec_IntSize(vNodes) > p->pPars->nWinSizeMax);
 }
 int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
 {
-    int i, k, iTemp, nDivStart;
+    int i, k, iTemp;
     abctime clkDiv, clkWin = Abc_Clock();
 
     assert( Sfm_ObjIsNode( p, iNode ) );
     p->iPivotNode = iNode;
-    Vec_IntClear( p->vLeaves ); // leaves 
-    Vec_IntClear( p->vLeaves2 );// leaves 
     Vec_IntClear( p->vNodes );  // internal
-    Vec_IntClear( p->vNodes2 ); // internal
     Vec_IntClear( p->vDivs );   // divisors
     Vec_IntClear( p->vRoots );  // roots
     Vec_IntClear( p->vTfo );    // roots
+    Vec_IntClear( p->vOrder );  // variable order
 
     // collect transitive fanin
     Sfm_NtkIncrementTravId( p );
-    if ( Sfm_NtkCollectTfi_rec( p, iNode, p->vLeaves, p->vNodes ) )
+    if ( Sfm_NtkCollectTfi_rec( p, iNode, p->vNodes ) )
     {
         p->nMaxDivs++;
         p->timeWin += Abc_Clock() - clkWin;
@@ -310,13 +303,9 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     // create divisors
     clkDiv = Abc_Clock();
     Vec_IntClear( p->vDivs );
-    Vec_IntForEachEntry( p->vLeaves, iTemp, i )
-        Vec_IntPush( p->vDivs, iTemp );
-    Vec_IntForEachEntry( p->vNodes, iTemp, i )
-        Vec_IntPush( p->vDivs, iTemp );
+    Vec_IntAppend( p->vDivs, p->vNodes );
     Vec_IntPop( p->vDivs );
     // add non-topological divisors
-    nDivStart = Vec_IntSize(p->vDivs);
     if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
     {
         Sfm_NtkIncrementTravId2( p );
@@ -352,7 +341,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     clkDiv = Abc_Clock() - clkDiv;
     p->timeDiv += clkDiv;
     p->nTotalDivs += Vec_IntSize(p->vDivs);
-
+ 
     // collect TFO and window roots
     if ( p->pPars->nTfoLevMax > 0 && !Sfm_NtkCheckRoot(p, iNode, Sfm_ObjLevel(p, iNode) + p->pPars->nTfoLevMax) )
     {
@@ -364,39 +353,34 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
         // compute new leaves and nodes
         Sfm_NtkIncrementTravId( p );
         Vec_IntForEachEntry( p->vRoots, iTemp, i )
-            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vLeaves2, p->vNodes2 ) )
+            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
+            {
+                Vec_IntClear( p->vRoots );
+                Vec_IntClear( p->vTfo );
+                Vec_IntClear( p->vOrder );
                 break;
-        if ( i == Vec_IntSize(p->vRoots) )
-        {
-//        printf( "%d -> %d   %d -> %d\n", Vec_IntSize(p->vLeaves), Vec_IntSize(p->vLeaves2), Vec_IntSize(p->vNodes), Vec_IntSize(p->vNodes2) );
-            // swap leaves and nodes
-            ABC_SWAP( Vec_Int_t *, p->vLeaves, p->vLeaves2 );
-            ABC_SWAP( Vec_Int_t *, p->vNodes,  p->vNodes2 );
-        }
-        else
-        {
-            Vec_IntClear( p->vRoots );
-            Vec_IntClear( p->vTfo );
-        }
-//        printf( "Roots = %d.  TFO = %d.\n", Vec_IntSize(p->vRoots), Vec_IntSize(p->vTfo) );
+            }
+        if ( Vec_IntSize(p->vRoots) > 0 )
+        Vec_IntForEachEntry( p->vDivs, iTemp, i )
+            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
+            {
+                Vec_IntClear( p->vRoots );
+                Vec_IntClear( p->vTfo );
+                Vec_IntClear( p->vOrder );
+                break;
+            }
     }
 
-    // create ordering of the nodes, leaves and divisors that are not among nodes/leaves
-    Vec_IntClear( p->vOrder );
-    Sfm_NtkIncrementTravId2( p );
-    Vec_IntForEachEntryReverse( p->vNodes, iTemp, i )
-    {
-        Sfm_ObjSetTravIdCurrent2( p, iTemp );
-        Vec_IntPush( p->vOrder, iTemp );
-    }
-    Vec_IntForEachEntry( p->vLeaves, iTemp, i )
+    if ( Vec_IntSize(p->vOrder) == 0 )
     {
-        Sfm_ObjSetTravIdCurrent2( p, iTemp );
-        Vec_IntPush( p->vOrder, iTemp );
+        int Temp = p->pPars->nWinSizeMax;
+        p->pPars->nWinSizeMax = 0;
+        Sfm_NtkIncrementTravId( p );
+        Sfm_NtkCollectTfi_rec( p, iNode, p->vOrder );
+        Vec_IntForEachEntry( p->vDivs, iTemp, i )
+            Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder );
+        p->pPars->nWinSizeMax = Temp;
     }
-    Vec_IntForEachEntry( p->vDivs, iTemp, i )
-        if ( !Sfm_ObjIsTravIdCurrent2(p, iTemp) )
-            Vec_IntPush( p->vOrder, iTemp );
 
     // statistics
     p->timeWin += Abc_Clock() - clkWin - clkDiv;
@@ -405,7 +389,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
 
     // print stats about the window
     printf( "%6d : ", iNode );
-    printf( "Leaves = %5d. ", Vec_IntSize(p->vLeaves) );
+    printf( "Leaves = %5d. ", 0 );
     printf( "Nodes = %5d. ",  Vec_IntSize(p->vNodes) );
     printf( "Roots = %5d. ",  Vec_IntSize(p->vRoots) );
     printf( "Divs = %5d. ",   Vec_IntSize(p->vDivs) );