diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-06-18 12:12:01 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-06-18 12:12:01 -0700 |
| commit | 91f06107bfaa79e7526774e09ecdc5c9f0d489f8 (patch) | |
| tree | 1722325cf0bbbf90e66d0707c8ea51cd8bc8591c | |
| parent | ac4962eb2d35d905c2d0ae2d41905e8c4d1df157 (diff) | |
| download | abc-91f06107bfaa79e7526774e09ecdc5c9f0d489f8.tar.gz abc-91f06107bfaa79e7526774e09ecdc5c9f0d489f8.tar.bz2 abc-91f06107bfaa79e7526774e09ecdc5c9f0d489f8.zip | |
Bug fixes in the implementation of varius resource limits in 'pdr'.
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 7cd60d9e..d3084f29 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -640,7 +640,17 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); - if ( p->pPars->nConfLimit ) + if ( p->timeToStop && Abc_Clock() > p->timeToStop ) + Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); + else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) + Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); + else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne ) + { + Pdr_QueueClean( p ); + pCube = NULL; + break; // keep solving + } + else if ( p->pPars->nConfLimit ) Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); else if ( p->pPars->fVerbose ) Abc_Print( 1, "Computation cancelled by the callback.\n" ); @@ -654,9 +664,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); - if ( p->pPars->nConfLimit ) - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); - else if ( p->timeToStop && Abc_Clock() > p->timeToStop ) + if ( p->timeToStop && Abc_Clock() > p->timeToStop ) Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); @@ -666,6 +674,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) pCube = NULL; break; // keep solving } + else if ( p->pPars->nConfLimit ) + Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); else if ( p->pPars->fVerbose ) Abc_Print( 1, "Computation cancelled by the callback.\n" ); p->pPars->iFrame = k; @@ -720,12 +730,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) abctime timeSince = Abc_Clock() - clkOne; assert( p->pTime4Outs[p->iOutCur] > 0 ); p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0; - if ( p->pTime4Outs[p->iOutCur] == 0 && p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) + if ( p->pTime4Outs[p->iOutCur] == 0 && (p->vCexes == NULL || Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL) ) { p->pPars->nDropOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); // printf( "Dropping output %d.\n", p->iOutCur ); } + p->timeToStopOne = 0; } } @@ -842,10 +853,10 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) Pdr_Man_t * p; int k, RetValue; abctime clk = Abc_Clock(); - if ( pPars->nTimeOutOne ) - pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1; if ( pPars->nTimeOutOne && !pPars->fSolveAll ) pPars->nTimeOutOne = 0; + if ( pPars->nTimeOutOne ) + pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0); if ( pPars->fVerbose ) { // Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); |