31 lines
1.3 KiB
Diff
31 lines
1.3 KiB
Diff
--- ./src/prop/minisat/core/SolverTypes.h.orig 2014-06-22 01:17:45.510946923 -0600
|
|
+++ ./src/prop/minisat/core/SolverTypes.h 2015-03-11 21:00:00.000000000 -0600
|
|
@@ -340,7 +340,7 @@ class OccLists
|
|
OccLists(const Deleted& d) : deleted(d) {}
|
|
|
|
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
|
|
- void resizeTo (const Idx& idx){ int shrinkSize = occs.size() - (toInt(idx) + 1); occs.shrink(shrinkSize); }
|
|
+ void resizeTo (const Idx& idx);
|
|
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
|
|
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
|
|
Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
|
|
@@ -386,6 +386,18 @@ void OccLists<Idx,Vec,Deleted>::clean(co
|
|
}
|
|
|
|
|
|
+template<class Idx, class Vec, class Deleted>
|
|
+void OccLists<Idx,Vec,Deleted>::resizeTo(const Idx& idx)
|
|
+{
|
|
+ for (int i = 0; i < dirties.size(); i++)
|
|
+ if (toInt(dirties[i]) > toInt(idx))
|
|
+ clean(dirties[i]);
|
|
+
|
|
+ int shrinkSize = occs.size() - (toInt(idx) + 1);
|
|
+ occs.shrink(shrinkSize);
|
|
+}
|
|
+
|
|
+
|
|
//=================================================================================================
|
|
// CMap -- a class for mapping clauses to values:
|
|
|