10 files changed, 23 insertions, 14 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 810987a0c..d61f2d15b 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -18,6 +18,8 @@
 
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 91653785f..d701adfc4 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -19,11 +19,10 @@
 
 #include "context/cdhashmap.h"
 #include "context/context.h"
+#include "theory/decision_strategy.h"
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
 
-#include "theory/decision_manager.h"
-
 namespace CVC4 {
 namespace theory {
 namespace uf {
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index bfcb829ff..59dc3943d 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -17,9 +17,12 @@
 
 #include "theory/uf/equality_engine.h"
 
+#include "base/output.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/rewriter.h"
+#include "theory/uf/eq_proof.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 7e297134e..b81a17dcf 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -22,18 +22,14 @@
 
 #include <deque>
 #include <queue>
-#include <memory>
 #include <unordered_map>
 #include <vector>
 
-#include "base/output.h"
 #include "context/cdhashmap.h"
 #include "context/cdo.h"
 #include "expr/kind_map.h"
 #include "expr/node.h"
-#include "theory/rewriter.h"
 #include "theory/theory_id.h"
-#include "theory/uf/eq_proof.h"
 #include "theory/uf/equality_engine_iterator.h"
 #include "theory/uf/equality_engine_notify.h"
 #include "theory/uf/equality_engine_types.h"
@@ -45,6 +41,7 @@ namespace eq {
 
 class EqClassesIterator;
 class EqClassIterator;
+class EqProof;
 
 /**
  * Class for keeping an incremental congruence closure over a set of terms. It provides
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 0a7418e8d..7db887b56 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -15,7 +15,11 @@
 #include "theory/uf/proof_equality_engine.h"
 
 #include "expr/lazy_proof_chain.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
 #include "theory/rewriter.h"
+#include "theory/uf/eq_proof.h"
+#include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 1ce623683..adf8d2c18 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
 #define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
 
-#include <map>
 #include <vector>
 
 #include "context/cdhashmap.h"
@@ -25,15 +24,18 @@
 #include "expr/buffered_proof_generator.h"
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
 #include "theory/eager_proof_generator.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
+
+class ProofNode;
+class ProofNodeManager;
+
 namespace theory {
 namespace eq {
 
+class EqualityEngine;
+
 /**
  * A layer on top of an EqualityEngine. The goal of this class is manage the
  * use of an EqualityEngine object in such a way that the proper proofs are
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index caa15e69e..273e81740 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -26,6 +26,7 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
 #include "theory/uf/cardinality_extension.h"
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 7f136f9c1..be63be373 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -20,15 +20,12 @@
 #ifndef CVC4__THEORY__UF__THEORY_UF_H
 #define CVC4__THEORY__UF__THEORY_UF_H
 
-#include "context/cdo.h"
 #include "expr/node.h"
 #include "expr/node_trie.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
 #include "theory/theory_state.h"
-#include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
-#include "theory/uf/proof_equality_engine.h"
 #include "theory/uf/symmetry_breaker.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 3613a9b22..393f1f705 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -18,6 +18,8 @@
 
 #include "expr/attribute.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 3c5cc681b..62ec8204f 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -20,10 +20,12 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
 namespace theory {
+
+class TheoryModel;
+
 namespace uf {
 
 class UfModelTreeNode