New MFS package.

9 files changed, 67 insertions, 38 deletions

diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index 5259ea03..9c0513de 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -53,7 +53,11 @@ Vec_Ptr_t * Abc_NtkAssignIDs( Abc_Ntk_t * pNtk )
     Abc_NtkForEachPi( pNtk, pObj, i )
         pObj->iTemp = i;
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
         pObj->iTemp = Abc_NtkPiNum(pNtk) + i;
+//printf( "%d->%d ", pObj->Id, pObj->iTemp );
+    }
+//printf( "\n" );
     Abc_NtkForEachPo( pNtk, pObj, i )
         pObj->iTemp = Abc_NtkPiNum(pNtk) + Vec_PtrSize(vNodes) + i;
     return vNodes;
@@ -119,6 +123,7 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
     Vec_Int_t * vMap, * vArray;
     Abc_Obj_t * pNode;
     int i, k, Fanin;
+    word * pTruth;
     // map new IDs into old nodes
     vMap = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachPi( pNtk, pNode, i )
@@ -131,18 +136,27 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
         Abc_ObjRemoveFanins( pNode );
     // create new fanins
     Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( pNode->iTemp > 0 && !Sfm_NodeReadFixed(p, pNode->iTemp) )
+    {
+        if ( pNode->iTemp == 0 || Sfm_NodeReadFixed(p, pNode->iTemp) )
+            continue;
+        if ( !Sfm_NodeReadUsed(p, pNode->iTemp) )
         {
-            vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
-            if ( Vec_IntSize(vArray) == 0 )
-            {
-                Abc_NtkDeleteObj( pNode );
-                continue;
-            }
-            Vec_IntForEachEntry( vArray, Fanin, k )
-                Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
-            pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)Sfm_NodeReadTruth(p, pNode->iTemp) );
+            Abc_NtkDeleteObj( pNode );
+            continue;
         }
+        // update fanins
+        vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
+        Vec_IntForEachEntry( vArray, Fanin, k )
+            Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
+        // update function
+        pTruth = Sfm_NodeReadTruth( p, pNode->iTemp );
+        if ( pTruth[0] == 0 )
+            pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 0\n" );
+        else if ( ~pTruth[0] == 0 )
+            pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" );
+        else
+            pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth );
+    }
     Vec_IntFree( vMap );
 }
 
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index fe7a1852..9e50333f 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -101,7 +101,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
         return 1;
     // compute the divisors of the window
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
-    p->nTotalDivs += Vec_PtrSize(p->vDivs);
+    p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
     // construct AIG for the window
     p->pAigWin = Abc_NtkConstructAig( p, pNode );
     // translate it into CNF
@@ -250,7 +250,7 @@ p->timeWin += clock() - clk;
     // compute the divisors of the window
 clk = clock();
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
-    p->nTotalDivs += Vec_PtrSize(p->vDivs);
+    p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
 p->timeDiv += clock() - clk;
     // construct AIG for the window
 clk = clock();
diff --git a/src/opt/mfs/mfsCore_.c b/src/opt/mfs/mfsCore_.c
index ceee04cf..49105da6 100644
--- a/src/opt/mfs/mfsCore_.c
+++ b/src/opt/mfs/mfsCore_.c
@@ -89,7 +89,7 @@ p->timeWin += clock() - clk;
     // compute the divisors of the window
 clk = clock();
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
-    p->nTotalDivs += Vec_PtrSize(p->vDivs);
+    p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
 p->timeDiv += clock() - clk;
     // construct AIG for the window
 clk = clock();
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index b67fc8df..f6380e65 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -73,6 +73,7 @@ extern void         Sfm_NtkFree( Sfm_Ntk_t * p );
 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 );
 /*=== sfmSat.c ==========================================================*/
 
 
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index 126b6ca0..f04a6970 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -122,12 +122,12 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
     Vec_Wec_t * vCnfs;
     Vec_Str_t * vCnf, * vCnfBase;
     word uTruth;
-    int i;
+    int i, nCubes;
     vCnf = Vec_StrAlloc( 100 );
     vCnfs = Vec_WecStart( p->nObjs );
     Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
     {
-        Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
+        nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf );
         vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
         Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
         memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 35c092fa..acdee9c1 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -48,8 +48,8 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
     pPars->nTfoLevMax   =    2;  // the maximum fanout levels
     pPars->nFanoutMax   =   10;  // the maximum number of fanouts
     pPars->nDepthMax    =    0;  // the maximum depth to try  
-    pPars->nDivNumMax   =  200;  // the maximum number of divisors
-    pPars->nWinSizeMax  =  500;  // the maximum window size
+    pPars->nDivNumMax   =  300;  // the maximum number of divisors
+    pPars->nWinSizeMax  =  300;  // the maximum window size
     pPars->nBTLimit     =    0;  // the maximum number of conflicts in one SAT run
     pPars->fFixLevel    =    1;  // does not allow level to increase
     pPars->fArea        =    0;  // performs optimization for area
@@ -111,14 +111,18 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
     clock_t clk;
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) );
+    if ( iNode == 211 )
+    {
+        int i = 0;
+    }
     if ( fRemoveOnly )
         p->nTryRemoves++;
     else
         p->nTryResubs++;
     // report init stats
     if ( p->pPars->fVeryVerbose )
-        printf( "Node %5d : Level = %2d. Divs = %3d.  Fanin = %d (out of %d). MFFC = %d\n", 
-            iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode), 
+        printf( "%5d : Lev =%3d. Leaf =%3d.  Node =%3d.  Div=%3d.  Fanin = %d/%d. MFFC = %d\n", 
+            iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode), 
             Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 );
     // clean simulation info
     p->nCexes = 0;
@@ -187,9 +191,9 @@ finish:
     if ( p->pPars->fVeryVerbose )
     {
         if ( iVar == -1 )
-            printf( "Node %d: Fanin %d can be removed.  ", iNode, f );
+            printf( "Node %d: Fanin %d (%d) can be removed.  ", iNode, f, Sfm_ObjFanin(p, iNode, f) );
         else
-            printf( "Node %d: Fanin %d can be replaced by divisor %d.   ", iNode, f, iVar );
+            printf( "Node %d: Fanin %d (%d) can be replaced by divisor %d.   ", iNode, f, Sfm_ObjFanin(p, iNode, f), iVar );
         Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" );
     }
     if ( iVar == -1 )
@@ -205,9 +209,10 @@ finish:
 int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
 {
     int i, iFanin;
-    p->nNodesTried++;
     // prepare SAT solver
-    Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose );
+    if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) )
+        return 0;
+    p->nNodesTried++;
     Sfm_NtkWindowToSolver( p );
     Sfm_NtkPrepareDivisors( p, iNode );
     // try replacing area critical fanins
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index 29463de6..53ec4153 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -243,6 +243,10 @@ 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 ( iNode == 202 )
+    {
+        int s = 0;
+    }
     if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) )
         return;
     assert( Sfm_ObjIsNode(p, iNode) );
@@ -304,6 +308,10 @@ int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
 {
     return (int)Vec_StrEntry( p->vFixed, i );
 }
+int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
+{
+    return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index f5355503..4a06dde6 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -123,8 +123,14 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
     RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
     assert( RetValue );
     // finalize
-    sat_solver_compress( pSat0 );
-    sat_solver_compress( pSat1 );
+    RetValue = sat_solver_simplify( pSat0 );
+    assert( RetValue );
+    RetValue = sat_solver_simplify( pSat1 );
+    if ( RetValue == 0 )
+    {
+        Sat_SolverWriteDimacs( pSat1, "test.cnf", NULL, NULL, 0 );
+    }
+    assert( RetValue );
     // return the result
     if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
     if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 893a4592..54cf924d 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -179,7 +179,7 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode )
+void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
 {
     int i, iFanout;
     Sfm_ObjForEachFanout( p, iNode, iFanout, i )
@@ -187,7 +187,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode )
         // skip TFI nodes, PO nodes, and nodes with high fanout or nodes with high logic level
         if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) || 
             Sfm_ObjFanoutNum(p, iFanout) >= p->pPars->nFanoutMax ||
-            (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= Sfm_ObjLevel(p, iNode)) )
+            (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
             continue;
         // handle single-input nodes
         if ( Sfm_ObjFaninNum(p, iFanout) == 1 )
@@ -235,23 +235,18 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
 {
     int i, iTemp;
     clock_t clk = clock();
-/*
-    if ( iNode == 7 )
-    {
-        int iLevel = Sfm_ObjLevel(p, iNode);
-        int s = 0;
-    }
-*/
     assert( Sfm_ObjIsNode( p, iNode ) );
     Vec_IntClear( p->vLeaves ); // leaves 
     Vec_IntClear( p->vNodes );  // internal
     Vec_IntClear( p->vDivs );   // divisors
+    Vec_IntClear( p->vRoots );  // roots
+    Vec_IntClear( p->vTfo );    // roots
     // collect transitive fanin
     Sfm_NtkIncrementTravId( p );
     Sfm_NtkCollectTfi_rec( p, iNode );
+    if ( Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) > p->pPars->nWinSizeMax )
+        return 0;
     // collect TFO (currently use only one level of TFO)
-    Vec_IntClear( p->vRoots );  // roots
-    Vec_IntClear( p->vTfo );    // roots
     if ( Sfm_NtkCheckFanouts(p, iNode) )
     {
         Sfm_ObjForEachFanout( p, iNode, iTemp, i )
@@ -271,8 +266,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     Vec_IntAppend( p->vDivs, p->vNodes );
     Sfm_NtkIncrementTravId2( p );
     Vec_IntForEachEntry( p->vDivs, iTemp, i )
-        if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
-            Sfm_NtkAddDivisors( p, iTemp );
+        if ( iTemp != iNode && Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
+            Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
     p->nTotalDivs += Vec_IntSize(p->vDivs);
     p->timeDiv += clock() - clk;
     if ( !fVerbose )