Changes to Glucose to enable resetting the solver.

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]; }

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);
+}

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;
+}
+
+

src/sat/glucose/SimpSolver.h

@@ -66,6 +66,7 @@ class SimpSolver : public Solver {
 
     // Memory managment:
     //
+    virtual void reset();
     virtual void garbageCollect();
 
 

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();