diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 13:22:05 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 13:22:05 -0700 |
| commit | dfcdffe4be3e7da5e1eeb2f151e8fa8b45d6d76f (patch) | |
| tree | 8050ddfe26fbc62fc04d972a286ddd55ec33e743 /src/proof/pdr | |
| parent | c83e1d906a427aa8a60b17e988520db3528ba595 (diff) | |
| download | abc-dfcdffe4be3e7da5e1eeb2f151e8fa8b45d6d76f.tar.gz abc-dfcdffe4be3e7da5e1eeb2f151e8fa8b45d6d76f.tar.bz2 abc-dfcdffe4be3e7da5e1eeb2f151e8fa8b45d6d76f.zip | |
Fixed gap timeout in 'pdr'.
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index f2ba7ba6..987a1a3e 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -540,6 +540,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) return -1; if ( p->timeToStopOne && clock() > p->timeToStopOne ) return -1; + if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) + return -1; } return 1; } @@ -656,6 +658,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) 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->nTimeOutGap && p->pPars->timeLastSolved && 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 && clock() > p->timeToStopOne ) { Pdr_QueueClean( p ); |