From 12d21480de5f5434df72f577afcc7208b2dc0683 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 18 Sep 2017 08:43:55 -0700 Subject: Changes to Glucose to enable resetting the solver. --- src/sat/glucose/SimpSolver.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'src/sat/glucose/SimpSolver.cpp') 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 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; +} + + -- cgit v1.2.3