Reorder NodeValue class according to our code style guidelines. (#3374)

2 files changed, 171 insertions, 160 deletions

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index d7faf0814..ef1cd966e 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -78,5 +78,19 @@ void NodeValue::printAst(std::ostream& out, int ind) const {
   out << ')';
 }
 
+NodeValue::iterator<NodeTemplate<true> > operator+(
+    NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+    NodeValue::iterator<NodeTemplate<true> > i)
+{
+  return i + p;
+}
+
+NodeValue::iterator<NodeTemplate<false> > operator+(
+    NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+    NodeValue::iterator<NodeTemplate<false> > i)
+{
+  return i + p;
+}
+
 } /* CVC4::expr namespace */
 } /* CVC4 namespace */
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 0174bdd15..bd26d22fc 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -69,43 +69,13 @@ namespace expr {
 /**
  * This is a NodeValue.
  */
-class NodeValue {
-  static const uint32_t NBITS_REFCOUNT =
-      CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
-  static const uint32_t NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND;
-  static const uint32_t NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID;
-  static const uint32_t NBITS_NCHILDREN =
-      CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
-
-  /** Maximum reference count possible.  Used for sticky
-   *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
-  static const uint32_t MAX_RC = (((uint32_t)1) << NBITS_REFCOUNT) - 1;
-
-  /** A mask for d_kind */
-  static const uint32_t kindMask = (((uint32_t)1) << NBITS_KIND) - 1;
-
-  // This header fits into 96 bits
-
-  /** The ID (0 is reserved for the null value) */
-  uint64_t d_id        : NBITS_ID;
-
-  /** The expression's reference count.  @see cvc4::Node. */
-  uint32_t d_rc : NBITS_REFCOUNT;
-
-  /** Kind of the expression */
-  uint32_t d_kind : NBITS_KIND;
-
-  /** Number of children */
-  uint32_t d_nchildren : NBITS_NCHILDREN;
-
-  /** Variable number of child nodes */
-  NodeValue* d_children[0];
-
-  // todo add exprMgr ref in debug case
-
-  template <bool> friend class ::CVC4::NodeTemplate;
+class NodeValue
+{
+  template <bool>
+  friend class ::CVC4::NodeTemplate;
   friend class ::CVC4::TypeNode;
-  template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder;
+  template <unsigned nchild_thresh>
+  friend class ::CVC4::NodeBuilder;
   friend class ::CVC4::NodeManager;
 
   template <Kind k, bool pool>
@@ -116,34 +86,19 @@ class NodeValue {
 
   friend void ::CVC4::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
 
-  void inc();
-  void dec();
-
-  // Returns true if the reference count is maximized.
-  inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; }
+  friend class RefCountGuard;
 
-  /**
-   * Uninitializing constructor for NodeBuilder's use.
-   */
-  NodeValue() { /* do not initialize! */ }
-
-private:
-  /** Private constructor for the null value. */
-  NodeValue(int);
+  /* ------------------------------------------------------------------------ */
+ public:
+  /* ------------------------------------------------------------------------ */
 
   typedef NodeValue** nv_iterator;
   typedef NodeValue const* const* const_nv_iterator;
 
-  nv_iterator nv_begin();
-  nv_iterator nv_end();
-
-  const_nv_iterator nv_begin() const;
-  const_nv_iterator nv_end() const;
-
   template <class T>
-  class iterator {
-    const_nv_iterator d_i;
-  public:
+  class iterator
+  {
+   public:
     typedef std::random_access_iterator_tag iterator_category;
     typedef T value_type;
     typedef std::ptrdiff_t difference_type;
@@ -153,83 +108,83 @@ private:
     iterator() : d_i(NULL) {}
     explicit iterator(const_nv_iterator i) : d_i(i) {}
 
-    // conversion of a TNode iterator to a Node iterator
-    inline operator NodeValue::iterator<NodeTemplate<true> >() {
+    /** Conversion of a TNode iterator to a Node iterator. */
+    inline operator NodeValue::iterator<NodeTemplate<true> >()
+    {
       return iterator<NodeTemplate<true> >(d_i);
     }
 
     inline T operator*() const;
 
-    bool operator==(const iterator& i) const {
-      return d_i == i.d_i;
-    }
+    bool operator==(const iterator& i) const { return d_i == i.d_i; }
 
-    bool operator!=(const iterator& i) const {
-      return d_i != i.d_i;
-    }
+    bool operator!=(const iterator& i) const { return d_i != i.d_i; }
 
-    iterator& operator++() {
+    iterator& operator++()
+    {
       ++d_i;
       return *this;
     }
 
-    iterator operator++(int) {
-      return iterator(d_i++);
-    }
+    iterator operator++(int) { return iterator(d_i++); }
 
-    iterator& operator--() {
+    iterator& operator--()
+    {
       --d_i;
       return *this;
     }
 
-    iterator operator--(int) {
-      return iterator(d_i--);
-    }
+    iterator operator--(int) { return iterator(d_i--); }
 
-    iterator& operator+=(difference_type p) {
+    iterator& operator+=(difference_type p)
+    {
       d_i += p;
       return *this;
     }
 
-    iterator& operator-=(difference_type p) {
+    iterator& operator-=(difference_type p)
+    {
       d_i -= p;
       return *this;
     }
 
-    iterator operator+(difference_type p) {
-      return iterator(d_i + p);
-    }
+    iterator operator+(difference_type p) { return iterator(d_i + p); }
 
-    iterator operator-(difference_type p) {
-      return iterator(d_i - p);
-    }
+    iterator operator-(difference_type p) { return iterator(d_i - p); }
 
-    difference_type operator-(iterator i) {
-      return d_i - i.d_i;
-    }
-  };/* class NodeValue::iterator<T> */
+    difference_type operator-(iterator i) { return d_i - i.d_i; }
 
-  // operator+ (as a function) cannot be a template, so we have to
-  // define two versions
-  friend NodeValue::iterator<NodeTemplate<true> >
-  operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
-            NodeValue::iterator<NodeTemplate<true> > i);
-  friend NodeValue::iterator<NodeTemplate<false> >
-  operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
-            NodeValue::iterator<NodeTemplate<false> > i);
+   private:
+    const_nv_iterator d_i;
 
-  /** Decrement ref counts of children */
-  inline void decrRefCounts();
+  }; /* class NodeValue::iterator<T> */
 
-  bool isBeingDeleted() const;
+  uint64_t getId() const { return d_id; }
 
-public:
+  Kind getKind() const { return dKindToKind(d_kind); }
 
-  template <typename T>
-  inline iterator<T> begin() const;
+  kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
 
-  template <typename T>
-  inline iterator<T> end() const;
+  uint32_t getNumChildren() const
+  {
+    return (getMetaKind() == kind::metakind::PARAMETERIZED) ? d_nchildren - 1
+                                                            : d_nchildren;
+  }
+
+  unsigned getRefCount() const { return d_rc; }
+
+  NodeValue* getOperator() const;
+  NodeValue* getChild(int i) const;
+
+  /** If this is a CONST_* Node, extract the constant from it.  */
+  template <class T>
+  inline const T& getConst() const;
+
+  static inline NodeValue& null()
+  {
+    static NodeValue* s_null = new NodeValue(0);
+    return *s_null;
+  }
 
   /**
    * Hash this NodeValue.  For hash_maps, hash_sets, etc.. but this is
@@ -238,39 +193,24 @@ public:
    * collisions for all VARIABLEs.
    * @return the hash value of this expression.
    */
-  size_t poolHash() const {
-    if(getMetaKind() == kind::metakind::CONSTANT) {
+  size_t poolHash() const
+  {
+    if (getMetaKind() == kind::metakind::CONSTANT)
+    {
       return kind::metakind::NodeValueCompare::constHash(this);
     }
 
     size_t hash = d_kind;
     const_nv_iterator i = nv_begin();
     const_nv_iterator i_end = nv_end();
-    while(i != i_end) {
+    while (i != i_end)
+    {
       hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
       ++i;
     }
     return hash;
   }
 
-  uint64_t getId() const { return d_id; }
-
-  Kind getKind() const { return dKindToKind(d_kind); }
-
-  kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
-
-  uint32_t getNumChildren() const
-  {
-    return (getMetaKind() == kind::metakind::PARAMETERIZED) ? d_nchildren - 1
-                                                            : d_nchildren;
-  }
-
-  unsigned getRefCount() const { return d_rc; }
-
-  std::string toString() const;
-  void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
-                OutputLanguage = language::output::LANG_AUTO) const;
-
   static inline uint32_t kindToDKind(Kind k)
   {
     return ((uint32_t)k) & kindMask;
@@ -281,23 +221,24 @@ public:
     return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }
 
-  static inline NodeValue& null() {
-    static NodeValue* s_null = new NodeValue(0);
-    return *s_null;
-  }
-
-  /**
-   * If this is a CONST_* Node, extract the constant from it.
-   */
-  template <class T>
-  inline const T& getConst() const;
+  std::string toString() const;
 
-  NodeValue* getOperator() const;
-  NodeValue* getChild(int i) const;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                bool types = false,
+                size_t dag = 1,
+                OutputLanguage = language::output::LANG_AUTO) const;
 
   void printAst(std::ostream& out, int indent = 0) const;
 
-private:
+  template <typename T>
+  inline iterator<T> begin() const;
+  template <typename T>
+  inline iterator<T> end() const;
+
+  /* ------------------------------------------------------------------------ */
+ private:
+  /* ------------------------------------------------------------------------ */
 
   /**
    * RAII guard that increases the reference count if the reference count to be
@@ -305,63 +246,119 @@ private:
    * reference count to avoid maxing out the d_rc field. This is only for low
    * level functions.
    */
-  class RefCountGuard {
-    NodeValue* d_nv;
-    bool d_increased;
-  public:
-    RefCountGuard(const NodeValue* nv) :
-      d_nv(const_cast<NodeValue*>(nv)) {
+  class RefCountGuard
+  {
+   public:
+    RefCountGuard(const NodeValue* nv) : d_nv(const_cast<NodeValue*>(nv))
+    {
       d_increased = (d_nv->d_rc == 0);
-      if(d_increased) {
+      if (d_increased)
+      {
         d_nv->d_rc = 1;
       }
     }
-    ~RefCountGuard() {
+    ~RefCountGuard()
+    {
       // dec() without marking for deletion: we don't want to garbage
       // collect this NodeValue if ours is the last reference to it.
       // E.g., this can happen when debugging code calls the print
       // routines below.  As RefCountGuards are scoped on the stack,
       // this should be fine---but not in multithreaded contexts!
-      if(d_increased) {
+      if (d_increased)
+      {
         --d_nv->d_rc;
       }
     }
-  };/* NodeValue::RefCountGuard */
 
-  friend class RefCountGuard;
+   private:
+    NodeValue* d_nv;
+    bool d_increased;
+  }; /* NodeValue::RefCountGuard */
+
+  /* ------------------------------ Header ---------------------------------- */
+  static const uint32_t NBITS_REFCOUNT =
+      CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
+  static const uint32_t NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+  static const uint32_t NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID;
+  static const uint32_t NBITS_NCHILDREN =
+      CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+
+  /** Maximum reference count possible.  Used for sticky
+   *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
+  static const uint32_t MAX_RC = (((uint32_t)1) << NBITS_REFCOUNT) - 1;
+
+  /** A mask for d_kind */
+  static const uint32_t kindMask = (((uint32_t)1) << NBITS_KIND) - 1;
+  /* ------------------- This header fits into 96 bits ---------------------- */
+
+  /** Uninitializing constructor for NodeBuilder's use.  */
+  NodeValue()
+  { /* do not initialize! */
+  }
+  /** Private constructor for the null value. */
+  NodeValue(int);
+
+  void inc();
+  void dec();
+
+  /** Decrement ref counts of children */
+  inline void decrRefCounts();
+
+  bool isBeingDeleted() const;
+
+  /** Returns true if the reference count is maximized. */
+  inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; }
+
+  nv_iterator nv_begin();
+  nv_iterator nv_end();
+
+  const_nv_iterator nv_begin() const;
+  const_nv_iterator nv_end() const;
 
   /**
    * Indents the given stream a given amount of spaces.
    * @param out the stream to indent
    * @param indent the numer of spaces
    */
-  static inline void indent(std::ostream& out, int indent) {
-    for(int i = 0; i < indent; i++) {
+  static inline void indent(std::ostream& out, int indent)
+  {
+    for (int i = 0; i < indent; i++)
+    {
       out << ' ';
     }
   }
 
-};/* class NodeValue */
+  /** The ID (0 is reserved for the null value) */
+  uint64_t d_id : NBITS_ID;
+
+  /** The expression's reference count.  @see cvc4::Node. */
+  uint32_t d_rc : NBITS_REFCOUNT;
+
+  /** Kind of the expression */
+  uint32_t d_kind : NBITS_KIND;
+
+  /** Number of children */
+  uint32_t d_nchildren : NBITS_NCHILDREN;
+
+  /** Variable number of child nodes */
+  NodeValue* d_children[0];
+}; /* class NodeValue */
 
 /**
  * Provides a symmetric addition operator to that already defined in
  * the iterator class.
  */
-inline NodeValue::iterator<NodeTemplate<true> >
-operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
-          NodeValue::iterator<NodeTemplate<true> > i) {
-  return i + p;
-}
+NodeValue::iterator<NodeTemplate<true> > operator+(
+    NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+    NodeValue::iterator<NodeTemplate<true> > i);
 
 /**
  * Provides a symmetric addition operator to that already defined in
  * the iterator class.
  */
-inline NodeValue::iterator<NodeTemplate<false> >
-operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
-          NodeValue::iterator<NodeTemplate<false> > i) {
-  return i + p;
-}
+NodeValue::iterator<NodeTemplate<false> > operator+(
+    NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+    NodeValue::iterator<NodeTemplate<false> > i);
 
 /**
  * For hash_maps, hash_sets, etc.. but this is for expr package