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.

101 files changed, 384 insertions, 184 deletions

diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index ed7f54182..cd1014e38 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -25,9 +25,10 @@
 
 #include <unordered_map>
 
-#include "expr/node.h"
-#include "context/cdo.h"
 #include "context/cdinsert_hashmap.h"
+#include "context/cdo.h"
+#include "expr/node.h"
+#include "util/integer.h"
 
 namespace cvc5 {
 namespace preprocessing {
diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index 724f83e07..3ca649211 100644
--- a/src/theory/arith/arith_msum.cpp
+++ b/src/theory/arith/arith_msum.cpp
@@ -16,6 +16,7 @@
 #include "theory/arith/arith_msum.h"
 
 #include "theory/rewriter.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index b8135127d..4d632e043 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -16,6 +16,8 @@
  * \todo document this file
  */
 
+#include "theory/arith/arith_rewriter.h"
+
 #include <set>
 #include <sstream>
 #include <stack>
@@ -23,11 +25,12 @@
 
 #include "smt/logic_exception.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
+#include "util/bitvector.h"
+#include "util/divisible.h"
 #include "util/iand.h"
 
 namespace cvc5 {
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index e1eda5d85..396befb35 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -44,10 +44,11 @@ operator ARCCOTANGENT 1 "arc cotangent"
 operator SQRT 1 "square root"
 
 constant DIVISIBLE_OP \
-        ::cvc5::Divisible \
-        ::cvc5::DivisibleHashFunction \
-        "util/divisible.h" \
-        "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class"
+  struct \
+  Divisible \
+  ::cvc5::DivisibleHashFunction \
+  "util/divisible.h" \
+  "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class"
 
 sort REAL_TYPE \
     Cardinality::REALS \
@@ -63,7 +64,8 @@ sort INTEGER_TYPE \
     "integer type"
 
 constant CONST_RATIONAL \
-    ::cvc5::Rational \
+    class \
+    Rational \
     ::cvc5::RationalHashFunction \
     "util/rational.h" \
     "a multiple-precision rational constant; payload is an instance of the cvc5::Rational class"
@@ -82,10 +84,11 @@ operator GEQ 2 "greater than or equal, x >= y"
 
 # represents an indexed root predicate. See util/indexed_root_predicate.h for more documentation.
 constant INDEXED_ROOT_PREDICATE_OP \
-	::cvc5::IndexedRootPredicate \
-	::cvc5::IndexedRootPredicateHashFunction \
-	"util/indexed_root_predicate.h" \
-	"operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class"
+  struct \
+  IndexedRootPredicate \
+  ::cvc5::IndexedRootPredicateHashFunction \
+  "util/indexed_root_predicate.h" \
+  "operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class"
 parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial"
 
 operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)"
@@ -157,10 +160,11 @@ typerule PI ::cvc5::theory::arith::RealNullaryOperatorTypeRule
 # (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2)))
 # for all integers i1, i2.
 constant IAND_OP \
-	::cvc5::IntAnd \
-	"::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \
-	"util/iand.h" \
-	"operator for integer AND; payload is an instance of the cvc5::IntAnd class"
+  struct \
+  IntAnd \
+  "::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \
+  "util/iand.h" \
+  "operator for integer AND; payload is an instance of the cvc5::IntAnd class"
 parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms"
 
 typerule IAND_OP ::cvc5::theory::arith::IAndOpTypeRule
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index 374a7e4ef..a74913d99 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -19,6 +19,7 @@
 
 #include "proof/lazy_tree_proof_generator.h"
 #include "theory/arith/nl/poly_conversion.h"
+#include "util/indexed_root_predicate.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index c1937797e..7db6c266f 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -23,6 +23,7 @@
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index d6b732eb9..4c79564e3 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -23,6 +23,7 @@
 #include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index bf38bc8f0..330cd57a3 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -22,6 +22,7 @@
 #include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 9efa9c0f2..d2a5e628a 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -22,6 +22,7 @@
 #include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index cb2fdab6f..8200ff08e 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -24,6 +24,7 @@
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 #include "util/iand.h"
 
 using namespace cvc5::kind;
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index cc35a4675..45881e1bb 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -20,6 +20,7 @@
 #include "cvc5_private.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp
index ba4c7dcb5..1ba501f90 100644
--- a/src/theory/arith/theory_arith_type_rules.cpp
+++ b/src/theory/arith/theory_arith_type_rules.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/arith/theory_arith_type_rules.h"
 
+#include "util/rational.h"
+
 namespace cvc5 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index e39f30c6e..67abc149d 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -36,7 +36,8 @@ operator EQ_RANGE 4 "equality of two arrays over an index range lower/upper"
 
 # storeall t e  is  \all i in indexType(t) <= e
 constant STORE_ALL \
-    ::cvc5::ArrayStoreAll \
+    class \
+    ArrayStoreAll \
     ::cvc5::ArrayStoreAllHashFunction \
     "expr/array_store_all.h" \
     "array store-all; payload is an instance of the cvc5::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)"
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0bdccfd17..ea18b3180 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -18,6 +18,7 @@
 #include <map>
 #include <memory>
 
+#include "expr/array_store_all.h"
 #include "expr/kind.h"
 #include "expr/node_algorithm.h"
 #include "options/arrays_options.h"
diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
index 8ad7a5f95..1072ffaf4 100644
--- a/src/theory/arrays/theory_arrays_rewriter.cpp
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -16,9 +16,12 @@
  * \todo document this file
  */
 
-#include "expr/attribute.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 
+#include "expr/array_store_all.h"
+#include "expr/attribute.h"
+#include "util/cardinality.h"
+
 namespace cvc5 {
 namespace theory {
 namespace arrays {
diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index 04a2f1a74..6d16e4020 100644
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -16,8 +16,10 @@
 #include "theory/arrays/theory_arrays_type_rules.h"
 
 // for array-constant attributes
+#include "expr/array_store_all.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/type_enumerator.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 181a42da4..6fc026b19 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -18,10 +18,11 @@
 #ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
 #define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
 
-#include "theory/type_enumerator.h"
-#include "expr/type_node.h"
+#include "expr/array_store_all.h"
 #include "expr/kind.h"
+#include "expr/type_node.h"
 #include "theory/rewriter.h"
+#include "theory/type_enumerator.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 47eb90f45..203903d88 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -21,6 +21,7 @@
 #include "theory/bags/solver_state.h"
 #include "theory/bags/term_registry.h"
 #include "theory/uf/equality_engine_iterator.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::context;
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 3d1a94f22..b9f620d51 100644
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -15,7 +15,9 @@
 
 #include "theory/bags/bags_rewriter.h"
 
+#include "expr/emptybag.h"
 #include "theory/bags/normal_form.h"
+#include "util/rational.h"
 #include "util/statistics_registry.h"
 
 using namespace cvc5::kind;
diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index 6286f20b7..556dc76d6 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -21,6 +21,7 @@
 #include "theory/bags/inference_manager.h"
 #include "theory/bags/solver_state.h"
 #include "theory/uf/equality_engine.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
index 038e7dd7f..795410239 100644
--- a/src/theory/bags/kinds
+++ b/src/theory/bags/kinds
@@ -16,7 +16,8 @@ properties check presolve
 
 # constants
 constant EMPTYBAG \
-    ::cvc5::EmptyBag \
+    class \
+    EmptyBag \
     ::cvc5::EmptyBagHashFunction \
     "expr/emptybag.h" \
     "the empty bag constant; payload is an instance of the cvc5::EmptyBag class"
@@ -50,7 +51,8 @@ operator BAG_COUNT         2  "multiplicity of an element in a bag"
 operator DUPLICATE_REMOVAL 1  "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)"
 
 constant MK_BAG_OP \
-	::cvc5::MakeBagOp \
+  class \
+	MakeBagOp \
 	::cvc5::MakeBagOpHashFunction \
 	"theory/bags/make_bag_op.h" \
 	"operator for MK_BAG; payload is an instance of the cvc5::MakeBagOp class"
diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
index 08142e6f9..ec32d0138 100644
--- a/src/theory/bags/normal_form.cpp
+++ b/src/theory/bags/normal_form.cpp
@@ -14,8 +14,10 @@
  */
 #include "normal_form.h"
 
+#include "expr/emptybag.h"
 #include "theory/sets/normal_form.h"
 #include "theory/type_enumerator.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 2db38e62b..659886e83 100644
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/bags/term_registry.h"
 
+#include "expr/emptyset.h"
 #include "theory/bags/inference_manager.h"
 #include "theory/bags/solver_state.h"
 
diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp
index 4695c1db7..be9e0cd4d 100644
--- a/src/theory/bags/theory_bags_type_enumerator.cpp
+++ b/src/theory/bags/theory_bags_type_enumerator.cpp
@@ -18,6 +18,7 @@
 #include "expr/emptybag.h"
 #include "theory/rewriter.h"
 #include "theory_bags_type_enumerator.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp
index 133059cd0..d820ce6e1 100644
--- a/src/theory/bags/theory_bags_type_rules.cpp
+++ b/src/theory/bags/theory_bags_type_rules.cpp
@@ -18,7 +18,11 @@
 #include <sstream>
 
 #include "base/check.h"
+#include "expr/emptybag.h"
+#include "theory/bags/make_bag_op.h"
 #include "theory/bags/normal_form.h"
+#include "util/cardinality.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
@@ -279,6 +283,11 @@ TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager,
   return setType;
 }
 
+Cardinality BagsProperties::computeCardinality(TypeNode type)
+{
+  return Cardinality::INTEGERS;
+}
+
 bool BagsProperties::isWellFounded(TypeNode type)
 {
   return type[0].isWellFounded();
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index a633d604f..487423309 100644
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -125,10 +125,7 @@ struct ToSetTypeRule
 
 struct BagsProperties
 {
-  static Cardinality computeCardinality(TypeNode type)
-  {
-    return Cardinality::INTEGERS;
-  }
+  static Cardinality computeCardinality(TypeNode type);
 
   static bool isWellFounded(TypeNode type);
 
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 6560cdd1a..da5642057 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -19,6 +19,7 @@ sort BOOLEAN_TYPE \
     "Boolean type"
 
 constant CONST_BOOLEAN \
+    skip \
     bool \
     ::cvc5::BoolHashFunction \
     "util/bool.h" \
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index f7e788e9a..6c4e0f96b 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -19,6 +19,7 @@
 
 #include "proof/proof_node.h"
 #include "proof/proof_node_manager.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 44d337c28..a5c63522d 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -16,11 +16,13 @@
  * \todo document this file
  */
 
+#include "theory/booleans/theory_bool_rewriter.h"
+
 #include <algorithm>
 #include <unordered_set>
 
 #include "expr/node_value.h"
-#include "theory/booleans/theory_bool_rewriter.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index dffe0baf3..d4a8782b5 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -119,12 +119,14 @@
 #     For consistency these should start with "APPLY_", but this is
 #     not enforced.
 #
-#   constant K T Hasher header ["comment"]
+#   constant K F T Hasher header ["comment"]
 #
-#     Declares a constant kind K.  T is the C++ type representing the
-#     constant internally (and it should be
-#     ::fully::qualified::like::this), and header is the header needed
-#     to define it.  Hasher is a hash functor type defined like this:
+#     Declares a constant kind K.  F is the type of the forward declaration to
+#     generate (e.g., `class`, `struct`). If F is `skip` then then no forward
+#     declaration is generated.  T is the C++ type representing the constant
+#     internally (the type is expected to be in the cvc5 namespace), and header
+#     is the header needed to define it.  Hasher is a hash functor type defined
+#     like this:
 #
 #       struct MyHashFcn {
 #         size_t operator()(const T& val) const;
@@ -263,7 +265,8 @@ well-founded SORT_TYPE \
     "::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"
 
 constant UNINTERPRETED_CONSTANT \
-    ::cvc5::UninterpretedConstant \
+    class \
+    UninterpretedConstant \
     ::cvc5::UninterpretedConstantHashFunction \
     "expr/uninterpreted_constant.h" \
     "the kind of expressions representing uninterpreted constants; payload is an instance of the cvc5::UninterpretedConstant class (used in models)"
@@ -273,7 +276,8 @@ enumerator SORT_TYPE \
     "theory/builtin/type_enumerator.h"
 
 constant ABSTRACT_VALUE \
-    ::cvc5::AbstractValue \
+    class \
+    AbstractValue \
     ::cvc5::AbstractValueHashFunction \
     "util/abstract_value.h" \
     "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the cvc5::AbstractValue class (used in models)"
@@ -284,7 +288,8 @@ typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule
 # not stored that way.  If you ask for the operator of (EQUAL a b),
 # you'll get a special, singleton (BUILTIN EQUAL) Node.
 constant BUILTIN \
-    ::cvc5::Kind \
+    skip \
+    Kind \
     ::cvc5::kind::KindHashFunction \
     "expr/kind.h" \
     "the kind of expressions representing built-in operators"
@@ -301,7 +306,8 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec
 operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body"
 
 constant TYPE_CONSTANT \
-    ::cvc5::TypeConstant \
+    skip \
+    TypeConstant \
     ::cvc5::TypeConstantHashFunction \
     "expr/kind.h" \
     "a representation for basic types"
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 68d6e1ad1..0ee72fc5f 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -18,6 +18,7 @@
 
 #include "theory/builtin/theory_builtin_rewriter.h"
 
+#include "expr/array_store_all.h"
 #include "expr/attribute.h"
 #include "expr/node_algorithm.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp
index a448b2b69..f3c595720 100644
--- a/src/theory/builtin/theory_builtin_type_rules.cpp
+++ b/src/theory/builtin/theory_builtin_type_rules.cpp
@@ -17,11 +17,20 @@
 
 #include "expr/attribute.h"
 #include "expr/skolem_manager.h"
+#include "expr/uninterpreted_constant.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 namespace theory {
 namespace builtin {
 
+TypeNode UninterpretedConstantTypeRule::computeType(NodeManager* nodeManager,
+                                                    TNode n,
+                                                    bool check)
+{
+  return n.getConst<UninterpretedConstant>().getType();
+}
+
 /**
  * Attribute for caching the ground term for each type. Maps TypeNode to the
  * skolem to return for mkGroundTerm.
@@ -46,6 +55,25 @@ Node SortProperties::mkGroundTerm(TypeNode type)
   return k;
 }
 
+Cardinality FunctionProperties::computeCardinality(TypeNode type)
+{
+  // Don't assert this; allow other theories to use this cardinality
+  // computation.
+  //
+  // Assert(type.getKind() == kind::FUNCTION_TYPE);
+
+  Cardinality argsCard(1);
+  // get the largest cardinality of function arguments/return type
+  for (size_t i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i)
+  {
+    argsCard *= type[i].getCardinality();
+  }
+
+  Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality();
+
+  return valueCard ^ argsCard;
+}
+
 }  // namespace builtin
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 87ba12ed1..00649a5af 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -93,9 +93,7 @@ class SExprTypeRule {
 
 class UninterpretedConstantTypeRule {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    return n.getConst<UninterpretedConstant>().getType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };/* class UninterpretedConstantTypeRule */
 
 class AbstractValueTypeRule {
@@ -202,22 +200,8 @@ class SortProperties {
 
 class FunctionProperties {
  public:
-  inline static Cardinality computeCardinality(TypeNode type) {
-    // Don't assert this; allow other theories to use this cardinality
-    // computation.
-    //
-    // Assert(type.getKind() == kind::FUNCTION_TYPE);
-
-    Cardinality argsCard(1);
-    // get the largest cardinality of function arguments/return type
-    for(unsigned i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) {
-      argsCard *= type[i].getCardinality();
-    }
+  static Cardinality computeCardinality(TypeNode type);
 
-    Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality();
-
-    return valueCard ^ argsCard;
-  }
   /** Function type is well-founded if its component sorts are */
   static bool isWellFounded(TypeNode type)
   {
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index e6080ed4f..37758ad4a 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -24,6 +24,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 using namespace cvc5;
 using namespace cvc5::theory;
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index f5259dc93..f71f82ce1 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -25,6 +25,7 @@
 #include "theory/bv/bitblast/bitblast_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 32b6dbd7a..ba545e48b 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -27,6 +27,7 @@
 #include "context/cdo.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 3a9e460fe..65c1ec79c 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -29,6 +29,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "util/bitvector.h"
 
 using namespace cvc5::context;
 using namespace cvc5::prop;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 7c97d1bbc..2589418cc 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -23,6 +23,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ext_theory.h"
 #include "theory/theory_model.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5;
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 6af586735..9590d5522 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -13,19 +13,21 @@ properties check propagate presolve ppStaticLearn
 rewriter ::cvc5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
 constant BITVECTOR_TYPE \
-	::cvc5::BitVectorSize \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \
-	"util/bitvector.h" \
-	"bit-vector type"
+  struct \
+  BitVectorSize \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \
+  "util/bitvector.h" \
+  "bit-vector type"
 cardinality BITVECTOR_TYPE \
 	"::cvc5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
 	"theory/bv/theory_bv_type_rules.h"
 
 constant CONST_BITVECTOR \
-    ::cvc5::BitVector \
-    ::cvc5::BitVectorHashFunction \
-    "util/bitvector.h" \
-    "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class"
+  class \
+  BitVector \
+  ::cvc5::BitVectorHashFunction \
+  "util/bitvector.h" \
+  "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class"
 
 enumerator BITVECTOR_TYPE \
     "::cvc5::theory::bv::BitVectorEnumerator" \
@@ -101,59 +103,67 @@ operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bi
 ### parameterized operator kinds ----------------------------------------------
 
 constant BITVECTOR_BITOF_OP \
-	::cvc5::BitVectorBitOf \
-	::cvc5::BitVectorBitOfHashFunction \
-	"util/bitvector.h" \
-	"operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class"
+  struct \
+  BitVectorBitOf \
+  ::cvc5::BitVectorBitOfHashFunction \
+  "util/bitvector.h" \
+  "operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class"
 parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
 
 constant BITVECTOR_EXTRACT_OP \
-	::cvc5::BitVectorExtract \
-	::cvc5::BitVectorExtractHashFunction \
-	"util/bitvector.h" \
-	"operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class"
+  struct \
+  BitVectorExtract \
+  ::cvc5::BitVectorExtractHashFunction \
+  "util/bitvector.h" \
+  "operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class"
 parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
 
 constant BITVECTOR_REPEAT_OP \
-	::cvc5::BitVectorRepeat \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class"
+  struct \
+  BitVectorRepeat \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class"
 parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
 
 constant BITVECTOR_ROTATE_LEFT_OP \
-	::cvc5::BitVectorRotateLeft \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class"
+  struct \
+  BitVectorRotateLeft \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class"
 parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
 
 constant BITVECTOR_ROTATE_RIGHT_OP \
-	::cvc5::BitVectorRotateRight \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class"
+  struct \
+  BitVectorRotateRight \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class"
 parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
 
 constant BITVECTOR_SIGN_EXTEND_OP \
-	::cvc5::BitVectorSignExtend \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class"
+  struct \
+  BitVectorSignExtend \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class"
 parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term"
 
 constant BITVECTOR_ZERO_EXTEND_OP \
-	::cvc5::BitVectorZeroExtend \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class"
+  struct \
+  BitVectorZeroExtend \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class"
 parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
 
 constant INT_TO_BITVECTOR_OP \
-	::cvc5::IntToBitVector \
-	"::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \
-	"util/bitvector.h" \
-	"operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class"
+  struct \
+  IntToBitVector \
+  "::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \
+  "util/bitvector.h" \
+  "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class"
 parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term"
 
 ### type rules for non-parameterized operator kinds ---------------------------
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index af80ad00b..761f4efb2 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -22,6 +22,7 @@
 
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 45e313e48..5ead8a215 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -27,6 +27,7 @@
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index e44d1c9b7..496a625ee 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -23,6 +23,7 @@
 #include "options/bv_options.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 1e38aba0f..6d2ed4477 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -24,6 +24,7 @@
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_type_rules.cpp b/src/theory/bv/theory_bv_type_rules.cpp
index 304a2b9cf..707b5f8bb 100644
--- a/src/theory/bv/theory_bv_type_rules.cpp
+++ b/src/theory/bv/theory_bv_type_rules.cpp
@@ -18,6 +18,8 @@
 #include <algorithm>
 
 #include "expr/type_node.h"
+#include "util/bitvector.h"
+#include "util/cardinality.h"
 #include "util/integer.h"
 
 namespace cvc5 {
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 927a40b82..bc6096cbb 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -20,6 +20,8 @@
 #include "expr/skolem_manager.h"
 #include "options/theory_options.h"
 #include "theory/theory.h"
+#include "util/bitvector.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index fca449917..712f5b822 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node_manager.h"
+#include "util/integer.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 744160c8b..e0e2f7ac8 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -15,14 +15,18 @@
 
 #include "theory/datatypes/datatypes_rewriter.h"
 
+#include "expr/ascription_type.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "expr/sygus_datatype.h"
+#include "expr/uninterpreted_constant.h"
 #include "options/datatypes_options.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/datatypes/tuple_project_op.h"
+#include "util/rational.h"
 
 using namespace cvc5;
 using namespace cvc5::kind;
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 19f396a56..a4323a1d0 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -20,6 +20,7 @@
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/model_manager.h"
 #include "theory/rewriter.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 1b7808a8b..41d5ded76 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -48,10 +48,11 @@ parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is
 parameterized APPLY_UPDATER UPDATER_TYPE 2 "datatype updater application; first parameter is an update, second is a datatype term to update, third is the value to update with"
 
 constant DATATYPE_TYPE \
-    ::cvc5::DatatypeIndexConstant \
-    "::cvc5::DatatypeIndexConstantHashFunction" \
-    "expr/datatype_index.h" \
-    "a datatype type index"
+  class \
+  DatatypeIndexConstant \
+  "::cvc5::DatatypeIndexConstantHashFunction" \
+  "expr/datatype_index.h" \
+  "a datatype type index"
 cardinality DATATYPE_TYPE \
     "%TYPE%.getDType().getCardinality(%TYPE%)" \
     "expr/dtype.h"
@@ -80,10 +81,11 @@ enumerator PARAMETRIC_DATATYPE \
 parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
     "type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed"
 constant ASCRIPTION_TYPE \
-    ::cvc5::AscriptionType \
-    ::cvc5::AscriptionTypeHashFunction \
-    "expr/ascription_type.h" \
-    "a type parameter for type ascription; payload is an instance of the cvc5::AscriptionType class"
+  class \
+  AscriptionType \
+  ::cvc5::AscriptionTypeHashFunction \
+  "expr/ascription_type.h" \
+  "a type parameter for type ascription; payload is an instance of the cvc5::AscriptionType class"
 
 typerule APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRule
 typerule APPLY_SELECTOR ::cvc5::theory::datatypes::DatatypeSelectorTypeRule
@@ -131,10 +133,11 @@ typerule MATCH_BIND_CASE ::cvc5::theory::datatypes::MatchBindCaseTypeRule
 
 
 constant TUPLE_PROJECT_OP \
-	::cvc5::TupleProjectOp \
-	::cvc5::TupleProjectOpHashFunction \
-	"theory/datatypes/tuple_project_op.h" \
-	"operator for TUPLE_PROJECT; payload is an instance of the cvc5::TupleProjectOp class"
+  class \
+  TupleProjectOp \
+  ::cvc5::TupleProjectOpHashFunction \
+  "theory/datatypes/tuple_project_op.h" \
+  "operator for TUPLE_PROJECT; payload is an instance of the cvc5::TupleProjectOp class"
 
 parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \
     "projects a tuple from an existing tuple using indices passed in TupleProjectOp"
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index df644e9b2..6cb1f44e1 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -17,10 +17,13 @@
 
 #include <sstream>
 
+#include "expr/ascription_type.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/type_matcher.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/datatypes/tuple_project_op.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index bf74347d0..582f11c72 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/datatypes/theory_datatypes_utils.h"
 
+#include "expr/ascription_type.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 6cb2fdce9..39b48ece9 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -13,8 +13,10 @@
  * Enumerators for datatypes.
  */
 
-#include "expr/dtype_cons.h"
 #include "theory/datatypes/type_enumerator.h"
+
+#include "expr/ascription_type.h"
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 759c50db0..9ea121be4 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -21,6 +21,7 @@
 #include "expr/dtype.h"
 #include "expr/kind.h"
 #include "expr/type_node.h"
+#include "expr/uninterpreted_constant.h"
 #include "options/quantifiers_options.h"
 #include "theory/type_enumerator.h"
 
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 3a058772c..c767014cb 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -800,17 +800,19 @@ Node FpConverter::rmToNode(const rm &r) const
   Node value = nm->mkNode(
       kind::ITE,
       nm->mkNode(kind::EQUAL, transVar, RNE),
-      nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN),
-      nm->mkNode(kind::ITE,
-                 nm->mkNode(kind::EQUAL, transVar, RNA),
-                 nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY),
-                 nm->mkNode(kind::ITE,
-                            nm->mkNode(kind::EQUAL, transVar, RTP),
-                            nm->mkConst(ROUND_TOWARD_POSITIVE),
-                            nm->mkNode(kind::ITE,
-                                       nm->mkNode(kind::EQUAL, transVar, RTN),
-                                       nm->mkConst(ROUND_TOWARD_NEGATIVE),
-                                       nm->mkConst(ROUND_TOWARD_ZERO)))));
+      nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN),
+      nm->mkNode(
+          kind::ITE,
+          nm->mkNode(kind::EQUAL, transVar, RNA),
+          nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY),
+          nm->mkNode(
+              kind::ITE,
+              nm->mkNode(kind::EQUAL, transVar, RTP),
+              nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE),
+              nm->mkNode(kind::ITE,
+                         nm->mkNode(kind::EQUAL, transVar, RTN),
+                         nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE),
+                         nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO)))));
   return value;
 }
 
@@ -878,19 +880,19 @@ Node FpConverter::convert(TNode node)
             /******** Constants ********/
             switch (current.getConst<RoundingMode>())
             {
-              case ROUND_NEAREST_TIES_TO_EVEN:
+              case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN:
                 d_rmMap.insert(current, traits::RNE());
                 break;
-              case ROUND_NEAREST_TIES_TO_AWAY:
+              case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY:
                 d_rmMap.insert(current, traits::RNA());
                 break;
-              case ROUND_TOWARD_POSITIVE:
+              case RoundingMode::ROUND_TOWARD_POSITIVE:
                 d_rmMap.insert(current, traits::RTP());
                 break;
-              case ROUND_TOWARD_NEGATIVE:
+              case RoundingMode::ROUND_TOWARD_NEGATIVE:
                 d_rmMap.insert(current, traits::RTN());
                 break;
-              case ROUND_TOWARD_ZERO:
+              case RoundingMode::ROUND_TOWARD_ZERO:
                 d_rmMap.insert(current, traits::RTZ());
                 break;
               default: Unreachable() << "Unknown rounding mode"; break;
diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
index dac0d5136..11bb05c70 100644
--- a/src/theory/fp/fp_expand_defs.cpp
+++ b/src/theory/fp/fp_expand_defs.cpp
@@ -16,6 +16,7 @@
 #include "theory/fp/fp_expand_defs.h"
 
 #include "expr/skolem_manager.h"
+#include "util/floatingpoint.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
index d67738a63..c07e54463 100644
--- a/src/theory/fp/kinds
+++ b/src/theory/fp/kinds
@@ -14,7 +14,8 @@ properties check
 
 # constants...
 constant CONST_FLOATINGPOINT \
-    ::cvc5::FloatingPoint \
+    class \
+    FloatingPoint \
     ::cvc5::FloatingPointHashFunction \
     "util/floatingpoint.h" \
     "a floating-point literal"
@@ -22,9 +23,10 @@ typerule CONST_FLOATINGPOINT    ::cvc5::theory::fp::FloatingPointConstantTypeRul
 
 
 constant CONST_ROUNDINGMODE \
-    ::cvc5::RoundingMode \
+    "enum class" \
+    RoundingMode \
     ::cvc5::RoundingModeHashFunction \
-    "util/floatingpoint.h" \
+    "util/roundingmode.h" \
     "a floating-point rounding mode"    
 typerule CONST_ROUNDINGMODE    ::cvc5::theory::fp::RoundingModeConstantTypeRule
 
@@ -45,7 +47,8 @@ enumerator ROUNDINGMODE_TYPE \
 
 
 constant FLOATINGPOINT_TYPE \
-    ::cvc5::FloatingPointSize \
+    class \
+    FloatingPointSize \
     ::cvc5::FloatingPointSizeHashFunction \
     "util/floatingpoint.h" \
     "floating-point type"
@@ -155,7 +158,8 @@ typerule FLOATINGPOINT_ISPOS   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
 
 constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \
-    ::cvc5::FloatingPointToFPIEEEBitVector \
+    class \
+    FloatingPointToFPIEEEBitVector \
     "::cvc5::FloatingPointConvertSortHashFunction<0x1>" \
     "util/floatingpoint.h" \
     "operator for to_fp from bit vector"
@@ -167,7 +171,8 @@ typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR   ::cvc5::theory::fp::FloatingPointT
 
 
 constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \
-    ::cvc5::FloatingPointToFPFloatingPoint \
+    class \
+    FloatingPointToFPFloatingPoint \
     "::cvc5::FloatingPointConvertSortHashFunction<0x2>" \
     "util/floatingpoint.h" \
     "operator for to_fp from floating point"
@@ -180,7 +185,8 @@ typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT   ::cvc5::theory::fp::FloatingPointTo
 
 
 constant FLOATINGPOINT_TO_FP_REAL_OP \
-    ::cvc5::FloatingPointToFPReal \
+    class \
+    FloatingPointToFPReal \
     "::cvc5::FloatingPointConvertSortHashFunction<0x4>" \
     "util/floatingpoint.h" \
     "operator for to_fp from real"
@@ -192,7 +198,8 @@ typerule FLOATINGPOINT_TO_FP_REAL   ::cvc5::theory::fp::FloatingPointToFPRealTyp
 
 
 constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \
-    ::cvc5::FloatingPointToFPSignedBitVector \
+    class \
+    FloatingPointToFPSignedBitVector \
     "::cvc5::FloatingPointConvertSortHashFunction<0x8>" \
     "util/floatingpoint.h" \
     "operator for to_fp from signed bit vector"
@@ -204,7 +211,8 @@ typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR   ::cvc5::theory::fp::FloatingPoin
 
 
 constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \
-    ::cvc5::FloatingPointToFPUnsignedBitVector \
+    class \
+    FloatingPointToFPUnsignedBitVector \
     "::cvc5::FloatingPointConvertSortHashFunction<0x10>" \
     "util/floatingpoint.h" \
     "operator for to_fp from unsigned bit vector"
@@ -217,7 +225,8 @@ typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR   ::cvc5::theory::fp::FloatingPo
 
 
 constant FLOATINGPOINT_TO_FP_GENERIC_OP \
-    ::cvc5::FloatingPointToFPGeneric \
+    class \
+    FloatingPointToFPGeneric \
     "::cvc5::FloatingPointConvertSortHashFunction<0x11>" \
     "util/floatingpoint.h" \
     "operator for a generic to_fp"
@@ -232,7 +241,8 @@ typerule FLOATINGPOINT_TO_FP_GENERIC   ::cvc5::theory::fp::FloatingPointToFPGene
 
 
 constant FLOATINGPOINT_TO_UBV_OP \
-    ::cvc5::FloatingPointToUBV \
+    class \
+    FloatingPointToUBV \
     "::cvc5::FloatingPointToBVHashFunction<0x1>" \
     "util/floatingpoint.h" \
     "operator for to_ubv"
@@ -243,7 +253,8 @@ typerule FLOATINGPOINT_TO_UBV   ::cvc5::theory::fp::FloatingPointToUBVTypeRule
 
 
 constant FLOATINGPOINT_TO_UBV_TOTAL_OP \
-    ::cvc5::FloatingPointToUBVTotal \
+    class \
+    FloatingPointToUBVTotal \
     "::cvc5::FloatingPointToBVHashFunction<0x4>" \
     "util/floatingpoint.h" \
     "operator for to_ubv_total"
@@ -255,7 +266,8 @@ typerule FLOATINGPOINT_TO_UBV_TOTAL   ::cvc5::theory::fp::FloatingPointToUBVTota
 
 
 constant FLOATINGPOINT_TO_SBV_OP \
-    ::cvc5::FloatingPointToSBV \
+    class \
+    FloatingPointToSBV \
     "::cvc5::FloatingPointToBVHashFunction<0x2>" \
     "util/floatingpoint.h" \
     "operator for to_sbv"
@@ -266,7 +278,8 @@ typerule FLOATINGPOINT_TO_SBV   ::cvc5::theory::fp::FloatingPointToSBVTypeRule
 
 
 constant FLOATINGPOINT_TO_SBV_TOTAL_OP \
-    ::cvc5::FloatingPointToSBVTotal \
+    class \
+    FloatingPointToSBVTotal \
     "::cvc5::FloatingPointToBVHashFunction<0x8>" \
     "util/floatingpoint.h" \
     "operator for to_sbv_total"
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index ecb8ba2b4..a48f62c6d 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -29,6 +29,7 @@
 #include "theory/output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "util/floatingpoint.h"
 
 using namespace std;
 
@@ -362,7 +363,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
           nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
                      nm->mkConst(FloatingPointToFPReal(
                          concrete[0].getType().getConst<FloatingPointSize>())),
-                     nm->mkConst(ROUND_TOWARD_POSITIVE),
+                     nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE),
                      abstractValue));
 
       Node bg = nm->mkNode(
@@ -379,7 +380,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
           nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
                      nm->mkConst(FloatingPointToFPReal(
                          concrete[0].getType().getConst<FloatingPointSize>())),
-                     nm->mkConst(ROUND_TOWARD_NEGATIVE),
+                     nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE),
                      abstractValue));
 
       Node bl = nm->mkNode(
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 4f340e774..c52100209 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -39,6 +39,7 @@
 #include "base/check.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/fp/fp_converter.h"
+#include "util/floatingpoint.h"
 
 namespace cvc5 {
 namespace theory {
@@ -1084,23 +1085,23 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
     RoundingMode arg0(node[0].getConst<RoundingMode>());
     switch (arg0)
     {
-      case ROUND_NEAREST_TIES_TO_EVEN:
+      case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN:
         value = symfpuSymbolic::traits::RNE().getConst<BitVector>();
         break;
 
-      case ROUND_NEAREST_TIES_TO_AWAY:
+      case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY:
         value = symfpuSymbolic::traits::RNA().getConst<BitVector>();
         break;
 
-      case ROUND_TOWARD_POSITIVE:
+      case RoundingMode::ROUND_TOWARD_POSITIVE:
         value = symfpuSymbolic::traits::RTP().getConst<BitVector>();
         break;
 
-      case ROUND_TOWARD_NEGATIVE:
+      case RoundingMode::ROUND_TOWARD_NEGATIVE:
         value = symfpuSymbolic::traits::RTN().getConst<BitVector>();
         break;
 
-      case ROUND_TOWARD_ZERO:
+      case RoundingMode::ROUND_TOWARD_ZERO:
         value = symfpuSymbolic::traits::RTZ().getConst<BitVector>();
         break;
 
@@ -1499,11 +1500,11 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
 
             NodeManager* nm = NodeManager::currentNM();
 
-            Node rne(nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN));
-            Node rna(nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY));
-            Node rtz(nm->mkConst(ROUND_TOWARD_POSITIVE));
-            Node rtn(nm->mkConst(ROUND_TOWARD_NEGATIVE));
-            Node rtp(nm->mkConst(ROUND_TOWARD_ZERO));
+            Node rne(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN));
+            Node rna(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY));
+            Node rtz(nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE));
+            Node rtn(nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE));
+            Node rtp(nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO));
 
             TNode rm(res.d_node[0]);
 
diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp
index 5951decd4..b78ef24c7 100644
--- a/src/theory/fp/theory_fp_type_rules.cpp
+++ b/src/theory/fp/theory_fp_type_rules.cpp
@@ -17,6 +17,8 @@
 
 // This is only needed for checking that components are only applied to leaves.
 #include "theory/theory.h"
+#include "util/cardinality.h"
+#include "util/floatingpoint.h"
 #include "util/roundingmode.h"
 
 namespace cvc5 {
diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h
index c7c99adf2..edf297498 100644
--- a/src/theory/fp/type_enumerator.h
+++ b/src/theory/fp/type_enumerator.h
@@ -84,7 +84,7 @@ class RoundingModeEnumerator
  public:
   RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
       : TypeEnumeratorBase<RoundingModeEnumerator>(type),
-        d_rm(ROUND_NEAREST_TIES_TO_EVEN),
+        d_rm(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN),
         d_enumerationComplete(false)
   {
   }
@@ -99,11 +99,21 @@ class RoundingModeEnumerator
 
   RoundingModeEnumerator& operator++() override {
     switch (d_rm) {
-      case ROUND_NEAREST_TIES_TO_EVEN: d_rm = ROUND_TOWARD_POSITIVE; break;
-      case ROUND_TOWARD_POSITIVE: d_rm = ROUND_TOWARD_NEGATIVE; break;
-      case ROUND_TOWARD_NEGATIVE: d_rm = ROUND_TOWARD_ZERO; break;
-      case ROUND_TOWARD_ZERO: d_rm = ROUND_NEAREST_TIES_TO_AWAY; break;
-      case ROUND_NEAREST_TIES_TO_AWAY: d_enumerationComplete = true; break;
+      case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN:
+        d_rm = RoundingMode::ROUND_TOWARD_POSITIVE;
+        break;
+      case RoundingMode::ROUND_TOWARD_POSITIVE:
+        d_rm = RoundingMode::ROUND_TOWARD_NEGATIVE;
+        break;
+      case RoundingMode::ROUND_TOWARD_NEGATIVE:
+        d_rm = RoundingMode::ROUND_TOWARD_ZERO;
+        break;
+      case RoundingMode::ROUND_TOWARD_ZERO:
+        d_rm = RoundingMode::ROUND_NEAREST_TIES_TO_AWAY;
+        break;
+      case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY:
+        d_enumerationComplete = true;
+        break;
       default: Unreachable() << "Unknown rounding mode?"; break;
     }
     return *this;
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index fd204fffd..cfcc5f5a1 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/bv_inverter_utils.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index ca4abf497..fe47f1dd1 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -20,6 +20,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/rewriter.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index d5af43242..83234d115 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 7ee22dc5b..1ed386485 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -18,6 +18,7 @@
 #include <sstream>
 #include <stack>
 
+#include "expr/ascription_type.h"
 #include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -30,6 +31,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 #include "theory/strings/word.h"
+#include "util/floatingpoint.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index a5c7af161..28506d0bd 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -19,10 +19,11 @@
 #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
 
 #include <map>
-#include "options/main_options.h"
-#include "theory/quantifiers/sygus/sygus_unif.h"
 
+#include "options/main_options.h"
 #include "theory/quantifiers/lazy_trie.h"
+#include "theory/quantifiers/sygus/sygus_unif.h"
+#include "util/bool.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 0c9cb91d7..746cc7f11 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -20,8 +20,10 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
-#include "theory/strings/word.h"
 #include "theory/rewriter.h"
+#include "theory/strings/word.h"
+#include "util/bitvector.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 22b77c4fb..6d1b9955a 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -18,6 +18,7 @@
 #include <map>
 
 #include "base/map_util.h"
+#include "expr/emptyset.h"
 #include "expr/kind.h"
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
@@ -32,6 +33,7 @@
 #include "theory/sep/theory_sep_rewriter.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
+#include "util/cardinality.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 8e6cd08c6..afd860288 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -15,10 +15,12 @@
  * \todo document this file
  */
 
-#include "expr/attribute.h"
 #include "theory/sep/theory_sep_rewriter.h"
-#include "theory/quantifiers/quant_util.h"
+
+#include "expr/attribute.h"
+#include "expr/emptyset.h"
 #include "options/sep_options.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index ec5abfacc..063c440a5 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -25,6 +25,8 @@
 #include "theory/sets/normal_form.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
+#include "util/cardinality.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 0f15727e0..4bde524f7 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -16,10 +16,11 @@ properties check presolve
 
 # constants
 constant EMPTYSET \
-    ::cvc5::EmptySet \
-    ::cvc5::EmptySetHashFunction \
-    "expr/emptyset.h" \
-    "the empty set constant; payload is an instance of the cvc5::EmptySet class"
+  class \
+  EmptySet \
+  ::cvc5::EmptySetHashFunction \
+  "expr/emptyset.h" \
+  "the empty set constant; payload is an instance of the cvc5::EmptySet class"
 
 # the type
 operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
@@ -42,10 +43,11 @@ operator SUBSET         2  "subset predicate; first parameter a subset of second
 operator MEMBER         2  "set membership predicate; first parameter a member of second"
 
 constant SINGLETON_OP \
-	::cvc5::SingletonOp \
-	::cvc5::SingletonOpHashFunction \
-	"theory/sets/singleton_op.h" \
-	"operator for singletons; payload is an instance of the cvc5::SingletonOp class"
+  class \
+  SingletonOp \
+  ::cvc5::SingletonOpHashFunction \
+  "theory/sets/singleton_op.h" \
+  "operator for singletons; payload is an instance of the cvc5::SingletonOp class"
 parameterized SINGLETON SINGLETON_OP 1  \
 "constructs a set of a single element. First parameter is a SingletonOp. Second is a term"
 
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 930f7da86..eb839e1c0 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -18,6 +18,8 @@
 #ifndef CVC5__THEORY__SETS__NORMAL_FORM_H
 #define CVC5__THEORY__SETS__NORMAL_FORM_H
 
+#include "expr/emptyset.h"
+
 namespace cvc5 {
 namespace theory {
 namespace sets {
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index fad14bb71..42e317402 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -26,6 +26,7 @@
 #include "theory/sets/normal_form.h"
 #include "theory/sets/theory_sets.h"
 #include "theory/theory_model.h"
+#include "util/rational.h"
 #include "util/result.h"
 
 using namespace std;
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 69780b04c..0546c7f95 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -18,6 +18,7 @@
 #include "expr/skolem_manager.h"
 #include "theory/sets/theory_sets.h"
 #include "theory/sets/theory_sets_private.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index d05318cc8..14b5c6d52 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -20,6 +20,7 @@
 #include "options/sets_options.h"
 #include "theory/sets/normal_form.h"
 #include "theory/sets/rels_utils.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp
index 503a33ebd..8c395a958 100644
--- a/src/theory/sets/theory_sets_type_enumerator.cpp
+++ b/src/theory/sets/theory_sets_type_enumerator.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/sets/theory_sets_type_enumerator.h"
 
+#include "util/bitvector.h"
+
 namespace cvc5 {
 namespace theory {
 namespace sets {
diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp
index 232865994..91c592f18 100644
--- a/src/theory/sets/theory_sets_type_rules.cpp
+++ b/src/theory/sets/theory_sets_type_rules.cpp
@@ -19,6 +19,8 @@
 #include <sstream>
 
 #include "theory/sets/normal_form.h"
+#include "theory/sets/singleton_op.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index 4c3b2f17e..66e3cf634 100644
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -22,6 +22,7 @@
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 #include "theory/theory.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 6ee88b298..00491128a 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -21,6 +21,7 @@
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::context;
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index a6e4ce698..fb1d086a4 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -16,6 +16,7 @@
 #include "theory/strings/core_solver.h"
 
 #include "base/configuration.h"
+#include "expr/sequence.h"
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
 #include "theory/rewriter.h"
@@ -23,6 +24,8 @@
 #include "theory/strings/strings_entail.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
+#include "util/string.h"
 
 using namespace std;
 using namespace cvc5::context;
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 3dbb6b89b..94d99732a 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -20,6 +20,7 @@
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::context;
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index b9847e22a..1353ca964 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -58,10 +58,11 @@ enumerator STRING_TYPE \
     "theory/strings/type_enumerator.h"
 
 constant CONST_STRING \
-    ::cvc5::String \
-    ::cvc5::strings::StringHashFunction \
-    "util/string.h" \
-    "a string of characters"
+  class \
+  String \
+  ::cvc5::strings::StringHashFunction \
+  "util/string.h" \
+  "a string of characters"
 
 # the type
 operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements"
@@ -77,10 +78,11 @@ enumerator SEQUENCE_TYPE \
     "theory/strings/type_enumerator.h"
 
 constant CONST_SEQUENCE \
-    ::cvc5::Sequence \
-    ::cvc5::SequenceHashFunction \
-    "expr/sequence.h" \
-    "a sequence of characters"
+  class \
+  Sequence \
+  ::cvc5::SequenceHashFunction \
+  "expr/sequence.h" \
+  "a sequence of characters"
 
 operator SEQ_UNIT 1 "a sequence of length one"
 operator SEQ_NTH 2 "The nth element of a sequence"
@@ -102,17 +104,19 @@ operator REGEXP_EMPTY 0 "regexp empty"
 operator REGEXP_SIGMA 0 "regexp all characters"
 
 constant REGEXP_REPEAT_OP \
-	::cvc5::RegExpRepeat \
-	::cvc5::RegExpRepeatHashFunction \
-	"util/regexp.h" \
-	"operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class"
+  struct \
+  RegExpRepeat \
+  ::cvc5::RegExpRepeatHashFunction \
+  "util/regexp.h" \
+  "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class"
 parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term"
 
 constant REGEXP_LOOP_OP \
-	::cvc5::RegExpLoop \
-	::cvc5::RegExpLoopHashFunction \
-	"util/regexp.h" \
-	"operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class"
+  struct \
+  RegExpLoop \
+  ::cvc5::RegExpLoopHashFunction \
+  "util/regexp.h" \
+  "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class"
 parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term"
 
 #internal
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index f635cdc39..ac0e487f9 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -20,6 +20,8 @@
 #include "theory/rewriter.h"
 #include "theory/strings/regexp_entail.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "util/rational.h"
+#include "util/string.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index b789db6a4..3d4a2d143 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -18,6 +18,8 @@
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
+#include "util/string.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 96351cda9..106ce09d0 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -23,6 +23,7 @@
 #include "theory/strings/regexp_entail.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/regexp.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 5b046fbc5..15c37070a 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -25,7 +25,10 @@
 #include "theory/strings/strings_rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
+#include "util/regexp.h"
 #include "util/statistics_registry.h"
+#include "util/string.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index e5e014f9d..1ddf2af58 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -18,6 +18,7 @@
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::context;
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index a5d01eefd..a527d99dc 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -21,6 +21,8 @@
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
+#include "util/string.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp
index f5ccc3bef..9bb6a2420 100644
--- a/src/theory/strings/strings_fmf.cpp
+++ b/src/theory/strings/strings_fmf.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/strings/strings_fmf.h"
 
+#include "util/rational.h"
+
 using namespace std;
 using namespace cvc5::context;
 using namespace cvc5::kind;
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 41a8ac448..b455d8a9b 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -19,6 +19,7 @@
 #include "expr/node_builder.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "util/rational.h"
+#include "util/string.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index ced2c7dae..af2eecde8 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -23,6 +23,8 @@
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
+#include "util/string.h"
 
 using namespace std;
 using namespace cvc5::context;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index f1b591e43..356ae28ac 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -24,7 +24,9 @@
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
 #include "util/statistics_registry.h"
+#include "util/string.h"
 
 using namespace cvc5;
 using namespace cvc5::kind;
diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp
index a7e891d86..183344aa2 100644
--- a/src/theory/strings/theory_strings_type_rules.cpp
+++ b/src/theory/strings/theory_strings_type_rules.cpp
@@ -19,6 +19,7 @@
 #include "expr/node_manager.h"
 #include "expr/sequence.h"
 #include "options/strings_options.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 5df744412..6897d5272 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -22,6 +22,9 @@
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/strings_entail.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
+#include "util/regexp.h"
+#include "util/string.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index 1f2f31a61..5641312cb 100644
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/strings/type_enumerator.h"
 
+#include "expr/sequence.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "util/string.h"
 
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index e2a81f54a..02fa85faa 100644
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -19,6 +19,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/strings/word.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index dd1e0b883..8eec7f911 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_engine.h"
 #include "theory/rewriter.h"
 #include "theory/trust_substitutions.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 951a62cae..4034e43bd 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -26,6 +26,7 @@
 #include "theory/type_enumerator.h"
 #include "theory/type_set.h"
 #include "theory/uf/equality_engine.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 0a038845c..e3e197953 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
+#include "expr/uninterpreted_constant.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index aaeea6a4f..97bf7aaac 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -22,6 +22,7 @@
 #include "base/exception.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "util/integer.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 166df3c80..5b919860e 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -28,6 +28,7 @@
 #include "theory/theory_model.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp
index f81abdca1..e95c8963e 100644
--- a/src/theory/uf/theory_uf_type_rules.cpp
+++ b/src/theory/uf/theory_uf_type_rules.cpp
@@ -18,6 +18,8 @@
 #include <climits>
 #include <sstream>
 
+#include "util/rational.h"
+
 namespace cvc5 {
 namespace theory {
 namespace uf {