Clean up includes to reduce compile times (#6031)

This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.

154 files changed, 300 insertions, 108 deletions

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 31eb8bb8f..26f51c8b8 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/arith/arith_preprocess.h"
 
+#include "theory/arith/inference_manager.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 6c858d1eb..396395e1f 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -21,7 +21,6 @@
 #define CVC4__THEORY__ARITH__ARITH_REWRITER_H
 
 #include "theory/arith/rewrites.h"
-#include "theory/theory.h"
 #include "theory/theory_rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 72f8e49ff..61715df9b 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 374b17d88..5d4bc9b1e 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 
 
 using namespace std;
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 85af862fa..8cb249c46 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "util/statistics_registry.h"
 
 using namespace std;
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 1bd4416e0..e001d98d4 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -52,6 +52,7 @@
 
 #pragma once
 
+#include "theory/arith/error_set.h"
 #include "theory/arith/simplex.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index df3ba37f3..04165c289 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "theory/arith/nl/cad/projections.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
+#include "theory/arith/nl/nl_model.h"
 
 namespace std {
 /** Generic streaming operator for std::vector. */
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 4511d0c55..8736b7a08 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -32,12 +32,14 @@
 #include "theory/arith/nl/cad/constraints.h"
 #include "theory/arith/nl/cad/proof_generator.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
+
+class NlModel;
+
 namespace cad {
 
 /**
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 74c0457a8..efc5c465a 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -14,15 +14,11 @@
 
 #include "theory/arith/nl/cad_solver.h"
 
-#ifdef CVC4_POLY_IMP
-#include <poly/polyxx.h>
-#endif
-
-#include "options/arith_options.h"
 #include "theory/inference_id.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/poly_conversion.h"
-#include "util/poly_util.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 21fbbab2e..b67d78f0d 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -17,17 +17,22 @@
 
 #include <vector>
 
+#include "context/context.h"
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/cad/proof_checker.h"
-#include "theory/arith/nl/nl_model.h"
+#include "util/real_algebraic_number.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 /**
  * A solver for nonlinear arithmetic that implements the CAD-based method
  * described in https://arxiv.org/pdf/2003.05633.pdf.
diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index 5da5319a1..7e77efb16 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -17,6 +17,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/arith/nl/nl_model.h"
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index 863b3f879..285189ccc 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -19,15 +19,21 @@
 
 #include "expr/node.h"
 #include "expr/proof_set.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
+
+class CDProof;
+
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 struct ExtState
 {
   ExtState(InferenceManager& im,
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 7b4d98037..09cfd7410 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -15,10 +15,12 @@
 #include "theory/arith/nl/ext/factoring_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "expr/skolem_manager.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 5ae898bd2..ad6fd36b8 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -15,11 +15,13 @@
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index a3e56358b..d970bd95d 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/ext/monomial_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index 51179826a..05908ecc7 100644
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -16,6 +16,7 @@
 #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
 
 #include "expr/node.h"
+#include "theory/theory_inference.h"
 #include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 1e9b444e3..5bcdb801d 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -15,9 +15,11 @@
 #include "theory/arith/nl/ext/split_zero_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index e8730e496..0e7ad0999 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -16,6 +16,7 @@
 #define CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
 
 #include "expr/node.h"
+#include "context/cdhashset.h"
 #include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 3d646a684..2d04c2b5c 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -15,9 +15,11 @@
 #include "theory/arith/nl/ext/tangent_plane_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp
index 62e1fa904..ee12d17d6 100644
--- a/src/theory/arith/nl/ext_theory_callback.cpp
+++ b/src/theory/arith/nl/ext_theory_callback.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/ext_theory_callback.h"
 
 #include "theory/arith/arith_utilities.h"
+#include "theory/uf/equality_engine.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index a5b4e87bd..6487b48ec 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -18,7 +18,10 @@
 #include "options/smt_options.h"
 #include "preprocessing/passes/bv_to_int.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/arith/arith_state.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
 #include "util/iand.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index c854f3ab7..044a37abc 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -20,17 +20,20 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
-#include "theory/arith/arith_state.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/iand_utils.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class ArithState;
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 /** Integer and solver class
  *
  */
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 17eb518a2..652f0eec7 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -19,6 +19,8 @@
 
 #include "cvc4_private.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h
index a05defc0a..4c1de0196 100644
--- a/src/theory/arith/nl/iand_utils.h
+++ b/src/theory/arith/nl/iand_utils.h
@@ -16,7 +16,7 @@
 #ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
 #define CVC4__THEORY__ARITH__IAND_TABLE_H
 
-#include <tuple>
+#include <map>
 #include <vector>
 
 #include "expr/node.h"
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index af86d69fd..7d698a221 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -20,6 +20,7 @@
 #include "base/output.h"
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/poly_conversion.h"
 #include "theory/arith/normal_form.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index 176549d8b..b9ecfc437 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -23,7 +23,6 @@
 
 #include "expr/node.h"
 #include "theory/arith/bound_inference.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/icp/candidate.h"
 #include "theory/arith/nl/icp/contraction_origins.h"
 #include "theory/arith/nl/icp/intersection.h"
@@ -32,6 +31,9 @@
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 namespace icp {
 
diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp
index aa8fcf543..b5fedb7eb 100644
--- a/src/theory/arith/nl/icp/intersection.cpp
+++ b/src/theory/arith/nl/icp/intersection.cpp
@@ -18,6 +18,8 @@
 
 #include <iostream>
 
+#include <poly/polyxx.h>
+
 #include "base/check.h"
 #include "base/output.h"
 #include "theory/arith/nl/poly_conversion.h"
diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index 0df6caf34..cdc166139 100644
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -18,7 +18,9 @@
 #include "util/real_algebraic_number.h"
 
 #ifdef CVC4_POLY_IMP
-#include <poly/polyxx.h>
+namespace poly {
+  class Interval;
+}
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 5c4140430..9255d3349 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -20,6 +20,7 @@
 #include "options/theory_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/theory_model.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index cd2d15563..4d5585545 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -19,15 +19,20 @@
 #include <unordered_map>
 #include <vector>
 
-#include "context/cdo.h"
-#include "context/context.h"
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
+
+namespace context {
+class Context;
+}
+
 namespace theory {
+
+class TheoryModel;
+
 namespace arith {
 namespace nl {
 
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index c46781e76..f269f1d69 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -18,10 +18,10 @@
 #include "theory/arith/nl/nonlinear_extension.h"
 
 #include "options/arith_options.h"
-#include "options/theory_options.h"
 #include "theory/arith/arith_state.h"
-#include "theory/arith/arith_utilities.h"
 #include "theory/arith/bound_inference.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
 #include "theory/theory_model.h"
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index fba9e8e87..6a38021a0 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -21,10 +21,7 @@
 #include <map>
 #include <vector>
 
-#include "context/cdlist.h"
-#include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad_solver.h"
 #include "theory/arith/nl/ext/factoring_check.h"
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
@@ -35,19 +32,25 @@
 #include "theory/arith/nl/ext_theory_callback.h"
 #include "theory/arith/nl/iand_solver.h"
 #include "theory/arith/nl/icp/icp_solver.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/stats.h"
 #include "theory/arith/nl/strategy.h"
 #include "theory/arith/nl/transcendental/transcendental_solver.h"
 #include "theory/ext_theory.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
+namespace eq {
+  class EqualityEngine;
+}
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlLemma;
+
 /** Non-linear extension class
  *
  * This class implements model-based refinement schemes
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index 5b7edb3ef..67cfd5807 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -20,9 +20,8 @@
 
 #include "expr/node.h"
 #include "expr/node_manager_attributes.h"
-#include "util/integer.h"
+#include "theory/arith/bound_inference.h"
 #include "util/poly_util.h"
-#include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 37d816179..102d2d6ae 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -23,15 +23,18 @@
 
 #include <poly/polyxx.h>
 
-#include <iostream>
+#include <cstddef>
+#include <map>
+#include <utility>
 
 #include "expr/node.h"
-#include "theory/arith/bound_inference.h"
-#include "util/real_algebraic_number.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class BoundInference;
+
 namespace nl {
 
 /** Bijective mapping between CVC4 variables and poly variables. */
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index f869d83a4..fab4de35a 100644
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -17,8 +17,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__STATS_H
 #define CVC4__THEORY__ARITH__NL__STATS_H
 
-#include "expr/kind.h"
-#include "theory/inference_id.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h
index 526ae36f1..1f7b85b60 100644
--- a/src/theory/arith/nl/strategy.h
+++ b/src/theory/arith/nl/strategy.h
@@ -16,7 +16,6 @@
 #define CVC4__THEORY__ARITH__NL__STRATEGY_H
 
 #include <iosfwd>
-#include <map>
 #include <vector>
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 86b17376c..74766926b 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -19,9 +19,11 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index b874e1a4b..ddef4faf7 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -21,8 +21,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index f5dc49da8..11852ac3a 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index da4b48fd6..a009df09b 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -21,8 +21,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index 375f1757e..f45b906bc 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index ccdc80e0f..0e1248f7c 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -16,12 +16,14 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
 
 #include "expr/node.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 class TaylorGenerator
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index e58da1aad..d1355c746 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index 8135ba1fb..343f303d1 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -9,37 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-/*********************                                                        */
-/*! \file transcendental_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Solving for handling transcendental functions.
  **/
 
 #ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
 
-#include <map>
-#include <unordered_map>
-#include <unordered_set>
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/exponential_solver.h"
 #include "theory/arith/nl/transcendental/sine_solver.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
@@ -47,7 +25,13 @@
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 /** Transcendental solver class
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 76c3d5357..ae8c1eea7 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -14,8 +14,10 @@
 
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
+#include "expr/proof.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 93ac4627a..d0678fb9a 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -23,6 +23,7 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
 namespace CVC4 {
+class CDProof;
 namespace theory {
 namespace arith {
 namespace nl {
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 5c1b90663..d0a7f7fc4 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -19,6 +19,7 @@
 #include "base/output.h"
 #include "options/arith_options.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "theory/arith/simplex.h"
 
 
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 6740c8e1c..e34696cb5 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -57,7 +57,6 @@
 
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/error_set.h"
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
@@ -68,6 +67,8 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class ErrorSet;
+
 class SimplexDecisionProcedure {
 protected:
   typedef std::vector< std::pair<ArithVar, int> > AVIntPairVec;
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 18169474d..796cd9412 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "util/statistics_registry.h"
 
 using namespace std;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index eba84e339..f3344cbda 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,13 +22,15 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+namespace nl {
+class NonlinearExtension;
+}
 
 class TheoryArithPrivate;
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 3b5f0dd82..40bd81795 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -65,6 +65,7 @@
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/dense_map.h"
 #include "util/integer.h"
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 56e8fa4b0..818393cc7 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -43,6 +43,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/dio_solver.h"
 #include "theory/arith/dual_simplex.h"
+#include "theory/arith/error_set.h"
 #include "theory/arith/fc_simplex.h"
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/linear_equality.h"
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index 96f2b02c3..b5bb9be14 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "options/smt_options.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 4dd7dcafd..49f530e32 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -28,8 +28,10 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arrays/skolem_cache.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/decision_manager.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 
 using namespace std;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 7e4f0e36c..e02c30296 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -29,7 +29,9 @@
 #include "theory/arrays/inference_manager.h"
 #include "theory/arrays/proof_checker.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/decision_strategy.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_equality_engine.h"
 #include "util/statistics_registry.h"
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 76c001ba2..c39e0198b 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -17,6 +17,7 @@
 #include "theory/bags/bag_solver.h"
 
 #include "theory/bags/inference_generator.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace std;
 using namespace CVC4::context;
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 48cd9c419..d9f736c4f 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -19,6 +19,7 @@
 
 #include "theory/bags/rewrites.h"
 #include "theory/rewriter.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 726160d83..f00bffb2e 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "theory/booleans/proof_circuit_propagator.h"
 #include "util/utility.h"
 
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 90de1d8da..b5ad16b1c 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -25,6 +25,7 @@
 #include "theory/booleans/theory_bool_rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
 
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 551c18612..4c7311945 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -15,6 +15,7 @@
 #include "theory/bv/bitblast/simple_bitblaster.h"
 
 #include "theory/theory_model.h"
+#include "theory/theory_state.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 38e4b3aa6..d9adf06fb 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -24,6 +24,7 @@
 #include <unordered_map>
 #include <unordered_set>
 
+#include "context/cdhashset.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
 #include "theory/theory.h"
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index d8d8dbed7..3cadac621 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -30,6 +30,7 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::theory::bv::utils;
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 55a0ff46b..47974fc03 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -21,6 +21,7 @@
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/bv_solver_simple.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/ee_setup_info.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 2aa722e48..fafde0601 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -24,6 +24,7 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
+#include "theory/theory_state.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h
index 40553f01b..6793d6e90 100644
--- a/src/theory/care_graph.h
+++ b/src/theory/care_graph.h
@@ -21,8 +21,8 @@
 
 #include <set>
 
-#include "expr/kind.h"  // For TheoryId.
 #include "expr/node.h"
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 4dbf26062..5334e76df 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "options/datatypes_options.h"
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 14dc9fbf1..ea5928a42 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/infer_proof_cons.h"
 
+#include "expr/proof.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 9702a5584..4c7773e29 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -17,7 +17,11 @@
 #include "expr/dtype.h"
 #include "options/datatypes_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index ba46d2a42..610383ff1 100644
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -25,6 +25,9 @@
 
 namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace datatypes {
 
 /**
diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 6bfa20151..9a9f7cb7b 100644
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/proof_checker.h"
 
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 60bf36139..6169d3752 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/sygus_datatype_utils.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "smt/smt_engine.h"
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 7efd2a9ac..8622ec483 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -15,6 +15,7 @@
 #include "theory/datatypes/sygus_extension.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_manager.h"
 #include "expr/sygus_datatype.h"
 #include "options/base_options.h"
diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index b7ab9b4f7..a2530f4ac 100644
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/sygus_simple_sym.h"
 
+#include "expr/dtype_cons.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 45787ee04..9105cdfd6 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -19,7 +19,9 @@
 
 #include "base/check.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/kind.h"
+#include "expr/proof_node_manager.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 2834b86ba..73aef4dd7 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/type_matcher.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 
diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index c55b4a14f..1247ecca5 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/theory_datatypes_utils.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 079430342..25bdd2f94 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -14,6 +14,7 @@
  ** Enumerators for datatypes.
  **/
 
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/type_enumerator.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index 7b4936a53..030d9a497 100644
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -20,7 +20,9 @@
 
 #include "base/check.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/substitutions.h"
 
 using namespace std;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 6df991ef9..e9b59fdae 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -22,9 +22,12 @@
 #include <unordered_set>
 #include <vector>
 
+#include "base/configuration.h"
 #include "options/fp_options.h"
+#include "smt/logic_exception.h"
 #include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
+#include "theory/output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 1a745b3a3..bd6e70ff1 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -23,9 +23,11 @@
 #include <string>
 #include <utility>
 
+#include "context/cdhashset.h"
 #include "context/cdo.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 0c143f265..3e4b921db 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index bb2bf937a..24570f9a6 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -18,6 +18,7 @@
 #include "options/theory_options.h"
 #include "prop/prop_engine.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index 16f0f3957..7a584c146 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 0d1a51a30..bda4e31fc 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -18,6 +18,8 @@
 #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index e782a1b6f..0c416fdf4 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -17,6 +17,7 @@
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index eb02eb19e..c553a1239 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -14,11 +14,13 @@
 
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 5df350fe5..1875dc631 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -16,7 +16,10 @@
 
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
 #include "util/hash.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index ce535d5e8..07cb74a83 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 5c5dcfef1..dfe2e3ae9 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -15,7 +15,9 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi.h"
 
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
index 66433ba78..00a233d6a 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -14,6 +14,8 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/term_util.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 6b2f1b7f8..f9692bd76 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -14,6 +14,11 @@
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 
 #include "theory/quantifiers/ematching/trigger_term_info.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index e7635f200..9768e7f2c 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/quant_relevance.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 #include "util/random.h"
 
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index 14913bdc1..c2b5f78ae 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
 
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index a64dc4424..6564f407e 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@ -18,6 +18,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 79bd5c1dd..9d8b64e25 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -22,10 +22,12 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index 8448fe810..17baf5000 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -13,7 +13,9 @@
  **/
 #include "theory/quantifiers/ematching/var_match_generator.h"
 
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 759d3e69f..6ce561b2d 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -19,6 +19,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 700ae2c64..fb0505bae 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -16,10 +16,12 @@
 
 #include "theory/quantifiers/fmf/bounded_integers.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/term_enumeration.h"
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 9d4a414e9..3e7466ed2 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -23,6 +23,7 @@
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "expr/attribute.h"
+#include "theory/decision_strategy.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 96e8a40be..c248167cb 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/inst_match.h"
 
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index 993fad90a..ab5dcb166 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace CVC4::context;
 
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 2eb99a774..3164ff5ce 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/instantiate.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index a0b776819..37cc49f17 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -19,6 +19,8 @@
 
 #include <map>
 
+#include "context/cdhashset.h"
+#include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "expr/proof.h"
 #include "theory/quantifiers/inst_match_trie.h"
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index f89f9f0ea..cf37bc746 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/quant_conflict_find.h"
 
+#include "base/configuration.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp
index 5bb50c926..58716f809 100644
--- a/src/theory/quantifiers/quant_rep_bound_ext.cpp
+++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/quant_rep_bound_ext.h"
 
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index a0b780836..e3bd2072f 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -13,6 +13,9 @@
  **/
 
 #include "theory/quantifiers/quant_split.h"
+
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/first_order_model.h"
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2126bf1f0..ec7e7fd2c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
@@ -27,6 +28,7 @@
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 0bcca266e..55f680897 100644
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/quantifiers_state.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 3cef2884f..b97a8e539 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index a9ac7d0d2..42729ef5b 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/skolemize.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index b296a4421..77714f87d 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "smt/command.h"
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index db2a972d5..a58ce894d 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/cegis_core_connective.h"
 
+#include "expr/dtype_cons.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 9db77fd95..5da6f2121 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -19,6 +19,7 @@
 #include <map>
 #include <vector>
 
+#include "theory/decision_strategy.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 360476399..f6e34e8a1 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/sygus/enum_stream_substitution.h"
 
+#include "expr/dtype_cons.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index e0159049b..2fa6009d3 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 882c9ca77..90765284a 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -14,10 +14,12 @@
 
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 0f9d2ccd1..5965e9430 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_explain.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 538d80e44..98a177f86 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -16,6 +16,7 @@
 
 #include <stack>
 
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 7d757ca98..953eac7b0 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 6e36222b6..cc29e7b0a 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index 1e67bb8cc..a2675dd96 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -19,6 +19,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 81120da28..8b741b6d7 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 
 #include "api/cvc4cpp.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index f0d3e47b6..1c0cfcc55 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -15,12 +15,14 @@
 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_unif.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 0fcba916b..56691c7c1 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -14,6 +14,7 @@
  **/
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
+#include "base/configuration.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index bc5cd1fda..f393601ad 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 #include "base/check.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
@@ -23,6 +24,8 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index d44d2eda8..8e29ab9d6 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -16,6 +16,7 @@
 
 #include "base/check.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 9fdf0aa7f..a46d4e445 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -18,11 +18,14 @@
 #include <unordered_set>
 
 #include "expr/node_algorithm.h"
+#include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 3116f35e6..17cb1c9a1 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -21,6 +21,7 @@
 #include <unordered_set>
 
 #include "context/cdhashset.h"
+#include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 62eef124a..a72054f6d 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus_sampler.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cb5c7dfec..281d5c844 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -21,6 +21,8 @@
 #include "options/uf_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9a031f99c..b121b2c46 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -20,6 +20,8 @@
 #include <map>
 #include <unordered_set>
 
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
 #include "expr/attribute.h"
 #include "expr/node_trie.h"
 #include "theory/quantifiers/quant_util.h"
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 9cbf2cf53..33f74c7c4 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/strings/word.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 036b63b27..98bb9bec3 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -18,7 +18,6 @@
 #define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
 
 #include <map>
-#include <unordered_set>
 
 #include "expr/attribute.h"
 #include "expr/node.h"
@@ -55,8 +54,6 @@ typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
 
 namespace quantifiers {
 
-class TermDatabase;
-
 // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
 class TermUtil
 {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7046a8ef0..79422b418 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -20,10 +20,22 @@
 #include "options/uf_options.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/equality_query.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_modules.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/skolemize.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f464b24d4..d08e32f6e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -20,23 +20,11 @@
 #include <map>
 #include <unordered_map>
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
-#include "expr/attribute.h"
-#include "theory/quantifiers/ematching/trigger_trie.h"
-#include "theory/quantifiers/equality_query.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/model_builder.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/quantifiers_inference_manager.h"
-#include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -46,9 +34,24 @@ class TheoryEngine;
 namespace theory {
 
 class DecisionManager;
+class QuantifiersModule;
+class RepSetIterator;
 
+namespace inst {
+class TriggerTrie;
+}
 namespace quantifiers {
+class EqualityQueryQuantifiersEngine;
+class FirstOrderModel;
+class Instantiate;
+class QModelBuilder;
+class QuantifiersInferenceManager;
 class QuantifiersModules;
+class QuantifiersState;
+class Skolemize;
+class TermDb;
+class TermDbSygus;
+class TermEnumeration;
 }
 
 // TODO: organize this more/review this, github issue #1163
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index be26510c6..fc98e6198 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/rewriter.h"
 
+#include "expr/term_conversion_proof_generator.h"
 #include "options/theory_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 572662483..f5c1348ad 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -19,20 +19,21 @@
 #pragma once
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
 #include "theory/theory_rewriter.h"
-#include "theory/trust_node.h"
-#include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
+
+class TConvProofGenerator;
+class ProofNodeManager;
+
 namespace theory {
 
+class TrustNode;
+
 namespace builtin {
 class BuiltinProofRuleChecker;
 }
 
-class RewriterInitializer;
-
 /**
  * The rewrite environment holds everything that the individual rewrites have
  * access to.
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 2a409a304..0a8039ed1 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -24,6 +24,7 @@
 #include "options/sep_options.h"
 #include "options/smt_options.h"
 #include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index b2cd6bf45..198273993 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -23,9 +23,11 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
+#include "theory/decision_strategy.h"
 #include "theory/inference_manager_buffered.h"
 #include "theory/sep/theory_sep_rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 13ee672db..0d832b646 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -18,6 +18,7 @@
 #define SRC_THEORY_SETS_RELS_UTILS_H_
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index e06a8cb52..5c6300059 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -20,6 +20,7 @@
 #include "theory/sets/theory_sets_private.h"
 #include "theory/sets/theory_sets_rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 1e4473d6f..eb802af4a 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/sets/theory_sets_rewriter.h"
 
 #include "expr/attribute.h"
+#include "expr/dtype_cons.h"
 #include "options/sets_options.h"
 #include "theory/sets/normal_form.h"
 #include "theory/sets/rels_utils.h"
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 5446f67be..642a4d4ae 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 "options/strings_options.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/strings_entail.h"
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 770991286..620cca185 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/strings/regexp_elim.h"
 
+#include "expr/proof_node_manager.h"
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
 #include "theory/strings/regexp_entail.h"
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0157a47f0..bd95933a5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -19,6 +19,7 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 82463367e..a725f4d88 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/term_registration_visitor.h"
 
+#include "base/configuration.h"
 #include "options/quantifiers_options.h"
 #include "theory/theory_engine.h"
 
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index fef3fdc67..19fc91312 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -26,10 +26,16 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/ee_setup_info.h"
 #include "theory/ext_theory.h"
+#include "theory/output_channel.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/substitutions.h"
+#include "theory/theory_inference_manager.h"
+#include "theory/theory_model.h"
 #include "theory/theory_rewriter.h"
+#include "theory/theory_state.h"
+#include "theory/trust_substitutions.h"
 
 using namespace std;
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index fa26ab65e..5f4698e56 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -20,49 +20,39 @@
 #define CVC4__THEORY__THEORY_H
 
 #include <iosfwd>
-#include <map>
 #include <set>
 #include <string>
 #include <unordered_set>
 
-#include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "options/options.h"
 #include "options/theory_options.h"
-#include "smt/logic_request.h"
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
-#include "theory/decision_manager.h"
-#include "theory/ee_setup_info.h"
 #include "theory/logic_info.h"
-#include "theory/output_channel.h"
 #include "theory/theory_id.h"
-#include "theory/theory_inference_manager.h"
-#include "theory/theory_rewriter.h"
-#include "theory/theory_state.h"
 #include "theory/trust_node.h"
-#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 
-class TheoryEngine;
 class ProofNodeManager;
+class TheoryEngine;
 
 namespace theory {
 
+class DecisionManager;
+struct EeSetupInfo;
+class OutputChannel;
 class QuantifiersEngine;
+class TheoryInferenceManager;
 class TheoryModel;
-class SubstitutionMap;
 class TheoryRewriter;
-
-namespace rrinst {
-  class CandidateGenerator;
-}/* CVC4::theory::rrinst namespace */
+class TheoryState;
+class TrustSubstitutionMap;
 
 namespace eq {
   class EqualityEngine;
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 53a812653..810f31ce5 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -15,8 +15,11 @@
 #include "theory/theory_inference_manager.h"
 
 #include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index d3a317cbc..61b105dac 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -23,9 +23,8 @@
 #include "expr/node.h"
 #include "theory/inference_id.h"
 #include "theory/output_channel.h"
-#include "theory/theory_state.h"
 #include "theory/trust_node.h"
-#include "theory/uf/proof_equality_engine.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -34,8 +33,10 @@ class ProofNodeManager;
 namespace theory {
 
 class Theory;
+class TheoryState;
 namespace eq {
 class EqualityEngine;
+class ProofEqEngine;
 }
 
 /**
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 9604dc72b..89f53acb8 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -14,6 +14,7 @@
 #include "theory/theory_model_builder.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index a0586bd0c..d4d2a78a5 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -18,11 +18,11 @@
 #define CVC4__THEORY__TRUST_NODE_H
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 
 class ProofGenerator;
+class ProofNode;
 
 namespace theory {
 
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 7ab43091a..58d5f4924 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/uf/eq_proof.h"
 
+#include "base/configuration.h"
 #include "expr/proof.h"
 #include "options/uf_options.h"
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 497e394c7..49e19c15f 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -25,6 +25,7 @@
 #include "expr/node_trie.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
 #include "theory/uf/proof_equality_engine.h"