Adding comments to NodeManager

Minor name changes for cleanup and hash function templates

13 files changed, 250 insertions, 170 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 62619e2b6..efd33d83b 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -45,7 +45,7 @@ namespace attr {
  * A hash function for attribute table keys.  Attribute table keys are
  * pairs, (unique-attribute-id, Node).
  */
-struct AttrHashFcn {
+struct AttrHashStrategy {
   enum { LARGE_PRIME = 32452843ul };
   std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
     return p.first * LARGE_PRIME + p.second->getId();
@@ -57,7 +57,7 @@ struct AttrHashFcn {
  * don't have to store a pair as the key, because we use a known bit
  * in [0..63] for each attribute
  */
-struct AttrHashBoolFcn {
+struct AttrHashBoolStrategy {
   std::size_t operator()(NodeValue* nv) const {
     return (size_t)nv->getId();
   }
@@ -161,7 +161,7 @@ template <class value_type>
 struct AttrHash :
     public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
                                value_type,
-                               AttrHashFcn> {
+                               AttrHashStrategy> {
 };
 
 /**
@@ -172,10 +172,10 @@ template <>
 class AttrHash<bool> :
     protected __gnu_cxx::hash_map<NodeValue*,
                                   uint64_t,
-                                  AttrHashBoolFcn> {
+                                  AttrHashBoolStrategy> {
 
   /** A "super" type, like in Java, for easy reference below. */
-  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolFcn> super;
+  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
 
   /**
    * BitAccessor allows us to return a bit "by reference."  Of course,
@@ -362,12 +362,12 @@ template <class value_type>
 class CDAttrHash :
     public CVC4::context::CDMap<std::pair<uint64_t, NodeValue*>,
                                 value_type,
-                                AttrHashFcn> {
+                                AttrHashStrategy> {
 public:
   CDAttrHash(context::Context* ctxt) :
     context::CDMap<std::pair<uint64_t, NodeValue*>,
                    value_type,
-                   AttrHashFcn>(ctxt) {
+                   AttrHashStrategy>(ctxt) {
   }
 };
 
@@ -389,99 +389,99 @@ public:
 namespace attr {
 
 /** Default cleanup for unmanaged Attribute<> */
-struct NullCleanupFcn {
-};/* struct NullCleanupFcn */
+struct NullCleanupStrategy {
+};/* struct NullCleanupStrategy */
 
 /** Default cleanup for ManagedAttribute<> */
 template <class T>
-struct ManagedAttributeCleanupFcn {
-};/* struct ManagedAttributeCleanupFcn<> */
+struct ManagedAttributeCleanupStrategy {
+};/* struct ManagedAttributeCleanupStrategy<> */
 
 /** Specialization for T* */
 template <class T>
-struct ManagedAttributeCleanupFcn<T*> {
+struct ManagedAttributeCleanupStrategy<T*> {
   static inline void cleanup(T* p) { delete p; }
-};/* struct ManagedAttributeCleanupFcn<T*> */
+};/* struct ManagedAttributeCleanupStrategy<T*> */
 
 /** Specialization for const T* */
 template <class T>
-struct ManagedAttributeCleanupFcn<const T*> {
+struct ManagedAttributeCleanupStrategy<const T*> {
   static inline void cleanup(const T* p) { delete p; }
-};/* struct ManagedAttributeCleanupFcn<const T*> */
+};/* struct ManagedAttributeCleanupStrategy<const T*> */
 
 /**
  * Helper for Attribute<> class below to determine whether a cleanup
  * is defined or not.
  */
 template <class T, class C>
-struct getCleanupFcn {
+struct getCleanupStrategy {
   typedef T value_type;
   typedef KindValueToTableValueMapping<value_type> mapping;
   static void fn(typename mapping::table_value_type t) {
     C::cleanup(mapping::convertBack(t));
   }
-};/* struct getCleanupFcn<> */
+};/* struct getCleanupStrategy<> */
 
 /**
- * Specialization for NullCleanupFcn.
+ * Specialization for NullCleanupStrategy.
  */
 template <class T>
-struct getCleanupFcn<T, NullCleanupFcn> {
+struct getCleanupStrategy<T, NullCleanupStrategy> {
   typedef T value_type;
   typedef KindValueToTableValueMapping<value_type> mapping;
   static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupFcn<T, NullCleanupFcn> */
+};/* struct getCleanupStrategy<T, NullCleanupStrategy> */
 
 // out-of-class initialization required (because it's a non-integral type)
 template <class T>
-void (*const getCleanupFcn<T, NullCleanupFcn>::fn)(typename getCleanupFcn<T, NullCleanupFcn>::mapping::table_value_type) = NULL;
+void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)(typename getCleanupStrategy<T, NullCleanupStrategy>::mapping::table_value_type) = NULL;
 
 /**
- * Specialization for ManagedAttributeCleanupFcn<T>.
+ * Specialization for ManagedAttributeCleanupStrategy<T>.
  */
 template <class T>
-struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > {
+struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > {
   typedef T value_type;
   typedef KindValueToTableValueMapping<value_type> mapping;
   static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > */
+};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */
 
 // out-of-class initialization required (because it's a non-integral type)
 template <class T>
-void (*const getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::fn)(typename getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::mapping::table_value_type) = NULL;
+void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn)(typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::mapping::table_value_type) = NULL;
 
 /**
- * Specialization for ManagedAttributeCleanupFcn<T*>.
+ * Specialization for ManagedAttributeCleanupStrategy<T*>.
  */
 template <class T>
-struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > {
+struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > {
   typedef T* value_type;
-  typedef ManagedAttributeCleanupFcn<value_type> C;
+  typedef ManagedAttributeCleanupStrategy<value_type> C;
   typedef KindValueToTableValueMapping<value_type> mapping;
   static void fn(typename mapping::table_value_type t) {
     C::cleanup(mapping::convertBack(t));
   }
-};/* struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > */
+};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */
 
 /**
- * Specialization for ManagedAttributeCleanupFcn<const T*>.
+ * Specialization for ManagedAttributeCleanupStrategy<const T*>.
  */
 template <class T>
-struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > {
+struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > {
   typedef const T* value_type;
-  typedef ManagedAttributeCleanupFcn<value_type> C;
+  typedef ManagedAttributeCleanupStrategy<value_type> C;
   typedef KindValueToTableValueMapping<value_type> mapping;
   static void fn(typename mapping::table_value_type t) {
     C::cleanup(mapping::convertBack(t));
   }
-};/* struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > */
+};/* struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > */
 
 /**
  * Cause compile-time error for improperly-instantiated
- * getCleanupFcn<>.
+ * getCleanupStrategy<>.
  */
 template <class T, class U>
-struct getCleanupFcn<T, ManagedAttributeCleanupFcn<U> >;
+struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >;
 
 }/* CVC4::expr::attr namespace */
 
@@ -533,7 +533,7 @@ std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
  *
  * @param value_t the underlying value_type for the attribute kind
  *
- * @param CleanupFcn Clean-up routine for associated values when the
+ * @param CleanupStrategy Clean-up routine for associated values when the
  * Node goes away.  Useful, e.g., for pointer-valued attributes when
  * the values are "owned" by the table.
  *
@@ -542,7 +542,7 @@ std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
  */
 template <class T,
           class value_t,
-          class CleanupFcn = attr::NullCleanupFcn,
+          class CleanupStrategy = attr::NullCleanupStrategy,
           bool context_dep = false>
 class Attribute {
   /**
@@ -582,7 +582,7 @@ public:
     typedef attr::AttributeTraits<table_value_type, context_dep> traits;
     uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
     Assert(traits::cleanup.size() == id);// sanity check
-    traits::cleanup.push_back(attr::getCleanupFcn<value_t, CleanupFcn>::fn);
+    traits::cleanup.push_back(attr::getCleanupStrategy<value_t, CleanupStrategy>::fn);
     return id;
   }
 };/* class Attribute<> */
@@ -593,8 +593,8 @@ public:
  * flag attributes with a specialized cleanup function.
  */
 /* -- doesn't work; other specialization is "more specific" ??
-template <class T, class CleanupFcn, bool context_dep>
-class Attribute<T, bool, CleanupFcn, context_dep> {
+template <class T, class CleanupStrategy, bool context_dep>
+class Attribute<T, bool, CleanupStrategy, context_dep> {
   template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
   ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
 };
@@ -604,7 +604,7 @@ class Attribute<T, bool, CleanupFcn, context_dep> {
  * An "attribute type" structure for boolean flags (special).
  */
 template <class T, bool context_dep>
-class Attribute<T, bool, attr::NullCleanupFcn, context_dep> {
+class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> {
   /** IDs for bool-valued attributes are actually bit assignments. */
   static const uint64_t s_id;
 
@@ -658,7 +658,7 @@ public:
 template <class T,
           class value_type>
 struct CDAttribute :
-    public Attribute<T, value_type, attr::NullCleanupFcn, true> {};
+    public Attribute<T, value_type, attr::NullCleanupStrategy, true> {};
 
 /**
  * This is a managed attribute kind (the only difference between
@@ -673,9 +673,9 @@ struct CDAttribute :
  */
 template <class T,
           class value_type,
-          class CleanupFcn = attr::ManagedAttributeCleanupFcn<value_type> >
+          class CleanupStrategy = attr::ManagedAttributeCleanupStrategy<value_type> >
 struct ManagedAttribute :
-    public Attribute<T, value_type, CleanupFcn, false> {};
+    public Attribute<T, value_type, CleanupStrategy, false> {};
 
 // ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
 
@@ -685,15 +685,15 @@ struct ManagedAttribute :
 // "cleanup" vector before registerAttribute() is called.  This is
 // important because otherwise the vector is initialized later,
 // clearing the first-pushed cleanup function.
-template <class T, class value_t, class CleanupFcn, bool context_dep>
-const uint64_t Attribute<T, value_t, CleanupFcn, context_dep>::s_id =
+template <class T, class value_t, class CleanupStrategy, bool context_dep>
+const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
   ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(),
-    Attribute<T, value_t, CleanupFcn, context_dep>::registerAttribute() );
+    Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
 
 /** Assign unique IDs to attributes at load time. */
 template <class T, bool context_dep>
-const uint64_t Attribute<T, bool, attr::NullCleanupFcn, context_dep>::s_id =
-  Attribute<T, bool, attr::NullCleanupFcn, context_dep>::registerAttribute();
+const uint64_t Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::s_id =
+  Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::registerAttribute();
 
 // ATTRIBUTE MANAGER ===========================================================
 
@@ -800,7 +800,7 @@ public:
    * @return true if the given node has the given attribute
    */
   template <class AttrKind>
-  bool hasAttribute(NodeValue* nv,
+  bool getAttribute(NodeValue* nv,
                     const AttrKind&,
                     typename AttrKind::value_type& ret) const;
 
@@ -1033,7 +1033,7 @@ struct HasAttribute<true, AttrKind> {
    * This implementation returns the AttrKind's default value if the
    * Node doesn't have the given attribute.
    */
-  static inline bool hasAttribute(const AttributeManager* am,
+  static inline bool getAttribute(const AttributeManager* am,
                                   NodeValue* nv,
                                   typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
@@ -1075,7 +1075,7 @@ struct HasAttribute<false, AttrKind> {
     return true;
   }
 
-  static inline bool hasAttribute(const AttributeManager* am,
+  static inline bool getAttribute(const AttributeManager* am,
                                   NodeValue* nv,
                                   typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
@@ -1102,10 +1102,10 @@ bool AttributeManager::hasAttribute(NodeValue* nv,
 }
 
 template <class AttrKind>
-bool AttributeManager::hasAttribute(NodeValue* nv,
+bool AttributeManager::getAttribute(NodeValue* nv,
                                     const AttrKind&,
                                     typename AttrKind::value_type& ret) const {
-  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, nv, ret);
+  return HasAttribute<AttrKind::has_default_value, AttrKind>::getAttribute(this, nv, ret);
 }
 
 template <class AttrKind>
diff --git a/src/expr/node.h b/src/expr/node.h
index f7cef5a4c..ebe06ead2 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -288,7 +288,7 @@ public:
    * @return true if this node has the requested attribute
    */
   template <class AttrKind>
-  inline bool hasAttribute(const AttrKind& attKind,
+  inline bool getAttribute(const AttrKind& attKind,
                            typename AttrKind::value_type& value) const;
 
   /**
@@ -410,7 +410,7 @@ inline std::ostream& operator<<(std::ostream& out, const Node& node) {
 namespace CVC4 {
 
 // for hash_maps, hash_sets..
-struct NodeHashFcn {
+struct NodeHashFunction {
   size_t operator()(const CVC4::Node& node) const {
     return (size_t) node.getId();
   }
@@ -443,12 +443,12 @@ hasAttribute(const AttrKind&) const {
 
 template <bool ref_count>
 template <class AttrKind>
-inline bool NodeTemplate<ref_count>::hasAttribute(const AttrKind&,
+inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
                                                   typename AttrKind::value_type& ret) const {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-  return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
+  return NodeManager::currentNM()->getAttribute(*this, AttrKind(), ret);
 }
 
 template <bool ref_count>
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 044deac7f..5e6d431b6 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -45,42 +45,40 @@ struct Type {};
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarName, std::string> VarNameAttr;
-typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupFcn> TypeAttr;
+typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupStrategy> TypeAttr;
 
 }/* CVC4::expr namespace */
 
 class NodeManager {
-  static __thread NodeManager* s_current;
-
   template <class Builder> friend class CVC4::NodeBuilderBase;
+  friend class NodeManagerScope;
+  friend class expr::NodeValue;
 
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValueInternalHashFcn,
+                              expr::NodeValueInternalHashFunction,
                               expr::NodeValue::NodeValueEq> NodeValuePool;
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValueIDHashFcn,
+                              expr::NodeValueIDHashFunction,
                               expr::NodeValue::NodeValueEq> ZombieSet;
 
+  static __thread NodeManager* s_current;
+
   NodeValuePool d_nodeValuePool;
 
   expr::attr::AttributeManager d_attrManager;
+  expr::NodeValue* d_underTheShotgun;
+
+  bool d_reclaiming;
+  ZombieSet d_zombies;
 
   expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
   void poolInsert(expr::NodeValue* nv);
   void poolRemove(expr::NodeValue* nv);
 
-  friend class NodeManagerScope;
-  friend class expr::NodeValue;
-
   bool isCurrentlyDeleting(const expr::NodeValue *nv) const{
     return d_underTheShotgun == nv;
   }
 
-  expr::NodeValue* d_underTheShotgun;
-
-  bool d_reclaiming;
-  ZombieSet d_zombies;
-
   /**
    * Register a NodeValue as a zombie.
    */
@@ -114,70 +112,147 @@ public:
     d_underTheShotgun(NULL),
     d_reclaiming(false)
 
-  {
+  { // static initialization
     poolInsert( &expr::NodeValue::s_null );
   }
 
   ~NodeManager();
 
+  /** The node manager in the current context. */
   static NodeManager* currentNM() { return s_current; }
 
   // general expression-builders
+  /** Create a node with no children. */
   Node mkNode(Kind kind);
+
+  /** Create a node with one child. */
   Node mkNode(Kind kind, TNode child1);
+
+  /** Create a node with two children. */
   Node mkNode(Kind kind, TNode child1, TNode child2);
+
+  /** Create a node with three children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
+
+  /** Create a node with four children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4);
+
+  /** Create a node with five children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5);
-  // N-ary version
+
+  /** Create a node with an arbitrary number of children. */
   Node mkNode(Kind kind, const std::vector<Node>& children);
 
-  // variables are special, because duplicates are permitted
+  // NOTE: variables are special, because duplicates are permitted
+
+  /** Create a variable with the given type and name. */
   Node mkVar(Type* type, const std::string& name);
+
+  /** Create a variable with the given type. */
   Node mkVar(Type* type);
+
+  /** Create a variable of unknown type (?). */
   Node mkVar();
 
+  /** Retrieve an attribute for a node.
+   *
+   * @param nv the node value
+   * @param attr an instance of the attribute kind to retrieve.
+   * @returns the attribute, if set, or a default-constructed
+   * <code>AttrKind::value_type</code> if not.
+   */
   template <class AttrKind>
   inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
-                                                    const AttrKind&) const;
-
-  // Note that there are two, distinct hasAttribute() declarations for
-  // a reason (rather than using a pointer-valued argument with a
-  // default value): they permit more optimized code in the underlying
-  // hasAttribute() implementations.
-
+                                                    const AttrKind& attr) const;
+
+  /* NOTE: there are two, distinct hasAttribute() declarations for
+   a reason (rather than using a pointer-valued argument with a
+   default value): they permit more optimized code in the underlying
+   hasAttribute() implementations. */
+
+  /** Check whether an attribute is set for a node.
+   *
+   * @param nv the node value
+   * @param attr an instance of the attribute kind to check
+   * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+   */
   template <class AttrKind>
   inline bool hasAttribute(expr::NodeValue* nv,
-                           const AttrKind&) const;
-
+                           const AttrKind& attr) const;
+
+  /** Check whether an attribute is set for a node.
+   *
+   * @param nv the node value
+   * @param attr an instance of the attribute kind to check
+   * @param value a reference to an object of the attribute's value type.
+   * <code>value</code> will be set to the value of the attribute, if it is
+   * set for <code>nv</code>; otherwise, it will be set to the default value of
+   * the attribute.
+   * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+   */
   template <class AttrKind>
-  inline bool hasAttribute(expr::NodeValue* nv,
-                           const AttrKind&,
-                           typename AttrKind::value_type&) const;
-
+  inline bool getAttribute(expr::NodeValue* nv,
+                           const AttrKind& attr,
+                           typename AttrKind::value_type& value) const;
+
+  /** Set an attribute for a node.
+    *
+    * @param nv the node value
+    * @param attr an instance of the attribute kind to set
+    * @param value the value of <code>attr</code> for <code>nv</code>
+    */
   template <class AttrKind>
   inline void setAttribute(expr::NodeValue* nv,
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
 
+  /** Retrieve an attribute for a TNode.
+   *
+   * @param n the node
+   * @param attr an instance of the attribute kind to retrieve.
+   * @returns the attribute, if set, or a default-constructed
+   * <code>AttrKind::value_type</code> if not.
+   */
   template <class AttrKind>
   inline typename AttrKind::value_type getAttribute(TNode n,
                                                     const AttrKind&) const;
 
-  // Note that there are two, distinct hasAttribute() declarations for
-  // a reason (rather than using a pointer-valued argument with a
-  // default value): they permit more optimized code in the underlying
-  // hasAttribute() implementations.
+  /* NOTE: there are two, distinct hasAttribute() declarations for
+   a reason (rather than using a pointer-valued argument with a
+   default value): they permit more optimized code in the underlying
+   hasAttribute() implementations. */
 
+  /** Check whether an attribute is set for a TNode.
+   *
+   * @param n the node
+   * @param attr an instance of the attribute kind to check
+   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+   */
   template <class AttrKind>
   inline bool hasAttribute(TNode n,
-                           const AttrKind&) const;
-
+                           const AttrKind& attr) const;
+
+  /** Check whether an attribute is set for a TNode.
+   *
+   * @param n the node
+   * @param attr an instance of the attribute kind to check
+   * @param value a reference to an object of the attribute's value type.
+   * <code>value</code> will be set to the value of the attribute, if it is
+   * set for <code>nv</code>; otherwise, it will be set to the default value of
+   * the attribute.
+   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+   */
   template <class AttrKind>
-  inline bool hasAttribute(TNode n,
-                           const AttrKind&,
-                           typename AttrKind::value_type&) const;
-
+  inline bool getAttribute(TNode n,
+                           const AttrKind& attr,
+                           typename AttrKind::value_type& value) const;
+
+  /** Set an attribute for a TNode.
+    *
+    * @param n the node
+    * @param attr an instance of the attribute kind to set
+    * @param value the value of <code>attr</code> for <code>n</code>
+    */
   template <class AttrKind>
   inline void setAttribute(TNode n,
                            const AttrKind&,
@@ -203,30 +278,36 @@ public:
   /** Make a new sort with the given name. */
   inline Type* mkSort(const std::string& name) const;
 
+  /** Get the type for the given node.
+   *
+   * TODO: Does this call compute the type if it's not already available?
+   */
   inline Type* getType(TNode n) const;
 };
 
 /**
- * Resource-acquisition-is-instantiation C++ idiom: create one of
- * these "scope" objects to temporarily change the thread-specific
- * notion of the "current" NodeManager for Node creation/deletion,
- * etc.  On destruction, the previous NodeManager pointer is restored.
- * Therefore such objects should only be created and destroyed in a
- * well-scoped manner (such as on the stack).
+ * This class changes the "current" thread-global
+ * <code>NodeManager</code> when it is created and reinstates the
+ * previous thread-global <code>NodeManager</code> when it is
+ * destroyed, effectively maintaining a set of nested
+ * <code>NodeManager</code> scopes.  This is especially useful on
+ * public-interface calls into the CVC4 library, where CVC4's notion
+ * of the "current" <code>NodeManager</code> should be set to match
+ * the calling context.  See, for example, the implementations of
+ * public calls in the <code>ExprManager</code> and
+ * <code>SmtEngine</code> classes.
  *
- * This is especially useful on public-interface calls into the CVC4
- * library, where CVC4's notion of the "current" NodeManager should be
- * set to match the calling context.  See, for example, the
- * implementations of public calls in the ExprManager and SmtEngine
- * classes.
- *
- * You may create a NodeManagerScope with "new" and destroy it with
- * "delete", or place it as a data member of an object that is, but if
- * the scope of these new/delete pairs isn't properly maintained, the
- * incorrect "current" NodeManager pointer may be restored after a
- * delete.
+ * The client must be careful to create and destroy
+ * <code>NodeManagerScope</code> objects in a well-nested manner (such
+ * as on the stack). You may create a <code>NodeManagerScope</code>
+ * with <code>new</code> and destroy it with <code>delete</code>, or
+ * place it as a data member of an object that is, but if the scope of
+ * these <code>new</code>/<code>delete</code> pairs isn't properly
+ * maintained, the incorrect "current" <code>NodeManager</code>
+ * pointer may be restored after a delete.
  */
 class NodeManagerScope {
+  /** The old NodeManager, to be restored on destruction. */
   NodeManager *d_oldNodeManager;
 
 public:
@@ -243,18 +324,14 @@ public:
 };
 
 /**
- * A wrapper (essentially) for NodeManagerScope.  The current
- * "NodeManager" pointer is set to this Expr's underlying
- * ExpressionManager's NodeManager.  When the ExprManagerScope is
- * destroyed, the previous NodeManager is restored.
- *
- * This is especially useful on public-interface calls into the CVC4
- * library, where CVC4's notion of the "current" NodeManager should be
- * set to match the calling context.  See, for example, the
- * implementations of public calls in the Expr class.
- *
- * Without this, we'd need Expr to be a friend of ExprManager.
+ * Creates
+ * a <code>NodeManagerScope</code> with the underlying <code>NodeManager</code>
+ * of a given <code>Expr</code> or <code>ExprManager</code>.
+ * The <code>NodeManagerScope</code> is destroyed when the <code>ExprManagerScope</code>
+ * is destroyed. See <code>NodeManagerScope</code> for more information.
  */
+// NOTE: Without this, we'd need Expr to be a friend of ExprManager.
+// [chris 3/25/2010] Why?
 class ExprManagerScope {
   NodeManagerScope d_nms;
 public:
@@ -263,6 +340,9 @@ public:
           ? NodeManager::currentNM()
           : e.getExprManager()->getNodeManager()) {
   }
+  inline ExprManagerScope(const ExprManager& exprManager) :
+    d_nms(exprManager.getNodeManager()) {
+  }
 };
 
 template <class AttrKind>
@@ -278,10 +358,10 @@ inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
 }
 
 template <class AttrKind>
-inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
+inline bool NodeManager::getAttribute(expr::NodeValue* nv,
                                       const AttrKind&,
                                       typename AttrKind::value_type& ret) const {
-  return d_attrManager.hasAttribute(nv, AttrKind(), ret);
+  return d_attrManager.getAttribute(nv, AttrKind(), ret);
 }
 
 template <class AttrKind>
@@ -304,10 +384,10 @@ inline bool NodeManager::hasAttribute(TNode n,
 }
 
 template <class AttrKind>
-inline bool NodeManager::hasAttribute(TNode n,
+inline bool NodeManager::getAttribute(TNode n,
                                       const AttrKind&,
                                       typename AttrKind::value_type& ret) const {
-  return d_attrManager.hasAttribute(n.d_nv, AttrKind(), ret);
+  return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
 }
 
 template <class AttrKind>
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 7a4263d8a..840f41143 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -41,7 +41,7 @@ void NodeValue::toStream(std::ostream& out) const {
     string s;
     // conceptually "this" is const, and hasAttribute() doesn't change
     // its argument, but it requires a non-const key arg (for now)
-    if(NodeManager::currentNM()->hasAttribute(const_cast<NodeValue*>(this),
+    if(NodeManager::currentNM()->getAttribute(const_cast<NodeValue*>(this),
                                               VarNameAttr(), s)) {
       out << s;
     } else {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 9f1063715..995a63180 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -231,16 +231,16 @@ public:
  * PERFORMING for other uses!  NodeValue::internalHash() will lead to
  * collisions for all VARIABLEs.
  */
-struct NodeValueInternalHashFcn {
+struct NodeValueInternalHashFunction {
   inline size_t operator()(const NodeValue* nv) const {
     return (size_t) nv->internalHash();
   }
-};/* struct NodeValueHashFcn */
+};/* struct NodeValueInternalHashFunction */
 
 /**
  * For hash_maps, hash_sets, etc.
  */
-struct NodeValueIDHashFcn {
+struct NodeValueIDHashFunction {
   inline size_t operator()(const NodeValue* nv) const {
     return (size_t) nv->getId();
   }
diff --git a/src/expr/type.h b/src/expr/type.h
index fd9ea01d7..b406bfd76 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -28,7 +28,7 @@ namespace CVC4 {
 
 namespace expr {
   namespace attr {
-    struct TypeCleanupFcn;
+    struct TypeCleanupStrategy;
   }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 
@@ -116,7 +116,7 @@ protected:
   }
 
   friend class ::CVC4::NodeManager;
-  friend struct ::CVC4::expr::attr::TypeCleanupFcn;
+  friend struct ::CVC4::expr::attr::TypeCleanupStrategy;
 };
 
 /**
@@ -254,7 +254,7 @@ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
 namespace expr {
 namespace attr {
 
-struct TypeCleanupFcn {
+struct TypeCleanupStrategy {
   static void cleanup(Type* t) {
     // reference-count the Type
     t->dec();
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 4ab2fb521..3bcc080bd 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -26,7 +26,7 @@
 namespace CVC4 {
 namespace parser {
 
-struct StringHashFcn {
+struct StringHashFunction {
   size_t operator()(const std::string& str) const {
     return __gnu_cxx::hash<const char*>()(str.c_str());
   }
@@ -41,7 +41,7 @@ class SymbolTable {
 private:
 
   /** The name to expression bindings */
-  typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFcn>
+  typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFunction>
   LookupTable;
 
   /** The table iterator */
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 7d7912e10..7a05c618a 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -46,11 +46,11 @@ private:
   SatSolver *d_satSolver;
 
   /** Cache of what literal have been registered to a node. */
-  typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFcn> TranslationCache;
+  typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache;
   TranslationCache d_translationCache;
 
   /** Cache of what nodes have been registered to a literal. */
-  typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFcn> NodeCache;
+  typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
   NodeCache d_nodeCache;
 
 protected:
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 7844008e8..93e95eedf 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -73,7 +73,7 @@ class SatSolver {
 public:
 
   /** Hash function for literals */
-  struct SatLiteralHashFcn {
+  struct SatLiteralHashFunction {
     inline size_t operator()(const SatLiteral& literal) const;
   };
 
@@ -136,7 +136,7 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
 }
 
 inline size_t
-SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const {
+SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const {
   return (size_t) minisat::toInt(literal);
 }
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ee3cb4734..cd477a910 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -54,7 +54,7 @@ void TheoryUF::registerTerm(TNode n){
 
   ECData* ecN;
 
-  if(n.hasAttribute(ECAttr(), ecN)){
+  if(n.getAttribute(ECAttr(), ecN)){
     /* registerTerm(n) is only called when a node has not been seen in the
      * current context.  ECAttr() is not a context-dependent attribute.
      * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index ccbfa327a..9e57311b5 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -182,7 +182,7 @@ private:
  * Cleanup function for ECData. This will be used for called whenever
  * a ECAttr is being destructed.
  */
-struct ECCleanupFcn{
+struct ECCleanupStrategy{
   static void cleanup(ECData* ec){
     Debug("ufgc") << "cleaning up ECData " << ec << "\n";
     ec->deleteSelf();
@@ -195,7 +195,7 @@ struct EquivClass;
 /**
  * ECAttr is the attribute that maps a node to an equivalence class.
  */
-typedef expr::Attribute<EquivClass, ECData*, ECCleanupFcn > ECAttr;
+typedef expr::Attribute<EquivClass, ECData*, ECCleanupStrategy > ECAttr;
 
 } /* CVC4::theory::uf namespace */
 } /* CVC4::theory namespace */
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 12ecd347a..6125881df 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -74,9 +74,9 @@ public:
     MyData* data;
     MyData* data1;
     MyDataAttribute attr;
-    TS_ASSERT(!node->hasAttribute(attr, data));
+    TS_ASSERT(!node->getAttribute(attr, data));
     node->setAttribute(attr, new MyData());
-    TS_ASSERT(node->hasAttribute(attr, data1));
+    TS_ASSERT(node->getAttribute(attr, data1));
     TS_ASSERT(MyData::count == 1);
     delete node;
   }
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 7a0e538f6..d0c74c771 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -128,13 +128,13 @@ public:
     // test two-arg version of hasAttribute()
     bool bb;
     Debug("boolattr", "get flag 1 on a (should be F)\n");
-    TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb));
+    TS_ASSERT(a.getAttribute(TestFlag1cd(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 1 on b (should be F)\n");
-    TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb));
+    TS_ASSERT(b.getAttribute(TestFlag1cd(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 1 on c (should be F)\n");
-    TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb));
+    TS_ASSERT(c.getAttribute(TestFlag1cd(), bb));
     TS_ASSERT(! bb);
 
     // setting boolean flags
@@ -313,68 +313,68 @@ public:
     // test two-arg version of hasAttribute()
     bool bb;
     Debug("boolattr", "get flag 1 on a (should be F)\n");
-    TS_ASSERT(a.hasAttribute(TestFlag1(), bb));
+    TS_ASSERT(a.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 1 on b (should be F)\n");
-    TS_ASSERT(b.hasAttribute(TestFlag1(), bb));
+    TS_ASSERT(b.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 1 on c (should be F)\n");
-    TS_ASSERT(c.hasAttribute(TestFlag1(), bb));
+    TS_ASSERT(c.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 1 on unnamed (should be F)\n");
-    TS_ASSERT(unnamed.hasAttribute(TestFlag1(), bb));
+    TS_ASSERT(unnamed.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);
 
     Debug("boolattr", "get flag 2 on a (should be F)\n");
-    TS_ASSERT(a.hasAttribute(TestFlag2(), bb));
+    TS_ASSERT(a.getAttribute(TestFlag2(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 2 on b (should be F)\n");
-    TS_ASSERT(b.hasAttribute(TestFlag2(), bb));
+    TS_ASSERT(b.getAttribute(TestFlag2(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 2 on c (should be F)\n");
-    TS_ASSERT(c.hasAttribute(TestFlag2(), bb));
+    TS_ASSERT(c.getAttribute(TestFlag2(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
-    TS_ASSERT(unnamed.hasAttribute(TestFlag2(), bb));
+    TS_ASSERT(unnamed.getAttribute(TestFlag2(), bb));
     TS_ASSERT(! bb);
 
     Debug("boolattr", "get flag 3 on a (should be F)\n");
-    TS_ASSERT(a.hasAttribute(TestFlag3(), bb));
+    TS_ASSERT(a.getAttribute(TestFlag3(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 3 on b (should be F)\n");
-    TS_ASSERT(b.hasAttribute(TestFlag3(), bb));
+    TS_ASSERT(b.getAttribute(TestFlag3(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 3 on c (should be F)\n");
-    TS_ASSERT(c.hasAttribute(TestFlag3(), bb));
+    TS_ASSERT(c.getAttribute(TestFlag3(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 3 on unnamed (should be F)\n");
-    TS_ASSERT(unnamed.hasAttribute(TestFlag3(), bb));
+    TS_ASSERT(unnamed.getAttribute(TestFlag3(), bb));
     TS_ASSERT(! bb);
 
     Debug("boolattr", "get flag 4 on a (should be F)\n");
-    TS_ASSERT(a.hasAttribute(TestFlag4(), bb));
+    TS_ASSERT(a.getAttribute(TestFlag4(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 4 on b (should be F)\n");
-    TS_ASSERT(b.hasAttribute(TestFlag4(), bb));
+    TS_ASSERT(b.getAttribute(TestFlag4(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 4 on c (should be F)\n");
-    TS_ASSERT(c.hasAttribute(TestFlag4(), bb));
+    TS_ASSERT(c.getAttribute(TestFlag4(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 4 on unnamed (should be F)\n");
-    TS_ASSERT(unnamed.hasAttribute(TestFlag4(), bb));
+    TS_ASSERT(unnamed.getAttribute(TestFlag4(), bb));
     TS_ASSERT(! bb);
 
     Debug("boolattr", "get flag 5 on a (should be F)\n");
-    TS_ASSERT(a.hasAttribute(TestFlag5(), bb));
+    TS_ASSERT(a.getAttribute(TestFlag5(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 5 on b (should be F)\n");
-    TS_ASSERT(b.hasAttribute(TestFlag5(), bb));
+    TS_ASSERT(b.getAttribute(TestFlag5(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 5 on c (should be F)\n");
-    TS_ASSERT(c.hasAttribute(TestFlag5(), bb));
+    TS_ASSERT(c.getAttribute(TestFlag5(), bb));
     TS_ASSERT(! bb);
     Debug("boolattr", "get flag 5 on unnamed (should be F)\n");
-    TS_ASSERT(unnamed.hasAttribute(TestFlag5(), bb));
+    TS_ASSERT(unnamed.getAttribute(TestFlag5(), bb));
     TS_ASSERT(! bb);
 
     // setting boolean flags