Added 'gap timeout' to pdr.

3 files changed, 61 insertions, 43 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 263de03c..0a26bf4a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22404,23 +22404,10 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTGarmsdgvwzh" ) ) != EOF )
     {
         switch ( c )
         {
-/*
-        case 'O':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->iOutput = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->iOutput < 0 )
-                goto usage;
-            break;
-*/
         case 'M':
             if ( globalUtilOptind >= argc )
             {
@@ -22476,6 +22463,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeOut < 0 )
                 goto usage;
             break;
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTimeOutGap = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTimeOutGap < 0 )
+                goto usage;
+            break;
         case 'a':
             pPars->fSolveAll ^= 1;
             break;
@@ -22535,25 +22533,25 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCRTG <num>] [-armsdgvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
-//    Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" );
-    Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle );
-    Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
-    Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n",       pPars->nRecycle );
+    Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n",           pPars->nFrameMax );
+    Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n",          pPars->nConfLimit );
     Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
-    Abc_Print( -2, "\t-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
-    Abc_Print( -2, "\t-a     : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" );
-    Abc_Print( -2, "\t-r     : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
-    Abc_Print( -2, "\t-m     : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );
-    Abc_Print( -2, "\t-d     : toggle dumping inductive invariant [default = %s]\n", pPars->fDumpInv? "yes": "no" );
-    Abc_Print( -2, "\t-g     : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-w     : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n",              pPars->nTimeOut );
+    Abc_Print( -2, "\t-G num : approximate runtime gap since the last CEX (0 = no limit) [default = %d]\n",  pPars->nTimeOutGap );
+    Abc_Print( -2, "\t-a     : toggle solving all outputs even if one of them is SAT [default = %s]\n",      pPars->fSolveAll? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle using more effort in generalization [default = %s]\n",                 pPars->fTwoRounds? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle using monolythic CNF computation [default = %s]\n",                    pPars->fMonoCnf? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle creating only shortest counter-examples [default = %s]\n",             pPars->fShortest? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle dumping inductive invariant [default = %s]\n",                         pPars->fDumpInv? "yes": "no" );
+    Abc_Print( -2, "\t-g     : toggle skipping expensive generalization step [default = %s]\n",              pPars->fSkipGeneral? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n",                       pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing detailed stats default = %s]\n",                              pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n",             pPars->fNotVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index c2243761..e55eebb6 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -46,6 +46,7 @@ struct Pdr_Par_t_
     int nConfLimit;       // limit on SAT solver conflicts
     int nRestLimit;       // limit on the number of proof-obligations
     int nTimeOut;         // timeout in seconds
+    int nTimeOutGap;      // approximate timeout in seconds since the last change
     int fTwoRounds;       // use two rounds for generalization
     int fMonoCnf;         // monolythic CNF
     int fDumpInv;         // dump inductive invariant
@@ -60,6 +61,7 @@ struct Pdr_Par_t_
     int iFrame;           // explored up to this frame
     int RunId;            // PDR id in this run 
     int(*pFuncStop)(int); // callback to terminate
+    clock_t timeLastSolved; // the time when the last output was solved
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 548cf7e0..4a9985be 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -45,20 +45,22 @@ ABC_NAMESPACE_IMPL_START
 void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Pdr_Par_t) );
-//    pPars->iOutput       =      -1;  // zero-based output number
-    pPars->nRecycle      =     300;  // limit on vars for recycling
-    pPars->nFrameMax     =   10000;  // limit on number of timeframes
-    pPars->nTimeOut      =       0;  // timeout in seconds
-    pPars->nConfLimit    =       0;  // limit on SAT solver conflicts
-    pPars->nRestLimit    =       0;  // limit on the number of proof-obligations
-    pPars->fTwoRounds    =       0;  // use two rounds for generalization
-    pPars->fMonoCnf      =       0;  // monolythic CNF
-    pPars->fDumpInv      =       0;  // dump inductive invariant
-    pPars->fShortest     =       0;  // forces bug traces to be shortest
-    pPars->fVerbose      =       0;  // verbose output
-    pPars->fVeryVerbose  =       0;  // very verbose output
-    pPars->fNotVerbose   =       0;  // not printing line-by-line progress
-    pPars->iFrame        =      -1;  // explored up to this frame
+//    pPars->iOutput        =      -1;  // zero-based output number
+    pPars->nRecycle       =     300;  // limit on vars for recycling
+    pPars->nFrameMax      =   10000;  // limit on number of timeframes
+    pPars->nTimeOut       =       0;  // timeout in seconds
+    pPars->nTimeOutGap    =       0;  // timeout in seconds since the last solved
+    pPars->nConfLimit     =       0;  // limit on SAT solver conflicts
+    pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
+    pPars->fTwoRounds     =       0;  // use two rounds for generalization
+    pPars->fMonoCnf       =       0;  // monolythic CNF
+    pPars->fDumpInv       =       0;  // dump inductive invariant
+    pPars->fShortest      =       0;  // forces bug traces to be shortest
+    pPars->fVerbose       =       0;  // verbose output
+    pPars->fVeryVerbose   =       0;  // very verbose output
+    pPars->fNotVerbose    =       0;  // not printing line-by-line progress
+    pPars->iFrame         =      -1;  // explored up to this frame
+    pPars->timeLastSolved =       0;  // last one solved
 }
 
 /**Function*************************************************************
@@ -560,6 +562,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
     // create the first timeframe
+    p->pPars->timeLastSolved = clock();
     Pdr_ManCreateSolver( p, (k = 0) );
     while ( 1 )
     {
@@ -590,6 +593,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) );
                 if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                     return 0; // all SAT
+                p->pPars->timeLastSolved = clock();
                 continue;
             } 
             // try to solve this output
@@ -723,6 +727,20 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             p->pPars->iFrame = k;
             return p->vCexes ? 0 : -1;
         }
+        if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
+        {
+            if ( fPrintClauses )
+            {
+                Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+                Pdr_ManPrintClauses( p, 0 );
+            }
+            if ( p->pPars->fVerbose ) 
+                Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+            if ( !p->pPars->fSilent )
+                Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOut );
+            p->pPars->iFrame = k;
+            return p->vCexes ? 0 : -1;
+        }
         if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
         {
             if ( p->pPars->fVerbose )