Version abc80327

4 files changed, 70 insertions, 26 deletions

diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 59ee7488..2a2c9d43 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -101,6 +101,7 @@ p->timeSat += clock() - clk;
 int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     Hop_Obj_t * pObj;
+    int RetValue;
     extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
 
     int nGain, clk;
@@ -129,8 +130,15 @@ clk = clock();
     if ( p->pSat == NULL )
         return 0;
     // solve the SAT problem
-    Abc_NtkMfsSolveSat( p, pNode );
+    RetValue = Abc_NtkMfsSolveSat( p, pNode );
+    p->nTotConfLevel += p->pSat->stats.conflicts;
 p->timeSat += clock() - clk;
+    if ( RetValue == 0 )
+    {
+        p->nTimeOutsLevel++;
+        p->nTimeOuts++;
+        return 0;
+    }
     // minimize the local function of the node using bi-decomposition
     assert( p->nFanins == Abc_ObjFaninNum(pNode) );
     pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare );
@@ -139,6 +147,7 @@ p->timeSat += clock() - clk;
     {
         p->nNodesDec++;
         p->nNodesGained += nGain;
+        p->nNodesGainedLevel += nGain;
         pNode->pData = pObj;    
     }
     return 1;
@@ -163,7 +172,9 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     ProgressBar * pProgress;
     Mfs_Man_t * p;
     Abc_Obj_t * pObj;
-    int i, nFaninMax, clk = clock();
+    Vec_Vec_t * vLevels;
+    Vec_Ptr_t * vNodes;
+    int i, k, nNodes, nFaninMax, clk = clock(), clk2;
     int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
     int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
@@ -223,24 +234,44 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
 
     // compute don't-cares for each node
+    nNodes = 0;
     p->nTotalNodesBeg = nTotalNodesBeg;
     p->nTotalEdgesBeg = nTotalEdgesBeg;
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
-    Abc_NtkForEachNode( pNtk, pObj, i )
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    vLevels = Abc_NtkLevelize( pNtk );
+    Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
     {
-        if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
-            continue;
-        if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
-            continue;
         if ( !p->pPars->fVeryVerbose )
-            Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( pPars->fResub )
-            Abc_NtkMfsResub( p, pObj );
-        else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
-            Abc_NtkMfsNode( p, pObj );
+            Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
+        p->nNodesGainedLevel = 0;
+        p->nTotConfLevel = 0;
+        p->nTimeOutsLevel = 0;
+        clk2 = clock();
+        Vec_PtrForEachEntry( vNodes, pObj, i )
+        {
+            if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
+                break;
+            if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
+                continue;
+            if ( pPars->fResub )
+                Abc_NtkMfsResub( p, pObj );
+            else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
+                Abc_NtkMfsNode( p, pObj );
+        }
+        nNodes += Vec_PtrSize(vNodes);
+        if ( pPars->fVerbose )
+        {
+        printf( "Lev = %2d. Node = %4d. Ave gain = %6.2f. Ave conf = %6.2f. Timeouts = %6.2f %%  ", 
+            k, Vec_PtrSize(vNodes),
+            1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
+            1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
+            100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
+        PRT( "Time", clock() - clk2 );
+        }
     }
     Extra_ProgressBarStop( pProgress );
     Abc_NtkStopReverseLevels( pNtk );
+    Vec_VecFree( vLevels );
 
     // perform the sweeping
     if ( !pPars->fResub )
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index f4da45ef..37521189 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -70,6 +70,7 @@ struct Mfs_Man_t_
     Bdc_Man_t *         pManDec;
     int                 nNodesDec;
     int                 nNodesGained;
+    int                 nNodesGainedLevel;
     // solving data
     Aig_Man_t *         pAigWin;   // window AIG with constraints
     Cnf_Dat_t *         pCnf;      // the CNF for the window
@@ -78,6 +79,8 @@ struct Mfs_Man_t_
     Vec_Int_t *         vMem;      // memory for intermediate SOPs
     Vec_Vec_t *         vLevels;   // levelized structure for updating
     Vec_Ptr_t *         vFanins;   // the new set of fanins
+    int                 nTotConfLim; // total conflict limit
+    int                 nTotConfLevel; // total conflicts on this level
     // the result of solving
     int                 nFanins;   // the number of fanins
     int                 nWords;    // the number of words
@@ -91,6 +94,7 @@ struct Mfs_Man_t_
     int                 nNodesBad;
     int                 nTotalDivs;
     int                 nTimeOuts;
+    int                 nTimeOutsLevel;
     int                 nDcMints;
     double              dTotalRatios;
     // node/edge stats
@@ -136,7 +140,7 @@ extern int              Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode
 extern int              Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
 extern int              Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsSat.c ==========================================================*/
-extern void             Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int              Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsStrash.c ==========================================================*/
 extern Aig_Man_t *      Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
 extern double           Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index f1b3f44c..d0642368 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -126,13 +126,13 @@ void Mfs_ManPrint( Mfs_Man_t * p )
     }
     else
     {
-        printf( "Nodes = %d.  DC mints in local space = %d. Total mints = %d. Ratio = %5.2f.\n", 
-            p->nNodesTried, p->nMintsTotal-p->nMintsCare, p->nMintsTotal, 
+        printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", 
+            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, 
             1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
 //        printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", 
 //            1.0-(p->dTotalRatios/p->nNodesTried) );
-        printf( "Nodes resyn = %d. Ratio = %5.2f.  Total AIG node gain = %d.\n", 
-            p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained );
+        printf( "Nodes resyn = %d. Ratio = %5.2f.  Total AIG node gain = %d. Timeouts = %d.\n", 
+            p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts );
     }
 /*
     PRTP( "Win", p->timeWin            ,  p->timeTotal );
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index 2529e207..5023bf62 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -42,9 +42,14 @@
 int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
 {
     int Lits[MFS_FANIN_MAX];
-    int RetValue, iVar, b, Mint;
-    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
-    assert( RetValue == l_False || RetValue == l_True );
+    int RetValue, nBTLimit, iVar, b, Mint;
+    if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts )
+        return -1;
+    nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0;
+    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False );
+    if ( RetValue == l_Undef )
+        return -1;
     if ( RetValue == l_False )
         return 0;
     p->nCares++;
@@ -77,12 +82,12 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
   SideEffects []
 
   SeeAlso     []
-
+ 
 ***********************************************************************/
-void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
+int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     Aig_Obj_t * pObjPo;
-    int i;
+    int RetValue, i;
     // collect projection variables
     Vec_IntClear( p->vProjVars );
     Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
@@ -98,7 +103,10 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
     // iterate through the SAT assignments
     p->nCares = 0;
-    while ( Abc_NtkMfsSolveSat_iter(p) );
+    p->nTotConfLim = p->pPars->nBTLimit;
+    while ( (RetValue = Abc_NtkMfsSolveSat_iter(p)) == 1 );
+    if ( RetValue == -1 )
+        return 0;
 
     // write statistics
     p->nMintsCare  += p->nCares;
@@ -113,7 +121,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
     // map the care 
     if ( p->nFanins > 4 )
-        return;
+        return 1;
     if ( p->nFanins == 4 )
         p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16);
     if ( p->nFanins == 3 )
@@ -122,6 +130,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
         p->uCare[0] = p->uCare[0] | (p->uCare[0] <<  4) | (p->uCare[0] <<  8) | (p->uCare[0] << 12) |
               (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28);
     assert( p->nFanins != 1 );
+    return 1;
 }
 
 ////////////////////////////////////////////////////////////////////////