New MFS package.

6 files changed, 21 insertions, 20 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ac4a8efa..74c697c9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4318,7 +4318,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Abc_NtkMfsParsDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCdlraestpgvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCdraestpgvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4391,9 +4391,6 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fRrOnly ^= 1;
             break;
-        case 'l':
-            pPars->nGrowthLevel = 10000;
-            break;
         case 'r':
             pPars->fResub ^= 1;
             break;
@@ -4448,7 +4445,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs [-WFDMLC <num>] [-dlraestpgvh]\n" );
+    Abc_Print( -2, "usage: mfs [-WFDMLC <num>] [-draestpgvh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of logic networks\n" );
     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 );
@@ -4457,7 +4454,6 @@ usage:
     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" );
-    Abc_Print( -2, "\t-l       : allow logic level to increase [default = %s]\n", (pPars->nGrowthLevel > 0)? "yes": "no" );
     Abc_Print( -2, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
     Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
     Abc_Print( -2, "\t-e       : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
@@ -4491,7 +4487,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Sfm_ParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZdlaevwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZdaevwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4575,9 +4571,6 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fRrOnly ^= 1;
             break;
-        case 'l':
-            pPars->fFixLevel ^= 1;
-            break;
         case 'a':
             pPars->fArea ^= 1;
             break;
@@ -4615,7 +4608,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs2 [-WFDMLCZ <num>] [-dlaevwh]\n" );
+    Abc_Print( -2, "usage: mfs2 [-WFDMLCZ <num>] [-daevwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of logic networks\n" );
     Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
@@ -4625,7 +4618,6 @@ usage:
     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-Z <num> : treat the first <num> logic nodes as fixed (0 = none) [default = %d]\n", pPars->nFirstFixed );
     Abc_Print( -2, "\t-d       : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" );
-    Abc_Print( -2, "\t-l       : allow logic level to increase [default = %s]\n", !pPars->fFixLevel? "yes": "no" );
     Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
     Abc_Print( -2, "\t-e       : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index ef04da02..078026c5 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -49,7 +49,6 @@ struct Sfm_Par_t_
     int             nGrowthLevel;  // the maximum allowed growth in level
     int             nBTLimit;      // the maximum number of conflicts in one SAT run
     int             nFirstFixed;   // the number of first nodes to be treated as fixed
-    int             fFixLevel;     // does not allow level to increase
     int             fRrOnly;       // perform redundance removal
     int             fArea;         // performs optimization for area
     int             fMoreEffort;   // performs high-affort minimization
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 9efb70e2..ba690b18 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -51,7 +51,6 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
     pPars->nWinSizeMax  =  300;  // the maximum window size
     pPars->nGrowthLevel =    0;  // the maximum allowed growth in level
     pPars->nBTLimit     = 5000;  // the maximum number of conflicts in one SAT run
-    pPars->fFixLevel    =    1;  // does not allow level to increase
     pPars->fRrOnly      =    0;  // perform redundancy removal
     pPars->fArea        =    0;  // performs optimization for area
     pPars->fMoreEffort  =    0;  // performs high-affort minimization
@@ -213,7 +212,8 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
     // prepare SAT solver
     if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) )
         return 0;
-    Sfm_NtkWindowToSolver( p );
+    if ( !Sfm_NtkWindowToSolver( p ) )
+        return 0;
     // try replacing area critical fanins
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
         if ( Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1 )
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index c9ccbc89..b193fd9e 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -182,7 +182,7 @@ extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPo
 extern void         Sfm_NtkPrepare( Sfm_Ntk_t * p );
 extern void         Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth );
 /*=== sfmSat.c ==========================================================*/
-extern void         Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
+extern int          Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
 extern word         Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
 /*=== sfmWin.c ==========================================================*/
 extern int          Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj );
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 7dc3e565..7e1635dd 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -51,7 +51,7 @@ static word s_Truths6[6] = {
   SeeAlso     []
 
 ***********************************************************************/
-void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
+int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
 {
     // p->vOrder contains all variables in the window in a good order
     // p->vDivs is a subset of nodes in p->vOrder used as divisor candidates
@@ -137,12 +137,14 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
         }
         // make OR clause for the last nRoots variables
         RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
-        assert( RetValue );
+        if ( RetValue == 0 )
+            return 0;
     }
     // finalize
     RetValue = sat_solver_simplify( p->pSat );
     assert( RetValue );
     p->timeCnf += Abc_Clock() - clk;
+    return 1;
 } 
 
 /**Function*************************************************************
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index f12474c9..fa0b484b 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -214,8 +214,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
         if ( p->pPars->nFanoutMax && i > p->pPars->nFanoutMax )
             return;
         // skip TFI nodes, PO nodes, or nodes with high logic level
-        if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
-            (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) > nLevelMax) )
+        if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || Sfm_ObjLevel(p, iFanout) > nLevelMax )
             continue;
         // handle single-input nodes
         if ( Sfm_ObjFaninNum(p, iFanout) == 1 )
@@ -362,6 +361,15 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
                 break;
             }
         if ( Vec_IntSize(p->vRoots) > 0 )
+        Vec_IntForEachEntry( p->vTfo, iTemp, i )
+            if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
+            {
+                Vec_IntClear( p->vRoots );
+                Vec_IntClear( p->vTfo );
+                Vec_IntClear( p->vOrder );
+                break;
+            }
+        if ( Vec_IntSize(p->vRoots) > 0 )
         Vec_IntForEachEntry( p->vDivs, iTemp, i )
             if ( Sfm_NtkCollectTfi_rec( p, iTemp, p->vOrder ) )
             {