Clean up includes to reduce compile times (#6031)

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

206 files changed, 374 insertions, 180 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0c94320c3..7a191cd8a 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -39,6 +39,8 @@
 #include "base/check.h"
 #include "base/configuration.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
+#include "expr/dtype_selector.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index 2a8dc8d10..cddef79fd 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -28,24 +28,24 @@ using namespace std;
 
 namespace CVC4 {
 
-thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL;
+thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = nullptr;
 
-LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {}
+LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {}
 
 LastExceptionBuffer::~LastExceptionBuffer() {
-  if(d_contents != NULL){
+  if(d_contents != nullptr){
     free(d_contents);
-    d_contents = NULL;
+    d_contents = nullptr;
   }
 }
 
 void LastExceptionBuffer::setContents(const char* string) {
-  if(d_contents != NULL){
+  if(d_contents != nullptr){
     free(d_contents);
-    d_contents = NULL;
+    d_contents = nullptr;
   }
 
-  if(string != NULL){
+  if(string != nullptr){
     d_contents = strdup(string);
   }
 }
@@ -61,7 +61,7 @@ std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
   va_start(args, format);
 
   int n = 512;
-  char* buf = NULL;
+  char* buf = nullptr;
 
   for (int i = 0; i < 2; ++i){
     Assert(n > 0);
@@ -80,9 +80,9 @@ std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
       break;
     }
   }
-  // buf is not NULL is an invariant.
+  // buf is not nullptr is an invariant.
   // buf is also 0 terminated.
-  Assert(buf != NULL);
+  Assert(buf != nullptr);
   std::string result(buf);
   delete [] buf;
   va_end(args);
@@ -107,7 +107,7 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
     buf = new char[n];
 
     int size;
-    if(extra == NULL) {
+    if(extra == nullptr) {
       size = snprintf(buf, n, "%s\n%s\n%s",
                       header, function, tail);
     } else {
@@ -129,8 +129,8 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
 #ifdef CVC4_DEBUG
   LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
-  if(buffer != NULL){
-    if(buffer->getContents() == NULL) {
+  if(buffer != nullptr){
+    if(buffer->getContents() == nullptr) {
       buffer->setContents(buf);
     }
   }
@@ -149,7 +149,7 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
     buf = new char[n];
 
     int size;
-    if(extra == NULL) {
+    if(extra == nullptr) {
       size = snprintf(buf, n, "%s.\n%s\n",
                       header, function);
     } else {
@@ -170,8 +170,8 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
 #ifdef CVC4_DEBUG
   LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
-  if(buffer != NULL){
-    if(buffer->getContents() == NULL) {
+  if(buffer != nullptr){
+    if(buffer->getContents() == nullptr) {
       buffer->setContents(buf);
     }
   }
diff --git a/src/base/exception.h b/src/base/exception.h
index 1d49d94cc..8a89c99fc 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -151,7 +151,7 @@ public:
   static void setCurrent(LastExceptionBuffer* buffer) { s_currentBuffer = buffer; }
 
   static const char* currentContents() {
-    return (getCurrent() == NULL) ? NULL : getCurrent()->getContents();
+    return (getCurrent() == nullptr) ? nullptr : getCurrent()->getContents();
   }
 
 private:
diff --git a/src/base/listener.h b/src/base/listener.h
index 15256ab01..5c5a58128 100644
--- a/src/base/listener.h
+++ b/src/base/listener.h
@@ -20,8 +20,6 @@
 #ifndef CVC4__LISTENER_H
 #define CVC4__LISTENER_H
 
-#include <list>
-
 namespace CVC4 {
 
 /**
diff --git a/src/base/output.h b/src/base/output.h
index 96cb9f8ac..9de1d9b09 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -21,10 +21,8 @@
 
 #include <ios>
 #include <iostream>
-#include <streambuf>
 #include <string>
 #include <cstdio>
-#include <cstdarg>
 #include <set>
 #include <utility>
 
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index cb5e552ac..0515d7126 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -20,6 +20,7 @@
 #ifndef CVC4__CONTEXT__CDLIST_H
 #define CVC4__CONTEXT__CDLIST_H
 
+#include <cstring>
 #include <iterator>
 #include <memory>
 #include <string>
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 19be126f8..1313daa9a 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -16,6 +16,7 @@
 
 
 #include <iostream>
+#include <string>
 #include <vector>
 
 #include "base/check.h"
diff --git a/src/context/context.h b/src/context/context.h
index 15b4307b9..afec59747 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -20,10 +20,8 @@
 #define CVC4__CONTEXT__CONTEXT_H
 
 #include <cstdlib>
-#include <cstring>
 #include <iostream>
 #include <memory>
-#include <new>
 #include <typeinfo>
 #include <vector>
 
diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
index f6753a601..266cfb18a 100644
--- a/src/expr/buffered_proof_generator.cpp
+++ b/src/expr/buffered_proof_generator.cpp
@@ -15,6 +15,7 @@
 #include "expr/buffered_proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index f774e383d..da80891a2 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -17,17 +17,14 @@
 #ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
 #define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
 
-#include <map>
-#include <vector>
-
 #include "context/cdhashmap.h"
-#include "context/cdhashset.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 #include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * The proof generator for buffered steps. This class is a context-dependent
  * mapping from formulas to proof steps. It does not generate ProofNodes until it
diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp
index 694d75db6..23d6b3ca1 100644
--- a/src/expr/datatype_index.cpp
+++ b/src/expr/datatype_index.cpp
@@ -15,6 +15,7 @@
 
 #include <sstream>
 #include <string>
+#include "util/hash.h"
 #include "util/integer.h"
 
 using namespace std;
diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h
index c7f170ff6..08640e1d5 100644
--- a/src/expr/datatype_index.h
+++ b/src/expr/datatype_index.h
@@ -18,7 +18,6 @@
 #define CVC4__DATATYPE_INDEX_H
 
 #include <iosfwd>
-#include "util/hash.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 5cb76858a..f94f0063a 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -13,6 +13,7 @@
  **/
 #include "expr/dtype.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/type_matcher.h"
 
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index e4bae29b8..c68a7d44a 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -20,10 +20,8 @@
 #include <map>
 #include <string>
 #include <vector>
-#include "expr/dtype_cons.h"
-#include "expr/dtype_selector.h"
+#include "expr/attribute.h"
 #include "expr/node.h"
-#include "expr/node_manager_attributes.h"
 #include "expr/type_node.h"
 
 namespace CVC4 {
@@ -76,7 +74,7 @@ struct DTypeUFiniteComputedTag
 typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
 // ----------------------- end datatype attributes
 
-class NodeManager;
+class DTypeConstructor;
 
 /**
  * The Node-level representation of an inductive datatype, which currently
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 0c209f393..8d8d2741f 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -15,6 +15,7 @@
 #include "expr/lazy_proof.h"
 
 #include "expr/proof_ensure_closed.h"
+#include "expr/proof_node_manager.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index e2bba3015..83dc90e4d 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -22,10 +22,11 @@
 
 #include "expr/proof.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) lazy proof. This class is an extension of CDProof
  * that additionally maps facts to proof generators in a context-dependent
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 2edad1647..f80ab099c 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -17,6 +17,7 @@
 #include "expr/proof.h"
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/proof_options.h"
 
 namespace CVC4 {
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 59cab72c9..1604bf182 100644
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -22,10 +22,11 @@
 
 #include "context/cdhashmap.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) lazy generator for proof chains. This class is an
  * extension of ProofGenerator that additionally that maps facts to proof
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index c45295622..1aca73d2e 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -21,6 +21,7 @@
 #include "base/exception.h"
 #include "base/output.h"
 #include "expr/attribute.h"
+#include "expr/type_checker.h"
 
 using namespace std;
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 559ce5ddb..06c327018 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -22,8 +22,6 @@
 #ifndef CVC4__NODE_H
 #define CVC4__NODE_H
 
-#include <algorithm>
-#include <functional>
 #include <iostream>
 #include <string>
 #include <unordered_map>
@@ -32,14 +30,12 @@
 #include <vector>
 
 #include "base/check.h"
-#include "base/configuration.h"
 #include "base/exception.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
-#include "expr/type.h"
 #include "options/language.h"
 #include "options/set_language.h"
 #include "util/hash.h"
@@ -980,7 +976,6 @@ std::ostream& operator<<(
 
 //#include "expr/attribute.h"
 #include "expr/node_manager.h"
-#include "expr/type_checker.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 883febd6f..4404e3445 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -26,6 +26,7 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp
index 75a11eac7..0b778ebef 100644
--- a/src/expr/node_traversal.cpp
+++ b/src/expr/node_traversal.cpp
@@ -14,6 +14,8 @@
 
 #include "node_traversal.h"
 
+#include <functional>
+
 namespace CVC4 {
 
 NodeDfsIterator::NodeDfsIterator(TNode n,
diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h
index e7e49db45..124372f79 100644
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__EXPR__NODE_TRAVERSAL_H
 #define CVC4__EXPR__NODE_TRAVERSAL_H
 
-#include <functional>
 #include <iterator>
 #include <unordered_map>
 #include <vector>
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 0635e983b..1ad498ecd 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -399,7 +399,6 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 }/* CVC4 namespace */
 
 #include "expr/node_manager.h"
-#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace expr {
@@ -501,7 +500,6 @@ inline NodeValue* NodeValue::getChild(int i) const {
 }/* CVC4 namespace */
 
 #include "expr/node.h"
-#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace expr {
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 1c21a59e7..b512b5869 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/proof.h"
 
+#include "expr/proof_node_manager.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
diff --git a/src/expr/proof.h b/src/expr/proof.h
index 8350b4954..3a26f0975 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -24,11 +24,12 @@
 #include "expr/node.h"
 #include "expr/proof_generator.h"
 #include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
 #include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) proof.
  *
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 840cb4c66..ea73b7958 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 707d1314c..7e6371aa9 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -17,6 +17,7 @@
 #include "preprocessing/preprocessing_pass_context.h"
 
 #include "expr/node_algorithm.h"
+#include "smt/logic_request.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 173e67fd9..82798d074 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -25,6 +25,8 @@
 #include <vector>
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
+#include "expr/dtype_selector.h"
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "expr/node_visitor.h"
 #include "expr/sequence.h"
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c7962417a..fd9d20e4b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -17,12 +17,14 @@
 #include "printer/smt2/smt2_printer.h"
 
 #include <iostream>
+#include <list>
 #include <string>
 #include <typeinfo>
 #include <vector>
 
 #include "api/cvc4cpp.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/node_visitor.h"
 #include "expr/sequence.h"
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index ac90d0c36..d0c75a924 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -33,6 +33,7 @@
 #include "prop/prop_proof_manager.h"
 #include "prop/sat_solver_types.h"
 #include "theory/trust_node.h"
+#include "theory/theory_inference_manager.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
 #include "util/unsafe_interrupt_exception.h"
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index cdaaa0558..f10191c75 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -39,6 +39,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "util/sexpr.h"
+#include "util/unsafe_interrupt_exception.h"
 #include "util/utility.h"
 
 using namespace std;
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index b1fb0589c..aedd946c1 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -16,6 +16,7 @@
 
 #include "smt/dump.h"
 
+#include "base/configuration.h"
 #include "base/output.h"
 #include "lib/strtok_r.h"
 #include "preprocessing/preprocessing_pass_registry.h"
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 0347a24ef..f0fad93fe 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/listeners.h"
 
+#include "base/configuration.h"
 #include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
 #include "options/smt_options.h"
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
index 3210de7b1..4e8dcce6c 100644
--- a/src/smt/logic_request.h
+++ b/src/smt/logic_request.h
@@ -26,7 +26,7 @@
 #ifndef CVC4__LOGIC_REQUEST_H
 #define CVC4__LOGIC_REQUEST_H
 
-#include "expr/kind.h"
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 98fbfe1b3..3d306a7a2 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -35,6 +35,7 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
 #include "theory/theory.h"
 
 using namespace CVC4::theory;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 941fd111a..ed5e73d5d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -42,7 +42,6 @@
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
-#include "smt/logic_request.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 eb8eb6ca0..53a5b7f2f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -23,20 +23,15 @@
 #include <vector>
 #include <map>
 
-#include "base/modal_exception.h"
 #include "context/cdhashmap_forward.h"
-#include "context/cdhashset_forward.h"
 #include "context/cdlist_forward.h"
 #include "options/options.h"
-#include "smt/logic_exception.h"
 #include "smt/output_manager.h"
 #include "smt/smt_mode.h"
 #include "theory/logic_info.h"
-#include "util/hash.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/statistics.h"
-#include "util/unsafe_interrupt_exception.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -51,7 +46,6 @@ class TypeNode;
 struct NodeHashFunction;
 
 class NodeManager;
-class DecisionEngine;
 class TheoryEngine;
 class ProofManager;
 class UnsatCore;
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 31eb8bb8f..26f51c8b8 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/arith/arith_preprocess.h"
 
+#include "theory/arith/inference_manager.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 6c858d1eb..396395e1f 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -21,7 +21,6 @@
 #define CVC4__THEORY__ARITH__ARITH_REWRITER_H
 
 #include "theory/arith/rewrites.h"
-#include "theory/theory.h"
 #include "theory/theory_rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 72f8e49ff..61715df9b 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 374b17d88..5d4bc9b1e 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 
 
 using namespace std;
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 85af862fa..8cb249c46 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "util/statistics_registry.h"
 
 using namespace std;
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 1bd4416e0..e001d98d4 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -52,6 +52,7 @@
 
 #pragma once
 
+#include "theory/arith/error_set.h"
 #include "theory/arith/simplex.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index df3ba37f3..04165c289 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "theory/arith/nl/cad/projections.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
+#include "theory/arith/nl/nl_model.h"
 
 namespace std {
 /** Generic streaming operator for std::vector. */
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 4511d0c55..8736b7a08 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -32,12 +32,14 @@
 #include "theory/arith/nl/cad/constraints.h"
 #include "theory/arith/nl/cad/proof_generator.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
+
+class NlModel;
+
 namespace cad {
 
 /**
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 74c0457a8..efc5c465a 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -14,15 +14,11 @@
 
 #include "theory/arith/nl/cad_solver.h"
 
-#ifdef CVC4_POLY_IMP
-#include <poly/polyxx.h>
-#endif
-
-#include "options/arith_options.h"
 #include "theory/inference_id.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/poly_conversion.h"
-#include "util/poly_util.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 21fbbab2e..b67d78f0d 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -17,17 +17,22 @@
 
 #include <vector>
 
+#include "context/context.h"
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/cad/proof_checker.h"
-#include "theory/arith/nl/nl_model.h"
+#include "util/real_algebraic_number.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 /**
  * A solver for nonlinear arithmetic that implements the CAD-based method
  * described in https://arxiv.org/pdf/2003.05633.pdf.
diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index 5da5319a1..7e77efb16 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -17,6 +17,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/arith/nl/nl_model.h"
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index 863b3f879..285189ccc 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -19,15 +19,21 @@
 
 #include "expr/node.h"
 #include "expr/proof_set.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
+
+class CDProof;
+
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 struct ExtState
 {
   ExtState(InferenceManager& im,
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 7b4d98037..09cfd7410 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -15,10 +15,12 @@
 #include "theory/arith/nl/ext/factoring_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "expr/skolem_manager.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 5ae898bd2..ad6fd36b8 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -15,11 +15,13 @@
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index a3e56358b..d970bd95d 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/ext/monomial_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index 51179826a..05908ecc7 100644
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -16,6 +16,7 @@
 #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
 
 #include "expr/node.h"
+#include "theory/theory_inference.h"
 #include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 1e9b444e3..5bcdb801d 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -15,9 +15,11 @@
 #include "theory/arith/nl/ext/split_zero_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index e8730e496..0e7ad0999 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -16,6 +16,7 @@
 #define CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
 
 #include "expr/node.h"
+#include "context/cdhashset.h"
 #include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 3d646a684..2d04c2b5c 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -15,9 +15,11 @@
 #include "theory/arith/nl/ext/tangent_plane_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp
index 62e1fa904..ee12d17d6 100644
--- a/src/theory/arith/nl/ext_theory_callback.cpp
+++ b/src/theory/arith/nl/ext_theory_callback.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/ext_theory_callback.h"
 
 #include "theory/arith/arith_utilities.h"
+#include "theory/uf/equality_engine.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index a5b4e87bd..6487b48ec 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -18,7 +18,10 @@
 #include "options/smt_options.h"
 #include "preprocessing/passes/bv_to_int.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/arith/arith_state.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
 #include "util/iand.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index c854f3ab7..044a37abc 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -20,17 +20,20 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
-#include "theory/arith/arith_state.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/iand_utils.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class ArithState;
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 /** Integer and solver class
  *
  */
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 17eb518a2..652f0eec7 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -19,6 +19,8 @@
 
 #include "cvc4_private.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h
index a05defc0a..4c1de0196 100644
--- a/src/theory/arith/nl/iand_utils.h
+++ b/src/theory/arith/nl/iand_utils.h
@@ -16,7 +16,7 @@
 #ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
 #define CVC4__THEORY__ARITH__IAND_TABLE_H
 
-#include <tuple>
+#include <map>
 #include <vector>
 
 #include "expr/node.h"
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index af86d69fd..7d698a221 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -20,6 +20,7 @@
 #include "base/output.h"
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/poly_conversion.h"
 #include "theory/arith/normal_form.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index 176549d8b..b9ecfc437 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -23,7 +23,6 @@
 
 #include "expr/node.h"
 #include "theory/arith/bound_inference.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/icp/candidate.h"
 #include "theory/arith/nl/icp/contraction_origins.h"
 #include "theory/arith/nl/icp/intersection.h"
@@ -32,6 +31,9 @@
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 namespace icp {
 
diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp
index aa8fcf543..b5fedb7eb 100644
--- a/src/theory/arith/nl/icp/intersection.cpp
+++ b/src/theory/arith/nl/icp/intersection.cpp
@@ -18,6 +18,8 @@
 
 #include <iostream>
 
+#include <poly/polyxx.h>
+
 #include "base/check.h"
 #include "base/output.h"
 #include "theory/arith/nl/poly_conversion.h"
diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index 0df6caf34..cdc166139 100644
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -18,7 +18,9 @@
 #include "util/real_algebraic_number.h"
 
 #ifdef CVC4_POLY_IMP
-#include <poly/polyxx.h>
+namespace poly {
+  class Interval;
+}
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 5c4140430..9255d3349 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -20,6 +20,7 @@
 #include "options/theory_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/theory_model.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index cd2d15563..4d5585545 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -19,15 +19,20 @@
 #include <unordered_map>
 #include <vector>
 
-#include "context/cdo.h"
-#include "context/context.h"
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
+
+namespace context {
+class Context;
+}
+
 namespace theory {
+
+class TheoryModel;
+
 namespace arith {
 namespace nl {
 
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index c46781e76..f269f1d69 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -18,10 +18,10 @@
 #include "theory/arith/nl/nonlinear_extension.h"
 
 #include "options/arith_options.h"
-#include "options/theory_options.h"
 #include "theory/arith/arith_state.h"
-#include "theory/arith/arith_utilities.h"
 #include "theory/arith/bound_inference.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
 #include "theory/theory_model.h"
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index fba9e8e87..6a38021a0 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -21,10 +21,7 @@
 #include <map>
 #include <vector>
 
-#include "context/cdlist.h"
-#include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad_solver.h"
 #include "theory/arith/nl/ext/factoring_check.h"
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
@@ -35,19 +32,25 @@
 #include "theory/arith/nl/ext_theory_callback.h"
 #include "theory/arith/nl/iand_solver.h"
 #include "theory/arith/nl/icp/icp_solver.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/stats.h"
 #include "theory/arith/nl/strategy.h"
 #include "theory/arith/nl/transcendental/transcendental_solver.h"
 #include "theory/ext_theory.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
+namespace eq {
+  class EqualityEngine;
+}
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlLemma;
+
 /** Non-linear extension class
  *
  * This class implements model-based refinement schemes
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index 5b7edb3ef..67cfd5807 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -20,9 +20,8 @@
 
 #include "expr/node.h"
 #include "expr/node_manager_attributes.h"
-#include "util/integer.h"
+#include "theory/arith/bound_inference.h"
 #include "util/poly_util.h"
-#include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 37d816179..102d2d6ae 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -23,15 +23,18 @@
 
 #include <poly/polyxx.h>
 
-#include <iostream>
+#include <cstddef>
+#include <map>
+#include <utility>
 
 #include "expr/node.h"
-#include "theory/arith/bound_inference.h"
-#include "util/real_algebraic_number.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class BoundInference;
+
 namespace nl {
 
 /** Bijective mapping between CVC4 variables and poly variables. */
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index f869d83a4..fab4de35a 100644
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -17,8 +17,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__STATS_H
 #define CVC4__THEORY__ARITH__NL__STATS_H
 
-#include "expr/kind.h"
-#include "theory/inference_id.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h
index 526ae36f1..1f7b85b60 100644
--- a/src/theory/arith/nl/strategy.h
+++ b/src/theory/arith/nl/strategy.h
@@ -16,7 +16,6 @@
 #define CVC4__THEORY__ARITH__NL__STRATEGY_H
 
 #include <iosfwd>
-#include <map>
 #include <vector>
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 86b17376c..74766926b 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -19,9 +19,11 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index b874e1a4b..ddef4faf7 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -21,8 +21,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index f5dc49da8..11852ac3a 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index da4b48fd6..a009df09b 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -21,8 +21,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index 375f1757e..f45b906bc 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index ccdc80e0f..0e1248f7c 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -16,12 +16,14 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
 
 #include "expr/node.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 class TaylorGenerator
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index e58da1aad..d1355c746 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index 8135ba1fb..343f303d1 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -9,37 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-/*********************                                                        */
-/*! \file transcendental_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Solving for handling transcendental functions.
  **/
 
 #ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
 
-#include <map>
-#include <unordered_map>
-#include <unordered_set>
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/exponential_solver.h"
 #include "theory/arith/nl/transcendental/sine_solver.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
@@ -47,7 +25,13 @@
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 /** Transcendental solver class
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 76c3d5357..ae8c1eea7 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -14,8 +14,10 @@
 
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
+#include "expr/proof.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 93ac4627a..d0678fb9a 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -23,6 +23,7 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
 namespace CVC4 {
+class CDProof;
 namespace theory {
 namespace arith {
 namespace nl {
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 5c1b90663..d0a7f7fc4 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -19,6 +19,7 @@
 #include "base/output.h"
 #include "options/arith_options.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "theory/arith/simplex.h"
 
 
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 6740c8e1c..e34696cb5 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -57,7 +57,6 @@
 
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/error_set.h"
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
@@ -68,6 +67,8 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class ErrorSet;
+
 class SimplexDecisionProcedure {
 protected:
   typedef std::vector< std::pair<ArithVar, int> > AVIntPairVec;
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 18169474d..796cd9412 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "util/statistics_registry.h"
 
 using namespace std;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index eba84e339..f3344cbda 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,13 +22,15 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+namespace nl {
+class NonlinearExtension;
+}
 
 class TheoryArithPrivate;
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 3b5f0dd82..40bd81795 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -65,6 +65,7 @@
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/dense_map.h"
 #include "util/integer.h"
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 56e8fa4b0..818393cc7 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -43,6 +43,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/dio_solver.h"
 #include "theory/arith/dual_simplex.h"
+#include "theory/arith/error_set.h"
 #include "theory/arith/fc_simplex.h"
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/linear_equality.h"
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index 96f2b02c3..b5bb9be14 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "options/smt_options.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 4dd7dcafd..49f530e32 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -28,8 +28,10 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arrays/skolem_cache.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/decision_manager.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 
 using namespace std;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 7e4f0e36c..e02c30296 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -29,7 +29,9 @@
 #include "theory/arrays/inference_manager.h"
 #include "theory/arrays/proof_checker.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/decision_strategy.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_equality_engine.h"
 #include "util/statistics_registry.h"
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 76c001ba2..c39e0198b 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -17,6 +17,7 @@
 #include "theory/bags/bag_solver.h"
 
 #include "theory/bags/inference_generator.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace std;
 using namespace CVC4::context;
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 48cd9c419..d9f736c4f 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -19,6 +19,7 @@
 
 #include "theory/bags/rewrites.h"
 #include "theory/rewriter.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 726160d83..f00bffb2e 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "theory/booleans/proof_circuit_propagator.h"
 #include "util/utility.h"
 
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 90de1d8da..b5ad16b1c 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -25,6 +25,7 @@
 #include "theory/booleans/theory_bool_rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
 
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 551c18612..4c7311945 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -15,6 +15,7 @@
 #include "theory/bv/bitblast/simple_bitblaster.h"
 
 #include "theory/theory_model.h"
+#include "theory/theory_state.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 38e4b3aa6..d9adf06fb 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -24,6 +24,7 @@
 #include <unordered_map>
 #include <unordered_set>
 
+#include "context/cdhashset.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
 #include "theory/theory.h"
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index d8d8dbed7..3cadac621 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -30,6 +30,7 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::theory::bv::utils;
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 55a0ff46b..47974fc03 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -21,6 +21,7 @@
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/bv_solver_simple.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/ee_setup_info.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 2aa722e48..fafde0601 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -24,6 +24,7 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
+#include "theory/theory_state.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h
index 40553f01b..6793d6e90 100644
--- a/src/theory/care_graph.h
+++ b/src/theory/care_graph.h
@@ -21,8 +21,8 @@
 
 #include <set>
 
-#include "expr/kind.h"  // For TheoryId.
 #include "expr/node.h"
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 4dbf26062..5334e76df 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "options/datatypes_options.h"
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 14dc9fbf1..ea5928a42 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/infer_proof_cons.h"
 
+#include "expr/proof.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 9702a5584..4c7773e29 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -17,7 +17,11 @@
 #include "expr/dtype.h"
 #include "options/datatypes_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index ba46d2a42..610383ff1 100644
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -25,6 +25,9 @@
 
 namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace datatypes {
 
 /**
diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 6bfa20151..9a9f7cb7b 100644
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/proof_checker.h"
 
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 60bf36139..6169d3752 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/sygus_datatype_utils.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "smt/smt_engine.h"
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 7efd2a9ac..8622ec483 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -15,6 +15,7 @@
 #include "theory/datatypes/sygus_extension.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_manager.h"
 #include "expr/sygus_datatype.h"
 #include "options/base_options.h"
diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index b7ab9b4f7..a2530f4ac 100644
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/sygus_simple_sym.h"
 
+#include "expr/dtype_cons.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 45787ee04..9105cdfd6 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -19,7 +19,9 @@
 
 #include "base/check.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/kind.h"
+#include "expr/proof_node_manager.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 2834b86ba..73aef4dd7 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/type_matcher.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 
diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index c55b4a14f..1247ecca5 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/theory_datatypes_utils.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 079430342..25bdd2f94 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -14,6 +14,7 @@
  ** Enumerators for datatypes.
  **/
 
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/type_enumerator.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index 7b4936a53..030d9a497 100644
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -20,7 +20,9 @@
 
 #include "base/check.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/substitutions.h"
 
 using namespace std;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 6df991ef9..e9b59fdae 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -22,9 +22,12 @@
 #include <unordered_set>
 #include <vector>
 
+#include "base/configuration.h"
 #include "options/fp_options.h"
+#include "smt/logic_exception.h"
 #include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
+#include "theory/output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 1a745b3a3..bd6e70ff1 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -23,9 +23,11 @@
 #include <string>
 #include <utility>
 
+#include "context/cdhashset.h"
 #include "context/cdo.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 0c143f265..3e4b921db 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index bb2bf937a..24570f9a6 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -18,6 +18,7 @@
 #include "options/theory_options.h"
 #include "prop/prop_engine.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index 16f0f3957..7a584c146 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 0d1a51a30..bda4e31fc 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -18,6 +18,8 @@
 #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index e782a1b6f..0c416fdf4 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -17,6 +17,7 @@
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index eb02eb19e..c553a1239 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -14,11 +14,13 @@
 
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 5df350fe5..1875dc631 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -16,7 +16,10 @@
 
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
 #include "util/hash.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index ce535d5e8..07cb74a83 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 5c5dcfef1..dfe2e3ae9 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -15,7 +15,9 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi.h"
 
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
index 66433ba78..00a233d6a 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -14,6 +14,8 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/term_util.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 6b2f1b7f8..f9692bd76 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -14,6 +14,11 @@
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 
 #include "theory/quantifiers/ematching/trigger_term_info.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index e7635f200..9768e7f2c 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/quant_relevance.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 #include "util/random.h"
 
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index 14913bdc1..c2b5f78ae 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
 
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index a64dc4424..6564f407e 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@ -18,6 +18,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 79bd5c1dd..9d8b64e25 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -22,10 +22,12 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index 8448fe810..17baf5000 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -13,7 +13,9 @@
  **/
 #include "theory/quantifiers/ematching/var_match_generator.h"
 
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 759d3e69f..6ce561b2d 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -19,6 +19,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 700ae2c64..fb0505bae 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -16,10 +16,12 @@
 
 #include "theory/quantifiers/fmf/bounded_integers.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/term_enumeration.h"
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 9d4a414e9..3e7466ed2 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -23,6 +23,7 @@
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "expr/attribute.h"
+#include "theory/decision_strategy.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 96e8a40be..c248167cb 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/inst_match.h"
 
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index 993fad90a..ab5dcb166 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace CVC4::context;
 
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 2eb99a774..3164ff5ce 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/instantiate.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index a0b776819..37cc49f17 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -19,6 +19,8 @@
 
 #include <map>
 
+#include "context/cdhashset.h"
+#include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "expr/proof.h"
 #include "theory/quantifiers/inst_match_trie.h"
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index f89f9f0ea..cf37bc746 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/quant_conflict_find.h"
 
+#include "base/configuration.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp
index 5bb50c926..58716f809 100644
--- a/src/theory/quantifiers/quant_rep_bound_ext.cpp
+++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/quant_rep_bound_ext.h"
 
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index a0b780836..e3bd2072f 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -13,6 +13,9 @@
  **/
 
 #include "theory/quantifiers/quant_split.h"
+
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/first_order_model.h"
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2126bf1f0..ec7e7fd2c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
@@ -27,6 +28,7 @@
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 0bcca266e..55f680897 100644
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/quantifiers_state.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 3cef2884f..b97a8e539 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index a9ac7d0d2..42729ef5b 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/skolemize.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index b296a4421..77714f87d 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "smt/command.h"
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index db2a972d5..a58ce894d 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/cegis_core_connective.h"
 
+#include "expr/dtype_cons.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 9db77fd95..5da6f2121 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -19,6 +19,7 @@
 #include <map>
 #include <vector>
 
+#include "theory/decision_strategy.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 360476399..f6e34e8a1 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/sygus/enum_stream_substitution.h"
 
+#include "expr/dtype_cons.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index e0159049b..2fa6009d3 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 882c9ca77..90765284a 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -14,10 +14,12 @@
 
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 0f9d2ccd1..5965e9430 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_explain.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 538d80e44..98a177f86 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -16,6 +16,7 @@
 
 #include <stack>
 
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 7d757ca98..953eac7b0 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 6e36222b6..cc29e7b0a 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index 1e67bb8cc..a2675dd96 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -19,6 +19,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 81120da28..8b741b6d7 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 
 #include "api/cvc4cpp.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index f0d3e47b6..1c0cfcc55 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -15,12 +15,14 @@
 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_unif.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 0fcba916b..56691c7c1 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -14,6 +14,7 @@
  **/
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
+#include "base/configuration.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index bc5cd1fda..f393601ad 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 #include "base/check.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
@@ -23,6 +24,8 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index d44d2eda8..8e29ab9d6 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -16,6 +16,7 @@
 
 #include "base/check.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 9fdf0aa7f..a46d4e445 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -18,11 +18,14 @@
 #include <unordered_set>
 
 #include "expr/node_algorithm.h"
+#include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 3116f35e6..17cb1c9a1 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -21,6 +21,7 @@
 #include <unordered_set>
 
 #include "context/cdhashset.h"
+#include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 62eef124a..a72054f6d 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus_sampler.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cb5c7dfec..281d5c844 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -21,6 +21,8 @@
 #include "options/uf_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9a031f99c..b121b2c46 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -20,6 +20,8 @@
 #include <map>
 #include <unordered_set>
 
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
 #include "expr/attribute.h"
 #include "expr/node_trie.h"
 #include "theory/quantifiers/quant_util.h"
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 9cbf2cf53..33f74c7c4 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/strings/word.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 036b63b27..98bb9bec3 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -18,7 +18,6 @@
 #define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
 
 #include <map>
-#include <unordered_set>
 
 #include "expr/attribute.h"
 #include "expr/node.h"
@@ -55,8 +54,6 @@ typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
 
 namespace quantifiers {
 
-class TermDatabase;
-
 // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
 class TermUtil
 {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7046a8ef0..79422b418 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -20,10 +20,22 @@
 #include "options/uf_options.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/equality_query.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_modules.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/skolemize.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f464b24d4..d08e32f6e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -20,23 +20,11 @@
 #include <map>
 #include <unordered_map>
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
-#include "expr/attribute.h"
-#include "theory/quantifiers/ematching/trigger_trie.h"
-#include "theory/quantifiers/equality_query.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/model_builder.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/quantifiers_inference_manager.h"
-#include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -46,9 +34,24 @@ class TheoryEngine;
 namespace theory {
 
 class DecisionManager;
+class QuantifiersModule;
+class RepSetIterator;
 
+namespace inst {
+class TriggerTrie;
+}
 namespace quantifiers {
+class EqualityQueryQuantifiersEngine;
+class FirstOrderModel;
+class Instantiate;
+class QModelBuilder;
+class QuantifiersInferenceManager;
 class QuantifiersModules;
+class QuantifiersState;
+class Skolemize;
+class TermDb;
+class TermDbSygus;
+class TermEnumeration;
 }
 
 // TODO: organize this more/review this, github issue #1163
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index be26510c6..fc98e6198 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/rewriter.h"
 
+#include "expr/term_conversion_proof_generator.h"
 #include "options/theory_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 572662483..f5c1348ad 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -19,20 +19,21 @@
 #pragma once
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
 #include "theory/theory_rewriter.h"
-#include "theory/trust_node.h"
-#include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
+
+class TConvProofGenerator;
+class ProofNodeManager;
+
 namespace theory {
 
+class TrustNode;
+
 namespace builtin {
 class BuiltinProofRuleChecker;
 }
 
-class RewriterInitializer;
-
 /**
  * The rewrite environment holds everything that the individual rewrites have
  * access to.
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 2a409a304..0a8039ed1 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -24,6 +24,7 @@
 #include "options/sep_options.h"
 #include "options/smt_options.h"
 #include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index b2cd6bf45..198273993 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -23,9 +23,11 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
+#include "theory/decision_strategy.h"
 #include "theory/inference_manager_buffered.h"
 #include "theory/sep/theory_sep_rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 13ee672db..0d832b646 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -18,6 +18,7 @@
 #define SRC_THEORY_SETS_RELS_UTILS_H_
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index e06a8cb52..5c6300059 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -20,6 +20,7 @@
 #include "theory/sets/theory_sets_private.h"
 #include "theory/sets/theory_sets_rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 1e4473d6f..eb802af4a 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/sets/theory_sets_rewriter.h"
 
 #include "expr/attribute.h"
+#include "expr/dtype_cons.h"
 #include "options/sets_options.h"
 #include "theory/sets/normal_form.h"
 #include "theory/sets/rels_utils.h"
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 5446f67be..642a4d4ae 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/strings/core_solver.h"
 
+#include "base/configuration.h"
 #include "options/strings_options.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/strings_entail.h"
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 770991286..620cca185 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/strings/regexp_elim.h"
 
+#include "expr/proof_node_manager.h"
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
 #include "theory/strings/regexp_entail.h"
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0157a47f0..bd95933a5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -19,6 +19,7 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 82463367e..a725f4d88 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/term_registration_visitor.h"
 
+#include "base/configuration.h"
 #include "options/quantifiers_options.h"
 #include "theory/theory_engine.h"
 
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index fef3fdc67..19fc91312 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -26,10 +26,16 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/ee_setup_info.h"
 #include "theory/ext_theory.h"
+#include "theory/output_channel.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/substitutions.h"
+#include "theory/theory_inference_manager.h"
+#include "theory/theory_model.h"
 #include "theory/theory_rewriter.h"
+#include "theory/theory_state.h"
+#include "theory/trust_substitutions.h"
 
 using namespace std;
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index fa26ab65e..5f4698e56 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -20,49 +20,39 @@
 #define CVC4__THEORY__THEORY_H
 
 #include <iosfwd>
-#include <map>
 #include <set>
 #include <string>
 #include <unordered_set>
 
-#include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "options/options.h"
 #include "options/theory_options.h"
-#include "smt/logic_request.h"
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
-#include "theory/decision_manager.h"
-#include "theory/ee_setup_info.h"
 #include "theory/logic_info.h"
-#include "theory/output_channel.h"
 #include "theory/theory_id.h"
-#include "theory/theory_inference_manager.h"
-#include "theory/theory_rewriter.h"
-#include "theory/theory_state.h"
 #include "theory/trust_node.h"
-#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 
-class TheoryEngine;
 class ProofNodeManager;
+class TheoryEngine;
 
 namespace theory {
 
+class DecisionManager;
+struct EeSetupInfo;
+class OutputChannel;
 class QuantifiersEngine;
+class TheoryInferenceManager;
 class TheoryModel;
-class SubstitutionMap;
 class TheoryRewriter;
-
-namespace rrinst {
-  class CandidateGenerator;
-}/* CVC4::theory::rrinst namespace */
+class TheoryState;
+class TrustSubstitutionMap;
 
 namespace eq {
   class EqualityEngine;
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 53a812653..810f31ce5 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -15,8 +15,11 @@
 #include "theory/theory_inference_manager.h"
 
 #include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index d3a317cbc..61b105dac 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -23,9 +23,8 @@
 #include "expr/node.h"
 #include "theory/inference_id.h"
 #include "theory/output_channel.h"
-#include "theory/theory_state.h"
 #include "theory/trust_node.h"
-#include "theory/uf/proof_equality_engine.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -34,8 +33,10 @@ class ProofNodeManager;
 namespace theory {
 
 class Theory;
+class TheoryState;
 namespace eq {
 class EqualityEngine;
+class ProofEqEngine;
 }
 
 /**
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 9604dc72b..89f53acb8 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -14,6 +14,7 @@
 #include "theory/theory_model_builder.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index a0586bd0c..d4d2a78a5 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -18,11 +18,11 @@
 #define CVC4__THEORY__TRUST_NODE_H
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 
 class ProofGenerator;
+class ProofNode;
 
 namespace theory {
 
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 7ab43091a..58d5f4924 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/uf/eq_proof.h"
 
+#include "base/configuration.h"
 #include "expr/proof.h"
 #include "options/uf_options.h"
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 497e394c7..49e19c15f 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -25,6 +25,7 @@
 #include "expr/node_trie.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
 #include "theory/uf/proof_equality_engine.h"
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index 9233bde53..5d017cb0f 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -18,6 +18,8 @@
 
 #include "util/bitvector.h"
 
+#include "base/exception.h"
+
 namespace CVC4 {
 
 unsigned BitVector::getSize() const { return d_size; }
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 997293639..b1a27929a 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -21,7 +21,6 @@
 
 #include <iosfwd>
 
-#include "base/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 585512138..f78b076de 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -16,7 +16,10 @@
 
 #include "util/cardinality.h"
 
+#include <ostream>
+
 #include "base/check.h"
+#include "base/exception.h"
 
 namespace CVC4 {
 
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 8ad3edbe2..9218095a8 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -20,10 +20,8 @@
 #ifndef CVC4__CARDINALITY_H
 #define CVC4__CARDINALITY_H
 
-#include <iostream>
-#include <utility>
+#include <iosfwd>
 
-#include "base/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {
diff --git a/src/util/divisible.h b/src/util/divisible.h
index 36bb37db0..b2682b055 100644
--- a/src/util/divisible.h
+++ b/src/util/divisible.h
@@ -21,8 +21,9 @@
 #define CVC4__DIVISIBLE_H
 
 #include <iosfwd>
+#include <ostream>
+#include <stddef.h>
 
-#include "base/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {
diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp
index c97238892..ce8b50bc8 100644
--- a/src/util/ostream_util.cpp
+++ b/src/util/ostream_util.cpp
@@ -15,6 +15,8 @@
  **/
 #include "util/ostream_util.h"
 
+#include <ostream>
+
 namespace CVC4 {
 
 StreamFormatScope::StreamFormatScope(std::ostream& out)
diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h
index b27c22819..6e2a291a3 100644
--- a/src/util/ostream_util.h
+++ b/src/util/ostream_util.h
@@ -20,7 +20,7 @@
 #define CVC4__UTIL__OSTREAM_UTIL_H
 
 #include <ios>
-#include <ostream>
+#include <iosfwd>
 
 namespace CVC4 {
 
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 17dac50b3..0534be1b7 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -16,8 +16,13 @@
 **/
 #include "util/resource_manager.h"
 
+#include <algorithm>
+#include <ostream>
+
 #include "base/check.h"
+#include "base/listener.h"
 #include "base/output.h"
+#include "options/options.h"
 #include "options/smt_options.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 3be99021b..a4a9b7f4e 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -21,18 +21,15 @@
 #ifndef CVC4__RESOURCE_MANAGER_H
 #define CVC4__RESOURCE_MANAGER_H
 
-#include <sys/time.h>
-
+#include <stdint.h>
 #include <chrono>
 #include <memory>
-
-#include "base/exception.h"
-#include "base/listener.h"
-#include "options/options.h"
-#include "util/unsafe_interrupt_exception.h"
+#include <vector>
 
 namespace CVC4 {
 
+class Listener;
+class Options;
 class StatisticsRegistry;
 
 /**
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 73e6afb96..781c73aec 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -17,8 +17,6 @@
 
 #include "util/statistics.h"
 
-#include <typeinfo>
-
 #include "util/safe_print.h"
 #include "util/statistics_registry.h" // for details about class Stat
 
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index d2f7244f9..efa1de1c0 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -43,7 +43,6 @@
 #include <vector>
 
 #include "base/exception.h"
-#include "lib/clock_gettime.h"
 #include "util/safe_print.h"
 #include "util/statistics.h"
 
diff --git a/src/util/tuple.h b/src/util/tuple.h
index 240e41792..109d4640b 100644
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -20,7 +20,6 @@
 #define CVC4__TUPLE_H
 
 #include <iostream>
-#include <string>
 #include <vector>
 #include <utility>
 
diff --git a/src/util/utility.cpp b/src/util/utility.cpp
index 7a50eb7fd..2b848d924 100644
--- a/src/util/utility.cpp
+++ b/src/util/utility.cpp
@@ -19,7 +19,6 @@
 #include <unistd.h>
 
 #include <cstdlib>
-#include <iostream>
 
 #include "base/check.h"
 
diff --git a/src/util/utility.h b/src/util/utility.h
index 549b98d66..06155788f 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -21,10 +21,8 @@
 
 #include <algorithm>
 #include <fstream>
-#include <functional>
 #include <memory>
 #include <string>
-#include <utility>
 
 namespace CVC4 {