luke/abc
1
0
Fork 0
mirror of https://github.com/YosysHQ/abc.git synced 2026-09-02 10:47:31 +02:00
Code Issues Packages Projects Releases Wiki Activity

This code was accidentally deleted from the SAT solver (effectively disabling restarts!)

Browse Source
This commit is contained in:
Alan Mishchenko
2016-04-30 10:42:10 -07:00
parent 1c245b4a4a
commit e3e6236663
1 changed files with 7 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/sat/bsat/satSolver.c
+7
View File
@@ -1659,6 +1659,13 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
// NO CONFLICT
int next;
// Reached bound on number of conflicts:
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);
sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);
return l_Undef; }
// Reached bound on number of conflicts:
if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
(s->nInsLimit && s->stats.propagations > s->nInsLimit) )