New MFS package.

3 files changed, 28 insertions, 10 deletions

diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 9323aa47..18960183 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -75,7 +75,6 @@ extern Vec_Int_t *  Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
 extern word *       Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
 extern int          Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
 extern int          Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i );
-extern Vec_Int_t *  Sfm_NodeReadCover( Sfm_Ntk_t * p );
 /*=== sfmSat.c ==========================================================*/
 
 
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 79b7bb6a..2042eaec 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -57,7 +57,7 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t *
             assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
         // POs have one fanout
         if ( i + nPos >= Vec_WecSize(vFanins) )
-            assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
+            assert( Vec_StrEntry(vFixed, i) == (char)0 );
     }
 }
 
@@ -248,7 +248,7 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
 void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
-    if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) )
+    if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) || Sfm_ObjIsFixed(p, iNode) )
         return;
     assert( Sfm_ObjIsNode(p, iNode) );
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
@@ -258,6 +258,7 @@ void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
             Sfm_NtkDeleteObj_rec( p, iFanin );
     }
     Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
+    Vec_WrdWriteEntry( p->vTruths, iNode, (word)0 );
 }
 void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
 {
@@ -327,10 +328,6 @@ int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
 {
     return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
 }
-Vec_Int_t * Sfm_NodeReadCover( Sfm_Ntk_t * p )
-{
-    return p->vCover;
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 8ddd7865..3c30c480 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -190,9 +190,9 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
     {
         // skip some of the fanouts if the number is large
         if ( p->pPars->nFanoutMax && i > p->pPars->nFanoutMax )
-            break;
+            return;
         // skip TFI nodes, PO nodes, or nodes with high logic level
-        if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || Sfm_ObjIsFixed(p, iFanout) ||
+        if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
             (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
             continue;
         // handle single-input nodes
@@ -213,6 +213,28 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
 
 /**Function*************************************************************
 
+  Synopsis    [Fixed object is useful when it has a non-fixed fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sfm_ObjIsUseful( Sfm_Ntk_t * p, int iNode )
+{
+    int i, iFanout;
+    if ( !Sfm_ObjIsFixed(p, iNode) )
+        return 1;
+    Sfm_ObjForEachFanout( p, iNode, iFanout, i )
+        if ( !Sfm_ObjIsFixed(p, iFanout) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes structural window.]
 
   Description []
@@ -309,7 +331,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     // compact divisors
     k = 0;
     Vec_IntForEachEntry( p->vDivs, iTemp, i )
-        if ( !Sfm_ObjIsTravIdCurrent2( p, iTemp ) )
+        if ( !Sfm_ObjIsTravIdCurrent2(p, iTemp) && Sfm_ObjIsUseful(p, iTemp) )
             Vec_IntWriteEntry( p->vDivs, k++, iTemp );
     Vec_IntShrink( p->vDivs, k );
     assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );