Fixed some memory cleanup and destruction issues with ContextObj, ECData, CDList, and CDMap. Added the d_underTheShotgun field to NodeManager to keep track of which NodeValue is currently being deleted. If a Node or TNode has this node value, it can always be deleted. This avoids the need for introducing SoftNodes. Currently passes Debug and Production make check

1 files changed, 12 insertions, 0 deletions

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index cbe4e718a..9f1063715 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -141,6 +141,8 @@ private:
   /** Decrement ref counts of children */
   inline void decrRefCounts();
 
+  bool isBeingDeleted() const;
+
 public:
 
   template <bool ref_count>
@@ -266,6 +268,9 @@ inline void NodeValue::decrRefCounts() {
 }
 
 inline void NodeValue::inc() {
+  Assert(!isBeingDeleted(),
+         "NodeValue is currently being deleted "
+         "and increment is being called on it. Don't Do That!");
   // FIXME multithreading
   if(EXPECT_TRUE( d_rc < MAX_RC )) {
     ++d_rc;
@@ -301,6 +306,13 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
+
+inline bool NodeValue::isBeingDeleted() const
+{
+  return NodeManager::currentNM() != NULL &&
+    NodeManager::currentNM()->isCurrentlyDeleting(this);
+}
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */