Version abc80301

5 files changed, 39 insertions, 12 deletions

diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index cb2da431..d3f7277d 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -47,6 +47,7 @@ struct Mfs_Par_t_
     int           nDivMax;       // the maximum number of divisors
     int           nWinSizeMax;   // the maximum size of the window
     int           nGrowthLevel;  // the maximum allowed growth in level
+    int           nBTLimit;      // the maximum number of conflicts in one SAT run
     int           fResub;        // performs resubstitution
     int           fArea;         // performs optimization for area
     int           fMoreEffort;   // performs high-affort minimization
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 3c0349bb..f98f6239 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -84,6 +84,7 @@ struct Mfs_Man_t_
     int                 nMintsTotal;
     int                 nNodesBad;
     int                 nTotalDivs;
+    int                 nTimeOuts;
     // node/edge stats
     int                 nTotalNodesBeg;
     int                 nTotalNodesEnd;
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 65acd4eb..24617cd9 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -226,10 +226,10 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
 
     // solve the problem
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
     if ( status != l_False )
     {
-        printf( "Abc_NtkMfsInterplate(): Internal error. The problem is not UNSAT.\n" );
+        p->nTimeOuts++;
         return NULL;
     }
     // get the learned clauses
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 421f62af..99a60ef6 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -115,8 +115,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
             p->nTotalEdgesBeg-p->nTotalEdgesEnd, 
             100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
         printf( "\n" );
-        printf( "Nodes = %d. Tried = %d. Resub = %d. Divs = %d. SAT calls = %d.\n", 
-            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls );
+        printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", 
+            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
         if ( p->pPars->fSwapEdge )
             printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
                 p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 4171c111..8908da2f 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -100,10 +100,15 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
     unsigned * pData;
     int RetValue, iVar, i;
     p->nSatCalls++;
-    RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
-    assert( RetValue == l_False || RetValue == l_True );
+    RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+//    assert( RetValue == l_False || RetValue == l_True );
     if ( RetValue == l_False )
         return 1;
+    if ( RetValue != l_True )
+    {
+        p->nTimeOuts++;
+        return -1;
+    }
     p->nSatCexes++;
     // store the counter-example
     Vec_IntForEachEntry( p->vProjVars, iVar, i )
@@ -135,7 +140,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
     int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
     unsigned * pData;
     int pCands[MFS_FANIN_MAX];
-    int iVar, i, nCands, nWords, w, clk;
+    int RetValue, iVar, i, nCands, nWords, w, clk;
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
@@ -163,7 +168,10 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
         iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
         pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
     }
-    if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
+    RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
+    if ( RetValue == -1 )
+        return 0;
+    if ( RetValue == 1 )
     {
         if ( fVeryVerbose )
         printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
@@ -173,6 +181,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
 clk = clock();
         // derive the function
         pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
+        if ( pFunc == NULL )
+            return 0;
         // update the network
         Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
 p->timeInt += clock() - clk;
@@ -225,7 +235,10 @@ p->timeInt += clock() - clk;
             return 0;
 
         pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
-        if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
+        RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
+        if ( RetValue == -1 )
+            return 0;
+        if ( RetValue == 1 )
         {
             if ( fVeryVerbose )
             printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
@@ -235,6 +248,8 @@ p->timeInt += clock() - clk;
 clk = clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
+            if ( pFunc == NULL )
+                return 0;
             // update the network
             Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
             Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
@@ -263,7 +278,7 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
     int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
     unsigned * pData, * pData2;
     int pCands[MFS_FANIN_MAX];
-    int iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
+    int RetValue, iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
@@ -292,7 +307,10 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
         iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
         pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
     }
-    if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
+    RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
+    if ( RetValue == -1 )
+        return 0;
+    if ( RetValue == 1 )
     {
         if ( fVeryVerbose )
         printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
@@ -300,6 +318,8 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
 clk = clock();
         // derive the function
         pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
+        if ( pFunc == NULL )
+            return 0;
         // update the network
         Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
 p->timeInt += clock() - clk;
@@ -360,7 +380,10 @@ p->timeInt += clock() - clk;
 
         pCands[nCands]   = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
         pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
-        if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ) )
+        RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
+        if ( RetValue == -1 )
+            return 0;
+        if ( RetValue == 1 )
         {
             if ( fVeryVerbose )
             printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
@@ -368,6 +391,8 @@ p->timeInt += clock() - clk;
 clk = clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
+            if ( pFunc == NULL )
+                return 0;
             // update the network
             Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) );
             Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );