Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

239 files changed, 441 insertions, 277 deletions

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index e25945291..4ab552001 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -86,7 +86,6 @@
 #include <functional>
 #include <iterator>
 #include <unordered_map>
-#include <vector>
 
 #include "base/check.h"
 #include "context/cdhashmap_forward.h"
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 2abd0b824..b1c8229f0 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -22,9 +22,7 @@
 
 #include <cstring>
 #include <iterator>
-#include <memory>
 #include <string>
-#include <sstream>
 
 #include "base/check.h"
 #include "context/cdlist_forward.h"
diff --git a/src/context/cdtrail_queue.h b/src/context/cdtrail_queue.h
index cf36156cf..f505004cb 100644
--- a/src/context/cdtrail_queue.h
+++ b/src/context/cdtrail_queue.h
@@ -22,12 +22,13 @@
 #ifndef CVC4__CONTEXT__CDTRAIL_QUEUE_H
 #define CVC4__CONTEXT__CDTRAIL_QUEUE_H
 
-#include "context/context.h"
 #include "context/cdlist.h"
+#include "context/cdo.h"
 
 namespace CVC4 {
 namespace context {
 
+class Context;
 
 template <class T>
 class CDTrailQueue {
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index db9d89dd1..4d9413320 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -15,9 +15,11 @@
  **/
 
 #include <cstdlib>
-#include <vector>
 #include <deque>
+#include <limits>
 #include <new>
+#include <ostream>
+#include <vector>
 
 #ifdef CVC4_VALGRIND
 #include <valgrind/memcheck.h>
@@ -166,6 +168,12 @@ void ContextMemoryManager::pop() {
     d_freeChunks.pop_front();
   }
 }
+#else
+
+unsigned ContextMemoryManager::getMaxAllocationSize()
+{
+  return std::numeric_limits<unsigned>::max();
+}
 
 #endif /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */
 
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index 43e0e1f94..e20b9fdb9 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -20,8 +20,9 @@
 #ifndef CVC4__CONTEXT__CONTEXT_MM_H
 #define CVC4__CONTEXT__CONTEXT_MM_H
 
+#ifndef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
 #include <deque>
-#include <limits>
+#endif
 #include <vector>
 
 namespace CVC4 {
@@ -161,10 +162,7 @@ class ContextMemoryManager {
 class ContextMemoryManager
 {
  public:
-  static unsigned getMaxAllocationSize()
-  {
-    return std::numeric_limits<unsigned>::max();
-  }
+  static unsigned getMaxAllocationSize();
 
   ContextMemoryManager() { d_allocations.push_back(std::vector<char*>()); }
   ~ContextMemoryManager()
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 99e0bd969..7eba1b2ea 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -36,7 +36,6 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
-#include "options/options.h"
 
 namespace CVC4 {
 
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 5bea85b00..42c386220 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/node_manager.h"
 #include "options/smt_options.h"
+#include "expr/lazy_proof.h"
 #include "proof/proof_manager.h"
 #include "smt/preprocess_proof_generator.h"
 #include "theory/builtin/proof_checker.h"
diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp
index 82c1a14d4..9f26d3800 100644
--- a/src/printer/let_binding.cpp
+++ b/src/printer/let_binding.cpp
@@ -14,6 +14,8 @@
 
 #include "printer/let_binding.h"
 
+#include <sstream>
+
 namespace CVC4 {
 
 LetBinding::LetBinding(uint32_t thresh)
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 26bab2e5c..17d2f4d2f 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -32,6 +32,7 @@ namespace CVC4 {
 class ResourceManager;
 class DecisionEngine;
 class OutputManager;
+class ProofNodeManager;
 class TheoryEngine;
 
 namespace prop {
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 6ad0562ab..5fcb57beb 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/assertions.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/language.h"
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 167caf379..1a8a6e3d0 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -20,7 +20,6 @@
 #include <memory>
 #include <vector>
 
-#include "context/context.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 84c4acfac..ed19549c9 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -17,16 +17,18 @@
 #ifndef CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
 #define CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
 
-#include <map>
-
 #include "context/cdhashmap.h"
 #include "expr/lazy_proof.h"
+#include "expr/proof.h"
 #include "expr/proof_set.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class LazyCDProof;
+class ProofNodeManager;
+
 namespace smt {
 
 /**
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index a3c3a5ae2..e5dd7869c 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -15,6 +15,7 @@
 #include "smt/preprocessor.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "printer/printer.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 0191d17e5..eadbbedc5 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -30,6 +30,7 @@ class PreprocessingPassContext;
 namespace smt {
 
 class AbstractValues;
+class PreprocessProofGenerator;
 
 /**
  * The preprocessor module of an SMT engine.
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 45cd8284d..9a6486ded 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -14,7 +14,6 @@
 
 #include "smt/process_assertions.h"
 
-#include <stack>
 #include <utility>
 
 #include "expr/node_manager_attributes.h"
@@ -27,8 +26,10 @@
 #include "options/strings_options.h"
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_registry.h"
 #include "printer/printer.h"
+#include "smt/assertions.h"
 #include "smt/defined_function.h"
 #include "smt/dump.h"
 #include "smt/expand_definitions.h"
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index b05779780..f1c0aed3b 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -21,18 +21,21 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/type_node.h"
-#include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "smt/assertions.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
 
 class SmtEngine;
 
+namespace preprocessing {
+class AssertionPipeline;
+class PreprocessingPass;
+class PreprocessingPassContext;
+}
+
 namespace smt {
 
+class Assertions;
 class ExpandDefs;
 struct SmtEngineStatistics;
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 79678a5c0..7e8a4fb86 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -44,6 +44,7 @@
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
+#include "smt/logic_exception.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
 #include "smt/node_command.h"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 50f7ddfc7..4f10b6bc5 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -19,12 +19,12 @@
 #ifndef CVC4__SMT_ENGINE_H
 #define CVC4__SMT_ENGINE_H
 
+#include <map>
+#include <memory>
 #include <string>
 #include <vector>
-#include <map>
 
 #include "context/cdhashmap_forward.h"
-#include "context/cdlist_forward.h"
 #include "options/options.h"
 #include "smt/output_manager.h"
 #include "smt/smt_mode.h"
@@ -87,7 +87,6 @@ class Model;
 class SmtEngineState;
 class AbstractValues;
 class Assertions;
-class ExprNames;
 class DumpManager;
 class ResourceOutListener;
 class SmtNodeManagerListener;
@@ -110,7 +109,6 @@ class DefinedFunction;
 
 struct SmtEngineStatistics;
 class SmtScope;
-class ProcessAssertions;
 class PfManager;
 class UnsatCoreManager;
 
@@ -120,7 +118,6 @@ ProofManager* currentProofManager();
 /* -------------------------------------------------------------------------- */
 
 namespace theory {
-  class TheoryModel;
   class Rewriter;
   class QuantifiersEngine;
 }/* CVC4::theory namespace */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ab251503b..89e75d892 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_state.h"
 #include "smt/smt_engine_stats.h"
+#include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_traits.h"
 
diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h
index ba02b5746..daa83ed54 100644
--- a/src/smt/unsat_core_manager.h
+++ b/src/smt/unsat_core_manager.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__SMT__UNSAT_CORE_MANAGER_H
 #define CVC4__SMT__UNSAT_CORE_MANAGER_H
 
-#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/proof_node.h"
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index 66e35bd52..c48948ade 100644
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -19,7 +19,6 @@
 
 #include <unordered_set>
 
-#include "expr/node_manager.h"
 #include "expr/proof.h"
 #include "expr/proof_generator.h"
 #include "expr/term_conversion_proof_generator.h"
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 152146cdf..80690f39c 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -28,6 +28,7 @@
 #include "theory/arith/cut_log.h"
 #include "theory/arith/matrix.h"
 #include "theory/arith/normal_form.h"
+#include "theory/eager_proof_generator.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 58e115b81..46e252ec7 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -66,7 +66,6 @@ class NodeLog;
 class TreeLog;
 class ArithVariables;
 class CutInfo;
-class RowsDeleted;
 
 class ApproximateSimplex{
  public:
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 0c1923448..a075c87fe 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/arith/arith_preprocess.h"
 
+#include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/skolem_lemma.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 69cc02bb9..db0fd7d5e 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -18,16 +18,19 @@
 #define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
 
 #include "context/cdhashmap.h"
-#include "theory/arith/arith_state.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/logic_info.h"
-#include "theory/skolem_lemma.h"
 
 namespace CVC4 {
 namespace theory {
+
+class SkolemLemma;
+
 namespace arith {
 
+class ArithState;
+class InferenceManager;
+
 /**
  * This module can be used for (on demand) elimination of extended arithmetic
  * operators like div, mod, to_int, is_int, sqrt, and so on. It uses the
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 2b74e6005..799d0bcee 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -20,14 +20,15 @@
 #ifndef CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 #define CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 
-#include <set>
-
 #include "context/cdhashmap.h"
-#include "context/context.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/delta_rational.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index f9051328c..4f1f50b7a 100644
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -14,6 +14,8 @@
 
 #include "arith_utilities.h"
 
+#include <cmath>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -114,7 +116,7 @@ Node getApproximateConstant(Node c, bool isLower, unsigned prec)
   Rational cr = c.getConst<Rational>();
 
   unsigned lower = 0;
-  unsigned upper = pow(10, prec);
+  unsigned upper = std::pow(10, prec);
 
   Rational den = Rational(upper);
   if (cr.getDenominator() < den.getNumerator())
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index e4d6bd0ee..40ca7b8f6 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 #define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
-#include <math.h>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
@@ -25,7 +24,6 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
 #include "util/dense_map.h"
 #include "util/integer.h"
 #include "util/rational.h"
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index efcb96325..e5c995971 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -21,6 +21,8 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
+#include "theory/arith/tableau.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 84bfafcc8..ee412483b 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/arith/callbacks.h"
 
+#include "expr/proof_node.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/arith/theory_arith_private.h"
 
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 9fbe3b90f..574d289b0 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -18,13 +18,15 @@
 #pragma once
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/constraint_forward.h"
 #include "util/rational.h"
 
 namespace CVC4 {
+
+class ProofNode;
+
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 636cebe5f..f2210574b 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -18,9 +18,16 @@
 #include "theory/arith/congruence_manager.h"
 
 #include "base/output.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/partial_model.h"
+#include "theory/ee_setup_info.h"
+#include "theory/rewriter.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
 #include "options/arith_options.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index f2aef815f..9815ad9c8 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -19,27 +19,42 @@
 
 #pragma once
 
+#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "context/cdmaybe.h"
-#include "context/cdo.h"
 #include "context/cdtrail_queue.h"
-#include "context/context.h"
-#include "expr/proof_node_manager.h"
 #include "theory/arith/arithvar.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/callbacks.h"
 #include "theory/arith/constraint_forward.h"
-#include "theory/arith/partial_model.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/ee_setup_info.h"
 #include "theory/trust_node.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/proof_equality_engine.h"
+#include "theory/uf/equality_engine_notify.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
+namespace context {
+class Context;
+class UserContext;
+}
+
 namespace theory {
+
+class EagerProofGenerator;
+struct EeSetupInfo;
+
+namespace eq {
+class ProofEqEngine;
+class EqualityEngine;
+}
+
 namespace arith {
 
+class ArithVariables;
+
 class ArithCongruenceManager {
 private:
   context::CDRaised d_inConflict;
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 70106b14c..bafd4d682 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -21,9 +21,14 @@
 #include <unordered_set>
 
 #include "base/output.h"
+#include "expr/proof_node_manager.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/congruence_manager.h"
 #include "theory/arith/normal_form.h"
+#include "theory/arith/partial_model.h"
+#include "theory/rewriter.h"
 
 
 using namespace std;
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 6a73d69d2..6ac03bb82 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -78,36 +78,38 @@
 #ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
 #define CVC4__THEORY__ARITH__CONSTRAINT_H
 
-#include <list>
-#include <set>
 #include <unordered_map>
 #include <vector>
 
 #include "base/configuration_private.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "expr/node.h"
-#include "expr/proof_node_manager.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/callbacks.h"
-#include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/trust_node.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
-namespace theory {
-namespace arith {
-class Comparison;
-}
-}
+
+class ProofNodeManager;
+
+namespace context {
+class Context;
 }
-namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace arith {
 
+class Comparison;
+class ArithCongruenceManager;
+class ArithVariables;
+
 /**
  * Logs the types of different proofs.
  * Current, proof types:
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index f6f974fca..2b67026dc 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -22,13 +22,11 @@
 #include <unordered_map>
 #include <map>
 #include <set>
-#include <vector>
 
 #include "expr/kind.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
 #include "util/dense_map.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -230,7 +228,6 @@ public:
 };
 std::ostream& operator<<(std::ostream& os, const NodeLog& nl);
 
-class ApproximateSimplex;
 class TreeLog {
 private:
   int next_exec_ord;
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 2c06967c4..a232464e5 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -20,6 +20,7 @@
 #include "base/output.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/arith/partial_model.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 571c64a78..3ce7199c0 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -24,18 +24,18 @@
 #include <utility>
 #include <vector>
 
-#include "base/output.h"
 #include "context/cdlist.h"
 #include "context/cdmaybe.h"
 #include "context/cdo.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "theory/arith/normal_form.h"
-#include "theory/arith/partial_model.h"
 #include "util/rational.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 3784ec79b..5ad2f16c0 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
 
 
 using namespace std;
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 34d695f8a..7400a229f 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -62,7 +62,6 @@ namespace arith {
 
 
 class ErrorSet;
-class ErrorInfoMap;
 
 class ComparatorPivotRule {
 private:
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 658f7c23e..45a9b79bb 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -55,7 +55,9 @@
 #pragma once
 
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
 #include "theory/arith/simplex.h"
+#include "theory/arith/simplex_update.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index e1eb786d0..03ab8e53b 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -23,7 +23,6 @@
 
 #include "expr/node.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/theory.h"
 #include "util/integer.h"
 #include "util/maybe.h"
 #include "util/rational.h"
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index c4281f0bd..a281c825b 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/inference_manager.h"
 
 #include "options/arith_options.h"
+#include "theory/arith/arith_state.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index 80cb62201..dd617f4a3 100644
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -17,18 +17,16 @@
 #ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
 #define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
 
-#include <map>
 #include <vector>
 
-#include "theory/arith/arith_state.h"
 #include "theory/inference_id.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/inference_manager_buffered.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class ArithState;
 class TheoryArith;
 
 /**
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index f0a3fbe25..42f8920c8 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -23,12 +23,9 @@
 
 #include <poly/polyxx.h>
 
-#include <map>
 #include <tuple>
 #include <vector>
 
-#include "expr/kind.h"
-#include "expr/node_manager_attributes.h"
 #include "theory/arith/nl/poly_conversion.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index 9302cb7f2..33267cb7a 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -23,8 +23,6 @@
 
 #include <poly/polyxx.h>
 
-#include <algorithm>
-#include <iostream>
 #include <vector>
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
index f13e6f4a3..5ebe0c6b7 100644
--- a/src/theory/arith/nl/cad/proof_checker.h
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index 62d3c03ff..9f0799e7c 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -16,6 +16,9 @@
 
 #ifdef CVC4_POLY_IMP
 
+#include "theory/lazy_tree_proof_generator.h"
+#include "theory/arith/nl/poly_conversion.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 72f0f766b..4709b8e59 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -23,18 +23,21 @@
 
 #include <vector>
 
-#include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/proof_generator.h"
 #include "expr/proof_set.h"
 #include "theory/arith/nl/cad/cdcac_utils.h"
-#include "theory/arith/nl/poly_conversion.h"
 #include "theory/lazy_tree_proof_generator.h"
 
 namespace CVC4 {
+
+class ProofGenerator;
+
 namespace theory {
 namespace arith {
 namespace nl {
+
+struct VariableMapper;
+
 namespace cad {
 
 /**
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 3a7d5159a..b83398cd6 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -23,6 +23,9 @@
 #include "theory/arith/nl/cad/proof_checker.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp
index 452368640..9ec3b1fc1 100644
--- a/src/theory/arith/nl/ext/constraint.cpp
+++ b/src/theory/arith/nl/ext/constraint.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/ext/monomial.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h
index 2f439f65e..d5ed7ccfd 100644
--- a/src/theory/arith/nl/ext/constraint.h
+++ b/src/theory/arith/nl/ext/constraint.h
@@ -20,13 +20,14 @@
 
 #include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/nl/ext/monomial.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+class MonomialDb;
+
 /** constraint information
  *
  * The struct ( d_rhs, d_coeff, d_type ) represents that a literal is of the
diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index c7841748f..28373223b 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -21,6 +21,8 @@
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index f64fc8feb..7a0da42aa 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -20,6 +20,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h
index c8d27ec27..4c017d198 100644
--- a/src/theory/arith/nl/ext/factoring_check.h
+++ b/src/theory/arith/nl/ext/factoring_check.h
@@ -18,13 +18,17 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
+
+class CDProof;
+
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class FactoringCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 2c25a6e29..47cb5daec 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -20,6 +20,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h
index 103e2725f..e7ba4d861 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.h
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.h
@@ -17,13 +17,14 @@
 
 #include "expr/node.h"
 #include "theory/arith/nl/ext/constraint.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class MonomialBoundsCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index 3f62d0afb..7f99b876d 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -19,6 +19,8 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index b964f00a4..a08554476 100644
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -16,14 +16,16 @@
 #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
 
 #include "expr/node.h"
+#include "theory/arith/nl/ext/monomial.h"
 #include "theory/theory_inference.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class MonomialCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 09954bf19..45f4160a0 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index bee2fe405..030445737 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -17,13 +17,14 @@
 
 #include "expr/node.h"
 #include "context/cdhashset.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class SplitZeroCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 254151283..64ea19f3c 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h
index e0656789b..a771ae543 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.h
+++ b/src/theory/arith/nl/ext/tangent_plane_check.h
@@ -15,14 +15,17 @@
 #ifndef CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
 #define CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
 
+#include <map>
+
 #include "expr/node.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class TangentPlaneCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h
index f1ad3df20..a3dc74ec8 100644
--- a/src/theory/arith/nl/ext_theory_callback.h
+++ b/src/theory/arith/nl/ext_theory_callback.h
@@ -20,6 +20,9 @@
 
 namespace CVC4 {
 namespace theory {
+namespace eq {
+class EqualityEngine;
+}
 namespace arith {
 namespace nl {
 
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index e484252f2..137d430c0 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -21,7 +21,6 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "theory/arith/nl/iand_utils.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h
index 15ccab231..a84fcf978 100644
--- a/src/theory/arith/nl/iand_utils.h
+++ b/src/theory/arith/nl/iand_utils.h
@@ -17,7 +17,6 @@
 #define CVC4__THEORY__ARITH__IAND_TABLE_H
 
 #include <map>
-#include <vector>
 
 #include "expr/node.h"
 
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index dae13318c..5467c64ce 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/arith/nl/nl_lemma_utils.h"
 #include "theory/theory_model.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index f907963c1..cd52cb159 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -21,7 +21,6 @@
 
 #include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 
 namespace CVC4 {
 
@@ -36,6 +35,7 @@ class TheoryModel;
 namespace arith {
 namespace nl {
 
+class NlLemma;
 class NonlinearExtension;
 
 /** Non-linear model finder
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 38243823b..3f32e7075 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -24,6 +24,7 @@
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 47d62e607..baa0f886c 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -23,6 +23,7 @@
 
 #include "expr/node.h"
 #include "theory/arith/nl/cad_solver.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/ext/factoring_check.h"
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
 #include "theory/arith/nl/ext/monomial_check.h"
@@ -37,6 +38,7 @@
 #include "theory/arith/nl/strategy.h"
 #include "theory/arith/nl/transcendental/transcendental_solver.h"
 #include "theory/ext_theory.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -46,6 +48,7 @@ namespace eq {
 namespace arith {
 
 class InferenceManager;
+class TheoryArith;
 
 namespace nl {
 
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 68d5a5f31..8b6f4484d 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -24,6 +24,8 @@
 #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/arith/nl/transcendental/transcendental_state.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 76b14022f..484174d5f 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -16,12 +16,8 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
 
 #include <map>
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {
 namespace theory {
@@ -29,6 +25,8 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
+struct TranscendentalState;
+
 /** Transcendental solver class
  *
  * This class implements model-based refinement schemes
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 0e5c09a2f..528e0bea2 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -23,6 +23,9 @@
 #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/arith/nl/transcendental/transcendental_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index 0b2e9d920..c628559fc 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -16,9 +16,6 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
 
 #include <map>
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
 
 #include "expr/node.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index c6b929fec..f236b472a 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -23,6 +23,7 @@
 #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/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 438cc7047..593354794 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -16,6 +16,8 @@
 
 #include "expr/proof.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 33994fa3a..cd5466e89 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -17,8 +17,7 @@
 
 #include "expr/node.h"
 #include "expr/proof_set.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/transcendental/proof_checker.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
@@ -26,7 +25,13 @@ namespace CVC4 {
 class CDProof;
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 /**
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index bf8ec6c58..c3500e699 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -21,7 +21,6 @@
 #define CVC4__THEORY__ARITH__NORMAL_FORM_H
 
 #include <algorithm>
-#include <list>
 
 #include "base/output.h"
 #include "expr/node.h"
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 6a9a130ca..c6f961129 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -17,6 +17,7 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "options/arith_options.h"
 #include "smt/logic_exception.h"
 #include "theory/arith/arith_utilities.h"
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index 6dc535444..489974eac 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -17,12 +17,14 @@
 #include <map>
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/logic_info.h"
 #include "theory/skolem_lemma.h"
 
 namespace CVC4 {
+
+class TConvProofGenerator;
+
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index ec682b948..af0fe37ec 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -21,11 +21,9 @@
 #ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 #define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 
-#include <list>
 #include <vector>
 
 #include "context/cdlist.h"
-#include "context/context.h"
 #include "expr/node.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
@@ -35,6 +33,9 @@
 #include "theory/arith/delta_rational.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h
index 8d2a94215..0745bdd61 100644
--- a/src/theory/arith/proof_checker.h
+++ b/src/theory/arith/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index c383c3a85..fc3d919c3 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -15,12 +15,14 @@
  ** \todo document this file
  **/
 
+#include "theory/arith/simplex.h"
+
 #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"
-
+#include "theory/arith/linear_equality.h"
+#include "theory/arith/tableau.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d1f891676..110093068 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -56,19 +56,20 @@
 
 #include <unordered_map>
 
+#include "options/arith_options.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/linear_equality.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/tableau.h"
 #include "util/dense_map.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
 class ErrorSet;
+class LinearEqualityModule;
+class Tableau;
 
 class SimplexDecisionProcedure {
 protected:
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index d47dba70f..79136e77c 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/tableau.h"
 #include "util/statistics_registry.h"
 
 using namespace std;
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 5febe1bb0..d9d11dcc5 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -54,7 +54,9 @@
 
 #pragma once
 
+#include "theory/arith/linear_equality.h"
 #include "theory/arith/simplex.h"
+#include "theory/arith/simplex_update.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 42cd16efc..937901c57 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -25,6 +25,8 @@
 #include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/ext_theory.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1a41c9301..a208c9b10 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,7 +22,6 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
-#include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 583ff8dee..55a2472b3 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -18,22 +18,15 @@
 #pragma once
 
 #include <map>
-#include <queue>
 #include <vector>
 
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "expr/kind.h"
-#include "expr/metakind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/proof_generator.h"
-#include "options/arith_options.h"
-#include "smt/logic_exception.h"
-#include "smt_util/boolean_simplification.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
@@ -51,12 +44,8 @@
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/proof_checker.h"
-#include "theory/arith/simplex.h"
 #include "theory/arith/soi_simplex.h"
 #include "theory/arith/theory_arith.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/rewriter.h"
-#include "theory/theory_model.h"
 #include "theory/trust_node.h"
 #include "theory/valuation.h"
 #include "util/dense_map.h"
@@ -67,6 +56,10 @@
 
 namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+class TheoryModel;
+
 namespace arith {
 
 class BranchCutInfo;
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 5adb0e783..499f96bfb 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -18,14 +18,11 @@
 #ifndef CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 #define CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 
-#include <iostream>
-#include <map>
 #include <tuple>
 #include <unordered_map>
 
 #include "context/backtrackable.h"
 #include "context/cdlist.h"
-#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h
index a8d1407a8..053502788 100644
--- a/src/theory/arrays/proof_checker.h
+++ b/src/theory/arrays/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 34a7a71b9..689e72a44 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -33,7 +33,6 @@
 #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"
 
 namespace CVC4 {
diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h
index 05c159b4b..b8a653bc3 100644
--- a/src/theory/atom_requests.h
+++ b/src/theory/atom_requests.h
@@ -20,7 +20,7 @@
 #pragma once
 
 #include "expr/node.h"
-#include "theory/theory.h"
+#include "theory/theory_id.h"
 #include "context/cdlist.h"
 #include "context/cdhashset.h"
 #include "context/cdhashmap.h"
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 869b229ea..a7a0f8796 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -17,6 +17,10 @@
 #include "theory/bags/bag_solver.h"
 
 #include "theory/bags/inference_generator.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/normal_form.h"
+#include "theory/bags/solver_state.h"
+#include "theory/bags/term_registry.h"
 #include "theory/uf/equality_engine_iterator.h"
 
 using namespace std;
diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h
index e524f7422..914a12ae2 100644
--- a/src/theory/bags/bag_solver.h
+++ b/src/theory/bags/bag_solver.h
@@ -17,19 +17,16 @@
 #ifndef CVC4__THEORY__BAG__SOLVER_H
 #define CVC4__THEORY__BAG__SOLVER_H
 
-#include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "theory/bags/infer_info.h"
 #include "theory/bags/inference_generator.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/normal_form.h"
-#include "theory/bags/solver_state.h"
-#include "theory/bags/term_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+class TermRegistry;
+
 /** The solver for the theory of bags
  *
  */
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 3718aedb7..51b2e5438 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -18,7 +18,7 @@
 #define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
 
 #include "theory/bags/rewrites.h"
-#include "theory/rewriter.h"
+#include "theory/theory_rewriter.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index caf4070ec..f59c43cb6 100644
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__BAGS_STATISTICS_H
 #define CVC4__THEORY__BAGS_STATISTICS_H
 
-#include "expr/kind.h"
 #include "theory/bags/rewrites.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index c61075f51..0d56080c4 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -17,6 +17,8 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h
index d6fc184c7..bfaf5d0fc 100644
--- a/src/theory/bags/inference_generator.h
+++ b/src/theory/bags/inference_generator.h
@@ -17,18 +17,16 @@
 #ifndef CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
 #define CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
 
-#include <map>
-#include <vector>
-
 #include "expr/node.h"
 #include "infer_info.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/solver_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+
 /**
  * An inference generator class. This class is used by the core solver to
  * generate lemmas
diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index 44a18bcc4..dcc5387e9 100644
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/bags/inference_manager.h"
 
+#include "theory/bags/solver_state.h"
+
 using namespace std;
 using namespace CVC4::kind;
 
diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
index 8b0fe0590..d74d3c189 100644
--- a/src/theory/bags/inference_manager.h
+++ b/src/theory/bags/inference_manager.h
@@ -17,14 +17,14 @@
 #ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
 #define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
 
-#include "theory/bags/infer_info.h"
-#include "theory/bags/solver_state.h"
 #include "theory/inference_manager_buffered.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class SolverState;
+
 /** Inference manager
  *
  * This class manages inferences produced by the theory of bags. It manages
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index 93f1af11d..d8820d8c4 100644
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -18,7 +18,6 @@
 #define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
 
 #include <map>
-#include <vector>
 
 #include "theory/theory_state.h"
 
diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 38c494219..192fd6809 100644
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -14,6 +14,9 @@
 
 #include "theory/bags/term_registry.h"
 
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
+
 using namespace std;
 using namespace CVC4::kind;
 
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index fcd822e16..87e61a026 100644
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -18,16 +18,17 @@
 #define CVC4__THEORY__BAGS__TERM_REGISTRY_H
 
 #include <map>
-#include <vector>
 
 #include "context/cdhashmap.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/solver_state.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+
 /**
  * Term registry, the purpose of this class is to maintain a database of
  * commonly used terms, and mappings from bags to their "proxy variables".
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 253fe2b7f..2950739e4 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -14,6 +14,9 @@
 
 #include "theory/bags/theory_bags.h"
 
+#include "smt/logic_exception.h"
+#include "theory/bags/normal_form.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 3839629d4..df64c3f1c 100644
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -17,17 +17,15 @@
 #ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H
 #define CVC4__THEORY__BAGS__THEORY_BAGS_H
 
-#include <memory>
-
 #include "theory/bags/bag_solver.h"
 #include "theory/bags/bags_rewriter.h"
 #include "theory/bags/bags_statistics.h"
 #include "theory/bags/inference_generator.h"
 #include "theory/bags/inference_manager.h"
 #include "theory/bags/solver_state.h"
+#include "theory/bags/term_registry.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 1912d1ba6..b50ec34c7 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -21,8 +21,12 @@
 #include <vector>
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 #include "theory/booleans/proof_circuit_propagator.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/theory.h"
+#include "util/hash.h"
 #include "util/utility.h"
 
 using namespace std;
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index a2e4febad..ba8c5782d 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 
-#include <functional>
 #include <memory>
 #include <unordered_map>
 #include <vector>
@@ -30,15 +29,17 @@
 #include "context/context.h"
 #include "expr/lazy_proof_chain.h"
 #include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_node.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/theory.h"
 #include "theory/trust_node.h"
-#include "util/hash.h"
 
 namespace CVC4 {
+
+class ProofGenerator;
+class ProofNode;
+
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace booleans {
 
 /**
diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h
index b3d7c0f64..1d807fd90 100644
--- a/src/theory/booleans/proof_checker.h
+++ b/src/theory/booleans/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index a7ae4ac18..aaff82933 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -18,6 +18,7 @@
 
 #include <sstream>
 
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {
diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h
index f9a51e067..fa472b602 100644
--- a/src/theory/booleans/proof_circuit_propagator.h
+++ b/src/theory/booleans/proof_circuit_propagator.h
@@ -22,9 +22,13 @@
 #include <memory>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 
 namespace CVC4 {
+
+class ProofNode;
+class ProofNodeManager;
+
 namespace theory {
 namespace booleans {
 
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 5878a4da5..bf84d543b 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -20,7 +20,6 @@
 #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
 #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
 
-#include "theory/theory.h"
 #include "theory/theory_rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index aef88b539..84e64baa4 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -21,7 +21,6 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "theory/rewriter.h"
 #include "theory/builtin/theory_builtin_rewriter.h" // for array and lambda representation
 
 #include <sstream>
diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp
index faafacfc5..6f7082191 100644
--- a/src/theory/builtin/type_enumerator.cpp
+++ b/src/theory/builtin/type_enumerator.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/builtin/type_enumerator.h"
 
+#include "theory/builtin/theory_builtin_rewriter.h"
+
 namespace CVC4 {
 namespace theory {
 namespace builtin {
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 25f750cf9..7b4b09f84 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -22,7 +22,6 @@
 #include "expr/kind.h"
 #include "expr/type_node.h"
 #include "expr/uninterpreted_constant.h"
-#include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/type_enumerator.h"
 #include "util/integer.h"
 
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index b4d4960ed..465a8eb65 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -20,6 +20,7 @@
 #include "cvc4_private.h"
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
 
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 8f9deb2da..d3326f853 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -20,7 +20,6 @@
 #define CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
-#include "prop/sat_solver.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -35,6 +34,9 @@ class Cnf_Dat_t_;
 typedef Cnf_Dat_t_ Cnf_Dat_t;
 
 namespace CVC4 {
+namespace prop {
+class SatSolver;
+}
 namespace theory {
 namespace bv {
 
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index f2b462b6b..d66b46505 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -19,11 +19,11 @@
 #ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
 #define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
 
+#include <memory>
 #include <unordered_set>
 
 #include "theory/bv/bitblast/bitblaster.h"
 
-#include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 
 namespace CVC4 {
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 053ca6373..622369043 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -23,12 +23,14 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
-#include "prop/cnf_stream.h"
-#include "prop/registrar.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "theory/bv/abstraction.h"
 
 namespace CVC4 {
+namespace prop {
+class CnfStream;
+class NullRegistrat;
+}
 namespace theory {
 namespace bv {
 
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 28624a949..6a1d61a3b 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -19,9 +19,6 @@
 #ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H
 #define CVC4__THEORY__BV__BV_EAGER_SOLVER_H
 
-#include <unordered_set>
-#include <vector>
-
 #include "expr/node.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/theory_model.h"
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 39728c2ec..be5da70b2 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -19,16 +19,15 @@
 #ifndef CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 #define CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 
-#include <list>
 #include <queue>
 #include <unordered_map>
 #include <unordered_set>
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdo.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index dd1e7c9f7..a34ec98ad 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
 #define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
 
-#include <unordered_map>
-
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 43fd90030..38d94ea27 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -28,6 +28,7 @@
 #include "theory/bv/bv_quick_check.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::context;
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 9af95fa20..969ded528 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -21,7 +21,6 @@
 #include <unordered_map>
 #include <unordered_set>
 
-#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/ext_theory.h"
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 1b471dd68..aa3607a66 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -20,6 +20,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace std;
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index ab3c8d774..a19c18df8 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -15,6 +15,8 @@
  **/
 #include "theory/bv/slicer.h"
 
+#include <sstream>
+
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0151791b7..4e7cfdd2a 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__BV__THEORY_BV_H
 #define CVC4__THEORY__BV__THEORY_BV_H
 
-#include <unordered_map>
-
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index ee153a695..9ecc25973 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -21,13 +21,11 @@
 #define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
 #include "theory/theory_rewriter.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-struct AllRewriteRules;
 typedef RewriteResponse (*RewriteFunction) (TNode, bool);
 
 class TheoryBVRewriter : public TheoryRewriter
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 2a2639505..c6c03e561 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -19,7 +19,6 @@
 #pragma once
 
 #include <set>
-#include <sstream>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index 4290ff989..567a16636 100644
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -17,6 +17,7 @@
 #include "expr/node_visitor.h"
 #include "prop/prop_engine.h"
 #include "theory/care_graph.h"
+#include "theory/model_manager.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index ec2f7e336..160b56625 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -16,8 +16,11 @@
 
 #include "expr/node_visitor.h"
 #include "theory/care_graph.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/ee_manager_distributed.h"
+#include "theory/model_manager.h"
 #include "theory/model_manager_distributed.h"
+#include "theory/shared_solver.h"
 #include "theory/shared_solver_distributed.h"
 #include "theory/theory_engine.h"
 
diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 1e18ee558..a6331b406 100644
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -20,10 +20,7 @@
 #include <vector>
 #include <memory>
 
-#include "theory/eager_proof_generator.h"
 #include "theory/ee_manager.h"
-#include "theory/model_manager.h"
-#include "theory/shared_solver.h"
 #include "theory/valuation.h"
 
 namespace CVC4 {
@@ -32,6 +29,10 @@ class TheoryEngine;
 
 namespace theory {
 
+class EagerProofGenerator;
+class ModelManager;
+class SharedSolver;
+
 /**
  * Manager for doing theory combination. This class is responsible for:
  * (1) Initializing the various components of theory combination (equality
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index ad1947700..8ad927ce4 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -19,9 +19,7 @@
 #ifndef CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
 #define CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
 
-#include "expr/node_manager_attributes.h"
 #include "theory/theory_rewriter.h"
-#include "theory/type_enumerator.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 0c8db3eaf..b231e8fd4 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -15,7 +15,9 @@
 #include "theory/datatypes/infer_proof_cons.h"
 
 #include "expr/proof.h"
+#include "expr/proof_checker.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/model_manager.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h
index 11bc64095..eeb8214e2 100644
--- a/src/theory/datatypes/infer_proof_cons.h
+++ b/src/theory/datatypes/infer_proof_cons.h
@@ -17,14 +17,15 @@
 #ifndef CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H
 #define CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H
 
-#include <vector>
-
+#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/proof_generator.h"
 #include "theory/datatypes/inference.h"
-#include "theory/theory_proof_step_buffer.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
 namespace theory {
 namespace datatypes {
 
diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h
index aed58fa2d..9c19608c1 100644
--- a/src/theory/datatypes/inference.h
+++ b/src/theory/datatypes/inference.h
@@ -17,10 +17,10 @@
 #ifndef CVC4__THEORY__DATATYPES__INFERENCE_H
 #define CVC4__THEORY__DATATYPES__INFERENCE_H
 
-#include "context/cdhashmap.h"
 #include "expr/node.h"
-#include "theory/inference_manager_buffered.h"
 #include "theory/inference_id.h"
+#include "theory/theory_inference.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index 643ae669b..110747043 100644
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -17,10 +17,8 @@
 #ifndef CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H
 #define CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H
 
-#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "theory/datatypes/infer_proof_cons.h"
-#include "theory/datatypes/inference.h"
 #include "theory/inference_manager_buffered.h"
 
 namespace CVC4 {
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 206e97846..e75d1005f 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -22,11 +22,14 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "smt/logic_exception.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4;
diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h
index 16cd00cae..c35fc86ff 100644
--- a/src/theory/datatypes/sygus_extension.h
+++ b/src/theory/datatypes/sygus_extension.h
@@ -22,20 +22,18 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "context/cdo.h"
 #include "context/context.h"
-#include "expr/dtype.h"
 #include "expr/node.h"
 #include "theory/datatypes/sygus_simple_sym.h"
 #include "theory/decision_manager.h"
-#include "theory/quantifiers/sygus/sygus_explain.h"
-#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers/term_database.h"
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
+class SynthConjecture;
+}
 namespace datatypes {
 
 class InferenceManager;
diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h
index f1a77910f..713d1bdc2 100644
--- a/src/theory/datatypes/sygus_simple_sym.h
+++ b/src/theory/datatypes/sygus_simple_sym.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
 #define CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
 
-#include <map>
 #include "expr/dtype.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index bb6a84792..e20e3db9b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -27,11 +27,15 @@
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
+#include "smt/logic_exception.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/logic_info.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/theory_state.h"
 #include "theory/type_enumerator.h"
 #include "theory/valuation.h"
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 27caad03c..95dccf2e5 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -31,6 +31,7 @@
 #include "theory/datatypes/sygus_extension.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "util/hash.h"
 
diff --git a/src/theory/decision_strategy.h b/src/theory/decision_strategy.h
index ef0b6f09d..74edde7f9 100644
--- a/src/theory/decision_strategy.h
+++ b/src/theory/decision_strategy.h
@@ -18,7 +18,6 @@
 #ifndef CVC4__THEORY__DECISION_STRATEGY__H
 #define CVC4__THEORY__DECISION_STRATEGY__H
 
-#include <map>
 #include "context/cdo.h"
 #include "expr/node.h"
 #include "theory/valuation.h"
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index 2a6d28d56..7bbdc91d3 100644
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -15,6 +15,7 @@
 #include "theory/eager_proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {
diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h
index 3fd8118ed..256dfeee9 100644
--- a/src/theory/eager_proof_generator.h
+++ b/src/theory/eager_proof_generator.h
@@ -20,10 +20,14 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class ProofNode;
+class ProofNodeManager;
+
 namespace theory {
 
 /**
diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 0ba62065b..3757f153a 100644
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -17,6 +17,7 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/shared_solver.h"
 #include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h
index 3ae1a90de..26f3d9430 100644
--- a/src/theory/ee_manager_distributed.h
+++ b/src/theory/ee_manager_distributed.h
@@ -18,15 +18,17 @@
 #ifndef CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
 #define CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
 
-#include <map>
 #include <memory>
 
 #include "theory/ee_manager.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
 
+namespace eq {
+class EqualityEngine;
+}
+
 /**
  * The (distributed) equality engine manager. This encapsulates an architecture
  * in which all theories maintain their own copy of an equality engine.
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 3240ec77b..0bdccab1b 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 #include "theory/output_channel.h"
-#include "theory/theory.h"
+#include "theory/theory_id.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -28,6 +28,8 @@ class TheoryEngine;
 
 namespace theory {
 
+class Theory;
+
 /**
  * An output channel for Theory that passes messages back to a TheoryEngine
  * for a given Theory.
diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h
index ae54a8d3b..f2235c6bf 100644
--- a/src/theory/ext_theory.h
+++ b/src/theory/ext_theory.h
@@ -34,17 +34,18 @@
 #define CVC4__THEORY__EXT_THEORY_H
 
 #include <map>
-#include <set>
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
 
+class OutputChannel;
+
 /**
  * A callback class for ExtTheory below. This class is responsible for
  * determining how to apply context-dependent simplification.
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 60d229215..359079948 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -16,6 +16,8 @@
 
 #include <vector>
 
+#include "base/check.h"
+#include "expr/node_builder.h"
 #include "theory/theory.h"  // theory.h Only needed for the leaf test
 #include "util/floatingpoint.h"
 #include "util/floatingpoint_literal_symfpu.h"
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 8f02cc115..6623f308c 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -23,11 +23,9 @@
 #ifndef CVC4__THEORY__FP__FP_CONVERTER_H
 #define CVC4__THEORY__FP__FP_CONVERTER_H
 
-#include "base/check.h"
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/node_builder.h"
 #include "expr/type_node.h"
 #include "theory/valuation.h"
 #include "util/bitvector.h"
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 5f6b9cf4d..73f7a2404 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -14,14 +14,11 @@
 
 #include "cvc4_private.h"
 
+#include <iosfwd>
+
 #ifndef CVC4__THEORY__INFERENCE_ID_H
 #define CVC4__THEORY__INFERENCE_ID_H
 
-#include <map>
-#include <vector>
-
-#include "util/safe_print.h"
-
 namespace CVC4 {
 namespace theory {
 
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index f1ef4e096..2772385d2 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
 #define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
 
-#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "theory/theory_inference.h"
 #include "theory/theory_inference_manager.h"
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index f048e9e90..fe6d1cf62 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -23,7 +23,8 @@
 
 #include <string>
 #include <vector>
-#include "expr/kind.h"
+
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index cecb4ccc5..b9057604e 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/first_order_model.h"
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/theory_engine.h"
 
diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index 69efe6e5f..1e4c39066 100644
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -21,8 +21,6 @@
 
 #include "theory/ee_manager.h"
 #include "theory/logic_info.h"
-#include "theory/theory_model.h"
-#include "theory/theory_model_builder.h"
 
 namespace CVC4 {
 
@@ -30,6 +28,9 @@ class TheoryEngine;
 
 namespace theory {
 
+class TheoryEngineModelBuilder;
+class TheoryModel;
+
 /**
  * A base class for managing models. Its main feature is to implement a
  * buildModel command. Overall, its behavior is specific to the kind of equality
diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index 3177e16ff..838cf0ad6 100644
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
+#include "theory/theory_model_builder.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h
index f8cbf2322..d41b6fa3b 100644
--- a/src/theory/model_manager_distributed.h
+++ b/src/theory/model_manager_distributed.h
@@ -17,8 +17,6 @@
 #ifndef CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H
 #define CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H
 
-#include <memory>
-
 #include "theory/ee_manager.h"
 #include "theory/model_manager.h"
 
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 0441b1126..8c10a1348 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -19,11 +19,6 @@
 #ifndef CVC4__THEORY__OUTPUT_CHANNEL_H
 #define CVC4__THEORY__OUTPUT_CHANNEL_H
 
-#include <memory>
-
-#include "expr/proof_node.h"
-#include "smt/logic_exception.h"
-#include "theory/interrupted.h"
 #include "theory/trust_node.h"
 #include "util/resource_manager.h"
 
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 7da13adcd..ca1d43b2f 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -23,6 +23,7 @@
 #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/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index 5260b4690..a5fb33a1f 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -17,10 +17,8 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
 #define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
 
-#include <map>
-#include <memory>
-#include <unordered_set>
 #include <vector>
+
 #include "theory/quantifiers/candidate_rewrite_filter.h"
 #include "theory/quantifiers/expr_miner.h"
 #include "theory/quantifiers/sygus_sampler.h"
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 7926116db..94c8b87e6 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -22,6 +22,7 @@
 #include "theory/arith/theory_arith_private.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "util/random.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 6f529ea83..56bd14b33 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/term_database.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/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index dfc79d5a7..f1ed9fe00 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "util/random.h"
 
 using namespace CVC4;
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 c6675745d..41f83269c 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 68f8e2e0d..91cb6e929 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/instantiate.h"
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 153f2e6ba..ef9b8063f 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 
 #include "expr/skolem_manager.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
@@ -23,12 +24,14 @@
 #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/inst_match.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"
+#include "theory/valuation.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 4211816b7..892f453ea 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -17,17 +17,13 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 #define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 
-#include <map>
-
 #include "expr/node.h"
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/valuation.h"
 
 namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
+class Valuation;
 
 namespace quantifiers {
 class QuantifiersState;
@@ -38,6 +34,7 @@ class QuantifiersRegistry;
 namespace inst {
 
 class IMGenerator;
+class InstMatch;
 class InstMatchGenerator;
 /** A collection of nodes representing a trigger.
 *
diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h
index 57246202d..910dbc79b 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.h
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
 #define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
 
-#include <map>
 #include "expr/node.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 3e70e5e69..2ecf3673f 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 8b8503022..878b4ddd3 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_rep_bound_ext.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/equality_engine.h"
 
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 121708a36..578554d79 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -18,15 +18,15 @@
 #define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
 
 #include "expr/node.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory_model_builder.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class FirstOrderModel;
+class QuantifiersState;
 
 class QModelBuilder : public TheoryEngineModelBuilder
 {
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index b91a81641..92e5ec71b 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -17,15 +17,14 @@
 #ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H
 #define CVC4__INST_STRATEGY_ENUMERATIVE_H
 
-#include "context/context.h"
-#include "context/context_mm.h"
 #include "theory/quantifiers/quant_module.h"
-#include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class RelevantDomain;
+
 /** Enumerative instantiation
  *
  * This class implements enumerative instantiation described
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 8fbb58fe0..f6fb9ed75 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -14,12 +14,14 @@
 
 #include "theory/quantifiers/instantiate.h"
 
+#include "expr/lazy_proof.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"
 #include "proof/proof_manager.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -29,6 +31,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace CVC4::context;
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index a1e08e274..e55e677df 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -20,7 +20,6 @@
 #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"
@@ -28,6 +27,9 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+class LazyCDProof;
+
 namespace theory {
 
 class QuantifiersEngine;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index d233dac62..17081bb7b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -28,6 +28,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 8b68457bb..0b1f18f5b 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 4c232ef78..3e223fd7c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 
 #include "options/quantifiers_options.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
@@ -27,6 +28,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace CVC4::kind;
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 5ac93d436..509e4905e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -29,6 +29,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 7c1ed40eb..56743e264 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index e2573bb52..3c6ab6bc1 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/sygus/transition_inference.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 #include "util/random.h"
 
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 742b3a3d9..fec15fdc6 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/cegis_unif.h"
 
+#include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h
index d9ec52aff..61c0327b7 100644
--- a/src/theory/quantifiers/sygus/example_infer.h
+++ b/src/theory/quantifiers/sygus/example_infer.h
@@ -18,8 +18,6 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
 #define CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
 
-#include "context/cdhashmap.h"
-#include "theory/quantifiers/sygus/sygus_module.h"
 #include "theory/quantifiers/sygus/sygus_unif_io.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index b550c3550..4f870830e 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -18,8 +18,11 @@
 #include "expr/node_algorithm.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
+#include "smt/logic_exception.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/sygus/type_node_id_trie.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 4fe2b8afc..9025b1a51 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -16,7 +16,9 @@
 
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
+#include "smt/logic_exception.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/sygus_invariance.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index bf6807151..262062f14 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -20,12 +20,14 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/quantifiers/sygus/sygus_invariance.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class SygusInvarianceTest;
+class TermDbSygus;
+
 /** Recursive term builder
  *
  * This is a utility used to generate variants
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 278233668..49c0f5f47 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/strings/word.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 4dd85e0ac..bb4bb6384 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -19,7 +19,6 @@
 
 #include <map>
 #include <memory>
-#include <string>
 #include <vector>
 
 #include "expr/node.h"
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index be6d4c7eb..1740ecc3d 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -17,6 +17,7 @@
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 4ef0f8f08..86d113edc 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
 #define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
 
-#include <map>
 #include <vector>
 
 #include "expr/node.h"
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index aa2551251..bc9da0c4d 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/example_infer.h"
+#include "theory/quantifiers/sygus/sygus_unif_io.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 52e574d49..7b20df8de 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -17,14 +17,13 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
 #define CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
 
-#include "context/cdhashmap.h"
 #include "theory/quantifiers/sygus/sygus_module.h"
-#include "theory/quantifiers/sygus/sygus_unif_io.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class SygusUnifIo;
 class SynthConjecture;
 
 /** SygusPbe
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 1123830f3..3629164ee 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -15,10 +15,7 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
 #define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
 
-#include <string>
-#include <vector>
 #include "expr/node.h"
-#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 1400882eb..0911b73c2 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -24,6 +24,7 @@
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/logic_info.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index 30d04c8e2..319497f77 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -19,16 +19,17 @@
 
 #include <unordered_set>
 #include "expr/node.h"
-#include "theory/logic_info.h"
 
 namespace CVC4 {
+
+class LogicInfo;
+
 namespace theory {
 
 class QuantifiersEngine;
 
 namespace quantifiers {
 
-class CegConjecture;
 class TermDbSygus;
 
 /** SygusRepairConst
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 2c0ac227b..a9891aa72 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/strings/word.h"
 #include "util/random.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 732b52bf9..a3cf5ed19 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -19,6 +19,7 @@
 #include "printer/printer.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/rewriter.h"
 #include "util/random.h"
 
 #include <math.h>
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 57043086b..dc864fbd8 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -19,6 +19,7 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -29,9 +30,12 @@
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 #include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 47ebe6853..27c565795 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -20,7 +20,6 @@
 
 #include <memory>
 
-#include "theory/decision_manager.h"
 #include "theory/quantifiers/expr_miner_manager.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus/cegis.h"
@@ -28,8 +27,6 @@
 #include "theory/quantifiers/sygus/cegis_unif.h"
 #include "theory/quantifiers/sygus/example_eval_cache.h"
 #include "theory/quantifiers/sygus/example_infer.h"
-#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
-#include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 #include "theory/quantifiers/sygus/sygus_stats.h"
@@ -39,6 +36,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class CegGrammarConstructor;
+class SygusPbe;
 class SygusStatistics;
 
 /**
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
index 0a50f90c7..543d5e7f0 100644
--- a/src/theory/quantifiers/sygus/transition_inference.cpp
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index a8f247b58..9266a3f9d 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -20,6 +20,7 @@
 #include "expr/sygus_datatype.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/sygus/type_node_id_trie.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h
index 43a6cd07a..7b45d115b 100644
--- a/src/theory/quantifiers/sygus/type_info.h
+++ b/src/theory/quantifiers/sygus/type_info.h
@@ -18,10 +18,8 @@
 #define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
 
 #include <map>
-#include <unordered_set>
 
 #include "expr/node.h"
-#include "theory/quantifiers/sygus/type_node_id_trie.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h
index 5625a8d1f..020c8d086 100644
--- a/src/theory/quantifiers/sygus/type_node_id_trie.h
+++ b/src/theory/quantifiers/sygus/type_node_id_trie.h
@@ -26,8 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class TermDbSygus;
-
 /**
  * A trie indexed by types that assigns unique identifiers to nodes based on
  * a vector of types.
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index eeeb5385e..fa6d80085 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 588201fbf..61754ac32 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -18,7 +18,7 @@
 #define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 
 #include <map>
-#include <unordered_set>
+#include <unordered_map>
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f72c970ba..401857206 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -31,6 +31,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index 9b26c3817..d38170563 100644
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/relevance_manager.h"
 
+#include <sstream>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index fc1e7dffa..5c3e2d38d 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -19,6 +19,7 @@
 #include "expr/node_algorithm.h"
 #include "options/sets_options.h"
 #include "smt/logic_exception.h"
+#include "theory/rewriter.h"
 #include "theory/sets/normal_form.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 8997d2b47..9e16bfb97 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -15,6 +15,7 @@
 #include "theory/sets/inference_manager.h"
 
 #include "options/sets_options.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index e9529d4e0..3937a32b6 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -21,6 +21,7 @@
 
 #include <memory>
 
+#include "smt/logic_exception.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/skolem_cache.h"
 #include "theory/sets/solver_state.h"
diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
index fcdb7810f..91e008f80 100644
--- a/src/theory/shared_solver.cpp
+++ b/src/theory/shared_solver.cpp
@@ -15,6 +15,8 @@
 #include "theory/shared_solver.h"
 
 #include "expr/node_visitor.h"
+#include "theory/ee_setup_info.h"
+#include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
index d1c6f6c03..a4d08bd1b 100644
--- a/src/theory/shared_solver.h
+++ b/src/theory/shared_solver.h
@@ -18,19 +18,20 @@
 #define CVC4__THEORY__SHARED_SOLVER__H
 
 #include "expr/node.h"
-#include "expr/proof_node_manager.h"
-#include "theory/ee_setup_info.h"
-#include "theory/logic_info.h"
 #include "theory/shared_terms_database.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/valuation.h"
 
 namespace CVC4 {
 
+class LogicInfo;
+class ProofNodeManager;
 class TheoryEngine;
 
 namespace theory {
 
+struct EeSetupInfo;
+
 /**
  * A base class for shared solver. The shared solver is the component of theory
  * engine that behaves like a theory solver, and whose purpose is to ensure the
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 9ad91ed33..cc99e75b4 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -18,7 +18,6 @@
 #ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
 #define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
 
-#include <map>
 #include <memory>
 #include <vector>
 
diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index c1e5b1fa8..822416da3 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -17,10 +17,9 @@
 #ifndef CVC4__SORT_INFERENCE_H
 #define CVC4__SORT_INFERENCE_H
 
-#include <iostream>
-#include <string>
-#include <vector>
 #include <map>
+#include <vector>
+
 #include "expr/node.h"
 #include "expr/type_node.h"
 
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index c6bdad898..8a8abbf81 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/sequence.h"
 #include "options/strings_options.h"
+#include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 5dab55e65..b746f2961 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -18,6 +18,8 @@
 
 #include "base/configuration.h"
 #include "options/strings_options.h"
+#include "smt/logic_exception.h"
+#include "theory/rewriter.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/strings_entail.h"
 #include "theory/strings/theory_strings_utils.h"
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index b6db6175f..a02566a41 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/strings/infer_proof_cons.h"
 
+#include "expr/proof_node_manager.h"
 #include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 0a938b236..f252196d8 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -19,6 +19,7 @@
 #include <cmath>
 
 #include "options/strings_options.h"
+#include "smt/logic_exception.h"
 #include "theory/ext_theory.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/theory_model.h"
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 1fd0169b0..456cd492b 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/strings/solver_state.h"
 
+#include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 9ea9042cd..3a3003ba9 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -17,6 +17,7 @@
 
 #include "base/configuration.h"
 #include "options/quantifiers_options.h"
+#include "smt/logic_exception.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::theory;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8a5c40fd8..f34aebe8b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -32,12 +32,14 @@
 #include "prop/prop_engine.h"
 #include "smt/dump.h"
 #include "smt/logic_exception.h"
+#include "smt/output_manager.h"
 #include "theory/combination_care_graph.h"
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/relevance_manager.h"
 #include "theory/rewriter.h"
+#include "theory/shared_solver.h"
 #include "theory/theory.h"
 #include "theory/theory_engine_proof_generator.h"
 #include "theory/theory_id.h"
@@ -48,7 +50,6 @@
 
 using namespace std;
 
-using namespace CVC4::preprocessing;
 using namespace CVC4::theory;
 
 namespace CVC4 {
diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h
index 96ac5bef0..1833f1cac 100644
--- a/src/theory/theory_id.h
+++ b/src/theory/theory_id.h
@@ -20,7 +20,7 @@
 #ifndef CVC4__THEORY__THEORY_ID_H
 #define CVC4__THEORY__THEORY_ID_H
 
-#include <iostream>
+#include <iosfwd>
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index f970ce41e..68f70b740 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
+#include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 6e9622e23..a599afa23 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -21,6 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "expr/proof_rule.h"
 #include "theory/inference_id.h"
 #include "theory/output_channel.h"
 #include "theory/trust_node.h"
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 10eb789b2..0c1ea7a7a 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -19,6 +19,7 @@
 #include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "smt/smt_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 73b1d1d80..0d83fa42d 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -19,6 +19,7 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "theory/rewriter.h"
 #include "theory/uf/theory_uf_model.h"
 
 using namespace std;
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 6d76968ad..51f2155d3 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/lazy_proof.h"
 #include "expr/skolem_manager.h"
+#include "smt/logic_exception.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 810987a0c..d61f2d15b 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -18,6 +18,8 @@
 
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 91653785f..d701adfc4 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -19,11 +19,10 @@
 
 #include "context/cdhashmap.h"
 #include "context/context.h"
+#include "theory/decision_strategy.h"
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
 
-#include "theory/decision_manager.h"
-
 namespace CVC4 {
 namespace theory {
 namespace uf {
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index bfcb829ff..59dc3943d 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -17,9 +17,12 @@
 
 #include "theory/uf/equality_engine.h"
 
+#include "base/output.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/rewriter.h"
+#include "theory/uf/eq_proof.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 7e297134e..b81a17dcf 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -22,18 +22,14 @@
 
 #include <deque>
 #include <queue>
-#include <memory>
 #include <unordered_map>
 #include <vector>
 
-#include "base/output.h"
 #include "context/cdhashmap.h"
 #include "context/cdo.h"
 #include "expr/kind_map.h"
 #include "expr/node.h"
-#include "theory/rewriter.h"
 #include "theory/theory_id.h"
-#include "theory/uf/eq_proof.h"
 #include "theory/uf/equality_engine_iterator.h"
 #include "theory/uf/equality_engine_notify.h"
 #include "theory/uf/equality_engine_types.h"
@@ -45,6 +41,7 @@ namespace eq {
 
 class EqClassesIterator;
 class EqClassIterator;
+class EqProof;
 
 /**
  * Class for keeping an incremental congruence closure over a set of terms. It provides
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 0a7418e8d..7db887b56 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -15,7 +15,11 @@
 #include "theory/uf/proof_equality_engine.h"
 
 #include "expr/lazy_proof_chain.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
 #include "theory/rewriter.h"
+#include "theory/uf/eq_proof.h"
+#include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 1ce623683..adf8d2c18 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
 #define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
 
-#include <map>
 #include <vector>
 
 #include "context/cdhashmap.h"
@@ -25,15 +24,18 @@
 #include "expr/buffered_proof_generator.h"
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
 #include "theory/eager_proof_generator.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
+
+class ProofNode;
+class ProofNodeManager;
+
 namespace theory {
 namespace eq {
 
+class EqualityEngine;
+
 /**
  * A layer on top of an EqualityEngine. The goal of this class is manage the
  * use of an EqualityEngine object in such a way that the proper proofs are
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index caa15e69e..273e81740 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -26,6 +26,7 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
 #include "theory/uf/cardinality_extension.h"
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 7f136f9c1..be63be373 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -20,15 +20,12 @@
 #ifndef CVC4__THEORY__UF__THEORY_UF_H
 #define CVC4__THEORY__UF__THEORY_UF_H
 
-#include "context/cdo.h"
 #include "expr/node.h"
 #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"
 #include "theory/uf/symmetry_breaker.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 3613a9b22..393f1f705 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -18,6 +18,8 @@
 
 #include "expr/attribute.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 3c5cc681b..62ec8204f 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -20,10 +20,12 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
 namespace theory {
+
+class TheoryModel;
+
 namespace uf {
 
 class UfModelTreeNode
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 54b71f9f8..e46f38a28 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -19,6 +19,7 @@
 #include "expr/node.h"
 #include "options/theory_options.h"
 #include "prop/prop_engine.h"
+#include "theory/assertion.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 840da860f..860517451 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -24,7 +24,6 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "options/theory_options.h"
-#include "theory/assertion.h"
 
 namespace CVC4 {
 
@@ -32,6 +31,7 @@ class TheoryEngine;
 
 namespace theory {
 
+struct Assertion;
 class TheoryModel;
 class SortInference;