New MFS package.

5 files changed, 17 insertions, 8 deletions

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 ) )
             {