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.

1 files changed, 13 insertions, 7 deletions

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());