diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-19 22:33:40 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-19 22:33:40 -0700 |
| commit | 2ded89cca5cd0e899d5549476e6774cf7264132d (patch) | |
| tree | 5c0fa2bfa936211c68427deb9f58a15b48b38e78 /src/sat/bsat | |
| parent | 2d0a8fb4cbb8907e6733728340995e4f93cde86d (diff) | |
| download | abc-2ded89cca5cd0e899d5549476e6774cf7264132d.tar.gz abc-2ded89cca5cd0e899d5549476e6774cf7264132d.tar.bz2 abc-2ded89cca5cd0e899d5549476e6774cf7264132d.zip | |
Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index e8e13ee7..f1f6345e 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1660,7 +1660,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) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){ + if ( (!s->fNoRestarts && 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); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index c4888c73..7ef2c9e8 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -179,6 +179,7 @@ struct sat_solver_t int fSkipSimplify; // set to one to skip simplification of the clause database int fNotUseRandom; // do not allow random decisions with a fixed probability + int fNoRestarts; // disables periodic restarts int * pGlobalVars; // for experiments with global vars during interpolation // clause store |