summaryrefslogtreecommitdiff
path: root/src/smt
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/smt
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/smt')
-rw-r--r--src/smt/command.cpp1
-rw-r--r--src/smt/dump.cpp1
-rw-r--r--src/smt/listeners.cpp1
-rw-r--r--src/smt/logic_request.h2
-rw-r--r--src/smt/set_defaults.cpp1
-rw-r--r--src/smt/smt_engine.cpp1
-rw-r--r--src/smt/smt_engine.h6
7 files changed, 5 insertions, 8 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index cdaaa0558..f10191c75 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -39,6 +39,7 @@
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "util/sexpr.h"
+#include "util/unsafe_interrupt_exception.h"
#include "util/utility.h"
using namespace std;
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index b1fb0589c..aedd946c1 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -16,6 +16,7 @@
#include "smt/dump.h"
+#include "base/configuration.h"
#include "base/output.h"
#include "lib/strtok_r.h"
#include "preprocessing/preprocessing_pass_registry.h"
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 0347a24ef..f0fad93fe 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -14,6 +14,7 @@
#include "smt/listeners.h"
+#include "base/configuration.h"
#include "expr/attribute.h"
#include "expr/node_manager_attributes.h"
#include "options/smt_options.h"
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
index 3210de7b1..4e8dcce6c 100644
--- a/src/smt/logic_request.h
+++ b/src/smt/logic_request.h
@@ -26,7 +26,7 @@
#ifndef CVC4__LOGIC_REQUEST_H
#define CVC4__LOGIC_REQUEST_H
-#include "expr/kind.h"
+#include "theory/theory_id.h"
namespace CVC4 {
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 98fbfe1b3..3d306a7a2 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -35,6 +35,7 @@
#include "options/strings_options.h"
#include "options/theory_options.h"
#include "options/uf_options.h"
+#include "smt/logic_exception.h"
#include "theory/theory.h"
using namespace CVC4::theory;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 941fd111a..ed5e73d5d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -42,7 +42,6 @@
#include "smt/dump_manager.h"
#include "smt/interpolation_solver.h"
#include "smt/listeners.h"
-#include "smt/logic_request.h"
#include "smt/model_blocker.h"
#include "smt/model_core_builder.h"
#include "smt/node_command.h"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eb8eb6ca0..53a5b7f2f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -23,20 +23,15 @@
#include <vector>
#include <map>
-#include "base/modal_exception.h"
#include "context/cdhashmap_forward.h"
-#include "context/cdhashset_forward.h"
#include "context/cdlist_forward.h"
#include "options/options.h"
-#include "smt/logic_exception.h"
#include "smt/output_manager.h"
#include "smt/smt_mode.h"
#include "theory/logic_info.h"
-#include "util/hash.h"
#include "util/result.h"
#include "util/sexpr.h"
#include "util/statistics.h"
-#include "util/unsafe_interrupt_exception.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
@@ -51,7 +46,6 @@ class TypeNode;
struct NodeHashFunction;
class NodeManager;
-class DecisionEngine;
class TheoryEngine;
class ProofManager;
class UnsatCore;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback