Fixing a garbage collection issue in simplifyWithCare(). Bug 729.

2 files changed, 148 insertions, 110 deletions

diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index e5c56a2a4..3ae9bc019 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -658,6 +658,7 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){
   if(thenB.isConst() && elseB.isConst()){
     NodeVec* pair = new NodeVec(2);
     d_allocatedConstantLeaves.push_back(pair);
+
     (*pair)[0] = std::min(thenB, elseB);
     (*pair)[1] = std::max(thenB, elseB);
     d_constantLeaves[ite] = pair;
@@ -1401,25 +1402,32 @@ Node ITESimplifier::simpITE(TNode assertion)
 }
 
 ITECareSimplifier::ITECareSimplifier()
-  : d_usedSets()
+    : d_careSetsOutstanding(0)
+    , d_usedSets()
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 }
 
-ITECareSimplifier::~ITECareSimplifier(){}
+ITECareSimplifier::~ITECareSimplifier(){
+  Assert(d_usedSets.empty());
+  Assert(d_careSetsOutstanding == 0);
+}
 
 void ITECareSimplifier::clear(){
-  d_usedSets.clear();
+  Assert(d_usedSets.empty());
+  Assert(d_careSetsOutstanding == 0);
 }
 
 ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
 {
   if (d_usedSets.empty()) {
+    d_careSetsOutstanding++;
     return ITECareSimplifier::CareSetPtr::mkNew(*this);
   }
   else {
-    ITECareSimplifier::CareSetPtr cs = ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
+    ITECareSimplifier::CareSetPtr cs =
+        ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
     cs.getCareSet().clear();
     d_usedSets.pop_back();
     return cs;
@@ -1490,125 +1498,144 @@ Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cach
 Node ITECareSimplifier::simplifyWithCare(TNode e)
 {
   TNodeMap substTable;
-  CareMap queue;
-  CareMap::iterator it;
-  ITECareSimplifier::CareSetPtr cs = getNewSet();
-  ITECareSimplifier::CareSetPtr cs2;
-  queue[e] = cs;
-
-  TNode v;
-  bool done;
-  unsigned i;
-
-  while (!queue.empty()) {
-    it = queue.end();
-    --it;
-    v = it->first;
-    cs = it->second;
-    set<Node>& css = cs.getCareSet();
-    queue.erase(v);
-
-    done = false;
-    set<Node>::iterator iCare, iCareEnd = css.end();
-
-    switch (v.getKind()) {
-      case kind::ITE: {
-        iCare = css.find(v[0]);
-        if (iCare != iCareEnd) {
-          Assert(substTable.find(v) == substTable.end());
-          substTable[v] = v[1];
-          updateQueue(queue, v[1], cs);
-          done = true;
-          break;
-        }
-        else {
-          iCare = css.find(v[0].negate());
+
+  /* This extra block is to trigger the destructors for cs and cs2
+   * before starting garbage collection.
+   */
+  {
+    CareMap queue;
+    CareMap::iterator it;
+    ITECareSimplifier::CareSetPtr cs = getNewSet();
+    ITECareSimplifier::CareSetPtr cs2;
+    queue[e] = cs;
+
+    TNode v;
+    bool done;
+    unsigned i;
+
+    while (!queue.empty()) {
+      it = queue.end();
+      --it;
+      v = it->first;
+      cs = it->second;
+      set<Node>& css = cs.getCareSet();
+      queue.erase(v);
+
+      done = false;
+      set<Node>::iterator iCare, iCareEnd = css.end();
+
+      switch (v.getKind()) {
+        case kind::ITE: {
+          iCare = css.find(v[0]);
           if (iCare != iCareEnd) {
             Assert(substTable.find(v) == substTable.end());
-            substTable[v] = v[2];
-            updateQueue(queue, v[2], cs);
+            substTable[v] = v[1];
+            updateQueue(queue, v[1], cs);
             done = true;
             break;
           }
-        }
-        updateQueue(queue, v[0], cs);
-        cs2 = getNewSet();
-        cs2.getCareSet() = css;
-        cs2.getCareSet().insert(v[0]);
-        updateQueue(queue, v[1], cs2);
-        cs2 = getNewSet();
-        cs2.getCareSet() = css;
-        cs2.getCareSet().insert(v[0].negate());
-        updateQueue(queue, v[2], cs2);
-        done = true;
-        break;
-      }
-      case kind::AND: {
-        for (i = 0; i < v.getNumChildren(); ++i) {
-          iCare = css.find(v[i].negate());
-          if (iCare != iCareEnd) {
-            Assert(substTable.find(v) == substTable.end());
-            substTable[v] = d_false;
-            done = true;
-            break;
+          else {
+            iCare = css.find(v[0].negate());
+            if (iCare != iCareEnd) {
+              Assert(substTable.find(v) == substTable.end());
+              substTable[v] = v[2];
+              updateQueue(queue, v[2], cs);
+              done = true;
+              break;
+            }
           }
+          updateQueue(queue, v[0], cs);
+          cs2 = getNewSet();
+          cs2.getCareSet() = css;
+          cs2.getCareSet().insert(v[0]);
+          updateQueue(queue, v[1], cs2);
+          cs2 = getNewSet();
+          cs2.getCareSet() = css;
+          cs2.getCareSet().insert(v[0].negate());
+          updateQueue(queue, v[2], cs2);
+          done = true;
+          break;
         }
-        if (done) break;
-
-        Assert(v.getNumChildren() > 1);
-        updateQueue(queue, v[0], cs);
-        cs2 = getNewSet();
-        cs2.getCareSet() = css;
-        cs2.getCareSet().insert(v[0]);
-        for (i = 1; i < v.getNumChildren(); ++i) {
-          updateQueue(queue, v[i], cs2);
-        }
-        done = true;
-        break;
-      }
-      case kind::OR: {
-        for (i = 0; i < v.getNumChildren(); ++i) {
-          iCare = css.find(v[i]);
-          if (iCare != iCareEnd) {
-            Assert(substTable.find(v) == substTable.end());
-            substTable[v] = d_true;
-            done = true;
-            break;
+        case kind::AND: {
+          for (i = 0; i < v.getNumChildren(); ++i) {
+            iCare = css.find(v[i].negate());
+            if (iCare != iCareEnd) {
+              Assert(substTable.find(v) == substTable.end());
+              substTable[v] = d_false;
+              done = true;
+              break;
+            }
+          }
+          if (done) break;
+
+          Assert(v.getNumChildren() > 1);
+          updateQueue(queue, v[0], cs);
+          cs2 = getNewSet();
+          cs2.getCareSet() = css;
+          cs2.getCareSet().insert(v[0]);
+          for (i = 1; i < v.getNumChildren(); ++i) {
+            updateQueue(queue, v[i], cs2);
           }
+          done = true;
+          break;
         }
-        if (done) break;
-
-        Assert(v.getNumChildren() > 1);
-        updateQueue(queue, v[0], cs);
-        cs2 = getNewSet();
-        cs2.getCareSet() = css;
-        cs2.getCareSet().insert(v[0].negate());
-        for (i = 1; i < v.getNumChildren(); ++i) {
-          updateQueue(queue, v[i], cs2);
+        case kind::OR: {
+          for (i = 0; i < v.getNumChildren(); ++i) {
+            iCare = css.find(v[i]);
+            if (iCare != iCareEnd) {
+              Assert(substTable.find(v) == substTable.end());
+              substTable[v] = d_true;
+              done = true;
+              break;
+            }
+          }
+          if (done) break;
+
+          Assert(v.getNumChildren() > 1);
+          updateQueue(queue, v[0], cs);
+          cs2 = getNewSet();
+          cs2.getCareSet() = css;
+          cs2.getCareSet().insert(v[0].negate());
+          for (i = 1; i < v.getNumChildren(); ++i) {
+            updateQueue(queue, v[i], cs2);
+          }
+          done = true;
+          break;
         }
-        done = true;
-        break;
+        default:
+          break;
       }
-      default:
-        break;
-    }
 
-    if (done) {
-      continue;
-    }
+      if (done) {
+        continue;
+      }
 
-    for (unsigned i = 0; i < v.getNumChildren(); ++i) {
-      updateQueue(queue, v[i], cs);
+      for (unsigned i = 0; i < v.getNumChildren(); ++i) {
+        updateQueue(queue, v[i], cs);
+      }
     }
   }
+  /* Perform garbage collection. */
   while (!d_usedSets.empty()) {
-    delete d_usedSets.back();
+    CareSetPtrVal* used = d_usedSets.back();
     d_usedSets.pop_back();
+    Assert(used->safeToGarbageCollect());
+    delete used;
+    Assert(d_careSetsOutstanding > 0);
+    d_careSetsOutstanding--;
   }
 
   TNodeMap cache;
   return substitute(e, substTable, cache);
 }
 
+ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew(
+    ITECareSimplifier& simp) {
+  CareSetPtrVal* val = new CareSetPtrVal(simp);
+  return CareSetPtr(val);
+}
+
+
+
 } /* namespace theory */
 } /* namespace CVC4 */
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index 10fe2853b..3c78a8790 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -133,7 +133,7 @@ public:
 private:
   typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
   NodeCountMap d_termITEHeight;
-};
+}; /* class TermITEHeightCounter */
 
 /**
  * A routine designed to undo the potentially large blow up
@@ -177,7 +177,7 @@ private:
     ~Statistics();
   };
   Statistics d_statistics;
-};
+}; /* class ITECompressor */
 
 class ITESimplifier {
 public:
@@ -302,6 +302,15 @@ public:
 
   void clear();
 private:
+
+  /**
+   * This should always equal the number of care sets allocated by
+   * this object - the number of these that have been deleted. This is
+   * initially 0 and should always be 0 at the *start* of
+   * ~ITECareSimplifier().
+   */
+  unsigned d_careSetsOutstanding;
+
   Node d_true;
   Node d_false;
 
@@ -309,12 +318,16 @@ private:
 
   class CareSetPtr;
   class CareSetPtrVal {
+   public:
+    bool safeToGarbageCollect() const { return d_refCount == 0; }
+   private:
     friend class ITECareSimplifier::CareSetPtr;
     ITECareSimplifier& d_iteSimplifier;
     unsigned d_refCount;
     std::set<Node> d_careSet;
-    CareSetPtrVal(ITECareSimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {}
-  };
+    CareSetPtrVal(ITECareSimplifier& simp)
+        : d_iteSimplifier(simp), d_refCount(1) {}
+  }; /* class ITECareSimplifier::CareSetPtrVal */
 
   std::vector<CareSetPtrVal*> d_usedSets;
   void careSetPtrGC(CareSetPtrVal* val) {
@@ -350,16 +363,14 @@ private:
       return *this;
     }
     std::set<Node>& getCareSet() { return d_val->d_careSet; }
-    static CareSetPtr mkNew(ITECareSimplifier& simp) {
-      CareSetPtrVal* val = new CareSetPtrVal(simp);
-      return CareSetPtr(val);
-    }
+
+    static CareSetPtr mkNew(ITECareSimplifier& simp);
     static CareSetPtr recycle(CareSetPtrVal* val) {
       Assert(val != NULL && val->d_refCount == 0);
       val->d_refCount = 1;
       return CareSetPtr(val);
     }
-  };
+  }; /* class ITECareSimplifier::CareSetPtr */
 
   CareSetPtr getNewSet();