diff options
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 11 | ||||
| -rw-r--r-- | src/proof/pdr/pdrSat.c | 9 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 2 |
4 files changed, 21 insertions, 3 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 03d522d3..3f74dd5f 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -135,6 +135,17 @@ struct Pdr_Man_t_ static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); } +static inline clock_t Pdr_ManTimeLimit( Pdr_Man_t * p ) +{ + if ( p->timeToStop == 0 ) + return p->timeToStopOne; + if ( p->timeToStopOne == 0 ) + return p->timeToStop; + if ( p->timeToStop < p->timeToStopOne ) + return p->timeToStop; + return p->timeToStopOne; +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index a68bbee4..c9028c24 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -256,10 +256,13 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) { sat_solver * pSat; Vec_Int_t * vLits; + clock_t Limit; int RetValue; pSat = Pdr_ManFetchSolver( p, k ); vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 ); + Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) ); RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); + sat_solver_set_runtime_limit( pSat, Limit ); if ( RetValue == l_Undef ) return -1; return (RetValue == l_False); @@ -284,14 +287,16 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr sat_solver * pSat; Vec_Int_t * vLits; int Lit, RetValue; - clock_t clk; + clock_t clk, Limit; p->nCalls++; pSat = Pdr_ManFetchSolver( p, k ); if ( pCube == NULL ) // solve the property { clk = clock(); Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails) + Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) ); RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 ); + sat_solver_set_runtime_limit( pSat, Limit ); if ( RetValue == l_Undef ) return -1; } @@ -320,7 +325,9 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr // solve clk = clock(); + Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) ); RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 ); + sat_solver_set_runtime_limit( pSat, Limit ); if ( RetValue == l_Undef ) return -1; /* diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 50df6a84..d1310c81 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1576,7 +1576,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) int next; // Reached bound on number of conflicts: - if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){ s->progress_estimate = sat_solver_progress(s); sat_solver_canceluntil(s,s->root_level); veci_delete(&learnt_clause); diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index a3dad126..12d74c0d 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1037,7 +1037,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) // NO CONFLICT int next; - if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && clock() > s->nRuntimeLimit)){ // Reached bound on number of conflicts: s->progress_estimate = solver2_progress(s); solver2_canceluntil(s,s->root_level); |