Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

5 files changed, 7 insertions, 6 deletions

diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
index c6675745d..41f83269c 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 68f8e2e0d..91cb6e929 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/instantiate.h"
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 153f2e6ba..ef9b8063f 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 
 #include "expr/skolem_manager.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
@@ -23,12 +24,14 @@
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/valuation.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 4211816b7..892f453ea 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -17,17 +17,13 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 #define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 
-#include <map>
-
 #include "expr/node.h"
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/valuation.h"
 
 namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
+class Valuation;
 
 namespace quantifiers {
 class QuantifiersState;
@@ -38,6 +34,7 @@ class QuantifiersRegistry;
 namespace inst {
 
 class IMGenerator;
+class InstMatch;
 class InstMatchGenerator;
 /** A collection of nodes representing a trigger.
 *
diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h
index 57246202d..910dbc79b 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.h
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
 #define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
 
-#include <map>
 #include "expr/node.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"