NodeValue: Eliminate redundant NBITS macros. (#3400)

Previously, the metakind header defined macros for the number of bits
reserved for fields in the NodeValue "header" (for the reference count,
the node kind, the number of children and the node id). These macros
were redundant, since the only one using them was the NodeValue itself,
which redefined them (while using them) as constants in the class.
Additionally, MAX_CHILDREN was defined (using these macros) not only
in the metakind header, but redefined in other places.

This commit defines the above values as constexpr members of the
NodeValue class and cleans up redundancy.

6 files changed, 47 insertions, 50 deletions

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 7d9ec28c6..1f2a36676 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -33,8 +33,7 @@ namespace api {
  *
  * Note that the underlying type of Kind must be signed (to enable range
  * checks for validity). The size of this type depends on the size of
- * CVC4::Kind (CVC4__EXPR__NODE_VALUE__NBITS__KIND, currently 10 bits,
- * see expr/metakind_template.h).
+ * CVC4::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h).
  */
 enum CVC4_PUBLIC Kind : int32_t
 {
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index c651a5f28..1615d461b 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -114,21 +114,6 @@ typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
 MetaKind metaKindOf(Kind k);
 }/* CVC4::kind namespace */
 
-namespace kind {
-namespace metakind {
-
-/* these are #defines so their sum can be #if-checked in node_value.h */
-#define CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 20
-#define CVC4__EXPR__NODE_VALUE__NBITS__KIND 10
-#define CVC4__EXPR__NODE_VALUE__NBITS__ID 40
-#define CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26
-
-static const uint32_t MAX_CHILDREN =
-    (((uint32_t)1) << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
-
-}/* CVC4::kind::metakind namespace */
-}/* CVC4::kind namespace */
-
 namespace expr {
 
 // Comparison predicate
@@ -216,7 +201,7 @@ Kind operatorToKind(::CVC4::expr::NodeValue* nv);
 
 }/* CVC4::kind namespace */
 
-#line 220 "${template}"
+#line 205 "${template}"
 
 namespace theory {
 
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 1cfcf253a..fe8a152df 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -329,7 +329,7 @@ function register_metakind {
     ub=$nc
   elif expr "$nc" : '[0-9][0-9]*:$' >/dev/null; then
     let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
-    ub=MAX_CHILDREN
+    ub="expr::NodeValue::MAX_CHILDREN"
   elif expr "$nc" : '[0-9][0-9]*:[0-9][0-9]*$' >/dev/null; then
     let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
     if [ $ub -lt $lb ]; then
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index d07790f92..b5e99c6fd 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -272,10 +272,12 @@ class NodeBuilder {
    * NodeValue is evacuated, make sure its children won't be
    * double-decremented later (on destruction/clear).
    */
-  inline void realloc() {
+  inline void realloc()
+  {
     size_t newSize = 2 * size_t(d_nvMaxChildren);
-    size_t hardLimit = (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
-    realloc(__builtin_expect( ( newSize > hardLimit ), false ) ? hardLimit : newSize);
+    size_t hardLimit = expr::NodeValue::MAX_CHILDREN;
+    realloc(__builtin_expect((newSize > hardLimit), false) ? hardLimit
+                                                           : newSize);
   }
 
   /**
@@ -774,9 +776,11 @@ template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
   AlwaysAssert(toSize > d_nvMaxChildren,
                "attempt to realloc() a NodeBuilder to a smaller/equal size!");
-  Assert( toSize < (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN),
-          "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)",
-          toSize, (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 );
+  Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN),
+         "attempt to realloc() a NodeBuilder to size %lu (beyond hard limit of "
+         "%u)",
+         toSize,
+         expr::NodeValue::MAX_CHILDREN);
 
   if(__builtin_expect( ( nvIsAllocated() ), false )) {
     // Ensure d_nv is not modified on allocation failure
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index c86a07d6b..9d1a4f98e 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -59,13 +59,6 @@ namespace kind {
 
 namespace expr {
 
-#if CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \
-    CVC4__EXPR__NODE_VALUE__NBITS__KIND + \
-    CVC4__EXPR__NODE_VALUE__NBITS__ID + \
-    CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96
-#  error NodeValue header bit assignment does not sum to 96 !
-#endif /* sum != 96 */
-
 /**
  * This is a NodeValue.
  */
@@ -171,6 +164,23 @@ class NodeValue
                                                             : d_nchildren;
   }
 
+  /* ------------------------------ Header ---------------------------------- */
+  /** Number of bits reserved for reference counting. */
+  static constexpr uint32_t NBITS_REFCOUNT = 20;
+  /** Number of bits reserved for node kind. */
+  static constexpr uint32_t NBITS_KIND = 10;
+  /** Number of bits reserved for node id. */
+  static constexpr uint32_t NBITS_ID = 40;
+  /** Number of bits reserved for number of children. */
+  static const uint32_t NBITS_NCHILDREN = 26;
+  static_assert(NBITS_REFCOUNT + NBITS_KIND + NBITS_ID + NBITS_NCHILDREN == 96,
+                "NodeValue header bit assignment does not sum to 96 !");
+  /* ------------------- This header fits into 96 bits ---------------------- */
+
+  /** Maximum number of children possible. */
+  static constexpr uint32_t MAX_CHILDREN =
+      (static_cast<uint32_t>(1) << NBITS_NCHILDREN) - 1;
+
   uint32_t getRefCount() const { return d_rc; }
 
   NodeValue* getOperator() const;
@@ -275,21 +285,14 @@ class NodeValue
     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;
+  static constexpr uint32_t MAX_RC =
+      (static_cast<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 ---------------------- */
+  static constexpr uint32_t kindMask =
+      (static_cast<uint32_t>(1) << NBITS_KIND) - 1;
 
   /** Uninitializing constructor for NodeBuilder's use.  */
   NodeValue()
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 02267cf2c..c53610efa 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -18,6 +18,7 @@
 #include <algorithm>
 #include <unordered_set>
 
+#include "expr/node_value.h"
 #include "theory/booleans/theory_bool_rewriter.h"
 
 namespace CVC4 {
@@ -77,17 +78,22 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
 
   /* Trickery to stay under number of children possible in a node */
   NodeManager* nodeManager = NodeManager::currentNM();
-  static const unsigned MAX_CHILDREN = (1u << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1;
-  if (childList.size() < MAX_CHILDREN) {
+  if (childList.size() < expr::NodeValue::MAX_CHILDREN)
+  {
     Node retNode = nodeManager->mkNode(k, childList);
     return RewriteResponse(REWRITE_DONE, retNode);
-  } else {
-    Assert(childList.size() < size_t(MAX_CHILDREN) * size_t(MAX_CHILDREN) );
+  }
+  else
+  {
+    Assert(childList.size()
+           < static_cast<size_t>(expr::NodeValue::MAX_CHILDREN)
+                 * static_cast<size_t>(expr::NodeValue::MAX_CHILDREN));
     NodeBuilder<> nb(k);
     ChildList::iterator cur = childList.begin(), next, en = childList.end();
-    while( cur != en ) {
-      next = min(cur + MAX_CHILDREN, en);
-      nb << (nodeManager->mkNode(k, ChildList(cur, next) ));
+    while (cur != en)
+    {
+      next = min(cur + expr::NodeValue::MAX_CHILDREN, en);
+      nb << (nodeManager->mkNode(k, ChildList(cur, next)));
       cur = next;
     }
     return RewriteResponse(REWRITE_DONE, nb.constructNode());