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.

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 7d9ec28c6e2b253cee5aa00c47c10f99d2a20596..1f2a36676a2441c14d6d2dce5bbdd8f0a18483cf 100644 (file)
--- 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 c651a5f28ecc4ef00d92d71d9a81f99beb2fc016..1615d461b66f2d86479a1d18543cca70f7843dbc 100644 (file)
--- 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 1cfcf253a4f34740dc3c85e3f4d305db746914e5..fe8a152df18733973b4342a39606cb1a43d4e8a3 100755 (executable)
--- 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 d07790f92353c0ed50ca579f2f31c9d9a8cb238f..b5e99c6fd4b5d5d03ce4383336f095afaaa3c690 100644 (file)
--- 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 c86a07d6b6aae30f1e2b10b3fa5bdcd182e161a3..9d1a4f98e6356f00a3effad065166e327b0c79bd 100644 (file)
--- 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 02267cf2cc3459c0a5e28195d360553ef31375e6..c53610efaf569da1c0d17f5384d6ca204f56d6f4 100644 (file)
--- 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());