summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cppkind.h3
-rw-r--r--src/expr/metakind_template.h17
-rwxr-xr-xsrc/expr/mkmetakind2
-rw-r--r--src/expr/node_builder.h16
-rw-r--r--src/expr/node_value.h39
-rw-r--r--src/theory/booleans/theory_bool_rewriter.cpp20
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());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback