Several small changes to the MFS packages.

src/base/abci/abc.c

@@ -4361,9 +4361,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+            pPars->nWinMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nWinSizeMax < 0 )
+            if ( pPars->nWinMax < 0 )
                 goto usage;
             break;
         case 'L':
@@ -4450,7 +4450,7 @@ usage:
     Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
     Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
-    Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
+    Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinMax );
     Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-d       : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" );

src/base/abci/abcMfs.c

@@ -74,9 +74,10 @@ Vec_Ptr_t * Abc_NtkAssignIDs2( Abc_Ntk_t * pNtk )
     vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
+        pObj->iTemp = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes);
         Vec_PtrPush( vNodes, pObj );
-        pObj->iTemp = Abc_NtkCiNum(pNtk) + i;
     }
+    assert( Vec_PtrSize(vNodes) == Abc_NtkNodeNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pObj, i )
         pObj->iTemp = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + i;
     return vNodes;

src/opt/mfs/mfs.h

@@ -47,7 +47,7 @@ struct Mfs_Par_t_
     int           nFanoutsMax;   // the maximum number of fanouts
     int           nDepthMax;     // the maximum number of logic levels
     int           nDivMax;       // the maximum number of divisors
-    int           nWinSizeMax;   // the maximum size of the window
+    int           nWinMax;       // 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

src/opt/mfs/mfsCore.c

@@ -50,8 +50,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
     pPars->nWinTfoLevs  =    2;
     pPars->nFanoutsMax  =   30;
     pPars->nDepthMax    =   20;
-    pPars->nDivMax      =  250;
-    pPars->nWinSizeMax  =  300;
+    pPars->nWinMax      =  300;
     pPars->nGrowthLevel =    0;
     pPars->nBTLimit     = 5000;
     pPars->fRrOnly      =    0;
@@ -98,7 +97,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
     p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
     p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
     p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
-    if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+    if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
         return 1;
     // compute the divisors of the window
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
@@ -246,8 +245,11 @@ clk = clock();
     p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
     p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
 p->timeWin += clock() - clk;
-    if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+    if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
+    {
+        p->nMaxDivs++;
         return 1;
+    }
     // compute the divisors of the window
 clk = clock();
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );

src/opt/mfs/mfsCore_.c

@@ -48,7 +48,6 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
     pPars->nWinTfoLevs  =    2;
     pPars->nFanoutsMax  =   10;
     pPars->nDepthMax    =   20;
-    pPars->nDivMax      =  250;
     pPars->nWinSizeMax  =  300;
     pPars->nGrowthLevel =    0;
     pPars->nBTLimit     = 5000;

src/opt/mfs/mfsDiv.c

@@ -223,7 +223,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
     // nodes to be avoided as divisors are marked with current trav ID
 
     // start collecting the divisors
-    vDivs = Vec_PtrAlloc( p->pPars->nDivMax );
+    vDivs = Vec_PtrAlloc( p->pPars->nWinMax );
     Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, k )
     {
         if ( !Abc_NodeIsTravIdPrevious(pObj) )
@@ -231,13 +231,13 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
         if ( (int)pObj->Level > nLevDivMax )
             continue;
         Vec_PtrPush( vDivs, pObj );
-        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+        if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
             break;
     }
     Vec_PtrFree( vCone );
 
     // explore the fanouts of already collected divisors
-    if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax )
+    if ( Vec_PtrSize(vDivs) < p->pPars->nWinMax )
     Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, k )
     {
         // consider fanouts of this node
@@ -273,12 +273,13 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
             Vec_PtrPushUnique( p->vNodes, pFanout );
             Abc_NodeSetTravIdPrevious( pFanout );
             nDivsPlus++;
-            if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+            if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
                 break;
         }
-        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+        if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
             break;
     }
+    p->nMaxDivs += (Vec_PtrSize(vDivs) >= p->pPars->nWinMax);
 
     // sort the divisors by level in the increasing order
     Vec_PtrSort( vDivs, (int (*)(void))Abc_NodeCompareLevelsIncrease );

src/opt/mfs/mfsInt.h

@@ -114,6 +114,7 @@ struct Mfs_Man_t_
     int                 nTimeOuts;
     int                 nTimeOutsLevel;
     int                 nDcMints;
+    int                 nMaxDivs;
     double              dTotalRatios;
     // node/edge stats
     int                 nTotalNodesBeg;

src/opt/mfs/mfsMan.c

@@ -52,8 +52,8 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
     p->vProjVarsCnf = Vec_IntAlloc( 100 );
     p->vProjVarsSat = Vec_IntAlloc( 100 );
     p->vDivLits  = Vec_IntAlloc( 100 );
-    p->nDivWords = Abc_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
-    p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
+    p->nDivWords = Abc_BitWordNum(p->pPars->nWinMax + MFS_FANIN_MAX);
+    p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nWinMax + MFS_FANIN_MAX + 1, p->nDivWords );
     p->pMan      = Int_ManAlloc();
     p->vMem      = Vec_IntAlloc( 0 );
     p->vLevels   = Vec_VecStart( 32 );
@@ -112,8 +112,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
 {
     if ( p->pPars->fResub )
     {
-        printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
-            p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
+        printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n",
+            p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs );
 
         printf( "Attempts :   " );
         printf( "Remove %6d out of %6d (%6.2f %%)   ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );

src/opt/mfs/mfsResub.c

@@ -297,7 +297,7 @@ p->timeInt += clock() - clk;
             p->nResubs++;
             return 1;
         }
-        if ( p->nCexes >= p->pPars->nDivMax )
+        if ( p->nCexes >= p->pPars->nWinMax )
             break;
     }
     if ( p->pPars->fVeryVerbose )
@@ -467,7 +467,7 @@ clk = clock();
 p->timeInt += clock() - clk;
             return 1;
         }
-        if ( p->nCexes >= p->pPars->nDivMax )
+        if ( p->nCexes >= p->pPars->nWinMax )
             break;
     }
     return 0;

src/opt/sfm/sfmWin.c

@@ -275,6 +275,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     Sfm_NtkIncrementTravId( p );
     if ( Sfm_NtkCollectTfi_rec( p, iNode, p->pPars->nWinSizeMax ) )
     {
+        p->nMaxDivs++;
         p->timeWin += clock() - clk;
         return 0;
     }