From 7adc34ad9e607bcdab161ad9a64bb87711365e81 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 7 Mar 2013 21:51:26 -0800 Subject: Fixing gap timeout in 'pdr'. --- src/proof/pdr/pdrCore.c | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) (limited to 'src/proof/pdr') 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; } -- cgit v1.2.3