summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2021-03-02 01:58:20 +0100
committerGitHub <noreply@github.com>2021-03-02 00:58:20 +0000
commitb5073e16ea49ce9214fcc5318ce080724719c809 (patch)
tree1073858c57a3590b67ae7fd8e6fa2d46872f9114 /src/theory/quantifiers_engine.h
parent822ae21e0b26e9a98b3a5585dbcd2694bbbce685 (diff)
Clean up includes to reduce compile times (#6031)
This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h31
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback