From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 2 Oct 2010 23:53:18 +0000 (+0000)
Subject: revert a workaround fix to CDMap that was committed as part of the arith-indexed... 
X-Git-Tag: cvc5-1.0.0~8834
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=036a23f59bbc23343dc690fd1e147541e79e9b9e;p=cvc5.git

revert a workaround fix to CDMap that was committed as part of the arith-indexed-vars merge, and fix the root cause (maybe?) in attribute.cpp: previously, items from the cdnodes attribute table weren't properly being "obliterated" from the table due to a typo
---

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index b7fc5dcc6..0b75ee284 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -344,13 +344,13 @@ public:
     emptyTrash();
     Debug("gc") << "done emptying trash for " << this << std::endl;
 
-    for(Element* i = d_first; i != NULL;) {
+    for(typename table_type::iterator i = d_map.begin();
+        i != d_map.end();
+        ++i) {
       // mark it as being a destruction (short-circuit restore())
-      Element* thisOne = i;
-      i = i->next();
-      thisOne->d_map = NULL;
-      if(!thisOne->d_noTrash) {
-        thisOne->deleteSelf();
+      (*i).second->d_map = NULL;
+      if(!(*i).second->d_noTrash) {
+        (*i).second->deleteSelf();
       }
     }
     d_map.clear();
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 5aaa7393a..295244473 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -38,24 +38,12 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   deleteFromTable(d_ptrs, nv);
 
   // FIXME CD-bools in optimized table
-  for(unsigned id = 0; id < attr::LastAttributeId<bool, true>::s_id; ++id) {
-    d_cdbools.obliterate(std::make_pair(id, nv));
-  }
-  for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, true>::s_id; ++id) {
-    d_cdints.obliterate(std::make_pair(id, nv));
-  }
-  for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) {
-    d_cdtnodes.obliterate(std::make_pair(id, nv));
-  }
-  for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) {
-    d_cdnodes.obliterate(std::make_pair(id, nv));
-  }
-  for(unsigned id = 0; id < attr::LastAttributeId<std::string, true>::s_id; ++id) {
-    d_cdstrings.obliterate(std::make_pair(id, nv));
-  }
-  for(unsigned id = 0; id < attr::LastAttributeId<void*, true>::s_id; ++id) {
-    d_cdptrs.obliterate(std::make_pair(id, nv));
-  }
+  deleteFromTable(d_cdbools, nv);
+  deleteFromTable(d_cdints, nv);
+  deleteFromTable(d_cdtnodes, nv);
+  deleteFromTable(d_cdnodes, nv);
+  deleteFromTable(d_cdstrings, nv);
+  deleteFromTable(d_cdptrs, nv);
 }
 
 void AttributeManager::deleteAllAttributes() {
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 2ef34a771..0668c5f8f 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -89,6 +89,9 @@ class AttributeManager {
   template <class T>
   void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
 
+  template <class T>
+  void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv);
+
   template <class T>
   void deleteAllFromTable(AttrHash<T>& table);
 
@@ -553,6 +556,17 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
   }
 }
 
+/**
+ * Obliterate a NodeValue from a (context-dependent) attribute table.
+ */
+template <class T>
+inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table,
+                                              NodeValue* nv) {
+  for(unsigned id = 0; id < attr::LastAttributeId<T, true>::s_id; ++id) {
+    table.obliterate(std::make_pair(id, nv));
+  }
+}
+
 /**
  * Remove all attributes from the table calling the cleanup function if one is defined.
  */