NodeValue: Eliminate redundant NBITS macros. (#3400)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 22 Oct 2019 21:03:09 +0000 (14:03 -0700)
committerGitHub <noreply@github.com>
Tue, 22 Oct 2019 21:03:09 +0000 (14:03 -0700)
commit2caeef9745366ad4c45f61dabedf1cd7f676a4a1
tree4ddcc391429293e4a4e75d6ff23019ee9f71e781
parent2bd74b751844230b82c58bfdd29666206562781d
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.
src/api/cvc4cppkind.h
src/expr/metakind_template.h
src/expr/mkmetakind
src/expr/node_builder.h
src/expr/node_value.h
src/theory/booleans/theory_bool_rewriter.cpp