diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cppkind.h | 3 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 17 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 2 | ||||
-rw-r--r-- | src/expr/node_builder.h | 16 | ||||
-rw-r--r-- | src/expr/node_value.h | 39 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 20 |
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()); |