diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-31 14:59:47 -0500 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-31 14:59:47 -0500 |
| commit | 868a1b9aeb2bf825a68c37c530107efe72d50d5d (patch) | |
| tree | 872e030d59ce89d595812f1c8ae4e776905d3112 /src/sat | |
| parent | f08be2742e892b7b81f234785cbbae85c61ab024 (diff) | |
| download | abc-868a1b9aeb2bf825a68c37c530107efe72d50d5d.tar.gz abc-868a1b9aeb2bf825a68c37c530107efe72d50d5d.tar.bz2 abc-868a1b9aeb2bf825a68c37c530107efe72d50d5d.zip | |
Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 7 | ||||
| -rw-r--r-- | src/sat/pdr/pdrCore.c | 6 |
2 files changed, 7 insertions, 6 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index a3da3e30..ac2202dc 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1485,7 +1485,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit // int nConfs = 0; double Ratio = (s->stats.learnts == 0)? 0.0 : s->stats.learnts_literals / (double)s->stats.learnts; - if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit ) + if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) break; if (s->verbosity >= 1) @@ -1510,7 +1510,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit // nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5; nof_learnts = nof_learnts * 11 / 10; //*= 1.1; - +//printf( "%d ", s->stats.conflicts ); // quit the loop if reached an external limit if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ) { @@ -1523,9 +1523,10 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit // printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit ); break; } - if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit ) + if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) break; } +//printf( "\n" ); if (s->verbosity >= 1) printf("==============================================================================\n"); diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c index 04caba1e..e3c3781f 100644 --- a/src/sat/pdr/pdrCore.c +++ b/src/sat/pdr/pdrCore.c @@ -514,7 +514,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) } // check the timeout - if ( p->timeToStop && clock() >= p->timeToStop ) + if ( p->timeToStop && time(NULL) > p->timeToStop ) return -1; } return 1; @@ -538,7 +538,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) int k, RetValue = -1; int clkTotal = clock(); int clkStart = clock(); - p->timeToStop = (p->pPars->nTimeOut == 0) ? 0 : clock() + (CLOCKS_PER_SEC * p->pPars->nTimeOut); + p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0; assert( Vec_PtrSize(p->vSolvers) == 0 ); // create the first timeframe Pdr_ManCreateSolver( p, (k = 0) ); @@ -619,7 +619,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } // check the timeout - if ( p->timeToStop && clock() >= p->timeToStop ) + if ( p->timeToStop && time(NULL) > p->timeToStop ) { if ( fPrintClauses ) { |