From 5f8a8a596a009046896acd8af6397acecc1e36a9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 Apr 2021 14:46:05 -0700 Subject: Upgrade to the circuit-based solver. --- src/sat/glucose2/SimpSolver2.cpp | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'src/sat/glucose2/SimpSolver2.cpp') diff --git a/src/sat/glucose2/SimpSolver2.cpp b/src/sat/glucose2/SimpSolver2.cpp index 7c2a3b26..37093277 100644 --- a/src/sat/glucose2/SimpSolver2.cpp +++ b/src/sat/glucose2/SimpSolver2.cpp @@ -707,7 +707,7 @@ void SimpSolver::cleanUpClauses() for (i = j = 0; i < clauses.size(); i++) if (ca[clauses[i]].mark() == 0) clauses[j++] = clauses[i]; - clauses.shrink(i - j); + clauses.shrink_(i - j); } @@ -760,18 +760,22 @@ 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; + + occurs.clear(false); + + touched .shrink_( touched .size() ); + n_occ .shrink_( n_occ .size() ); + eliminated .shrink_( eliminated .size() ); + frozen .shrink_( frozen .size() ); + elimclauses .shrink_( elimclauses .size() ); + + elim_heap .clear_(false); } ABC_NAMESPACE_IMPL_END -- cgit v1.2.3