12 files changed, 34 insertions, 16 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 {