Remove forward declarations in quantifiers engine (#3156)

7 files changed, 12 insertions, 7 deletions

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index f873b94f2..879771903 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 55ed5bdd2..8e6738e9e 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -18,8 +18,7 @@
 #ifndef CVC4__BOUNDED_INTEGERS_H
 #define CVC4__BOUNDED_INTEGERS_H
 
-
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 
 #include "context/context.h"
 #include "context/context_mm.h"
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index ace5c2b26..0f06cef74 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -13,6 +13,7 @@
  **/
 
 #include "theory/quantifiers/fmf/full_model_check.h"
+
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
@@ -20,6 +21,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 51cd8481f..cdbc5e391 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -15,13 +15,14 @@
 #include "theory/quantifiers/fmf/model_builder.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/fmf/model_engine.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 1b4d24779..c8f59defe 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -17,9 +17,10 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
 #define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
 
-#include "theory/quantifiers_engine.h"
+#include "expr/node.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_match.h"
 #include "theory/theory_model_builder.h"
-#include "theory/uf/theory_uf_model.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 5609cade6..f34dc1b85 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 41bc312e7..b39dd03f8 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -17,8 +17,8 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 #define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 
-#include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {