diff options
Diffstat (limited to 'src/sat/glucose')
-rw-r--r-- | src/sat/glucose/Glucose.cpp | 2 | ||||
-rw-r--r-- | src/sat/glucose/SolverTypes.h | 12 | ||||
-rw-r--r-- | src/sat/glucose/Vec.h | 3 |
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; } }; |