diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-07 21:51:26 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-07 21:51:26 -0800 |
| commit | 7adc34ad9e607bcdab161ad9a64bb87711365e81 (patch) | |
| tree | c56fa5baae4ecebd4f3768c97bd8c54b6299d47f /src/proof/pdr | |
| parent | a3bdba68757a16ed28208bfe4ab81bfdbe928d89 (diff) | |
| download | abc-7adc34ad9e607bcdab161ad9a64bb87711365e81.tar.gz abc-7adc34ad9e607bcdab161ad9a64bb87711365e81.tar.bz2 abc-7adc34ad9e607bcdab161ad9a64bb87711365e81.zip | |
Fixing gap timeout in 'pdr'.
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 4a9985be..837e01a3 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -599,6 +599,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // try to solve this output while ( 1 ) { + if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) + { + 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->nTimeOutGap ); + p->pPars->iFrame = k; + return p->vCexes ? 0 : -1; + } RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit ); if ( RetValue == 1 ) break; @@ -606,10 +615,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); - 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" ); + 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; return p->vCexes ? 0 : -1; } @@ -622,6 +631,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); if ( p->pPars->nConfLimit ) Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + else if ( p->timeToStop && clock() > p->timeToStop ) + Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); else if ( p->pPars->fVerbose ) Abc_Print( 1, "Computation cancelled by the callback.\n" ); p->pPars->iFrame = k; @@ -737,7 +748,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) 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 ); + Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); p->pPars->iFrame = k; return p->vCexes ? 0 : -1; } |