diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-06-28 12:21:48 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-06-28 12:21:48 -0700 |
| commit | 8c7ca72ea9a653772c9d1fd54f87fb3ee51fb873 (patch) | |
| tree | a8978f8390ae9b3dfcb2160a66d75be739624b2c /src/aig/saig | |
| parent | 184c5d4ea467731005c92bc159c68d57c83c6c6a (diff) | |
| download | abc-8c7ca72ea9a653772c9d1fd54f87fb3ee51fb873.tar.gz abc-8c7ca72ea9a653772c9d1fd54f87fb3ee51fb873.tar.bz2 abc-8c7ca72ea9a653772c9d1fd54f87fb3ee51fb873.zip | |
Adding timeout to command 'ind'.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigInd.c | 14 |
2 files changed, 11 insertions, 5 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 ); |