More cleanup of includes to reduce compilation times (#6037)

Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.

214 files changed, 571 insertions, 343 deletions

diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index cddef79fd..ad50ec351 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -20,6 +20,7 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cstring>
+#include <sstream>
 #include <string>
 
 #include "base/check.h"
@@ -28,6 +29,13 @@ using namespace std;
 
 namespace CVC4 {
 
+std::string Exception::toString() const
+{
+  std::stringstream ss;
+  toStream(ss);
+  return ss.str();
+}
+
 thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = nullptr;
 
 LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {}
diff --git a/src/base/exception.h b/src/base/exception.h
index 8a89c99fc..815e4011f 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -19,12 +19,8 @@
 #ifndef CVC4__EXCEPTION_H
 #define CVC4__EXCEPTION_H
 
-#include <cstdarg>
-#include <cstdlib>
 #include <exception>
 #include <iosfwd>
-#include <sstream>
-#include <stdexcept>
 #include <string>
 
 namespace CVC4 {
@@ -61,12 +57,7 @@ class CVC4_PUBLIC Exception : public std::exception {
    * toString(), there is no stream, so the parameters are default
    * and you'll get exprs and types printed using the AST language.
    */
-  std::string toString() const
-  {
-    std::stringstream ss;
-    toStream(ss);
-    return ss.str();
-  }
+  std::string toString() const;
 
   /**
    * Printing: feel free to redefine toStream().  When overridden in
diff --git a/src/base/listener.cpp b/src/base/listener.cpp
index 72f9ee086..6e9d659fd 100644
--- a/src/base/listener.cpp
+++ b/src/base/listener.cpp
@@ -16,10 +16,6 @@
 
 #include "base/listener.h"
 
-#include <list>
-
-#include "base/check.h"
-
 namespace CVC4 {
 
 Listener::Listener(){}
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index e1327c0a7..2cebfa447 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -20,6 +20,7 @@
 #include "expr/node.h"
 #include "options/decision_options.h"
 #include "options/smt_options.h"
+#include "util/resource_manager.h"
 
 using namespace std;
 
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 914636fe9..74a230e29 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -19,18 +19,15 @@
 #ifndef CVC4__DECISION__DECISION_ENGINE_H
 #define CVC4__DECISION__DECISION_ENGINE_H
 
-#include <vector>
-
 #include "base/output.h"
+#include "context/cdo.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
 #include "prop/cnf_stream.h"
-#include "prop/prop_engine.h"
+#include "prop/sat_solver.h"
 #include "prop/sat_solver_types.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/term_formula_removal.h"
+#include "util/result.h"
 
-using namespace std;
 using namespace CVC4::prop;
 using namespace CVC4::decision;
 
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 1d0b386e3..4950f4f3d 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -18,15 +18,18 @@
  **/
 #include "justification_heuristic.h"
 
+#include "decision/decision_attributes.h"
+#include "decision/decision_engine.h"
 #include "expr/kind.h"
 #include "expr/node_manager.h"
 #include "options/decision_options.h"
-#include "theory/rewriter.h"
-#include "smt/term_formula_removal.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/term_formula_removal.h"
+#include "theory/rewriter.h"
 #include "util/random.h"
 
 namespace CVC4 {
+namespace decision {
 
 JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
                                                context::UserContext* uc,
@@ -67,8 +70,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch)
 {
   if(options::decisionThreshold() > 0) {
     bool stopSearchTmp = false;
-    SatLiteral lit = getNextThresh(stopSearchTmp, options::decisionThreshold());
-    if(lit != undefSatLiteral) {
+    prop::SatLiteral lit =
+        getNextThresh(stopSearchTmp, options::decisionThreshold());
+    if (lit != prop::undefSatLiteral)
+    {
       Assert(stopSearchTmp == false);
       return lit;
     }
@@ -88,9 +93,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
     for(JustifiedSet::key_iterator i = d_justified.key_begin();
         i != d_justified.key_end(); ++i) {
       TNode n = *i;
-      SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
-        d_decisionEngine->getSatLiteral(n) : -1;
-      SatValue v = tryGetSatValue(n);
+      prop::SatLiteral l = d_decisionEngine->hasSatLiteral(n)
+                               ? d_decisionEngine->getSatLiteral(n)
+                               : -1;
+      prop::SatValue v = tryGetSatValue(n);
       Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl;
     }
   }
@@ -102,12 +108,13 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
     // Commenting out. See bug 374. In short, to do with how CNF stream works.
     // Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
 
-    SatValue desiredVal = SAT_VALUE_TRUE;
-    SatLiteral litDecision;
+    prop::SatValue desiredVal = prop::SAT_VALUE_TRUE;
+    prop::SatLiteral litDecision;
 
     litDecision = findSplitter(d_assertions[i], desiredVal);
 
-    if(litDecision != undefSatLiteral) {
+    if (litDecision != prop::undefSatLiteral)
+    {
       setPrvsIndex(i);
       Trace("decision") << "jh: splitting on " << litDecision << std::endl;
       ++d_helpfulness;
@@ -136,25 +143,26 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
 
   // SAT solver can stop...
   stopSearch = true;
-  if(d_curThreshold == 0)
-    d_decisionEngine->setResult(SAT_VALUE_TRUE);
+  if (d_curThreshold == 0) d_decisionEngine->setResult(prop::SAT_VALUE_TRUE);
   return prop::undefSatLiteral;
 }
 
-
-inline void computeXorIffDesiredValues
-(Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2)
+inline void computeXorIffDesiredValues(Kind k,
+                                       prop::SatValue desiredVal,
+                                       prop::SatValue& desiredVal1,
+                                       prop::SatValue& desiredVal2)
 {
   Assert(k == kind::EQUAL || k == kind::XOR);
 
   bool shouldInvert =
-    (desiredVal == SAT_VALUE_TRUE && k == kind::EQUAL) ||
-    (desiredVal == SAT_VALUE_FALSE && k == kind::XOR);
+      (desiredVal == prop::SAT_VALUE_TRUE && k == kind::EQUAL)
+      || (desiredVal == prop::SAT_VALUE_FALSE && k == kind::XOR);
 
-  if(desiredVal1 == SAT_VALUE_UNKNOWN &&
-     desiredVal2 == SAT_VALUE_UNKNOWN) {
+  if (desiredVal1 == prop::SAT_VALUE_UNKNOWN
+      && desiredVal2 == prop::SAT_VALUE_UNKNOWN)
+  {
     // CHOICE: pick one of them arbitarily
-    desiredVal1 = SAT_VALUE_FALSE;
+    desiredVal1 = prop::SAT_VALUE_FALSE;
   }
 
   if(desiredVal2 == SAT_VALUE_UNKNOWN) {
@@ -214,9 +222,9 @@ bool JustificationHeuristic::checkJustified(TNode n)
 
 DecisionWeight JustificationHeuristic::getExploredThreshold(TNode n)
 {
-  return
-    d_exploredThreshold.find(n) == d_exploredThreshold.end() ?
-    numeric_limits<DecisionWeight>::max() : d_exploredThreshold[n];
+  return d_exploredThreshold.find(n) == d_exploredThreshold.end()
+             ? std::numeric_limits<DecisionWeight>::max()
+             : d_exploredThreshold[n];
 }
 
 void JustificationHeuristic::setExploredThreshold(TNode n)
@@ -263,36 +271,36 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity
     } else {
 
       if(k == kind::OR) {
-        dW1 = numeric_limits<DecisionWeight>::max(), dW2 = 0;
+        dW1 = std::numeric_limits<DecisionWeight>::max(), dW2 = 0;
         for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
-          dW1 = min(dW1, getWeightPolarized(*i, true));
-          dW2 = max(dW2, getWeightPolarized(*i, false));
+          dW1 = std::min(dW1, getWeightPolarized(*i, true));
+          dW2 = std::max(dW2, getWeightPolarized(*i, false));
         }
       } else if(k == kind::AND) {
-        dW1 = 0, dW2 = numeric_limits<DecisionWeight>::max();
+        dW1 = 0, dW2 = std::numeric_limits<DecisionWeight>::max();
         for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
-          dW1 = max(dW1, getWeightPolarized(*i, true));
-          dW2 = min(dW2, getWeightPolarized(*i, false));
+          dW1 = std::max(dW1, getWeightPolarized(*i, true));
+          dW2 = std::min(dW2, getWeightPolarized(*i, false));
         }
       } else if(k == kind::IMPLIES) {
-        dW1 = min(getWeightPolarized(n[0], false),
-                  getWeightPolarized(n[1], true));
-        dW2 = max(getWeightPolarized(n[0], true),
-                  getWeightPolarized(n[1], false));
+        dW1 = std::min(getWeightPolarized(n[0], false),
+                       getWeightPolarized(n[1], true));
+        dW2 = std::max(getWeightPolarized(n[0], true),
+                       getWeightPolarized(n[1], false));
       } else if(k == kind::NOT) {
         dW1 = getWeightPolarized(n[0], false);
         dW2 = getWeightPolarized(n[0], true);
       } else {
         dW1 = 0;
         for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
-          dW1 = max(dW1, getWeightPolarized(*i, true));
-          dW1 = max(dW1, getWeightPolarized(*i, false));
+          dW1 = std::max(dW1, getWeightPolarized(*i, true));
+          dW1 = std::max(dW1, getWeightPolarized(*i, false));
         }
         dW2 = dW1;
       }
 
     }
-    d_weightCache[n] = make_pair(dW1, dW2);
+    d_weightCache[n] = std::make_pair(dW1, dW2);
   }
   return polarity ? d_weightCache[n].get().first : d_weightCache[n].get().second;
 }
@@ -315,7 +323,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
     {
       DecisionWeight dW = 0;
       for (TNode::iterator i = n.begin(); i != n.end(); ++i)
-        dW = max(dW, getWeight(*i));
+        dW = std::max(dW, getWeight(*i));
       n.setAttribute(DecisionWeightAttr(), dW);
     }
     else if (combiningFn == options::DecisionWeightInternal::SUM
@@ -323,7 +331,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
     {
       DecisionWeight dW = 0;
       for (TNode::iterator i = n.begin(); i != n.end(); ++i)
-        dW = max(dW, getWeight(*i));
+        dW = std::max(dW, getWeight(*i));
       n.setAttribute(DecisionWeightAttr(), dW);
     }
     else
@@ -334,7 +342,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
   return n.getAttribute(DecisionWeightAttr());
 }
 
-typedef vector<TNode> ChildList;
+typedef std::vector<TNode> ChildList;
 TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) {
   if(options::decisionUseWeight()) {
     // TODO: Optimize storing & access
@@ -389,7 +397,7 @@ void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l)
     SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]);
     if (it2 != d_skolemAssertions.end())
     {
-      l.push_back(make_pair(n[i], (*it2).second));
+      l.push_back(std::make_pair(n[i], (*it2).second));
       Assert(n[i].getNumChildren() == 0);
     }
     if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end())
@@ -610,8 +618,8 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TN
 {
   if(options::decisionUseWeight() &&
      getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
-    swap(node1, node2);
-    swap(desiredVal1, desiredVal2);
+    std::swap(node1, node2);
+    std::swap(desiredVal1, desiredVal2);
   }
 
   if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) {
@@ -635,8 +643,8 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TN
 {
   if(options::decisionUseWeight() &&
      getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
-    swap(node1, node2);
-    swap(desiredVal1, desiredVal2);
+    std::swap(node1, node2);
+    std::swap(desiredVal1, desiredVal2);
   }
 
   bool noSplitter = true;
@@ -722,4 +730,5 @@ JustificationHeuristic::handleEmbeddedSkolems(TNode node)
   return noSplitter ? NO_SPLITTER : DONT_KNOW;
 }
 
-} /* namespace CVC4 */
+} /* namespace decision */
+} /* namespace CVC4 */
\ No newline at end of file
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 0a16759e1..1cf2810fd 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -24,16 +24,17 @@
 #define CVC4__DECISION__JUSTIFICATION_HEURISTIC
 
 #include <unordered_set>
+#include <utility>
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
-#include "decision/decision_attributes.h"
-#include "decision/decision_engine.h"
+#include "context/cdo.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
-#include "preprocessing/assertion_pipeline.h"
+#include "options/decision_weight.h"
 #include "prop/sat_solver_types.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace decision {
@@ -42,12 +43,17 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   //                   TRUE           FALSE         MEH
   enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
 
-  typedef std::vector<pair<TNode, TNode> > SkolemList;
+  typedef std::vector<std::pair<TNode, TNode> > SkolemList;
   typedef context::CDHashMap<TNode, SkolemList, TNodeHashFunction> SkolemCache;
   typedef std::vector<TNode> ChildList;
-  typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache;
+  typedef context::
+      CDHashMap<TNode, std::pair<ChildList, ChildList>, TNodeHashFunction>
+          ChildCache;
   typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
-  typedef context::CDHashMap<TNode,pair<DecisionWeight,DecisionWeight>,TNodeHashFunction> WeightCache;
+  typedef context::CDHashMap<TNode,
+                             std::pair<DecisionWeight, DecisionWeight>,
+                             TNodeHashFunction>
+      WeightCache;
 
   // being 'justified' is monotonic with respect to decisions
   typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
@@ -91,7 +97,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   std::unordered_set<TNode, TNodeHashFunction> d_visitedComputeSkolems;
 
   /** current decision for the recursive call */
-  SatLiteral d_curDecision;
+  prop::SatLiteral d_curDecision;
   /** current threshold for the recursive call */
   DecisionWeight d_curThreshold;
 
@@ -136,12 +142,12 @@ public:
   /* getNext with an option to specify threshold */
   prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold);
 
-  SatLiteral findSplitter(TNode node, SatValue desiredVal);
+  prop::SatLiteral findSplitter(TNode node, prop::SatValue desiredVal);
 
   /**
    * Do all the hard work.
    */
-  SearchResult findSplitterRec(TNode node, SatValue value);
+  SearchResult findSplitterRec(TNode node, prop::SatValue value);
 
   /* Helper functions */
   void setJustified(TNode);
@@ -151,7 +157,7 @@ public:
   void setPrvsIndex(int);
   int  getPrvsIndex();
   DecisionWeight getWeightPolarized(TNode n, bool polarity);
-  DecisionWeight getWeightPolarized(TNode n, SatValue);
+  DecisionWeight getWeightPolarized(TNode n, prop::SatValue);
   static DecisionWeight getWeight(TNode);
   bool compareByWeightFalse(TNode, TNode);
   bool compareByWeightTrue(TNode, TNode);
@@ -159,7 +165,7 @@ public:
 
   /* If literal exists corresponding to the node return
      that. Otherwise an UNKNOWN */
-  SatValue tryGetSatValue(Node n);
+  prop::SatValue tryGetSatValue(Node n);
 
   /* Get list of all term-ITEs for the atomic formula v */
   JustificationHeuristic::SkolemList getSkolems(TNode n);
@@ -176,13 +182,17 @@ public:
   /* Compute all term-removal skolems in a node recursively */
   void computeSkolems(TNode n, SkolemList& l);
 
-  SearchResult handleAndOrEasy(TNode node, SatValue desiredVal);
-  SearchResult handleAndOrHard(TNode node, SatValue desiredVal);
-  SearchResult handleBinaryEasy(TNode node1, SatValue desiredVal1,
-                        TNode node2, SatValue desiredVal2);
-  SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1,
-                        TNode node2, SatValue desiredVal2);
-  SearchResult handleITE(TNode node, SatValue desiredVal);
+  SearchResult handleAndOrEasy(TNode node, prop::SatValue desiredVal);
+  SearchResult handleAndOrHard(TNode node, prop::SatValue desiredVal);
+  SearchResult handleBinaryEasy(TNode node1,
+                                prop::SatValue desiredVal1,
+                                TNode node2,
+                                prop::SatValue desiredVal2);
+  SearchResult handleBinaryHard(TNode node1,
+                                prop::SatValue desiredVal1,
+                                TNode node2,
+                                prop::SatValue desiredVal2);
+  SearchResult handleITE(TNode node, prop::SatValue desiredVal);
   SearchResult handleEmbeddedSkolems(TNode node);
 };/* class JustificationHeuristic */
 
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index da80891a2..15ae6ea83 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -19,11 +19,11 @@
 
 #include "context/cdhashmap.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
 class ProofNodeManager;
+class ProofStep;
 
 /**
  * The proof generator for buffered steps. This class is a context-dependent
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index f94f0063a..5451edc02 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -13,6 +13,8 @@
  **/
 #include "expr/dtype.h"
 
+#include <sstream>
+
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/type_matcher.h"
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 0bda68b7b..e82e614b3 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -15,6 +15,8 @@
  ** \todo document this file
  **/
 
+#include <sstream>
+
 #include "expr/kind.h"
 
 namespace CVC4 {
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 8d8d2741f..9c6d0e290 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.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 83dc90e4d..7c39164fe 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -17,14 +17,11 @@
 #ifndef CVC4__EXPR__LAZY_PROOF_H
 #define CVC4__EXPR__LAZY_PROOF_H
 
-#include <unordered_map>
-#include <vector>
-
 #include "expr/proof.h"
-#include "expr/proof_generator.h"
 
 namespace CVC4 {
 
+class ProofGenerator;
 class ProofNodeManager;
 
 /**
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index f80ab099c..0e5e8c376 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/proof.h"
 #include "expr/proof_ensure_closed.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_algorithm.h"
 #include "expr/proof_node_manager.h"
 #include "options/proof_options.h"
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 1604bf182..e1b0f3cd0 100644
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H
 #define CVC4__EXPR__LAZY_PROOF_CHAIN_H
 
-#include <unordered_map>
 #include <vector>
 
 #include "context/cdhashmap.h"
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 1aca73d2e..eee8d0136 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -15,8 +15,9 @@
  **/
 #include "expr/node.h"
 
-#include <iostream>
 #include <cstring>
+#include <iostream>
+#include <sstream>
 
 #include "base/exception.h"
 #include "base/output.h"
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index b512b5869..6596f6c5f 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/proof.h"
 
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
 using namespace CVC4::kind;
diff --git a/src/expr/proof.h b/src/expr/proof.h
index 3a26f0975..abb0b9b37 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -17,17 +17,16 @@
 #ifndef CVC4__EXPR__PROOF_H
 #define CVC4__EXPR__PROOF_H
 
-#include <map>
 #include <vector>
 
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node.h"
 #include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+class ProofNode;
 class ProofNodeManager;
 
 /**
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index dc87d1795..a5655c9db 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -14,6 +14,7 @@
 
 #include "expr/proof_checker.h"
 
+#include "expr/proof_node.h"
 #include "expr/skolem_manager.h"
 #include "options/proof_options.h"
 #include "smt/smt_statistics_registry.h"
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index ab9c24434..200a1839d 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -20,12 +20,13 @@
 #include <map>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 
 class ProofChecker;
+class ProofNode;
 
 /** A virtual base class for checking a proof rule */
 class ProofRuleChecker
diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
index 6eebcd3ec..183ff0d5b 100644
--- a/src/expr/proof_ensure_closed.cpp
+++ b/src/expr/proof_ensure_closed.cpp
@@ -14,6 +14,10 @@
 
 #include "expr/proof_ensure_closed.h"
 
+#include <sstream>
+
+#include "expr/proof_generator.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_algorithm.h"
 #include "options/proof_options.h"
 #include "options/smt_options.h"
diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index 7b970a71a..c54a5dfd5 100644
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -18,11 +18,12 @@
 #define CVC4__EXPR__PROOF_ENSURE_CLOSED_H
 
 #include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 
+class ProofGenerator;
+class ProofNode;
+
 /**
  * Debug check closed on Trace c. Context ctx is string for debugging.
  * This method throws an assertion failure if pg cannot provide a closed
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index d2206a570..31af09b7f 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -14,7 +14,10 @@
 
 #include "expr/proof_generator.h"
 
+#include <sstream>
+
 #include "expr/proof.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_algorithm.h"
 #include "options/smt_options.h"
 
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 869f226b8..3b376d77c 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -18,11 +18,11 @@
 #define CVC4__EXPR__PROOF_GENERATOR_H
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 
 class CDProof;
+class ProofNode;
 
 /** An overwrite policy for CDProof */
 enum class CDPOverwrite : uint32_t
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 2af296813..751dcc39e 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/proof_node_algorithm.h"
 
+#include "expr/proof_node.h"
+
 namespace CVC4 {
 namespace expr {
 
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index 43d06ea91..af8de066d 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -20,9 +20,11 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
+
+class ProofNode;
+
 namespace expr {
 
 /**
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index f5e15f6d6..91858f239 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -15,6 +15,8 @@
 #include "expr/proof_node_manager.h"
 
 #include "expr/proof.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_algorithm.h"
 #include "options/proof_options.h"
 #include "theory/rewriter.h"
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 3ad56c92d..e7be50065 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -19,11 +19,14 @@
 
 #include <vector>
 
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
+#include "expr/node.h"
+#include "expr/proof_rule.h"
 
 namespace CVC4 {
 
+class ProofChecker;
+class ProofNode;
+
 /**
  * A manager for proof node objects. This is a trusted interface for creating
  * and updating ProofNode objects.
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index fbfc3e3d4..6830326ba 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -15,7 +15,9 @@
 #include "expr/proof_node_to_sexpr.h"
 
 #include <iostream>
+#include <sstream>
 
+#include "expr/proof_node.h"
 #include "options/proof_options.h"
 
 using namespace CVC4::kind;
diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h
index 3e0d42a7d..e6c003d10 100644
--- a/src/expr/proof_node_to_sexpr.h
+++ b/src/expr/proof_node_to_sexpr.h
@@ -20,10 +20,12 @@
 #include <map>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 
 namespace CVC4 {
 
+class ProofNode;
+
 /** A class to convert ProofNode objects to s-expressions */
 class ProofNodeToSExpr
 {
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index e0f096075..f421ff4f3 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -17,6 +17,7 @@
 #include "expr/lazy_proof.h"
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 9814c8166..2df668384 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -18,14 +18,17 @@
 #define CVC4__EXPR__PROOF_NODE_UPDATER_H
 
 #include <map>
-#include <unordered_set>
+#include <memory>
 
-#include "expr/proof.h"
+#include "expr/node.h"
 #include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
+class CDProof;
+class ProofNode;
+class ProofNodeManager;
+
 /**
  * A virtual callback class for updating ProofNode. An example use case of this
  * class is to eliminate a proof rule by expansion.
diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp
index bb02aeb20..4c99855df 100644
--- a/src/expr/proof_step_buffer.cpp
+++ b/src/expr/proof_step_buffer.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/proof_step_buffer.h"
 
+#include "expr/proof_checker.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
index 4e463a7b3..1b09a8f96 100644
--- a/src/expr/proof_step_buffer.h
+++ b/src/expr/proof_step_buffer.h
@@ -20,11 +20,12 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/proof_checker.h"
 #include "expr/proof_rule.h"
 
 namespace CVC4 {
 
+class ProofChecker;
+
 /**
  * Information for constructing a step in a CDProof. Notice that the conclusion
  * of the proof step is intentionally not included in this data structure.
diff --git a/src/expr/record.h b/src/expr/record.h
index 4e1ff6772..1ab84c30c 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__RECORD_H
 #define CVC4__RECORD_H
 
-#include <functional>
 #include <iostream>
 #include <string>
 #include <vector>
diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index f65558184..68c4985bb 100644
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -14,6 +14,7 @@
 
 #include "expr/sequence.h"
 
+#include <sstream>
 #include <vector>
 
 #include "expr/node.h"
diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp
index 541db1ac5..3ca75050a 100644
--- a/src/expr/subs.cpp
+++ b/src/expr/subs.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/subs.h"
 
+#include <sstream>
+
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index 3401e55f7..e67a1befe 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/sygus_datatype.h"
 
+#include <sstream>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index fa5732854..73018d7ca 100644
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -19,7 +19,6 @@
 
 #include <map>
 #include <memory>
-#include <set>
 #include <string>
 
 #include "api/cvc4cpp.h"
diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp
index 8bd850488..105c811d4 100644
--- a/src/expr/tconv_seq_proof_generator.cpp
+++ b/src/expr/tconv_seq_proof_generator.cpp
@@ -14,6 +14,10 @@
 
 #include "expr/tconv_seq_proof_generator.h"
 
+#include <sstream>
+
+#include "expr/proof_node_manager.h"
+
 namespace CVC4 {
 
 TConvSeqProofGenerator::TConvSeqProofGenerator(
diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
index 95499d6b8..9197028d6 100644
--- a/src/expr/tconv_seq_proof_generator.h
+++ b/src/expr/tconv_seq_proof_generator.h
@@ -20,11 +20,12 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * The term conversion sequence proof generator. This is used for maintaining
  * a fixed sequence of proof generators that provide proofs for rewrites
diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp
index e5ebd0209..91f7f3190 100644
--- a/src/expr/term_canonize.cpp
+++ b/src/expr/term_canonize.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/term_canonize.h"
 
+#include <sstream>
+
 // TODO #1216: move the code in this include
 #include "theory/quantifiers/term_util.h"
 
diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h
index ff8187bbc..061cf1ed2 100644
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -18,11 +18,11 @@
 #define CVC4__EXPR__TERM_CONTEXT_NODE_H
 
 #include "expr/node.h"
-#include "expr/term_context.h"
 
 namespace CVC4 {
 
 class TCtxStack;
+class TermContext;
 
 /**
  * A (term-context) sensitive term. This is a wrapper around a Node that
diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp
index 64cab7035..f35514fa6 100644
--- a/src/expr/term_context_stack.cpp
+++ b/src/expr/term_context_stack.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/term_context_stack.h"
 
+#include "expr/term_context.h"
+
 namespace CVC4 {
 
 TCtxStack::TCtxStack(const TermContext* tctx) : d_tctx(tctx) {}
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index d37ccf914..a47214ae1 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -14,6 +14,9 @@
 
 #include "expr/term_conversion_proof_generator.h"
 
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+#include "expr/term_context.h"
 #include "expr/term_context_stack.h"
 
 using namespace CVC4::kind;
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index dcf8b3fa4..4d6a169cb 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -20,11 +20,12 @@
 #include "context/cdhashmap.h"
 #include "expr/lazy_proof.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
-#include "expr/term_context.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+class TermContext;
+
 /** A policy for how rewrite steps are applied in TConvProofGenerator */
 enum class TConvPolicy : uint32_t
 {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index dadbdc91d..cbc15e153 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -16,6 +16,7 @@
 #include "expr/type.h"
 
 #include <iostream>
+#include <sstream>
 #include <string>
 #include <vector>
 
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index e7685dba8..f5a729b36 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -14,6 +14,8 @@
  ** TypeChecker implementation.
  **/
 
+#include <sstream>
+
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/type_checker.h"
diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h
index 312ffe53a..32c1254de 100644
--- a/src/expr/type_checker_util.h
+++ b/src/expr/type_checker_util.h
@@ -19,6 +19,8 @@
 
 #include "cvc4_private.h"
 
+#include <sstream>
+
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h
index 47fc36eee..126175582 100644
--- a/src/expr/type_matcher.h
+++ b/src/expr/type_matcher.h
@@ -19,7 +19,6 @@
 
 #include <vector>
 
-#include "expr/node.h"
 #include "expr/type_node.h"
 
 namespace CVC4 {
diff --git a/src/options/language.cpp b/src/options/language.cpp
index c2eb13852..ee6da3e48 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -16,6 +16,11 @@
 
 #include "options/language.h"
 
+#include <sstream>
+
+#include "base/exception.h"
+#include "options/option_exception.h"
+
 namespace CVC4 {
 namespace language {
 
diff --git a/src/options/language.h b/src/options/language.h
index b34ac378e..e1e4dfed3 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -19,12 +19,9 @@
 #ifndef CVC4__LANGUAGE_H
 #define CVC4__LANGUAGE_H
 
-#include <sstream>
+#include <ostream>
 #include <string>
 
-#include "base/exception.h"
-#include "options/option_exception.h"
-
 namespace CVC4 {
 namespace language {
 
@@ -182,9 +179,9 @@ bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC;
 bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC;
 
 /**
-  * Is the language smtlib 2.5 or above? If exact=true, then this method returns
-  * false if the input language is not exactly SMT-LIB 2.6.
-  */
+ * Is the language smtlib 2.5 or above? If exact=true, then this method returns
+ * false if the input language is not exactly SMT-LIB 2.5.
+ */
 bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
 bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
 /**
diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h
index 6b6a1afb7..b62c56898 100644
--- a/src/options/open_ostream.h
+++ b/src/options/open_ostream.h
@@ -20,13 +20,11 @@
 #ifndef CVC4__OPEN_OSTREAM_H
 #define CVC4__OPEN_OSTREAM_H
 
+#include <iosfwd>
 #include <map>
-#include <ostream>
 #include <string>
 #include <utility>
 
-#include "options/option_exception.h"
-
 namespace CVC4 {
 
 class OstreamOpener {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 07e629976..9652c9f8e 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -22,17 +22,18 @@
 #include <ostream>
 #include <string>
 
-#include "base/modal_exception.h"
 #include "options/base_handlers.h"
 #include "options/bv_options.h"
 #include "options/decision_options.h"
 #include "options/language.h"
 #include "options/option_exception.h"
-#include "options/options.h"
 #include "options/printer_modes.h"
 #include "options/quantifiers_options.h"
 
 namespace CVC4 {
+
+class Options;
+
 namespace options {
 
 /**
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 4bc3323e5..250c0639c 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_manager.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
+#include "smt/preprocess_proof_generator.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 9d65329b0..408c0718c 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -21,13 +21,15 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
-#include "smt/preprocess_proof_generator.h"
-#include "smt/term_formula_removal.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class ProofGenerator;
+namespace smt {
+class PreprocessProofGenerator;
+}
+
 namespace preprocessing {
 
 using IteSkolemMap = std::unordered_map<size_t, Node>;
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index a092a8778..f8efa5de9 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -22,11 +22,15 @@
  **/
 
 #include "preprocessing/passes/ackermann.h"
+
 #include <cmath>
+
 #include "base/check.h"
 #include "expr/node_algorithm.h"
 #include "options/options.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -197,7 +201,7 @@ size_t getBVSkolemSize(size_t capacity)
  * a sufficient bit-vector size.
  * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
  * the fresh skolem BV variables. variables */
-void collectUSortsToBV(const unordered_set<TNode, TNodeHashFunction>& vars,
+void collectUSortsToBV(const std::unordered_set<TNode, TNodeHashFunction>& vars,
                        const USortToBVSizeMap& usortCardinality,
                        SubstitutionMap& usVarsToBVVars)
 {
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h
index cd0d059e4..e28a1ca2d 100644
--- a/src/preprocessing/passes/ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -27,9 +27,11 @@
 #define CVC4__PREPROCESSING__PASSES__ACKERMANN_H
 
 #include <unordered_map>
+
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/logic_info.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index c93895e79..0369dd0ed 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -18,6 +18,8 @@
 #include "preprocessing/passes/apply_substs.h"
 
 #include "context/cdo.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 
diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h
index 781fcc79e..197e08eaf 100644
--- a/src/preprocessing/passes/apply_substs.h
+++ b/src/preprocessing/passes/apply_substs.h
@@ -21,10 +21,12 @@
 #define CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
+
+class PreprocessingPassContext;
+
 namespace passes {
 
 class ApplySubsts : public PreprocessingPass
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 47a504d59..6a1d76fad 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -19,7 +19,10 @@
 
 #include "base/map_util.h"
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
index c5e6f3801..917954da6 100644
--- a/src/preprocessing/passes/bool_to_bv.h
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -18,10 +18,9 @@
 #ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 #define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 
+#include "expr/node.h"
 #include "options/bv_options.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index ebc169e42..67951d441 100644
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -26,8 +26,11 @@
 #include <vector>
 
 #include "options/bv_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h
index a49bdae2c..f9d633bbc 100644
--- a/src/preprocessing/passes/bv_abstraction.h
+++ b/src/preprocessing/passes/bv_abstraction.h
@@ -27,7 +27,6 @@
 #define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index 460ef2597..c521f736c 100644
--- a/src/preprocessing/passes/bv_eager_atoms.cpp
+++ b/src/preprocessing/passes/bv_eager_atoms.cpp
@@ -18,6 +18,9 @@
 
 #include "preprocessing/passes/bv_eager_atoms.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h
index 4c1bb136c..e0b063654 100644
--- a/src/preprocessing/passes/bv_eager_atoms.h
+++ b/src/preprocessing/passes/bv_eager_atoms.h
@@ -21,7 +21,6 @@
 #define CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 02a08b133..d8b309609 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -17,16 +17,17 @@
 
 #include "preprocessing/passes/bv_gauss.h"
 
+#include <unordered_map>
+#include <vector>
+
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
 
-#include <unordered_map>
-#include <vector>
-
-
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h
index 0b614251f..3b8197f9b 100644
--- a/src/preprocessing/passes/bv_gauss.h
+++ b/src/preprocessing/passes/bv_gauss.h
@@ -20,8 +20,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
 #define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
index 1e14e5b4b..573d36207 100644
--- a/src/preprocessing/passes/bv_intro_pow2.cpp
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -20,6 +20,8 @@
 
 #include <unordered_map>
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
 
diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h
index 92bdc2fc7..a270baa64 100644
--- a/src/preprocessing/passes/bv_intro_pow2.h
+++ b/src/preprocessing/passes/bv_intro_pow2.h
@@ -22,7 +22,6 @@
 #define CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index ac8b01d74..cf156692b 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -23,7 +23,10 @@
 
 #include "expr/node.h"
 #include "expr/node_visitor.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h
index 5054edfc4..a19116e77 100644
--- a/src/preprocessing/passes/bv_to_bool.h
+++ b/src/preprocessing/passes/bv_to_bool.h
@@ -19,9 +19,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
 #define CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 704214d06..5043718ca 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -18,6 +18,7 @@
 #include "preprocessing/passes/bv_to_int.h"
 
 #include <cmath>
+#include <sstream>
 #include <string>
 #include <unordered_map>
 #include <vector>
@@ -26,6 +27,8 @@
 #include "expr/node_traversal.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
@@ -34,6 +37,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index dd830d7cf..edcc84622 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -69,10 +69,8 @@
 #define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
 
 #include "context/cdhashmap.h"
-#include "context/cdo.h"
-#include "context/context.h"
+#include "context/cdhashset.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/arith/nl/iand_utils.h"
 
 namespace CVC4 {
@@ -104,7 +102,7 @@ class BVToInt : public PreprocessingPass
    * @return a node representing the shift.
    *
    */
-  Node createShiftNode(vector<Node> children,
+  Node createShiftNode(std::vector<Node> children,
                        uint64_t bvsize,
                        bool isLeftShift);
 
@@ -209,7 +207,7 @@ class BVToInt : public PreprocessingPass
    */
   Node reconstructNode(Node originalNode,
                        TypeNode resultType,
-                       const vector<Node>& translated_children);
+                       const std::vector<Node>& translated_children);
 
   /**
    * A useful utility function.
@@ -247,7 +245,7 @@ class BVToInt : public PreprocessingPass
    * that have children.
    */
   Node translateWithChildren(Node original,
-                             const vector<Node>& translated_children);
+                             const std::vector<Node>& translated_children);
 
   /**
    * Performs the actual translation to integers for nodes
diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index 95e107328..381e1b589 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -17,6 +17,8 @@
 #include "preprocessing/passes/extended_rewriter_pass.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h
index f4314a123..22b4d2da6 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.h
+++ b/src/preprocessing/passes/extended_rewriter_pass.h
@@ -20,7 +20,6 @@
 #define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
index c7bed4d31..6e898a3c2 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.cpp
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -17,6 +17,9 @@
 #include "preprocessing/passes/foreign_theory_rewrite.h"
 
 #include "expr/node_traversal.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h
index 2a882641e..aca3d0cfe 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.h
+++ b/src/preprocessing/passes/foreign_theory_rewrite.h
@@ -20,10 +20,8 @@
 #define CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
 
 #include "context/cdhashmap.h"
-#include "context/cdo.h"
-#include "context/context.h"
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -57,7 +55,7 @@ class ForeignTheoryRewrite : public PreprocessingPass
   /** construct a node with the same operator as originalNode whose children are
    * processedChildren
    */
-  static Node reconstructNode(Node originalNode, vector<Node> newChildren);
+  static Node reconstructNode(Node originalNode, std::vector<Node> newChildren);
   /** A cache to store the simplified nodes */
   CDNodeMap d_cache;
 };
diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 8c7a71021..1657aeafa 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -14,11 +14,16 @@
 
 #include "preprocessing/passes/fun_def_fmf.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "proof/proof_manager.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h
index 36d1166b7..d091d9db4 100644
--- a/src/preprocessing/passes/fun_def_fmf.h
+++ b/src/preprocessing/passes/fun_def_fmf.h
@@ -16,12 +16,11 @@
 #define CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H
 
 #include <map>
-#include <string>
 #include <vector>
 
+#include "context/cdlist.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 00ca1efd3..de7a7fb47 100644
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -17,6 +17,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 
 using namespace std;
diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
index af8ae5048..b59303870 100644
--- a/src/preprocessing/passes/global_negate.h
+++ b/src/preprocessing/passes/global_negate.h
@@ -25,8 +25,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
 #define CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 8cf4ad2ed..1f64e2e87 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h
index a1dc05b83..01683d2f5 100644
--- a/src/preprocessing/passes/ho_elim.h
+++ b/src/preprocessing/passes/ho_elim.h
@@ -19,8 +19,12 @@
 #ifndef __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H
 #define __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H
 
+#include <map>
+#include <unordered_map>
+#include <unordered_set>
+
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 5b0465772..2e237df2b 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -25,6 +25,7 @@
 #include "expr/node.h"
 #include "expr/node_traversal.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
@@ -32,6 +33,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h
index 208e7ab6a..a2085d6eb 100644
--- a/src/preprocessing/passes/int_to_bv.h
+++ b/src/preprocessing/passes/int_to_bv.h
@@ -22,7 +22,6 @@
 #define CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index f788338be..b82535804 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -18,6 +18,10 @@
 #include "preprocessing/passes/ite_removal.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "proof/proof_manager.h"
+#include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_preprocessor.h"
 
diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h
index 2b8a05fe4..a7ed87752 100644
--- a/src/preprocessing/passes/ite_removal.h
+++ b/src/preprocessing/passes/ite_removal.h
@@ -20,11 +20,7 @@
 #ifndef CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
 #define CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
 
-#include <unordered_set>
-#include <vector>
-
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 2a1f4c3e6..6ed149895 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -17,10 +17,15 @@
 #include <vector>
 
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/nary_builder.h"
 #include "theory/arith/arith_ite_utils.h"
+#include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
+using namespace std;
 using namespace CVC4;
 using namespace CVC4::theory;
 
diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h
index fe1dfa6e0..603e7889e 100644
--- a/src/preprocessing/passes/ite_simp.h
+++ b/src/preprocessing/passes/ite_simp.h
@@ -18,7 +18,7 @@
 #define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
+#include "preprocessing/util/ite_utilities.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 50dbc4a27..20a5fdbb0 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -15,14 +15,18 @@
 
 #include "preprocessing/passes/miplib_trick.h"
 
+#include <sstream>
 #include <vector>
 
 #include "expr/node_self_iterator.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/booleans/circuit_propagator.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 
@@ -30,6 +34,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 namespace {
diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h
index f7be87f18..99fd766ca 100644
--- a/src/preprocessing/passes/miplib_trick.h
+++ b/src/preprocessing/passes/miplib_trick.h
@@ -18,8 +18,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
 #define CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index 88bdf2e5c..553a85036 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -16,11 +16,14 @@
 
 #include "preprocessing/passes/nl_ext_purify.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 Node NlExtPurify::purifyNlTerms(TNode n,
diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h
index 5c7c5776e..df06dc22d 100644
--- a/src/preprocessing/passes/nl_ext_purify.h
+++ b/src/preprocessing/passes/nl_ext_purify.h
@@ -25,7 +25,6 @@
 
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 8cff66d72..6d6cfac41 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -20,7 +20,13 @@
 
 #include "context/cdo.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/preprocess_proof_generator.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/booleans/circuit_propagator.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 
@@ -289,7 +295,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       << "Resize non-clausal learned literals to " << j << std::endl;
   learned_literals.resize(j);
 
-  unordered_set<TNode, TNodeHashFunction> s;
+  std::unordered_set<TNode, TNodeHashFunction> s;
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     Node assertion = (*assertionsToPreprocess)[i];
diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h
index f94eb2d70..9539b6fd8 100644
--- a/src/preprocessing/passes/non_clausal_simp.h
+++ b/src/preprocessing/passes/non_clausal_simp.h
@@ -17,16 +17,23 @@
 #ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
 #define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
 
-#include <vector>
-
-#include "expr/lazy_proof.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "smt/preprocess_proof_generator.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class LazyCDProof;
+class ProofNodeManager;
+
+namespace smt {
+class PreprocessProofGenerator;
+}
+namespace theory {
+class TrustSubstitutionMap;
+}
+
 namespace preprocessing {
 namespace passes {
 
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index 2720d2f0b..a9396c570 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -18,6 +18,8 @@
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 
 #include "base/output.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 #include "theory/rewriter.h"
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h
index 03137dac5..b1338bb38 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.h
+++ b/src/preprocessing/passes/pseudo_boolean_processor.h
@@ -25,10 +25,8 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdo.h"
-#include "context/context.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/substitutions.h"
 #include "util/maybe.h"
 #include "util/rational.h"
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index ea73b7958..4e4d30649 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -20,6 +20,9 @@
 
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "proof/proof_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/arith/arith_msum.h"
@@ -29,6 +32,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4::theory;
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
index c5e557a9e..d5396be7d 100644
--- a/src/preprocessing/passes/quantifier_macros.h
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -18,12 +18,9 @@
 #define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
 
 #include <map>
-#include <string>
 #include <vector>
 #include "expr/node.h"
-#include "expr/type_node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp
index 6daafff2d..5caf37611 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.cpp
+++ b/src/preprocessing/passes/quantifiers_preprocess.cpp
@@ -20,6 +20,7 @@
 #include "preprocessing/passes/quantifiers_preprocess.h"
 
 #include "base/output.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/rewriter.h"
 
@@ -27,6 +28,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 QuantifiersPreprocess::QuantifiersPreprocess(PreprocessingPassContext* preprocContext)
diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h
index 43fce22b3..ad18a382c 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.h
+++ b/src/preprocessing/passes/quantifiers_preprocess.h
@@ -23,7 +23,6 @@
 #define CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 672e281d7..f7995c2d7 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -18,6 +18,8 @@
 
 #include <string>
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -26,6 +28,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq)
diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h
index 9fd8aca53..bab6f604c 100644
--- a/src/preprocessing/passes/real_to_int.h
+++ b/src/preprocessing/passes/real_to_int.h
@@ -19,12 +19,10 @@
 #ifndef CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
 #define CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
 
-#include <unordered_map>
 #include <vector>
 
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
index b8c9498e1..0684dde81 100644
--- a/src/preprocessing/passes/rewrite.cpp
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/rewrite.h"
 
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h
index 76493958a..73ce82873 100644
--- a/src/preprocessing/passes/rewrite.h
+++ b/src/preprocessing/passes/rewrite.h
@@ -20,7 +20,6 @@
 #define CVC4__PREPROCESSING__PASSES__REWRITE_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index ef2014b8a..20720668c 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -20,6 +20,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
@@ -28,6 +29,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 namespace {
diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h
index 912fd1b60..50ea641e2 100644
--- a/src/preprocessing/passes/sep_skolem_emp.h
+++ b/src/preprocessing/passes/sep_skolem_emp.h
@@ -19,7 +19,6 @@
 #define CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 918b13140..8e75acf9e 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -16,9 +16,13 @@
 
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/dump_manager.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 
diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h
index 1a18b6fd1..23a910780 100644
--- a/src/preprocessing/passes/sort_infer.h
+++ b/src/preprocessing/passes/sort_infer.h
@@ -15,13 +15,7 @@
 #ifndef CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
 #define CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
 
-#include <map>
-#include <string>
-#include <vector>
-
-#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index d48857396..26055f718 100644
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -18,7 +18,10 @@
 #include <string>
 
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h
index c86ebf90f..5c0ec816d 100644
--- a/src/preprocessing/passes/static_learning.h
+++ b/src/preprocessing/passes/static_learning.h
@@ -19,7 +19,6 @@
 #define CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp
index 69cb8914c..ddc7f4e21 100644
--- a/src/preprocessing/passes/strings_eager_pp.cpp
+++ b/src/preprocessing/passes/strings_eager_pp.cpp
@@ -14,8 +14,9 @@
 
 #include "preprocessing/passes/strings_eager_pp.h"
 
-#include "theory/strings/theory_strings_preprocess.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
+#include "theory/strings/theory_strings_preprocess.h"
 
 using namespace CVC4::theory;
 
diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h
index 299260c61..8679a6f70 100644
--- a/src/preprocessing/passes/strings_eager_pp.h
+++ b/src/preprocessing/passes/strings_eager_pp.h
@@ -18,7 +18,6 @@
 #define CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index caf63b0ec..933efbfde 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -14,6 +14,8 @@
 
 #include "preprocessing/passes/sygus_inference.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
@@ -21,6 +23,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_utils.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace std;
diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h
index 31d94efd2..4a67ae224 100644
--- a/src/preprocessing/passes/sygus_inference.h
+++ b/src/preprocessing/passes/sygus_inference.h
@@ -15,13 +15,10 @@
 #ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
 #define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
 
-#include <map>
-#include <string>
 #include <vector>
 #include "expr/node.h"
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 7b54fee61..b899b2de7 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -15,10 +15,13 @@
 
 #include "preprocessing/passes/synth_rew_rules.h"
 
+#include <sstream>
+
 #include "expr/sygus_datatype.h"
 #include "expr/term_canonize.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "printer/printer.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h
index 5613c1b22..3721f9457 100644
--- a/src/preprocessing/passes/synth_rew_rules.h
+++ b/src/preprocessing/passes/synth_rew_rules.h
@@ -17,7 +17,6 @@
 #define CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 22ae14762..04d761d2f 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -17,6 +17,10 @@
 #include "preprocessing/passes/theory_preprocess.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "proof/proof_manager.h"
+#include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
@@ -35,7 +39,7 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
   d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
   IteSkolemMap& imap = assertions->getIteSkolemMap();
-  PropEngine* propEngine = d_preprocContext->getPropEngine();
+  prop::PropEngine* propEngine = d_preprocContext->getPropEngine();
   // Remove all of the ITE occurrences and normalize
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h
index 49597828d..1635d4c3b 100644
--- a/src/preprocessing/passes/theory_preprocess.h
+++ b/src/preprocessing/passes/theory_preprocess.h
@@ -20,7 +20,6 @@
 #define CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 68de75194..95f70d0f6 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -14,6 +14,8 @@
 
 #include "preprocessing/passes/theory_rewrite_eq.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::theory;
diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h
index bc4027310..c15f5e36e 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.h
+++ b/src/preprocessing/passes/theory_rewrite_eq.h
@@ -17,8 +17,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H
 #define CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 6ebf1b8c8..e50548ff8 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -19,6 +19,9 @@
 #include "preprocessing/passes/unconstrained_simplifier.h"
 
 #include "expr/dtype.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
@@ -27,6 +30,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 UnconstrainedSimplifier::UnconstrainedSimplifier(
diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index ebfe51e79..b4d18a424 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -23,17 +23,16 @@
 
 #include <unordered_map>
 #include <unordered_set>
-#include <vector>
 
-#include "context/context.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/logic_info.h"
 #include "theory/substitutions.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace preprocessing {
 namespace passes {
 
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 169f10c9d..3eec24414 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -16,9 +16,13 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "printer/printer.h"
 #include "smt/dump.h"
+#include "smt/output_manager.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
-#include "printer/printer.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index b8ddb9846..3970ee8d3 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -33,14 +33,14 @@
 
 #include <string>
 
-#include "preprocessing/assertion_pipeline.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/logic_info.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace preprocessing {
 
+class AssertionPipeline;
+class PreprocessingPassContext;
+
 /**
  * Preprocessing passes return a result which indicates whether a conflict has
  * been detected during preprocessing.
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index c22a69255..2db213caf 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -21,18 +21,20 @@
 #ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 #define CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 
-#include "context/cdo.h"
-#include "context/context.h"
-#include "decision/decision_engine.h"
-#include "preprocessing/util/ite_utilities.h"
+#include "context/cdhashset.h"
 #include "smt/smt_engine.h"
-#include "smt/term_formula_removal.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/theory_engine.h"
 #include "theory/trust_substitutions.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
+class SmtEngine;
+class TheoryEngine;
+namespace theory::booleans {
+class CircuitPropagator;
+}
+namespace prop {
+class PropEngine;
+}
 namespace preprocessing {
 
 class PreprocessingPassContext
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index ce5c5da22..01bbab3a6 100644
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -19,15 +19,14 @@
 #ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
 #define CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
 
-#include <memory>
+#include <functional>
 #include <string>
 #include <unordered_map>
 
-#include "preprocessing/preprocessing_pass.h"
-
 namespace CVC4 {
 namespace preprocessing {
 
+class PreprocessingPass;
 class PreprocessingPassContext;
 
 /**
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 7e05af698..33d5cb826 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -21,6 +21,7 @@
 
 #include <utility>
 
+#include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/passes/rewrite.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index c82bf7958..fbe94302f 100644
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -27,16 +27,16 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "preprocessing/assertion_pipeline.h"
 #include "util/hash.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace preprocessing {
+
+class AssertionPipeline;
+
 namespace util {
 
-class IncomingArcCounter;
-class TermITEHeightCounter;
 class ITECompressor;
 class ITESimplifier;
 class ITECareSimplifier;
diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h
index 45a09d07f..1572ab014 100644
--- a/src/printer/let_binding.h
+++ b/src/printer/let_binding.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__PRINTER__LET_BINDING_H
 #define CVC4__PRINTER__LET_BINDING_H
 
-#include <map>
 #include <vector>
 
 #include "context/cdhashmap.h"
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 0a5ed1eac..dba29e524 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__PRINTER__PRINTER_H
 #define CVC4__PRINTER__PRINTER_H
 
-#include <map>
 #include <string>
 
 #include "expr/node.h"
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 286c4e0bf..acbfbb2a2 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -21,14 +21,12 @@
 #ifndef CVC4__CNF_PROOF_H
 #define CVC4__CNF_PROOF_H
 
-#include <iosfwd>
 #include <unordered_map>
 #include <unordered_set>
 
 #include "context/cdhashmap.h"
 #include "proof/clause_id.h"
-#include "proof/sat_proof.h"
-#include "util/maybe.h"
+#include "proof/proof_manager.h"
 
 namespace CVC4 {
 namespace prop {
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c7eb2282b..f05fb0386 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__PROOF_MANAGER_H
 #define CVC4__PROOF_MANAGER_H
 
-#include <iosfwd>
 #include <memory>
 #include <unordered_map>
 #include <unordered_set>
@@ -28,7 +27,6 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "proof/clause_id.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 9907b8d72..c76878da4 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -21,13 +21,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BVMinisat_SimpSolver_h
 #define BVMinisat_SimpSolver_h
 
-#include "context/context.h"
 #include "proof/clause_id.h"
 #include "prop/bvminisat/core/Solver.h"
 #include "prop/bvminisat/mtl/Queue.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+namespace context {
+class Context;
+}
+
 namespace BVMinisat {
 
 //=================================================================================================
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 69cbb0241..92bdd66ee 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -32,7 +32,7 @@
 #include "proof/proof_manager.h"
 #include "prop/proof_cnf_stream.h"
 #include "prop/registrar.h"
-#include "prop/theory_proxy.h"
+#include "prop/sat_solver_types.h"
 
 namespace CVC4 {
 
@@ -41,6 +41,8 @@ class OutputManager;
 namespace prop {
 
 class ProofCnfStream;
+class PropEngine;
+class SatSolver;
 
 /** A policy for how literals for formulas are handled in cnf_stream */
 enum class FormulaLitPolicy : uint32_t
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 8fa489f65..f685017a7 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -36,6 +36,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/utils/Options.h"
 #include "prop/sat_proof_manager.h"
 #include "theory/theory.h"
+#include "util/resource_manager.h"
 
 namespace CVC4 {
 template <class Solver> class TSatProof;
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 738b4dc9c..473449179 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -32,6 +32,7 @@
 #include "proof/proof_manager.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
+#include "prop/prop_proof_manager.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
@@ -83,7 +84,7 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_resourceManager(rm),
       d_outMgr(outMgr)
 {
-  Debug("prop") << "Constructing the PropEngine" << endl;
+  Debug("prop") << "Constructing the PropEngine" << std::endl;
 
   d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
   d_decisionEngine->init();  // enable appropriate strategies
@@ -146,7 +147,7 @@ void PropEngine::finishInit()
 }
 
 PropEngine::~PropEngine() {
-  Debug("prop") << "Destructing the PropEngine" << endl;
+  Debug("prop") << "Destructing the PropEngine" << std::endl;
   d_decisionEngine->shutdown();
   d_decisionEngine.reset(nullptr);
   delete d_cnfStream;
@@ -179,7 +180,7 @@ void PropEngine::notifyPreprocessedAssertions(
 
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
-  Debug("prop") << "assertFormula(" << node << ")" << endl;
+  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
   d_decisionEngine->addAssertion(node);
   assertInternal(node, false, false, true);
 }
@@ -187,7 +188,7 @@ void PropEngine::assertFormula(TNode node) {
 void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
-  Debug("prop") << "assertFormula(" << node << ")" << endl;
+  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
   d_decisionEngine->addSkolemDefinition(node, skolem);
   assertInternal(node, false, false, true);
 }
@@ -235,7 +236,7 @@ void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
                                             bool removable)
 {
   Node node = trn.getNode();
-  Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
+  Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
   bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
   Assert(!isProofEnabled() || trn.getGenerator() != nullptr);
   assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
@@ -292,7 +293,7 @@ void PropEngine::assertLemmasInternal(
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
-  Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl;
+  Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << std::endl;
 
   Assert(n.getType().isBoolean());
   SatLiteral lit = d_cnfStream->getLiteral(n);
@@ -307,26 +308,26 @@ bool PropEngine::isDecision(Node lit) const {
 void PropEngine::printSatisfyingAssignment(){
   const CnfStream::NodeToLiteralMap& transCache =
     d_cnfStream->getTranslationCache();
-  Debug("prop-value") << "Literal | Value | Expr" << endl
+  Debug("prop-value") << "Literal | Value | Expr" << std::endl
                       << "----------------------------------------"
-                      << "-----------------" << endl;
+                      << "-----------------" << std::endl;
   for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(),
       end = transCache.end();
       i != end;
       ++i) {
-    pair<Node, SatLiteral> curr = *i;
+    std::pair<Node, SatLiteral> curr = *i;
     SatLiteral l = curr.second;
     if(!l.isNegated()) {
       Node n = curr.first;
       SatValue value = d_satSolver->modelValue(l);
-      Debug("prop-value") << "'" << l << "' " << value << " " << n << endl;
+      Debug("prop-value") << "'" << l << "' " << value << " " << n << std::endl;
     }
   }
 }
 
 Result PropEngine::checkSat() {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
-  Debug("prop") << "PropEngine::checkSat()" << endl;
+  Debug("prop") << "PropEngine::checkSat()" << std::endl;
 
   // Mark that we are in the checkSat
   ScopedBool scopedBool(d_inCheckSat);
@@ -360,7 +361,7 @@ Result PropEngine::checkSat() {
     printSatisfyingAssignment();
   }
 
-  Debug("prop") << "PropEngine::checkSat() => " << result << endl;
+  Debug("prop") << "PropEngine::checkSat() => " << result << std::endl;
   if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) {
     return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
   }
@@ -491,20 +492,20 @@ void PropEngine::push()
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   d_satSolver->push();
-  Debug("prop") << "push()" << endl;
+  Debug("prop") << "push()" << std::endl;
 }
 
 void PropEngine::pop()
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   d_satSolver->pop();
-  Debug("prop") << "pop()" << endl;
+  Debug("prop") << "pop()" << std::endl;
 }
 
 void PropEngine::resetTrail()
 {
   d_satSolver->resetTrail();
-  Debug("prop") << "resetTrail()" << endl;
+  Debug("prop") << "resetTrail()" << std::endl;
 }
 
 unsigned PropEngine::getAssertionLevel() const
@@ -522,7 +523,7 @@ void PropEngine::interrupt()
 
   d_interrupted = true;
   d_satSolver->interrupt();
-  Debug("prop") << "interrupt()" << endl;
+  Debug("prop") << "interrupt()" << std::endl;
 }
 
 void PropEngine::spendResource(ResourceManager::Resource r)
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d0c75a924..834f35d90 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -21,22 +21,11 @@
 #ifndef CVC4__PROP_ENGINE_H
 #define CVC4__PROP_ENGINE_H
 
-#include <sys/time.h>
-
-#include "base/modal_exception.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
-#include "options/options.h"
-#include "proof/proof_manager.h"
-#include "prop/minisat/core/Solver.h"
-#include "prop/minisat/minisat.h"
-#include "prop/proof_cnf_stream.h"
-#include "prop/prop_proof_manager.h"
-#include "prop/sat_solver_types.h"
+#include "theory/output_channel.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"
 
 namespace CVC4 {
 
@@ -45,16 +34,12 @@ class DecisionEngine;
 class OutputManager;
 class TheoryEngine;
 
-namespace theory {
-  class TheoryRegistrar;
-}/* CVC4::theory namespace */
-
 namespace prop {
 
 class CnfStream;
 class CDCLTSatSolverInterface;
-
-class PropEngine;
+class ProofCnfStream;
+class PropPfManager;
 
 /**
  * PropEngine is the abstraction of a Sat Solver, providing methods for
diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index 3c18dc896..c19d09bb9 100644
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -16,6 +16,8 @@
 
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
+#include "prop/prop_proof_manager.h"
+#include "prop/sat_solver.h"
 
 namespace CVC4 {
 namespace prop {
diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h
index fc0151bcd..2e0d997df 100644
--- a/src/prop/prop_proof_manager.h
+++ b/src/prop/prop_proof_manager.h
@@ -27,6 +27,8 @@ namespace CVC4 {
 
 namespace prop {
 
+class CDCLTSatSolverInterface;
+
 /**
  * This class is responsible for managing the proof output of PropEngine, both
  * building and checking it.
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index 0555e7ba7..e05923268 100644
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -21,10 +21,7 @@
 #include "expr/buffered_proof_generator.h"
 #include "expr/lazy_proof_chain.h"
 #include "expr/node.h"
-#include "expr/proof.h"
-#include "expr/proof_node_manager.h"
 #include "prop/minisat/core/SolverTypes.h"
-#include "prop/cnf_stream.h"
 #include "prop/sat_solver_types.h"
 
 namespace Minisat {
@@ -32,8 +29,13 @@ class Solver;
 }
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
 namespace prop {
 
+class CnfStream;
+
 /**
  * This class is responsible for managing the proof production of the SAT
  * solver. It tracks resolutions produced during solving and stores them,
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index ac79cf967..049232868 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -23,19 +23,16 @@
 // Optional blocks below will be unconditionally included
 #define CVC4_USE_MINISAT
 
-#include <iosfwd>
 #include <unordered_set>
 
-#include "context/cdhashmap.h"
 #include "context/cdqueue.h"
 #include "expr/node.h"
 #include "prop/registrar.h"
-#include "prop/sat_solver.h"
+#include "prop/sat_solver_types.h"
 #include "theory/theory.h"
 #include "theory/theory_preprocessor.h"
 #include "theory/trust_node.h"
 #include "util/resource_manager.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 3f03c00e2..6a326ed2e 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/abduction_solver.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 6776b06e2..5c1e1b879 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -19,6 +19,7 @@
 #include "options/language.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
+#include "smt/abstract_values.h"
 #include "smt/smt_engine.h"
 
 using namespace CVC4::theory;
diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index 5ce2556a7..bba4d2e29 100644
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -20,14 +20,14 @@
 #include <vector>
 
 #include "context/cdlist.h"
-#include "context/context.h"
 #include "expr/node.h"
 #include "preprocessing/assertion_pipeline.h"
-#include "smt/abstract_values.h"
 
 namespace CVC4 {
 namespace smt {
 
+class AbstractValues;
+
 /**
  * Contains all information pertaining to the assertions of an SMT engine.
  *
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 310201f47..b211c61c2 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -15,8 +15,10 @@
 #include "smt/check_models.h"
 
 #include "options/smt_options.h"
+#include "smt/model.h"
 #include "smt/node_command.h"
 #include "smt/preprocessor.h"
+#include "smt/smt_solver.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory_engine.h"
diff --git a/src/smt/check_models.h b/src/smt/check_models.h
index 14af41b27..f9d527867 100644
--- a/src/smt/check_models.h
+++ b/src/smt/check_models.h
@@ -19,12 +19,13 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "smt/model.h"
-#include "smt/smt_solver.h"
 
 namespace CVC4 {
 namespace smt {
 
+class Model;
+class SmtSolver;
+
 /**
  * This utility is responsible for checking the current model.
  */
diff --git a/src/smt/command.h b/src/smt/command.h
index c11012944..a2230e12a 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -23,7 +23,6 @@
 #define CVC4__COMMAND_H
 
 #include <iosfwd>
-#include <map>
 #include <sstream>
 #include <string>
 #include <vector>
@@ -40,8 +39,6 @@ class Term;
 }  // namespace api
 
 class SymbolManager;
-class UnsatCore;
-class SmtEngine;
 class Command;
 class CommandStatus;
 
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 192bb2324..c7a05e21b 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -20,13 +20,17 @@
 #include <memory>
 #include <vector>
 
-#include "context/cdlist.h"
+#include "context/context.h"
 #include "expr/node.h"
 
 namespace CVC4 {
 
 class NodeCommand;
 
+namespace context {
+class UserContext;
+}
+
 namespace smt {
 
 /**
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index c2c4b6fd2..c01b5a243 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -18,8 +18,10 @@
 #include <utility>
 
 #include "expr/node_manager_attributes.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "smt/defined_function.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::preprocessing;
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index 486aa0c3a..0c2f9b2d5 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -20,17 +20,23 @@
 #include <unordered_map>
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
-#include "preprocessing/assertion_pipeline.h"
-#include "smt/smt_engine_stats.h"
-#include "util/resource_manager.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+class ResourceManager;
 class SmtEngine;
+class TConvProofGenerator;
+
+namespace preprocessing {
+class AssertionPipeline;
+}
 
 namespace smt {
 
+struct SmtEngineStatistics;
+
 /**
  * Module in charge of expanding definitions for an SMT engine.
  *
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 09ddfde75..965f49855 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/interpolation_solver.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index d4cf33554..2482f77ef 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -22,11 +22,10 @@
 
 #include <ostream>
 
-#include "options/open_ostream.h"
-#include "smt/update_ostream.h"
-
 namespace CVC4 {
 
+class OstreamOpener;
+
 /** This abstracts the management of ostream memory and initialization. */
 class ManagedOstream {
  public:
diff --git a/src/smt/model.h b/src/smt/model.h
index e7c2434a6..277803499 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -21,13 +21,15 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/theory_model.h"
-#include "util/cardinality.h"
 
 namespace CVC4 {
 
 class SmtEngine;
 
+namespace theory {
+class TheoryModel;
+}
+
 namespace smt {
 
 class Model;
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index cabd7bd20..95c9f1d18 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -18,6 +18,8 @@
 #include "expr/node.h"
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 5c45a6a56..6c453987e 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -21,10 +21,13 @@
 
 #include "expr/node.h"
 #include "options/smt_options.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
 
+namespace theory {
+class TheoryModel;
+}
+
 /**
  * A utility for blocking the current model.
  */
diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index 33b5d9953..3fc3a2e0c 100644
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -16,6 +16,8 @@
 
 #include "smt/node_command.h"
 
+#include <sstream>
+
 #include "printer/printer.h"
 
 namespace CVC4 {
diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
index 983b98b34..81b935f36 100644
--- a/src/smt/options_manager.h
+++ b/src/smt/options_manager.h
@@ -15,15 +15,15 @@
 #ifndef CVC4__SMT__OPTIONS_MANAGER_H
 #define CVC4__SMT__OPTIONS_MANAGER_H
 
-#include "options/options.h"
 #include "options/options_listener.h"
 #include "smt/managed_ostreams.h"
 
 namespace CVC4 {
 
-class SmtEngine;
 class LogicInfo;
+class Options;
 class ResourceManager;
+class SmtEngine;
 
 namespace smt {
 
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index ef80ebdae..261450dbb 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -16,6 +16,8 @@
 #include "smt/preprocess_proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
 #include "options/proof_options.h"
 #include "theory/rewriter.h"
 
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 01d9c89da..312e58453 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -20,12 +20,10 @@
 #include <map>
 
 #include "context/cdhashmap.h"
-#include "context/cdlist.h"
 #include "expr/lazy_proof.h"
 #include "expr/proof_set.h"
 #include "expr/proof_generator.h"
 #include "expr/proof_node_manager.h"
-#include "theory/eager_proof_generator.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 3e4ef0cdd..e5e9b98f4 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -19,8 +19,10 @@
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/dump.h"
+#include "smt/preprocess_proof_generator.h"
 #include "smt/smt_engine.h"
 
+using namespace std;
 using namespace CVC4::theory;
 using namespace CVC4::kind;
 
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 22b585e05..ece5fb5a8 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -17,14 +17,16 @@
 #ifndef CVC4__SMT__PREPROCESSOR_H
 #define CVC4__SMT__PREPROCESSOR_H
 
-#include <vector>
+#include <memory>
 
-#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/expand_definitions.h"
 #include "smt/process_assertions.h"
 #include "theory/booleans/circuit_propagator.h"
 
 namespace CVC4 {
+namespace preprocessing {
+class PreprocessingPassContext;
+}
 namespace smt {
 
 class AbstractValues;
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 0c01abbbb..23890d9fc 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -31,10 +31,13 @@
 #include "printer/printer.h"
 #include "smt/defined_function.h"
 #include "smt/dump.h"
+#include "smt/expand_definitions.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 
+using namespace std;
 using namespace CVC4::preprocessing;
 using namespace CVC4::theory;
 using namespace CVC4::kind;
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index ca834459d..891ef93f1 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -17,17 +17,14 @@
 #ifndef CVC4__SMT__PROCESS_ASSERTIONS_H
 #define CVC4__SMT__PROCESS_ASSERTIONS_H
 
-#include <map>
+#include <unordered_map>
 
-#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/assertions.h"
-#include "smt/expand_definitions.h"
-#include "smt/smt_engine_stats.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
@@ -36,6 +33,9 @@ class SmtEngine;
 
 namespace smt {
 
+class ExpandDefs;
+struct SmtEngineStatistics;
+
 /**
  * Module in charge of processing assertions for an SMT engine.
  *
@@ -54,7 +54,7 @@ class ProcessAssertions
 {
   /** The types for the recursive function definitions */
   typedef context::CDList<Node> NodeList;
-  typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+  typedef std::unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
  public:
   ProcessAssertions(SmtEngine& smt,
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index cb7943aed..2f7683e7c 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -14,11 +14,15 @@
 
 #include "smt/proof_manager.h"
 
+#include "expr/proof_checker.h"
 #include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/base_options.h"
 #include "options/proof_options.h"
 #include "smt/assertions.h"
 #include "smt/defined_function.h"
+#include "smt/preprocess_proof_generator.h"
+#include "smt/proof_post_processor.h"
 
 namespace CVC4 {
 namespace smt {
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index a6f284cad..abb984ea9 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -18,22 +18,21 @@
 #define CVC4__SMT__PROOF_MANAGER_H
 
 #include "context/cdhashmap.h"
-#include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
-#include "smt/preprocess_proof_generator.h"
-#include "smt/proof_post_processor.h"
 
 namespace CVC4 {
 
+class ProofChecker;
+class ProofNode;
+class ProofNodeManager;
 class SmtEngine;
 
 namespace smt {
 
 class Assertions;
 class DefinedFunction;
+class PreprocessProofGenerator;
+class ProofPostproccess;
 
 /**
  * This class is responsible for managing the proof output of SmtEngine, as
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 0898096f5..f7811911b 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/proof_post_processor.h"
 
+#include "expr/proof_node_manager.h"
 #include "expr/skolem_manager.h"
 #include "options/proof_options.h"
 #include "options/smt_options.h"
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index de74d4869..b3e636b58 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -22,6 +22,7 @@
 
 #include "expr/proof_node_updater.h"
 #include "smt/witness_form.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 80d7b96fa..891349809 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -34,11 +34,13 @@
 #include "printer/printer.h"
 #include "proof/proof_manager.h"
 #include "proof/unsat_core.h"
+#include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/check_models.h"
 #include "smt/defined_function.h"
+#include "smt/dump.h"
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8974e5e60..50e45c52f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -887,8 +887,6 @@ class CVC4_PUBLIC SmtEngine
   /* .......................................................................  */
  private:
   /* .......................................................................  */
-  /** The type of our internal assertion list */
-  typedef context::CDList<Node> AssertionList;
 
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) = delete;
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 996a51e90..9b5871139 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -20,9 +20,12 @@
 #include "smt/preprocessor.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_state.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_traits.h"
 
+using namespace std;
+
 namespace CVC4 {
 namespace smt {
 
@@ -67,12 +70,12 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
-                                    d_smt.getContext(),
-                                    d_smt.getUserContext(),
-                                    d_rm,
-                                    d_smt.getOutputManager(),
-                                    d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
+                                          d_smt.getContext(),
+                                          d_smt.getUserContext(),
+                                          d_rm,
+                                          d_smt.getOutputManager(),
+                                          d_pnm));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -88,12 +91,12 @@ void SmtSolver::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
-                                    d_smt.getContext(),
-                                    d_smt.getUserContext(),
-                                    d_rm,
-                                    d_smt.getOutputManager(),
-                                    d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
+                                          d_smt.getContext(),
+                                          d_smt.getUserContext(),
+                                          d_rm,
+                                          d_smt.getOutputManager(),
+                                          d_pnm));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 5f08efb14..133d1e692 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -18,8 +18,11 @@
 #include <vector>
 
 #include "expr/attribute.h"
+#include "expr/lazy_proof.h"
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
+#include "expr/term_context_stack.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 803021fc3..c2a88d718 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -18,22 +18,22 @@
 
 #pragma once
 
-#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "context/cdinsert_hashmap.h"
 #include "context/context.h"
-#include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/term_context_stack.h"
-#include "expr/term_conversion_proof_generator.h"
-#include "theory/eager_proof_generator.h"
+#include "expr/term_context.h"
 #include "theory/trust_node.h"
-#include "util/bool.h"
 #include "util/hash.h"
 
 namespace CVC4 {
 
+class LazyCDProof;
+class ProofNodeManager;
+class TConvProofGenerator;
+
 class RemoveTermFormulas {
  public:
   RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index f5a9a2a75..8107136c3 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -18,6 +18,8 @@
 
 #include "theory/arith/delta_rational.h"
 
+#include <sstream>
+
 using namespace std;
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 6487b48ec..5e34aebc7 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -22,6 +22,7 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 #include "util/iand.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index bc4e0c8ae..01b834482 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/booleans/proof_circuit_propagator.h"
 
+#include <sstream>
+
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index d71fae8d0..a1763d081 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -31,6 +31,7 @@
 #include "prop/sat_solver_types.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
+#include "theory/theory.h"
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 4eec45e4b..94f74a638 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -21,6 +21,7 @@
 
 #include <unordered_map>
 
+#include "context/cdqueue.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "theory/bv/bitblast/simple_bitblaster.h"
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 6169d3752..e11f773a3 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/datatypes/sygus_datatype_utils.h"
 
+#include <sstream>
+
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9105cdfd6..97600f76f 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -16,6 +16,7 @@
 #include "theory/datatypes/theory_datatypes.h"
 
 #include <map>
+#include <sstream>
 
 #include "base/check.h"
 #include "expr/dtype.h"
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index fda694e3d..94f90bc46 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/inference_id.h"
 
+#include <iostream>
+
 namespace CVC4 {
 namespace theory {
 
diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/theory/lazy_tree_proof_generator.cpp
index 126ce60b9..b6155f19e 100644
--- a/src/theory/lazy_tree_proof_generator.cpp
+++ b/src/theory/lazy_tree_proof_generator.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/node.h"
 #include "expr/proof_generator.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index f1307f142..842ef59bf 100644
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -14,6 +14,8 @@
  **/
 #include "theory/quantifiers/single_inv_partition.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index cdc43658d..69adc9a4b 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -18,11 +18,12 @@
 #define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
 
 #include <unordered_set>
+
 #include "expr/node.h"
 #include "expr/node_trie.h"
-
 #include "theory/evaluator.h"
 #include "theory/quantifiers/sygus/cegis.h"
+#include "util/result.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 67f02b558..e56312362 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/quantifiers/sygus/sygus_abduct.h"
 
+#include <sstream>
+
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 3edec96c7..9f8ac0e3c 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/quantifiers/sygus/sygus_interpol.h"
 
+#include <sstream>
+
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/smt_options.h"
diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp
index ca87e1049..d793fb718 100644
--- a/src/theory/quantifiers/sygus/sygus_utils.cpp
+++ b/src/theory/quantifiers/sygus/sygus_utils.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/quantifiers/sygus/sygus_utils.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 275e9a27f..a5be5871f 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index a72054f6d..c835369b7 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/lazy_trie.h"
+#include "theory/rewriter.h"
 #include "util/bitvector.h"
 #include "util/random.h"
 #include "util/sampler.h"
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 24d2e00bd..21480e8ec 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/strings/regexp_operation.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index b807fe1b3..4338d38c4 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/strings/theory_strings_utils.h"
 
+#include <sstream>
+
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e49ca8b05..07b23525e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/theory_engine.h"
 
+#include <sstream>
+
 #include "base/map_util.h"
 #include "decision/decision_engine.h"
 #include "expr/attribute.h"
diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp
index 2ba0a49ff..1eb191fd7 100644
--- a/src/theory/theory_engine_proof_generator.cpp
+++ b/src/theory/theory_engine_proof_generator.cpp
@@ -14,6 +14,10 @@
 
 #include "theory/theory_engine_proof_generator.h"
 
+#include <sstream>
+
+#include "expr/proof_node.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index e9111db8c..5859b5c99 100644
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -17,6 +17,8 @@
 
 #include "theory/theory_id.h"
 
+#include <sstream>
+
 #include "base/check.h"
 #include "lib/ffs.h"
 
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 94402e2d9..d2fc4cf9e 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/uf/cardinality_extension.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "theory/quantifiers/term_database.h"
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 58d5f4924..7a164c196 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -17,6 +17,7 @@
 
 #include "base/configuration.h"
 #include "expr/proof.h"
+#include "expr/proof_checker.h"
 #include "options/uf_options.h"
 
 namespace CVC4 {
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index db8b89d89..e6e809533 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -18,6 +18,7 @@
 #include "theory/uf/theory_uf.h"
 
 #include <memory>
+#include <sstream>
 
 #include "expr/node_algorithm.h"
 #include "expr/proof_node_manager.h"
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index b1a27929a..a5ef3a607 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -20,7 +20,9 @@
 #define CVC4__BITVECTOR_H
 
 #include <iosfwd>
+#include <iostream>
 
+#include "base/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index f78b076de..bf3a8ef2b 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -17,6 +17,7 @@
 #include "util/cardinality.h"
 
 #include <ostream>
+#include <sstream>
 
 #include "base/check.h"
 #include "base/exception.h"
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index fe05dc982..cca141094 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -20,13 +20,11 @@
 #ifndef CVC4__INTEGER_H
 #define CVC4__INTEGER_H
 
+#include <gmpxx.h>
+
 #include <iosfwd>
-#include <limits>
 #include <string>
 
-#include "base/exception.h"
-#include "util/gmp_util.h"
-
 namespace CVC4 {
 
 class Rational;
diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp
index ad769b779..2e2f200a3 100644
--- a/src/util/poly_util.cpp
+++ b/src/util/poly_util.cpp
@@ -27,6 +27,7 @@
 #include <poly/polyxx.h>
 
 #include <map>
+#include <sstream>
 
 #include "base/check.h"
 #include "maybe.h"
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index f166d9cdc..f6c9a1e44 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -24,7 +24,7 @@
 
 #include <string>
 
-#include "base/exception.h"
+#include "util/gmp_util.h"
 #include "util/integer.h"
 #include "util/maybe.h"
 
diff --git a/src/util/result.cpp b/src/util/result.cpp
index f4e4d13c7..09445fa3b 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -18,6 +18,7 @@
 #include <algorithm>
 #include <cctype>
 #include <iostream>
+#include <sstream>
 #include <string>
 
 #include "base/check.h"
diff --git a/src/util/result.h b/src/util/result.h
index 96fe919d0..d0b0896bc 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -19,10 +19,9 @@
 #ifndef CVC4__RESULT_H
 #define CVC4__RESULT_H
 
-#include <iostream>
+#include <iosfwd>
 #include <string>
 
-#include "base/exception.h"
 #include "options/language.h"
 
 namespace CVC4 {
diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp
index f45849736..aa2918cde 100644
--- a/src/util/safe_print.cpp
+++ b/src/util/safe_print.cpp
@@ -20,8 +20,11 @@
 
 #include "safe_print.h"
 
+#include <time.h>
 #include <unistd.h>
 
+#include <cstdlib>
+
 /* Size of buffers used */
 #define BUFFER_SIZE 20
 
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index 6f72569bb..b98b4f3e9 100644
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -40,10 +40,7 @@
 #include <unistd.h>
 
 #include <cstring>
-#include <type_traits>
-
-#include "lib/clock_gettime.h"
-#include "util/result.h"
+#include <string>
 
 namespace CVC4 {
 
diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp
index 20dfb92a7..8b1a2c3db 100644
--- a/src/util/sampler.cpp
+++ b/src/util/sampler.cpp
@@ -17,8 +17,11 @@
 
 #include "util/sampler.h"
 
+#include <sstream>
+
 #include "base/check.h"
 #include "util/bitvector.h"
+#include "util/random.h"
 
 namespace CVC4 {
 
diff --git a/src/util/sampler.h b/src/util/sampler.h
index 8968f5dc7..dad6605a5 100644
--- a/src/util/sampler.h
+++ b/src/util/sampler.h
@@ -21,7 +21,6 @@
 #define CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
 
 #include "util/floatingpoint.h"
-#include "util/random.h"
 
 namespace CVC4 {
 
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 3bcf36abf..5c47fa4fd 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -26,12 +26,10 @@
 #ifndef CVC4__SEXPR_H
 #define CVC4__SEXPR_H
 
-#include <iomanip>
 #include <iosfwd>
 #include <string>
 #include <vector>
 
-#include "base/exception.h"
 #include "options/language.h"
 #include "util/integer.h"
 #include "util/rational.h"
diff --git a/src/util/string.h b/src/util/string.h
index 9e503bb07..f908c2f0f 100644
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -17,10 +17,10 @@
 #ifndef CVC4__UTIL__STRING_H
 #define CVC4__UTIL__STRING_H
 
-#include <functional>
-#include <ostream>
+#include <iosfwd>
 #include <string>
 #include <vector>
+
 #include "util/rational.h"
 
 namespace CVC4 {
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 1a3412186..5e2e80e4a 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -20,6 +20,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/passes/bv_gauss.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp
index 569c8a0e1..ceaf69423 100644
--- a/test/unit/prop/cnf_stream_white.cpp
+++ b/test/unit/prop/cnf_stream_white.cpp
@@ -19,6 +19,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/registrar.h"
+#include "prop/sat_solver.h"
 #include "prop/theory_proxy.h"
 #include "test_smt.h"
 #include "theory/arith/theory_arith.h"
diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp
index 832965836..c5ffe0b87 100644
--- a/test/unit/util/cardinality_black.cpp
+++ b/test/unit/util/cardinality_black.cpp
@@ -17,6 +17,7 @@
 #include <sstream>
 #include <string>
 
+#include "base/exception.h"
 #include "test.h"
 #include "util/cardinality.h"
 #include "util/integer.h"
diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp
index 41497a7a4..f447246e2 100644
--- a/test/unit/util/integer_black.cpp
+++ b/test/unit/util/integer_black.cpp
@@ -17,6 +17,7 @@
 #include <limits>
 #include <sstream>
 
+#include "base/exception.h"
 #include "test.h"
 #include "util/integer.h"