Adding SAT-solver-level timeouts to the BMC engines.

5 files changed, 51 insertions, 29 deletions

diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 8e537142..1fc5a11a 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -767,7 +767,9 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
             nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
     } 
-
+    // set runtime limit
+    if ( nTimeOut )
+        sat_solver_set_runtime_limit( p->pSat, clock() + nTimeOut * CLOCKS_PER_SEC );
     for ( Iter = 0; ; Iter++ )
     {
         clk2 = clock();
@@ -841,8 +843,10 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
             printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
         else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
             printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-        else
+        else if ( nTimeOut == 0 || nTimeOut > clock() )
             printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+        else
+            printf( "Reached timeout (%d sec).\n", nTimeOut );
     }
     Saig_BmcManStop( p );
     return Status;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 570e8a26..e038d7a0 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1054,6 +1054,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
             pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
     } 
+    // set runtime limit
+    if ( p->pPars->nTimeOut )
+        sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC );
+    // perform frames
     for ( f = 0; f < pPars->nFramesMax; f++ )
     {
         pPars->iFrame = f;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index b28d3de4..d443c5e5 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1682,18 +1682,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
-
-/*
-    s_fInterrupt = 0;
-    if ( signal(SIGINT,sigfunc) == SIG_ERR ) 
-    {
-        printf("Could not setup signal handler for SIGINT!\n");
-        return RetValue;
-    }
-    printf("Waiting for SIGINT. Press Ctrl+C to exit.\n");
-//    while ( !s_fInterrupt );
-//    return RetValue;
-*/
+    int nTimeLimit = nTimeOut ? clock() + nTimeOut * CLOCKS_PER_SEC : 0;
 
     // derive the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
@@ -1715,17 +1704,23 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
         {
-//            printf( "No output was asserted in %d frames. ", iFrame );
+//            printf( "No output asserted in %d frames. ", iFrame );
             printf( "Incorrect return value.  " );
         }
         else if ( RetValue == -1 )
-            printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
+        {
+            printf( "No output asserted in %d frames. Resource limit reached ", iFrame );
+            if ( nTimeLimit < clock() )
+                printf( "(timeout %d sec). ", nTimeLimit );
+            else
+                printf( "(conf limit %d). ", nBTLimit );
+        }
         else // if ( RetValue == 0 )
         {
 //            extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 
             Abc_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+            printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
 
 //            Aig_ManCounterExampleValueTest( pMan, pCex );
         }
@@ -1741,12 +1736,12 @@ ABC_PRT( "Time", clock() - clk );
         if ( pNtk->pSeqModel )
         {
             Abc_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+            printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
             RetValue = 0;
         }
         else
         {
-            printf( "No output was asserted in %d frames. ", nFrames );
+            printf( "No output asserted in %d frames. ", nFrames );
             RetValue = 1;
         }
 */
@@ -1757,13 +1752,13 @@ ABC_PRT( "Time", clock() - clk );
         ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
-            printf( "No output was asserted in %d frames. ", iFrame );
+            printf( "No output asserted in %d frames. ", iFrame );
         else if ( RetValue == -1 )
-            printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
+            printf( "No output asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
         else // if ( RetValue == 0 )
         {
             Abc_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+            printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
         }
 */
         RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames );
@@ -1797,6 +1792,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
+    int nTimeOut = pPars->nTimeOut ? clock() + pPars->nTimeOut * CLOCKS_PER_SEC : 0;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
     {
@@ -1810,16 +1806,26 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     if ( RetValue == 1 )
     {
-//        printf( "No output was asserted in %d frames. ", pPars->iFrame );
+//        printf( "No output asserted in %d frames. ", pPars->iFrame );
         printf( "Incorrect return value.  " );
     }
     else if ( RetValue == -1 )
     {
         if ( pPars->nFailOuts == 0 )
-            printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", pPars->iFrame, pPars->nConfLimit );
+        {
+            printf( "No output asserted in %d frames. Resource limit reached ", pPars->iFrame );
+            if ( nTimeOut < clock() )
+                printf( "(timeout %d sec). ", pPars->nTimeOut );
+            else
+                printf( "(conf limit %d). ", pPars->nConfLimit );
+        }
         else
         {
-            printf( "The total of %d outputs was asserted in %d frames. Reached conflict limit (%d). ", pPars->nFailOuts, pPars->iFrame, pPars->nConfLimit );
+            printf( "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
+            if ( nTimeOut < clock() )
+                printf( "(timeout %d sec). ", pPars->nTimeOut );
+            else
+                printf( "(conf limit %d). ", pPars->nConfLimit );
             if ( pNtk->pSeqModelVec )
                 Vec_PtrFreeFree( pNtk->pSeqModelVec );
             pNtk->pSeqModelVec = pMan->pSeqModelVec;  pMan->pSeqModelVec = NULL;
@@ -1830,12 +1836,12 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
         if ( !pPars->fSolveAll )
         {
             Abc_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+            printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
         }
         else
         {
             printf( "Incorrect return value.  " );
-//            printf( "At least one output was asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame );
+//            printf( "At least one output asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame );
         }
     }
     ABC_PRT( "Time", clock() - clk );
@@ -2133,7 +2139,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
         if ( pNtk->pSeqModel )
         {
             Abc_Cex_t * pCex = pNtk->pSeqModel;
-            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
+            printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
             if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) )
                 printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
         }
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index aa8c7f08..de186047 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1521,6 +1521,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 //            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
             break;
         }
+        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+            break;
     }
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 2b148328..a33c7240 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -164,6 +164,7 @@ struct sat_solver_t
 
     ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
     ABC_INT64_T   nInsLimit;     // external limit on the number of implications
+    int           nRuntimeLimit; // external limit on runtime
 
     veci     act_vars;      // variables whose activity has changed
     double*  factors;       // the activity factors
@@ -220,7 +221,12 @@ static int sat_solver_final(sat_solver* s, int ** ppArray)
     return s->conf_final.size;
 }
 
-
+static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
+{
+    int nRuntimeLimit = s->nRuntimeLimit;
+    s->nRuntimeLimit = Limit;
+    return nRuntimeLimit;
+}
 
 ABC_NAMESPACE_HEADER_END