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/Alloc.h | 1 + src/sat/glucose/Glucose.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++ src/sat/glucose/SimpSolver.cpp | 21 ++++++++++++++ src/sat/glucose/SimpSolver.h | 1 + src/sat/glucose/Solver.h | 1 + 5 files changed, 87 insertions(+) diff --git a/src/sat/glucose/Alloc.h b/src/sat/glucose/Alloc.h index 997a2516..5dfad58a 100644 --- a/src/sat/glucose/Alloc.h +++ b/src/sat/glucose/Alloc.h @@ -58,6 +58,7 @@ class RegionAllocator Ref alloc (int size); void free_ (int size) { wasted_ += size; } + void clear () { sz = 0; wasted_=0; } // Deref, Load Effective Address (LEA), Inverse of LEA (AEL): T& operator[](Ref r) { assert(r >= 0 && r < sz); return memory[r]; } diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index 2a67d903..bfe90361 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -1428,3 +1428,66 @@ void Solver::garbageCollect() ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } + +void Solver::reset() +{ + // Reset everything + ok = true; + K = (double)opt_K; + R = (double)opt_R; + firstReduceDB = opt_first_reduce_db; + var_decay = (double)opt_var_decay; + //max_var_decay = opt_max_var_decay; + solves = starts = decisions = propagations = conflicts = conflictsRestarts = 0; + curRestart = 1; + cla_inc = var_inc = 1; + watches.clear(false); // We don't free the memory, new calls should be of the same size order. + watchesBin.clear(false); + //unaryWatches.clear(false); + qhead = 0; + simpDB_assigns = -1; + simpDB_props = 0; + order_heap.clear(false); + progress_estimate = 0; + //lastLearntClause = CRef_Undef; + conflict_budget = -1; + propagation_budget = -1; + nbVarsInitialFormula = INT32_MAX; + totalTime4Sat = 0.; + totalTime4Unsat = 0.; + nbSatCalls = nbUnsatCalls = 0; + MYFLAG = 0; + lbdQueue.clear(false); + lbdQueue.initSize(sizeLBDQueue); + trailQueue.clear(false); + trailQueue.initSize(sizeTrailQueue); + sumLBD = 0; + nbclausesbeforereduce = firstReduceDB; + //stats.clear(); + //stats.growTo(coreStatsSize, 0); + clauses.clear(false); + learnts.clear(false); + //permanentLearnts.clear(false); + //unaryWatchedClauses.clear(false); + model.clear(false); + conflict.clear(false); + activity.clear(false); + assigns.clear(false); + polarity.clear(false); + //forceUNSAT.clear(false); + decision.clear(false); + trail.clear(false); + nbpos.clear(false); + trail_lim.clear(false); + vardata.clear(false); + assumptions.clear(false); + permDiff.clear(false); + lastDecisionLevel.clear(false); + ca.clear(); + seen.clear(false); + analyze_stack.clear(false); + analyze_toclear.clear(false); + add_tmp.clear(false); + assumptionPositions.clear(false); + initialPositions.clear(false); +} \ No newline at end of file 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; +} + + diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h index 520a5cc9..6c9272a2 100644 --- a/src/sat/glucose/SimpSolver.h +++ b/src/sat/glucose/SimpSolver.h @@ -66,6 +66,7 @@ class SimpSolver : public Solver { // Memory managment: // + virtual void reset(); virtual void garbageCollect(); diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h index bb4c6d0f..43053062 100644 --- a/src/sat/glucose/Solver.h +++ b/src/sat/glucose/Solver.h @@ -131,6 +131,7 @@ public: // Memory managment: // + virtual void reset(); virtual void garbageCollect(); // virtuality causes segfault for some reason void checkGarbage(double gf); void checkGarbage(); -- cgit v1.2.3