diff options
Diffstat (limited to 'src/sat/bmc')
-rw-r--r-- | src/sat/bmc/bmc.h | 2 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmc3.c | 10 |
2 files changed, 12 insertions, 0 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index bac4a2dd..e799bea9 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -48,6 +48,7 @@ struct Saig_ParBmc_t_ int nConfLimitJump; // maximum number of conflicts after jumping int nFramesJump; // the number of tiemframes to jump int nTimeOut; // approximate timeout in seconds + int nTimeOutGap; // approximate timeout in seconds since the last change int nPisAbstract; // the number of PIs to abstract int fSolveAll; // does not stop at the first SAT output int fDropSatOuts; // replace sat outputs by constant 0 @@ -57,6 +58,7 @@ struct Saig_ParBmc_t_ int fNotVerbose; // skip line-by-line print-out int iFrame; // explored up to this frame int nFailOuts; // the number of failed outputs + clock_t timeLastSolved; // the time when the last output was solved }; diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index cd965c06..98689ff8 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1301,6 +1301,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) p->nConfLimitJump = 0; // maximum number of conflicts after jumping p->nFramesJump = 0; // the number of tiemframes to jump p->nTimeOut = 0; // approximate timeout in seconds + p->nTimeOutGap = 0; // time since the last CEX found p->nPisAbstract = 0; // the number of PIs to abstract p->fSolveAll = 0; // stops on the first SAT instance p->fDropSatOuts = 0; // replace sat outputs by constant 0 @@ -1308,6 +1309,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) p->fNotVerbose = 0; // skip line-by-line print-out p->iFrame = -1; // explored up to this frame p->nFailOuts = 0; // the number of failed outputs + p->timeLastSolved = 0; // time when the last one was solved } /**Function************************************************************* @@ -1405,6 +1407,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) Saig_Bmc3ManStop( p ); return RetValue; } + if ( pPars->nTimeOutGap && pPars->timeLastSolved && clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC ) + { + printf( "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap ); + Saig_Bmc3ManStop( p ); + return RetValue; + } // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; @@ -1433,6 +1441,7 @@ clkOther += clock() - clk2; p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); RetValue = 0; + pPars->timeLastSolved = clock(); continue; } // solve th is output @@ -1507,6 +1516,7 @@ clkOther += clock() - clk2; p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); RetValue = 0; + pPars->timeLastSolved = clock(); } else { |