diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/saigBmc2.c | 8 | ||||
-rw-r--r-- | src/aig/saig/saigBmc3.c | 4 |
2 files changed, 10 insertions, 2 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; |