1 files changed, 17 insertions, 14 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f464b24d4..d08e32f6e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -20,23 +20,11 @@
 #include <map>
 #include <unordered_map>
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
-#include "expr/attribute.h"
-#include "theory/quantifiers/ematching/trigger_trie.h"
-#include "theory/quantifiers/equality_query.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/model_builder.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/quantifiers_inference_manager.h"
-#include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -46,9 +34,24 @@ class TheoryEngine;
 namespace theory {
 
 class DecisionManager;
+class QuantifiersModule;
+class RepSetIterator;
 
+namespace inst {
+class TriggerTrie;
+}
 namespace quantifiers {
+class EqualityQueryQuantifiersEngine;
+class FirstOrderModel;
+class Instantiate;
+class QModelBuilder;
+class QuantifiersInferenceManager;
 class QuantifiersModules;
+class QuantifiersState;
+class Skolemize;
+class TermDb;
+class TermDbSygus;
+class TermEnumeration;
 }
 
 // TODO: organize this more/review this, github issue #1163