Upgrading the SAT solvers.

3 files changed, 12 insertions, 5 deletions

diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index 0f2d2fce..c975c6ca 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -609,7 +609,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
     for(i = 0;i<selectors.size();i++)  
       out_learnt.push(selectors[i]);       
 
-    out_learnt.copyTo(analyze_toclear);
+    out_learnt.copyTo_(analyze_toclear);
     if (ccmin_mode == 2){
         uint32_t abstract_level = 0;
         for (i = 1; i < out_learnt.size(); i++)
diff --git a/src/sat/glucose/SolverTypes.h b/src/sat/glucose/SolverTypes.h
index 4f2670a7..b29699fa 100644
--- a/src/sat/glucose/SolverTypes.h
+++ b/src/sat/glucose/SolverTypes.h
@@ -306,9 +306,15 @@ class OccLists
     }
 
     void  clear(bool free = true){
-        occs   .clear(free);
-        dirty  .clear(free);
-        dirties.clear(free);
+        if(free){
+            occs   .clear(free);
+            dirty  .clear(free);
+            dirties.clear(free);
+        } else {
+            occs   .shrink_(occs   .size());
+            dirty  .shrink_(dirty  .size());
+            dirties.shrink_(dirties.size());
+        }
     }
 };
 
diff --git a/src/sat/glucose/Vec.h b/src/sat/glucose/Vec.h
index da87af35..dd1bc20a 100644
--- a/src/sat/glucose/Vec.h
+++ b/src/sat/glucose/Vec.h
@@ -89,7 +89,8 @@ public:
     T&       operator [] (int index)       { return data[index]; }
 
     // Duplicatation (preferred instead):
-    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
+    void copyTo (vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
+    void copyTo_(vec<T>& copy) const { copy.shrink_(copy.size()); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
 };