More precise includes of `Node` constants (#6617)

We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).

The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.

13 files changed, 63 insertions, 46 deletions

diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
index e4b1be691..820c82d22 100644
--- a/src/expr/bound_var_manager.cpp
+++ b/src/expr/bound_var_manager.cpp
@@ -16,6 +16,7 @@
 #include "expr/bound_var_manager.h"
 
 #include "expr/node_manager_attributes.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 52c15a08d..80732eab4 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -20,6 +20,7 @@
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_matcher.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index 584dc1615..a608b9adb 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -21,9 +21,11 @@
 #include <map>
 #include <string>
 #include <vector>
+
 #include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 0baf65dd6..b71f49e87 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -14,6 +14,7 @@
  */
 #include "expr/dtype_cons.h"
 
+#include "expr/ascription_type.h"
 #include "expr/dtype.h"
 #include "expr/node_manager.h"
 #include "expr/skolem_manager.h"
diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp
index 1b05815d8..1d0f5dd50 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -20,6 +20,10 @@
 
 #include <iostream>
 
+// clang-format off
+${metakind_includes}
+// clang-format off
+
 namespace cvc5 {
 namespace kind {
 
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 760cda981..09469915f 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -129,14 +129,14 @@ struct NodeValuePoolEq {
 
 #endif /* CVC5__KIND__METAKIND_H */
 
-// clang-format off
-${metakind_includes}
-// clang-format on
-
 #ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP
 
 namespace cvc5 {
 
+// clang-format off
+${metakind_fwd_decls}
+// clang-format on
+
 namespace expr {
 // clang-format off
 ${metakind_getConst_decls}
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index a5801b9fe..88208d776 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -42,6 +42,7 @@ me=$(basename "$0")
 
 template=$1; shift
 
+metakind_fwd_decls=
 metakind_includes=
 metakind_kinds=
 metakind_constantMaps=
@@ -202,65 +203,60 @@ function parameterized {
 }
 
 function constant {
-  # constant K T Hasher header ["comment"]
+  # constant K F T Hasher header ["comment"]
 
   lineno=${BASH_LINENO[0]}
 
   check_theory_seen
 
-  if ! expr "$2" : '\(::*\)' >/dev/null; then
-    if ! primitive_type "$2"; then
-      # if there's an embedded space, we're probably doing something
-      # tricky to specify the CONST payload, like "int const*"; in any
-      # case, this warning gives too many false positives, so disable it
-      if ! expr "$2" : '..* ..*' >/dev/null; then
-        echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::cvc5::Rational)" >&2
-      fi
-    fi
+  if ! expr "$4" : '\(::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: constant $1 hasher \`$4' isn't fully-qualified (e.g., ::cvc5::RationalHashFunction)" >&2
   fi
-  if ! expr "$3" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::cvc5::RationalHashFunction)" >&2
+
+  if [[ "$2" != "skip" ]]; then
+    metakind_fwd_decls="${metakind_fwd_decls}
+$2 $3;"
   fi
 
   # Avoid including the same header multiple times
-  if [ -n "$4" ] && [[ "${metakind_includes}" != *"#include \"$4\""* ]]; then
+  if [ -n "$5" ] && [[ "${metakind_includes}" != *"#include \"$5\""* ]]; then
     metakind_includes="${metakind_includes}
-#include \"$4\""
+#include \"$5\""
   fi
   register_metakind CONSTANT "$1" 0
   metakind_getConst_decls="${metakind_getConst_decls}
 template <>
-$2 const& NodeValue::getConst< $2 >() const;
+$3 const& NodeValue::getConst< $3 >() const;
 "
   metakind_constantMaps_decls="${metakind_constantMaps_decls}
 template <>
-struct ConstantMap< $2 > {
+struct ConstantMap< $3 > {
   // typedef $theory_class OwningTheory;
   enum { kind = ::cvc5::kind::$1 };
-};/* ConstantMap< $2 > */
+};/* ConstantMap< $3 > */
 
 template <>
 struct ConstantMapReverse< ::cvc5::kind::$1 > {
-  typedef $2 T;
+  typedef $3 T;
 };/* ConstantMapReverse< ::cvc5::kind::$1 > */
   "
   metakind_constantMaps="${metakind_constantMaps}
-// The reinterpret_cast of d_children to \"$2 const*\"
+// The reinterpret_cast of d_children to \"$3 const*\"
 // flags a \"strict aliasing\" warning; it's okay, because we never access
 // the embedded constant as a NodeValue* child, and never access an embedded
 // NodeValue* child as a constant.
 #pragma GCC diagnostic ignored \"-Wstrict-aliasing\"
 
 template <>
-$2 const& NodeValue::getConst< $2 >() const {
+$3 const& NodeValue::getConst< $3 >() const {
   AssertArgument(getKind() == ::cvc5::kind::$1, *this,
-                 \"Improper kind for getConst<$2>()\");
+                 \"Improper kind for getConst<$3>()\");
   // To support non-inlined CONSTANT-kinded NodeValues (those that are
   // \"constructed\" when initially checking them against the NodeManager
   // pool), we must check d_nchildren here.
   return d_nchildren == 0
-    ? *reinterpret_cast< $2 const* >(d_children)
-    : *reinterpret_cast< $2 const* >(d_children[0]);
+    ? *reinterpret_cast< $3 const* >(d_children)
+    : *reinterpret_cast< $3 const* >(d_children[0]);
 }
 
 // re-enable the warning
@@ -273,17 +269,17 @@ $2 const& NodeValue::getConst< $2 >() const {
 "
   metakind_constHashes="${metakind_constHashes}
   case kind::$1:
-    return $3()(nv->getConst< $2 >());
+    return $4()(nv->getConst< $3 >());
 "
   metakind_constPrinters="${metakind_constPrinters}
   case kind::$1:
-    out << nv->getConst< $2 >();
+    out << nv->getConst< $3 >();
     break;
 "
-  cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'`
+  cname=`echo "$3" | awk 'BEGIN {FS="::"} {print$NF}'`
   metakind_constDeleters="${metakind_constDeleters}
   case kind::$1:
-    std::allocator< $2 >().destroy(reinterpret_cast< $2* >(nv->d_children));
+    std::allocator< $3 >().destroy(reinterpret_cast< $3* >(nv->d_children));
     break;
 "
 }
@@ -397,6 +393,7 @@ check_builtin_theory_seen
 
 text=$(cat "$template")
 for var in \
+    metakind_fwd_decls \
     metakind_includes \
     metakind_kinds \
     metakind_constantMaps \
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c44720b67..1e6a38815 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -23,12 +23,17 @@
 #include "base/listener.h"
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
+#include "expr/datatype_index.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/metakind.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
+#include "theory/bags/make_bag_op.h"
+#include "theory/sets/singleton_op.h"
+#include "util/abstract_value.h"
+#include "util/bitvector.h"
 #include "util/resource_manager.h"
 
 using namespace std;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index e99c70f7c..ad0593cee 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -23,14 +23,15 @@
 #ifndef CVC5__NODE_MANAGER_H
 #define CVC5__NODE_MANAGER_H
 
-#include <vector>
 #include <string>
 #include <unordered_set>
+#include <vector>
 
 #include "base/check.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
+#include "util/floatingpoint_size.h"
 
 namespace cvc5 {
 
diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index 4202c70ec..6b15f33e0 100644
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -15,6 +15,7 @@
 
 #include "expr/sequence.h"
 
+#include <limits>
 #include <sstream>
 #include <vector>
 
diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp
index 09f1de7f1..dbf4cccae 100644
--- a/src/expr/term_context_node.cpp
+++ b/src/expr/term_context_node.cpp
@@ -16,6 +16,7 @@
 #include "expr/term_context_node.h"
 
 #include "expr/term_context.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index b4f2f7efa..52a21040e 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -16,12 +16,15 @@
 
 #include <vector>
 
+#include "expr/datatype_index.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/type_properties.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/type_enumerator.h"
+#include "util/bitvector.h"
+#include "util/cardinality.h"
 
 using namespace std;
 
@@ -684,6 +687,18 @@ TypeNode TypeNode::getBagElementType() const
   return (*this)[0];
 }
 
+bool TypeNode::isBitVector(unsigned size) const
+{
+  return (getKind() == kind::BITVECTOR_TYPE
+          && getConst<BitVectorSize>() == size);
+}
+
+uint32_t TypeNode::getBitVectorSize() const
+{
+  Assert(isBitVector());
+  return getConst<BitVectorSize>();
+}
+
 }  // namespace cvc5
 
 namespace std {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 1840820dc..21e7b4d28 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -29,12 +29,12 @@
 #include "base/check.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
-#include "util/cardinality.h"
 #include "util/cardinality_class.h"
 
 namespace cvc5 {
 
 class NodeManager;
+class Cardinality;
 class DType;
 
 namespace expr {
@@ -657,7 +657,7 @@ private:
   unsigned getFloatingPointSignificandSize() const;
 
   /** Get the size of this bit-vector type */
-  unsigned getBitVectorSize() const;
+  uint32_t getBitVectorSize() const;
 
   /** Is this a sort kind */
   bool isSort() const;
@@ -1000,12 +1000,6 @@ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
           && getConst<FloatingPointSize>().significandWidth() == sig);
 }
 
-/** Is this a bit-vector type of size <code>size</code> */
-inline bool TypeNode::isBitVector(unsigned size) const {
-  return
-    ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size );
-}
-
 /** Get the exponent size of this floating-point type */
 inline unsigned TypeNode::getFloatingPointExponentSize() const {
   Assert(isFloatingPoint());
@@ -1018,12 +1012,6 @@ inline unsigned TypeNode::getFloatingPointSignificandSize() const {
   return getConst<FloatingPointSize>().significandWidth();
 }
 
-/** Get the size of this bit-vector type */
-inline unsigned TypeNode::getBitVectorSize() const {
-  Assert(isBitVector());
-  return getConst<BitVectorSize>();
-}
-
 #ifdef CVC5_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used