14 files changed, 15 insertions, 18 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index b4d4960ed..465a8eb65 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -20,6 +20,7 @@
 #include "cvc4_private.h"
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
 
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 8f9deb2da..d3326f853 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -20,7 +20,6 @@
 #define CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
-#include "prop/sat_solver.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -35,6 +34,9 @@ class Cnf_Dat_t_;
 typedef Cnf_Dat_t_ Cnf_Dat_t;
 
 namespace CVC4 {
+namespace prop {
+class SatSolver;
+}
 namespace theory {
 namespace bv {
 
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index f2b462b6b..d66b46505 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -19,11 +19,11 @@
 #ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
 #define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
 
+#include <memory>
 #include <unordered_set>
 
 #include "theory/bv/bitblast/bitblaster.h"
 
-#include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 
 namespace CVC4 {
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 053ca6373..622369043 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -23,12 +23,14 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
-#include "prop/cnf_stream.h"
-#include "prop/registrar.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "theory/bv/abstraction.h"
 
 namespace CVC4 {
+namespace prop {
+class CnfStream;
+class NullRegistrat;
+}
 namespace theory {
 namespace bv {
 
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 28624a949..6a1d61a3b 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -19,9 +19,6 @@
 #ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H
 #define CVC4__THEORY__BV__BV_EAGER_SOLVER_H
 
-#include <unordered_set>
-#include <vector>
-
 #include "expr/node.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/theory_model.h"
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 39728c2ec..be5da70b2 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -19,16 +19,15 @@
 #ifndef CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 #define CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 
-#include <list>
 #include <queue>
 #include <unordered_map>
 #include <unordered_set>
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdo.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index dd1e7c9f7..a34ec98ad 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
 #define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
 
-#include <unordered_map>
-
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 43fd90030..38d94ea27 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -28,6 +28,7 @@
 #include "theory/bv/bv_quick_check.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::context;
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 9af95fa20..969ded528 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -21,7 +21,6 @@
 #include <unordered_map>
 #include <unordered_set>
 
-#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/ext_theory.h"
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 1b471dd68..aa3607a66 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -20,6 +20,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace std;
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index ab3c8d774..a19c18df8 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -15,6 +15,8 @@
  **/
 #include "theory/bv/slicer.h"
 
+#include <sstream>
+
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0151791b7..4e7cfdd2a 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__BV__THEORY_BV_H
 #define CVC4__THEORY__BV__THEORY_BV_H
 
-#include <unordered_map>
-
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index ee153a695..9ecc25973 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -21,13 +21,11 @@
 #define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
 #include "theory/theory_rewriter.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-struct AllRewriteRules;
 typedef RewriteResponse (*RewriteFunction) (TNode, bool);
 
 class TheoryBVRewriter : public TheoryRewriter
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 2a2639505..c6c03e561 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -19,7 +19,6 @@
 #pragma once
 
 #include <set>
-#include <sstream>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>