diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-18 08:43:55 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-18 08:43:55 -0700 |
| commit | 12d21480de5f5434df72f577afcc7208b2dc0683 (patch) | |
| tree | 7449505bbb28794c575b163c3982d5fe88fc4b90 /src/sat/glucose/SimpSolver.cpp | |
| parent | 3a1032c151360c99334c559d93b0068bf4b2a3f5 (diff) | |
| download | abc-12d21480de5f5434df72f577afcc7208b2dc0683.tar.gz abc-12d21480de5f5434df72f577afcc7208b2dc0683.tar.bz2 abc-12d21480de5f5434df72f577afcc7208b2dc0683.zip | |
Changes to Glucose to enable resetting the solver.
Diffstat (limited to 'src/sat/glucose/SimpSolver.cpp')
| -rw-r--r-- | src/sat/glucose/SimpSolver.cpp | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp index c097a3ae..f46ae03e 100644 --- a/src/sat/glucose/SimpSolver.cpp +++ b/src/sat/glucose/SimpSolver.cpp @@ -751,3 +751,24 @@ void SimpSolver::garbageCollect() ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } + +void SimpSolver::reset() +{ + Solver::reset(); + grow = opt_grow; + asymm_lits = eliminated_vars = bwdsub_assigns = n_touched = 0; + elimclauses.clear(false); + touched.clear(false); + occurs.clear(false); + n_occ.clear(false); + elim_heap.clear(false); + subsumption_queue.clear(false); + frozen.clear(false); + eliminated.clear(false); + vec<Lit> dummy(1,lit_Undef); + ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. + bwdsub_tmpunit = ca.alloc(dummy); + remove_satisfied = false; +} + + |