diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-10-22 14:03:09 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-22 14:03:09 -0700 |
| commit | 2caeef9745366ad4c45f61dabedf1cd7f676a4a1 (patch) | |
| tree | 4ddcc391429293e4a4e75d6ff23019ee9f71e781 /src/api/cvc4cppkind.h | |
| parent | 2bd74b751844230b82c58bfdd29666206562781d (diff) | |
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.
Diffstat (limited to 'src/api/cvc4cppkind.h')
| -rw-r--r-- | src/api/cvc4cppkind.h | 3 |
1 files changed, 1 insertions, 2 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 { |