Adding timeout to command 'ind'.

4 files changed, 33 insertions, 13 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 89622491..475f476d 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -131,7 +131,7 @@ extern Aig_Man_t *       Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPo
 /*=== saigHaig.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 /*=== saigInd.c ==========================================================*/
-extern int               Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
+extern int               Saig_ManInduction( Aig_Man_t * p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
 /*=== saigIoa.c ==========================================================*/
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c
index 114db997..c7b50461 100644
--- a/src/aig/saig/saigInd.c
+++ b/src/aig/saig/saigInd.c
@@ -142,7 +142,7 @@ void Saig_ManAddUniqueness( sat_solver * pSat, Vec_Int_t * vState, int nRegs, in
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
+int Saig_ManInduction( Aig_Man_t * p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
 {
     sat_solver * pSat;
     Aig_Man_t * pAigPart;
@@ -152,7 +152,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
     Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
     int i, k, f, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
     int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
-    abctime clk;
+    abctime clk, nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
     assert( fUnique == 0 || fUniqueAll == 0 );
     assert( Saig_ManPoNum(p) == 1 );
     Aig_ManSetCioIds( p );
@@ -168,6 +168,10 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
     pSat = sat_solver_new();
     sat_solver_setnvars( pSat, 1000 );
 
+    // set runtime limit
+    if ( nTimeToStop )
+        sat_solver_set_runtime_limit( pSat, nTimeToStop );
+
     // iterate backward unrolling
     RetValue = -1;
     nSatVarNum = 0;
@@ -312,7 +316,7 @@ nextrun:
             }
             printf( "\n" );
         }
-        if ( f == nFramesMax - 1 )
+        if ( nFramesMax && f == nFramesMax - 1 )
         {
             // derive counter-example
             assert( status == l_True );
@@ -357,7 +361,9 @@ nextrun:
     }
     if ( fVerbose )
     {
-        if ( status == l_Undef )
+        if ( nTimeToStop && Abc_Clock() >= nTimeToStop )
+            printf( "Timeout (%d sec) was reached during iteration %d.\n", nTimeOut, f+1 );
+        else if ( status == l_Undef )
             printf( "Conflict limit (%d) was reached during iteration %d.\n", nConfMax, f+1 );
         else if ( fUnique || fUniqueAll )
             printf( "Completed %d interations and added %d uniqueness constraints.\n", f+1, nConstrs );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3d593d2e..cdd391e2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22492,6 +22492,7 @@ usage:
 int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int nTimeOut;
     int nFramesMax;
     int nConfMax;
     int fUnique;
@@ -22500,17 +22501,18 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int fVeryVerbose;
     int c;
-    extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
+    extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
     // set defaults
-    nFramesMax   =   100;
-    nConfMax     =  1000;
+    nTimeOut     =     0;
+    nFramesMax   =     0;
+    nConfMax     =     0;
     fUnique      =     0;
     fUniqueAll   =     0;
     fGetCex      =     0;
     fVerbose     =     0;
     fVeryVerbose =     0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCuaxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCTuaxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22536,6 +22538,17 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfMax < 0 )
                 goto usage;
             break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeOut < 0 )
+                goto usage;
+            break;
         case 'u':
             fUnique ^= 1;
             break;
@@ -22584,7 +22597,7 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    pAbc->Status = Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
+    pAbc->Status = Abc_NtkDarInduction( pNtk, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
     if ( fGetCex )
     {
         Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
@@ -22592,10 +22605,11 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     return 0;
 usage:
-    Abc_Print( -2, "usage: ind [-FC num] [-uaxvwh]\n" );
+    Abc_Print( -2, "usage: ind [-FCT num] [-uaxvwh]\n" );
     Abc_Print( -2, "\t         runs the inductive case of the K-step induction\n" );
     Abc_Print( -2, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
+    Abc_Print( -2, "\t-T num : the limit on runtime per output in seconds [default = %d]\n", nTimeOut );
     Abc_Print( -2, "\t-u     : toggle adding uniqueness constraints on demand [default = %s]\n", fUnique? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle adding uniqueness constraints always [default = %s]\n", fUniqueAll? "yes": "no" );
     Abc_Print( -2, "\t-x     : toggle returning CEX to induction for the top frame [default = %s]\n", fGetCex? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 552b124c..04b104e5 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3451,7 +3451,7 @@ Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nC
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
 { 
     Aig_Man_t * pMan;
     abctime clkTotal = Abc_Clock();
@@ -3459,7 +3459,7 @@ int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUn
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return -1;
-    RetValue = Saig_ManInduction( pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
+    RetValue = Saig_ManInduction( pMan, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
     if ( RetValue == 1 )
     {
         Abc_Print( 1, "Networks are equivalent.   " );