diff options
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 46 |
1 files changed, 32 insertions, 14 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 548cf7e0..4a9985be 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -45,20 +45,22 @@ ABC_NAMESPACE_IMPL_START void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) { memset( pPars, 0, sizeof(Pdr_Par_t) ); -// pPars->iOutput = -1; // zero-based output number - pPars->nRecycle = 300; // limit on vars for recycling - pPars->nFrameMax = 10000; // limit on number of timeframes - pPars->nTimeOut = 0; // timeout in seconds - pPars->nConfLimit = 0; // limit on SAT solver conflicts - pPars->nRestLimit = 0; // limit on the number of proof-obligations - pPars->fTwoRounds = 0; // use two rounds for generalization - pPars->fMonoCnf = 0; // monolythic CNF - pPars->fDumpInv = 0; // dump inductive invariant - pPars->fShortest = 0; // forces bug traces to be shortest - pPars->fVerbose = 0; // verbose output - pPars->fVeryVerbose = 0; // very verbose output - pPars->fNotVerbose = 0; // not printing line-by-line progress - pPars->iFrame = -1; // explored up to this frame +// pPars->iOutput = -1; // zero-based output number + pPars->nRecycle = 300; // limit on vars for recycling + pPars->nFrameMax = 10000; // limit on number of timeframes + pPars->nTimeOut = 0; // timeout in seconds + pPars->nTimeOutGap = 0; // timeout in seconds since the last solved + pPars->nConfLimit = 0; // limit on SAT solver conflicts + pPars->nRestLimit = 0; // limit on the number of proof-obligations + pPars->fTwoRounds = 0; // use two rounds for generalization + pPars->fMonoCnf = 0; // monolythic CNF + pPars->fDumpInv = 0; // dump inductive invariant + pPars->fShortest = 0; // forces bug traces to be shortest + pPars->fVerbose = 0; // verbose output + pPars->fVeryVerbose = 0; // very verbose output + pPars->fNotVerbose = 0; // not printing line-by-line progress + pPars->iFrame = -1; // explored up to this frame + pPars->timeLastSolved = 0; // last one solved } /**Function************************************************************* @@ -560,6 +562,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0; assert( Vec_PtrSize(p->vSolvers) == 0 ); // create the first timeframe + p->pPars->timeLastSolved = clock(); Pdr_ManCreateSolver( p, (k = 0) ); while ( 1 ) { @@ -590,6 +593,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT + p->pPars->timeLastSolved = clock(); continue; } // try to solve this output @@ -723,6 +727,20 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pPars->iFrame = k; return p->vCexes ? 0 : -1; } + if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) + { + if ( fPrintClauses ) + { + Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Pdr_ManPrintClauses( p, 0 ); + } + 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 ); + p->pPars->iFrame = k; + return p->vCexes ? 0 : -1; + } if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax ) { if ( p->pPars->fVerbose ) |