13 files changed, 29 insertions, 23 deletions
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 869b229ea..a7a0f8796 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -17,6 +17,10 @@
 #include "theory/bags/bag_solver.h"
 
 #include "theory/bags/inference_generator.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/normal_form.h"
+#include "theory/bags/solver_state.h"
+#include "theory/bags/term_registry.h"
 #include "theory/uf/equality_engine_iterator.h"
 
 using namespace std;
diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h
index e524f7422..914a12ae2 100644
--- a/src/theory/bags/bag_solver.h
+++ b/src/theory/bags/bag_solver.h
@@ -17,19 +17,16 @@
 #ifndef CVC4__THEORY__BAG__SOLVER_H
 #define CVC4__THEORY__BAG__SOLVER_H
 
-#include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "theory/bags/infer_info.h"
 #include "theory/bags/inference_generator.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/normal_form.h"
-#include "theory/bags/solver_state.h"
-#include "theory/bags/term_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+class TermRegistry;
+
 /** The solver for the theory of bags
  *
  */
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 3718aedb7..51b2e5438 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -18,7 +18,7 @@
 #define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
 
 #include "theory/bags/rewrites.h"
-#include "theory/rewriter.h"
+#include "theory/theory_rewriter.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index caf4070ec..f59c43cb6 100644
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__BAGS_STATISTICS_H
 #define CVC4__THEORY__BAGS_STATISTICS_H
 
-#include "expr/kind.h"
 #include "theory/bags/rewrites.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index c61075f51..0d56080c4 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -17,6 +17,8 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h
index d6fc184c7..bfaf5d0fc 100644
--- a/src/theory/bags/inference_generator.h
+++ b/src/theory/bags/inference_generator.h
@@ -17,18 +17,16 @@
 #ifndef CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
 #define CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
 
-#include <map>
-#include <vector>
-
 #include "expr/node.h"
 #include "infer_info.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/solver_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+
 /**
  * An inference generator class. This class is used by the core solver to
  * generate lemmas
diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index 44a18bcc4..dcc5387e9 100644
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/bags/inference_manager.h"
 
+#include "theory/bags/solver_state.h"
+
 using namespace std;
 using namespace CVC4::kind;
 
diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
index 8b0fe0590..d74d3c189 100644
--- a/src/theory/bags/inference_manager.h
+++ b/src/theory/bags/inference_manager.h
@@ -17,14 +17,14 @@
 #ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
 #define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
 
-#include "theory/bags/infer_info.h"
-#include "theory/bags/solver_state.h"
 #include "theory/inference_manager_buffered.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class SolverState;
+
 /** Inference manager
  *
  * This class manages inferences produced by the theory of bags. It manages
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index 93f1af11d..d8820d8c4 100644
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -18,7 +18,6 @@
 #define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
 
 #include <map>
-#include <vector>
 
 #include "theory/theory_state.h"
 
diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 38c494219..192fd6809 100644
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -14,6 +14,9 @@
 
 #include "theory/bags/term_registry.h"
 
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
+
 using namespace std;
 using namespace CVC4::kind;
 
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index fcd822e16..87e61a026 100644
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -18,16 +18,17 @@
 #define CVC4__THEORY__BAGS__TERM_REGISTRY_H
 
 #include <map>
-#include <vector>
 
 #include "context/cdhashmap.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/solver_state.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+
 /**
  * Term registry, the purpose of this class is to maintain a database of
  * commonly used terms, and mappings from bags to their "proxy variables".
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 253fe2b7f..2950739e4 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -14,6 +14,9 @@
 
 #include "theory/bags/theory_bags.h"
 
+#include "smt/logic_exception.h"
+#include "theory/bags/normal_form.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::kind;
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 3839629d4..df64c3f1c 100644
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -17,17 +17,15 @@
 #ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H
 #define CVC4__THEORY__BAGS__THEORY_BAGS_H
 
-#include <memory>
-
 #include "theory/bags/bag_solver.h"
 #include "theory/bags/bags_rewriter.h"
 #include "theory/bags/bags_statistics.h"
 #include "theory/bags/inference_generator.h"
 #include "theory/bags/inference_manager.h"
 #include "theory/bags/solver_state.h"
+#include "theory/bags/term_registry.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {