Cleanup some includes (#5847)

In particular, theory_engine.h is included many places spuriously.

A few blocks of code changed indentation, updated to guidelines.

10 files changed, 10 insertions, 0 deletions

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index af6cae796..075a50e06 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -26,6 +26,7 @@
 #include "base/check.h"
 #include "expr/node_algorithm.h"
 #include "options/options.h"
+#include "options/smt_options.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 04d6b7a0c..f5d840a49 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -24,6 +24,7 @@
 
 #include "expr/node.h"
 #include "expr/node_traversal.h"
+#include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index f1cdd5b5d..95e107328 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/extended_rewriter_pass.h"
 
+#include "options/smt_options.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index fd0800f23..5b0465772 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -24,6 +24,7 @@
 
 #include "expr/node.h"
 #include "expr/node_traversal.h"
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 66a32472b..c8b713894 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -17,6 +17,7 @@
 
 #include "preprocessing/passes/ite_removal.h"
 
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 #include "theory/theory_preprocessor.h"
 
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 746bf33bd..2a1f4c3e6 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -16,6 +16,7 @@
 
 #include <vector>
 
+#include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/nary_builder.h"
 #include "theory/arith/arith_ite_utils.h"
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 23a17c939..50dbc4a27 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node_self_iterator.h"
 #include "options/arith_options.h"
+#include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/booleans/circuit_propagator.h"
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 656822299..6db701565 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "context/cdo.h"
+#include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 35eeac125..69b665854 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "options/quantifiers_options.h"
+#include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/arith/arith_msum.h"
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 4552d13fc..50831f585 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/theory_preprocess.h"
 
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"