From: Dejan Jovanovic <dejan.jovanovic@gmail.com>
Date: Sat, 14 Mar 2015 07:24:24 +0000 (-0700)
Subject: Updating resize for occurence lists to properly resize the whole state.
X-Git-Tag: cvc5-1.0.0~6377
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=01856989542f8c0e13ed11d0eec78cd122a2a7da;p=cvc5.git

Updating resize for occurence lists to properly resize the whole state.
---

diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index a6413e674..bc60542e7 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -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)]; }
@@ -372,6 +372,19 @@ void OccLists<Idx,Vec,Deleted>::cleanAll()
     dirties.clear();
 }
 
+template<class Idx, class Vec, class Deleted>
+void OccLists<Idx,Vec,Deleted>::resizeTo(const Idx& idx)
+{
+    int shrinkSize = occs.size() - (toInt(idx) + 1);
+    occs.shrink(shrinkSize);
+    dirty.shrink(shrinkSize);
+    // Remove out-of-bound indices from dirties
+    int  i, j;
+    for (i = j = 0; i < dirties.size(); i++)
+        if (toInt(dirties[i]) < occs.size())
+            dirties[j++] = dirties[i];
+    dirties.shrink(i - j);
+}
 
 template<class Idx, class Vec, class Deleted>
 void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)