diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 1 | ||||
-rw-r--r-- | src/smt/dump.cpp | 1 | ||||
-rw-r--r-- | src/smt/listeners.cpp | 1 | ||||
-rw-r--r-- | src/smt/logic_request.h | 2 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 1 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 1 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 6 |
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; |