diff options
| author | Tim King <taking@cs.nyu.edu> | 2013-11-19 20:57:15 -0500 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2013-11-20 15:37:18 -0500 |
| commit | bd8e9319aab69db90692f72bc52288329879eefc (patch) | |
| tree | 7bfee530c06836827378fd5b9bd1f47bb4f1eea1 /src/expr/node_value.h | |
| parent | f806a8eedf01753116c225b4c1a5e29543fda370 (diff) | |
Changing the number of bits allocated per field in node values.
Diffstat (limited to 'src/expr/node_value.h')
| -rw-r--r-- | src/expr/node_value.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 56ac70c1e..e9d14c38e 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -65,9 +65,9 @@ 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 != 64 -# error NodeValue header bit assignment does not sum to 64 ! -#endif /* sum != 64 */ + __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96 +# error NodeValue header bit assignment does not sum to 96 ! +#endif /* sum != 96 */ /** * This is a NodeValue. @@ -92,7 +92,7 @@ class NodeValue { // this header fits into one 64-bit word /** The ID (0 is reserved for the null value) */ - unsigned d_id : NBITS_ID; + unsigned long d_id : NBITS_ID; /** The expression's reference count. @see cvc4::Node. */ unsigned d_rc : NBITS_REFCOUNT; @@ -255,7 +255,7 @@ public: return hash; } - unsigned getId() const { return d_id; } + unsigned long getId() const { return d_id; } Kind getKind() const { return dKindToKind(d_kind); } kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); } unsigned getNumChildren() const { |