1 files changed, 102 insertions, 14 deletions

diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index fe0d84c3..332a6ad9 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -6,7 +6,7 @@
 
   PackageName [The good old minimization with complete don't-cares.]
 
-  Synopsis    []
+  Synopsis    [Core procedures of this package.]
 
   Author      [Alan Mishchenko]
   
@@ -39,9 +39,64 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    int clk;
+    p->nNodesTried++;
+    // prepare data structure for this node
+    Mfs_ManClean( p ); 
+    // compute window roots, window support, and window nodes
+clk = clock();
+    p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
+    p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+    p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+p->timeWin += clock() - clk;
+    if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+        return 1;
+    // compute the divisors of the window
+clk = clock();
+    p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
+p->timeDiv += clock() - clk;
+    // construct AIG for the window
+clk = clock();
+    p->pAigWin = Abc_NtkConstructAig( p, pNode );
+p->timeAig += clock() - clk;
+    // translate it into CNF
+clk = clock();
+    p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
+p->timeCnf += clock() - clk;
+    // create the SAT problem
+clk = clock();
+    p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 );
+    if ( p->pSat == NULL )
+    {
+        p->nNodesBad++;
+        return 1;
+    }
+    // solve the SAT problem
+    if ( p->pPars->fArea )
+        Abc_NtkMfsResubArea( p, pNode );
+    else
+        Abc_NtkMfsResubEdge( p, pNode );
+p->timeSat += clock() - clk;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     int clk;
+    p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
     // compute window roots, window support, and window nodes
@@ -80,9 +135,14 @@ p->timeSat += clock() - clk;
 ***********************************************************************/
 int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 {
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
+
+    ProgressBar * pProgress;
     Mfs_Man_t * p;
     Abc_Obj_t * pObj;
-    int i, Counter;
+    int i, clk = clock();
+    int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
+    int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
     assert( Abc_NtkIsLogic(pNtk) );
     if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
@@ -99,30 +159,57 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
         return 0;
     }
     assert( Abc_NtkHasAig(pNtk) );
-    if ( pNtk->pManExdc != NULL )
-        printf( "Performing don't-care computation with don't-cares.\n" );
 
     // start the manager
-    p = Mfs_ManAlloc();
-    p->pPars = pPars;
+    p = Mfs_ManAlloc( pPars );
     p->pNtk  = pNtk;
-    p->pCare = pNtk->pManExdc;
+    if ( pNtk->pExcare )
+    {
+        Abc_Ntk_t * pTemp;
+        pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
+        p->pCare = Abc_NtkToDar( pTemp, 0 );
+        Abc_NtkDelete( pTemp );
+    }
+    if ( pPars->fVerbose )
+    {
+        if ( p->pCare != NULL )
+            printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
+        else
+            printf( "Performing optimization without constraints.\n" );
+    }
+    if ( !pPars->fResub )
+        printf( "Currently don't-cares are not used but the stats are printed.\n" );
 
     // label the register outputs
     if ( p->pCare )
     {
-        Counter = 1;
         Abc_NtkForEachCi( pNtk, pObj, i )
-            if ( Abc_ObjFaninNum(pObj) == 0 )
-                pObj->pData = NULL;
-            else
-                pObj->pData = (void *)Counter++;
-        assert( Counter == Abc_NtkLatchNum(pNtk) + 1 );
+            pObj->pData = (void *)i;
     }
+ 
+    // compute levels
+    Abc_NtkLevel( pNtk );
+    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
 
     // compute don't-cares for each node
+    p->nTotalNodesBeg = nTotalNodesBeg;
+    p->nTotalEdgesBeg = nTotalEdgesBeg;
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pObj, i )
-        Abc_NtkMfsNode( p, pObj );
+    {
+        if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
+            continue;
+        if ( !p->pPars->fVeryVerbose )
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( pPars->fResub )
+            Abc_NtkMfsResub( p, pObj );
+        else
+            Abc_NtkMfsNode( p, pObj );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Abc_NtkStopReverseLevels( pNtk );
+    p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
+    p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
 
     // undo labesl
     if ( p->pCare )
@@ -132,6 +219,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     }
 
     // free the manager
+    p->timeTotal = clock() - clk;
     Mfs_ManStop( p );
     return 1;
 }