Typos and renames for code review

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e735b7f09a145ab25300beca163dcea1875c8ee2..d953907aec3f9276df419ceae5e5f3ff957ad7ea 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -113,7 +113,7 @@ void NodeManager::reclaimZombies() {
   // NodeValue's children, which may (recursively) reclaim them.
   //
   // Let's say we're reclaiming zombie NodeValue "A" and its child "B"
-  // then becomes a zombie (NodeManager::gc(B) is called).
+  // then becomes a zombie (NodeManager::markForDeletion(B) is called).
   //
   // One way to handle B's zombification would be simply to put it
   // into d_zombies.  This is what we do.  However, if we were to

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 04d2ddac73d0f51f4ed161adc1895a3ac953fa4d..83f28a84259ea4d551ccadfcea09cf53ff1fe9c9 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -106,7 +106,7 @@ class NodeManager {
   /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
-   * NodeValue.  In particular, "non-inlined" constants are permited
+   * NodeValue.  In particular, "non-inlined" constants are permitted
    * (see below).
    *
    * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
@@ -155,7 +155,7 @@ class NodeManager {
   /**
    * Register a NodeValue as a zombie.
    */
-  inline void gc(expr::NodeValue* nv) {
+  inline void markForDeletion(expr::NodeValue* nv) {
     Assert(nv->d_rc == 0);
     // if d_reclaiming is set, make sure we don't call
     // reclaimZombies(), because it's already running.
@@ -532,7 +532,7 @@ public:
 // of Expr functions, it needs to set the current NodeManager
 // correctly (and to do that it needs access to
 // ExprManager::getNodeManager()).  So, we make ExprManagerScope a
-// friend of ExprManager's, since it's implementation is simple to
+// friend of ExprManager's, since its implementation is simple to
 // read and understand (and verify that it doesn't do any mischief).
 //
 // ExprManager::getNodeManager() can't just be made public, since

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 9e8854e8f5a7eb699a1267d32a37e0026f01de7e..a998dd8e4e0fb0872706cd4d74be03a373cd5218 100644 (file)
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -296,7 +296,7 @@ inline void NodeValue::dec() {
       Assert(NodeManager::currentNM() != NULL,
              "No current NodeManager on destruction of NodeValue: "
              "maybe a public CVC4 interface function is missing a NodeManagerScope ?");
-      NodeManager::currentNM()->gc(this);
+      NodeManager::currentNM()->markForDeletion(this);
     }
   }
 }