Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

68 files changed, 168 insertions, 90 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 152146cdf..80690f39c 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -28,6 +28,7 @@
 #include "theory/arith/cut_log.h"
 #include "theory/arith/matrix.h"
 #include "theory/arith/normal_form.h"
+#include "theory/eager_proof_generator.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 58e115b81..46e252ec7 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -66,7 +66,6 @@ class NodeLog;
 class TreeLog;
 class ArithVariables;
 class CutInfo;
-class RowsDeleted;
 
 class ApproximateSimplex{
  public:
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 0c1923448..a075c87fe 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/arith/arith_preprocess.h"
 
+#include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/skolem_lemma.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 69cc02bb9..db0fd7d5e 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -18,16 +18,19 @@
 #define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
 
 #include "context/cdhashmap.h"
-#include "theory/arith/arith_state.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/logic_info.h"
-#include "theory/skolem_lemma.h"
 
 namespace CVC4 {
 namespace theory {
+
+class SkolemLemma;
+
 namespace arith {
 
+class ArithState;
+class InferenceManager;
+
 /**
  * This module can be used for (on demand) elimination of extended arithmetic
  * operators like div, mod, to_int, is_int, sqrt, and so on. It uses the
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 2b74e6005..799d0bcee 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -20,14 +20,15 @@
 #ifndef CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 #define CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 
-#include <set>
-
 #include "context/cdhashmap.h"
-#include "context/context.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/delta_rational.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index f9051328c..4f1f50b7a 100644
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -14,6 +14,8 @@
 
 #include "arith_utilities.h"
 
+#include <cmath>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -114,7 +116,7 @@ Node getApproximateConstant(Node c, bool isLower, unsigned prec)
   Rational cr = c.getConst<Rational>();
 
   unsigned lower = 0;
-  unsigned upper = pow(10, prec);
+  unsigned upper = std::pow(10, prec);
 
   Rational den = Rational(upper);
   if (cr.getDenominator() < den.getNumerator())
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index e4d6bd0ee..40ca7b8f6 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 #define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
-#include <math.h>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
@@ -25,7 +24,6 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
 #include "util/dense_map.h"
 #include "util/integer.h"
 #include "util/rational.h"
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index efcb96325..e5c995971 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -21,6 +21,8 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
+#include "theory/arith/tableau.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 84bfafcc8..ee412483b 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/arith/callbacks.h"
 
+#include "expr/proof_node.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/arith/theory_arith_private.h"
 
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 9fbe3b90f..574d289b0 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -18,13 +18,15 @@
 #pragma once
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/constraint_forward.h"
 #include "util/rational.h"
 
 namespace CVC4 {
+
+class ProofNode;
+
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 636cebe5f..f2210574b 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -18,9 +18,16 @@
 #include "theory/arith/congruence_manager.h"
 
 #include "base/output.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/partial_model.h"
+#include "theory/ee_setup_info.h"
+#include "theory/rewriter.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
 #include "options/arith_options.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index f2aef815f..9815ad9c8 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -19,27 +19,42 @@
 
 #pragma once
 
+#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "context/cdmaybe.h"
-#include "context/cdo.h"
 #include "context/cdtrail_queue.h"
-#include "context/context.h"
-#include "expr/proof_node_manager.h"
 #include "theory/arith/arithvar.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/callbacks.h"
 #include "theory/arith/constraint_forward.h"
-#include "theory/arith/partial_model.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/ee_setup_info.h"
 #include "theory/trust_node.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/proof_equality_engine.h"
+#include "theory/uf/equality_engine_notify.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
+namespace context {
+class Context;
+class UserContext;
+}
+
 namespace theory {
+
+class EagerProofGenerator;
+struct EeSetupInfo;
+
+namespace eq {
+class ProofEqEngine;
+class EqualityEngine;
+}
+
 namespace arith {
 
+class ArithVariables;
+
 class ArithCongruenceManager {
 private:
   context::CDRaised d_inConflict;
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 70106b14c..bafd4d682 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -21,9 +21,14 @@
 #include <unordered_set>
 
 #include "base/output.h"
+#include "expr/proof_node_manager.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/congruence_manager.h"
 #include "theory/arith/normal_form.h"
+#include "theory/arith/partial_model.h"
+#include "theory/rewriter.h"
 
 
 using namespace std;
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 6a73d69d2..6ac03bb82 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -78,36 +78,38 @@
 #ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
 #define CVC4__THEORY__ARITH__CONSTRAINT_H
 
-#include <list>
-#include <set>
 #include <unordered_map>
 #include <vector>
 
 #include "base/configuration_private.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "expr/node.h"
-#include "expr/proof_node_manager.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/callbacks.h"
-#include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/trust_node.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
-namespace theory {
-namespace arith {
-class Comparison;
-}
-}
+
+class ProofNodeManager;
+
+namespace context {
+class Context;
 }
-namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace arith {
 
+class Comparison;
+class ArithCongruenceManager;
+class ArithVariables;
+
 /**
  * Logs the types of different proofs.
  * Current, proof types:
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index f6f974fca..2b67026dc 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -22,13 +22,11 @@
 #include <unordered_map>
 #include <map>
 #include <set>
-#include <vector>
 
 #include "expr/kind.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
 #include "util/dense_map.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -230,7 +228,6 @@ public:
 };
 std::ostream& operator<<(std::ostream& os, const NodeLog& nl);
 
-class ApproximateSimplex;
 class TreeLog {
 private:
   int next_exec_ord;
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 2c06967c4..a232464e5 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -20,6 +20,7 @@
 #include "base/output.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/arith/partial_model.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 571c64a78..3ce7199c0 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -24,18 +24,18 @@
 #include <utility>
 #include <vector>
 
-#include "base/output.h"
 #include "context/cdlist.h"
 #include "context/cdmaybe.h"
 #include "context/cdo.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "theory/arith/normal_form.h"
-#include "theory/arith/partial_model.h"
 #include "util/rational.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 3784ec79b..5ad2f16c0 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
 
 
 using namespace std;
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 34d695f8a..7400a229f 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -62,7 +62,6 @@ namespace arith {
 
 
 class ErrorSet;
-class ErrorInfoMap;
 
 class ComparatorPivotRule {
 private:
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 658f7c23e..45a9b79bb 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -55,7 +55,9 @@
 #pragma once
 
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
 #include "theory/arith/simplex.h"
+#include "theory/arith/simplex_update.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index e1eb786d0..03ab8e53b 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -23,7 +23,6 @@
 
 #include "expr/node.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/theory.h"
 #include "util/integer.h"
 #include "util/maybe.h"
 #include "util/rational.h"
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index c4281f0bd..a281c825b 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/inference_manager.h"
 
 #include "options/arith_options.h"
+#include "theory/arith/arith_state.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index 80cb62201..dd617f4a3 100644
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -17,18 +17,16 @@
 #ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
 #define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
 
-#include <map>
 #include <vector>
 
-#include "theory/arith/arith_state.h"
 #include "theory/inference_id.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/inference_manager_buffered.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class ArithState;
 class TheoryArith;
 
 /**
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index f0a3fbe25..42f8920c8 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -23,12 +23,9 @@
 
 #include <poly/polyxx.h>
 
-#include <map>
 #include <tuple>
 #include <vector>
 
-#include "expr/kind.h"
-#include "expr/node_manager_attributes.h"
 #include "theory/arith/nl/poly_conversion.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index 9302cb7f2..33267cb7a 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -23,8 +23,6 @@
 
 #include <poly/polyxx.h>
 
-#include <algorithm>
-#include <iostream>
 #include <vector>
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
index f13e6f4a3..5ebe0c6b7 100644
--- a/src/theory/arith/nl/cad/proof_checker.h
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index 62d3c03ff..9f0799e7c 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -16,6 +16,9 @@
 
 #ifdef CVC4_POLY_IMP
 
+#include "theory/lazy_tree_proof_generator.h"
+#include "theory/arith/nl/poly_conversion.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 72f0f766b..4709b8e59 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -23,18 +23,21 @@
 
 #include <vector>
 
-#include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/proof_generator.h"
 #include "expr/proof_set.h"
 #include "theory/arith/nl/cad/cdcac_utils.h"
-#include "theory/arith/nl/poly_conversion.h"
 #include "theory/lazy_tree_proof_generator.h"
 
 namespace CVC4 {
+
+class ProofGenerator;
+
 namespace theory {
 namespace arith {
 namespace nl {
+
+struct VariableMapper;
+
 namespace cad {
 
 /**
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 3a7d5159a..b83398cd6 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -23,6 +23,9 @@
 #include "theory/arith/nl/cad/proof_checker.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp
index 452368640..9ec3b1fc1 100644
--- a/src/theory/arith/nl/ext/constraint.cpp
+++ b/src/theory/arith/nl/ext/constraint.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/ext/monomial.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h
index 2f439f65e..d5ed7ccfd 100644
--- a/src/theory/arith/nl/ext/constraint.h
+++ b/src/theory/arith/nl/ext/constraint.h
@@ -20,13 +20,14 @@
 
 #include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/nl/ext/monomial.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+class MonomialDb;
+
 /** constraint information
  *
  * The struct ( d_rhs, d_coeff, d_type ) represents that a literal is of the
diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index c7841748f..28373223b 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -21,6 +21,8 @@
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index f64fc8feb..7a0da42aa 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -20,6 +20,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h
index c8d27ec27..4c017d198 100644
--- a/src/theory/arith/nl/ext/factoring_check.h
+++ b/src/theory/arith/nl/ext/factoring_check.h
@@ -18,13 +18,17 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
+
+class CDProof;
+
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class FactoringCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 2c25a6e29..47cb5daec 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -20,6 +20,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h
index 103e2725f..e7ba4d861 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.h
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.h
@@ -17,13 +17,14 @@
 
 #include "expr/node.h"
 #include "theory/arith/nl/ext/constraint.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class MonomialBoundsCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index 3f62d0afb..7f99b876d 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -19,6 +19,8 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index b964f00a4..a08554476 100644
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -16,14 +16,16 @@
 #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
 
 #include "expr/node.h"
+#include "theory/arith/nl/ext/monomial.h"
 #include "theory/theory_inference.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class MonomialCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 09954bf19..45f4160a0 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index bee2fe405..030445737 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -17,13 +17,14 @@
 
 #include "expr/node.h"
 #include "context/cdhashset.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class SplitZeroCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 254151283..64ea19f3c 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h
index e0656789b..a771ae543 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.h
+++ b/src/theory/arith/nl/ext/tangent_plane_check.h
@@ -15,14 +15,17 @@
 #ifndef CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
 #define CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
 
+#include <map>
+
 #include "expr/node.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class TangentPlaneCheck
 {
  public:
diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h
index f1ad3df20..a3dc74ec8 100644
--- a/src/theory/arith/nl/ext_theory_callback.h
+++ b/src/theory/arith/nl/ext_theory_callback.h
@@ -20,6 +20,9 @@
 
 namespace CVC4 {
 namespace theory {
+namespace eq {
+class EqualityEngine;
+}
 namespace arith {
 namespace nl {
 
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index e484252f2..137d430c0 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -21,7 +21,6 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "theory/arith/nl/iand_utils.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h
index 15ccab231..a84fcf978 100644
--- a/src/theory/arith/nl/iand_utils.h
+++ b/src/theory/arith/nl/iand_utils.h
@@ -17,7 +17,6 @@
 #define CVC4__THEORY__ARITH__IAND_TABLE_H
 
 #include <map>
-#include <vector>
 
 #include "expr/node.h"
 
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index dae13318c..5467c64ce 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -20,6 +20,7 @@
 #include "options/theory_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/theory_model.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index f907963c1..cd52cb159 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -21,7 +21,6 @@
 
 #include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 
 namespace CVC4 {
 
@@ -36,6 +35,7 @@ class TheoryModel;
 namespace arith {
 namespace nl {
 
+class NlLemma;
 class NonlinearExtension;
 
 /** Non-linear model finder
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 38243823b..3f32e7075 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -24,6 +24,7 @@
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 47d62e607..baa0f886c 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -23,6 +23,7 @@
 
 #include "expr/node.h"
 #include "theory/arith/nl/cad_solver.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/ext/factoring_check.h"
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
 #include "theory/arith/nl/ext/monomial_check.h"
@@ -37,6 +38,7 @@
 #include "theory/arith/nl/strategy.h"
 #include "theory/arith/nl/transcendental/transcendental_solver.h"
 #include "theory/ext_theory.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -46,6 +48,7 @@ namespace eq {
 namespace arith {
 
 class InferenceManager;
+class TheoryArith;
 
 namespace nl {
 
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 68d5a5f31..8b6f4484d 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -24,6 +24,8 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/transcendental/transcendental_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index 76b14022f..484174d5f 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -16,12 +16,8 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
 
 #include <map>
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {
 namespace theory {
@@ -29,6 +25,8 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
+struct TranscendentalState;
+
 /** Transcendental solver class
  *
  * This class implements model-based refinement schemes
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 0e5c09a2f..528e0bea2 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -23,6 +23,9 @@
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/transcendental/transcendental_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index 0b2e9d920..c628559fc 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -16,9 +16,6 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
 
 #include <map>
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
 
 #include "expr/node.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index c6b929fec..f236b472a 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -23,6 +23,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 438cc7047..593354794 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -16,6 +16,8 @@
 
 #include "expr/proof.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 33994fa3a..cd5466e89 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -17,8 +17,7 @@
 
 #include "expr/node.h"
 #include "expr/proof_set.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/transcendental/proof_checker.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
@@ -26,7 +25,13 @@ namespace CVC4 {
 class CDProof;
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 /**
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index bf8ec6c58..c3500e699 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -21,7 +21,6 @@
 #define CVC4__THEORY__ARITH__NORMAL_FORM_H
 
 #include <algorithm>
-#include <list>
 
 #include "base/output.h"
 #include "expr/node.h"
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 6a9a130ca..c6f961129 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -17,6 +17,7 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "options/arith_options.h"
 #include "smt/logic_exception.h"
 #include "theory/arith/arith_utilities.h"
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index 6dc535444..489974eac 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -17,12 +17,14 @@
 #include <map>
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/logic_info.h"
 #include "theory/skolem_lemma.h"
 
 namespace CVC4 {
+
+class TConvProofGenerator;
+
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index ec682b948..af0fe37ec 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -21,11 +21,9 @@
 #ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 #define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 
-#include <list>
 #include <vector>
 
 #include "context/cdlist.h"
-#include "context/context.h"
 #include "expr/node.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
@@ -35,6 +33,9 @@
 #include "theory/arith/delta_rational.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 
diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h
index 8d2a94215..0745bdd61 100644
--- a/src/theory/arith/proof_checker.h
+++ b/src/theory/arith/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index c383c3a85..fc3d919c3 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -15,12 +15,14 @@
  ** \todo document this file
  **/
 
+#include "theory/arith/simplex.h"
+
 #include "base/output.h"
 #include "options/arith_options.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
-#include "theory/arith/simplex.h"
-
+#include "theory/arith/linear_equality.h"
+#include "theory/arith/tableau.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d1f891676..110093068 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -56,19 +56,20 @@
 
 #include <unordered_map>
 
+#include "options/arith_options.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/linear_equality.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/tableau.h"
 #include "util/dense_map.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
 class ErrorSet;
+class LinearEqualityModule;
+class Tableau;
 
 class SimplexDecisionProcedure {
 protected:
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index d47dba70f..79136e77c 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/tableau.h"
 #include "util/statistics_registry.h"
 
 using namespace std;
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 5febe1bb0..d9d11dcc5 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -54,7 +54,9 @@
 
 #pragma once
 
+#include "theory/arith/linear_equality.h"
 #include "theory/arith/simplex.h"
+#include "theory/arith/simplex_update.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 42cd16efc..937901c57 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -25,6 +25,8 @@
 #include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/ext_theory.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1a41c9301..a208c9b10 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,7 +22,6 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
-#include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 583ff8dee..55a2472b3 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -18,22 +18,15 @@
 #pragma once
 
 #include <map>
-#include <queue>
 #include <vector>
 
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "expr/kind.h"
-#include "expr/metakind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/proof_generator.h"
-#include "options/arith_options.h"
-#include "smt/logic_exception.h"
-#include "smt_util/boolean_simplification.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
@@ -51,12 +44,8 @@
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/proof_checker.h"
-#include "theory/arith/simplex.h"
 #include "theory/arith/soi_simplex.h"
 #include "theory/arith/theory_arith.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/rewriter.h"
-#include "theory/theory_model.h"
 #include "theory/trust_node.h"
 #include "theory/valuation.h"
 #include "util/dense_map.h"
@@ -67,6 +56,10 @@
 
 namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+class TheoryModel;
+
 namespace arith {
 
 class BranchCutInfo;