Commit cec6bd64 by Alan Mishchenko

Limiting runtime limit checks in 'pdr'.

parent 77cef7ca
...@@ -1576,7 +1576,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) ...@@ -1576,7 +1576,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
int next; int next;
// Reached bound on number of conflicts: // Reached bound on number of conflicts:
if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
s->progress_estimate = sat_solver_progress(s); s->progress_estimate = sat_solver_progress(s);
sat_solver_canceluntil(s,s->root_level); sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause); veci_delete(&learnt_clause);
......
...@@ -1037,7 +1037,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) ...@@ -1037,7 +1037,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
// NO CONFLICT // NO CONFLICT
int next; int next;
if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
// Reached bound on number of conflicts: // Reached bound on number of conflicts:
s->progress_estimate = solver2_progress(s); s->progress_estimate = solver2_progress(s);
solver2_canceluntil(s,s->root_level); solver2_canceluntil(s,s->root_level);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment