New MFS package.

src/base/abci/abcMfs.c

@@ -126,10 +126,13 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
             Vec_IntPush( vArray, pFanin->iTemp );
     }
     Vec_PtrFree( vNodes );
-    // update fixed
-    assert( nFirstFixed >= 0 && nFirstFixed < Abc_NtkNodeNum(pNtk) );
     for ( i = Abc_NtkCiNum(pNtk); i < Abc_NtkCiNum(pNtk) + nFirstFixed; i++ )
         Vec_StrWriteEntry( vFixed, i, (char)1 );
+    // update fixed
+    assert( nFirstFixed >= 0 && nFirstFixed < Abc_NtkNodeNum(pNtk) );
+//    for ( i = Abc_NtkCiNum(pNtk); i + Abc_NtkCoNum(pNtk) < Abc_NtkObjNum(pNtk); i++ )
+//        if ( rand() % 10 == 0 )
+//            Vec_StrWriteEntry( vFixed, i, (char)1 );
     return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, vTruths );
 }
 
@@ -159,7 +162,8 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
             Vec_IntWriteEntry( vMap, pNode->iTemp, Abc_ObjId(pNode) );
     // remove old fanins
     Abc_NtkForEachNode( pNtk, pNode, i )
-        Abc_ObjRemoveFanins( pNode );
+        if ( !Sfm_NodeReadFixed(p, pNode->iTemp) )
+            Abc_ObjRemoveFanins( pNode );
     // create new fanins
     vCover = Vec_IntAlloc( 1 << 16 );
     Abc_NtkForEachNode( pNtk, pNode, i )

src/misc/vec/vecStr.h

@@ -636,6 +636,25 @@ static inline void Vec_StrReverseOrder( Vec_Str_t * p )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_StrSum( Vec_Str_t * p ) 
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nSize; i++ )
+        Counter += (int)p->pArray[i];
+    return Counter;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Compares two strings.]

src/opt/sfm/sfmCore.c

@@ -255,6 +255,8 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
     int i, k, Counter = 0;
     p->timeTotal = clock();
+    if ( pPars->fVerbose )
+        printf( "Performing MFS with %d fixed objected.\n", Vec_StrSum(p->vFixed) );
     p->pPars = pPars;
     Sfm_NtkPrepare( p );
 //    Sfm_ComputeInterpolantCheck( p );
@@ -270,7 +272,10 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
         if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
             continue;
         for ( k = 0; Sfm_NodeResub(p, i); k++ )
-            ;
+        {
+//            Counter++;
+//            break;
+        }
         Counter += (k > 0);
     }
     p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);

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_StrEntry(vFixed, i) == (char)0 );
+            assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
     }
 }
 
@@ -254,8 +254,7 @@ void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
     {
         int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
-        if ( Sfm_ObjFanoutNum(p, iFanin) == 0 )
-            Sfm_NtkDeleteObj_rec( p, iFanin );
+        Sfm_NtkDeleteObj_rec( p, iFanin );
     }
     Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
     Vec_WrdWriteEntry( p->vTruths, iNode, (word)0 );
@@ -281,8 +280,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
         Sfm_ObjForEachFanin( p, iNode, iFanin, f )
         {
             int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
-            if ( Sfm_ObjFanoutNum(p, iFanin) == 0 )
-                Sfm_NtkDeleteObj_rec( p, iFanin );
+            Sfm_NtkDeleteObj_rec( p, iFanin );
         }
         Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
     }