diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-02 12:25:21 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-02 12:25:21 -0600 |
commit | e05ad4759f2ae01cc06a9ca715c777d188f0f5fd (patch) | |
tree | a292cc67c0b41c3bdf325f5160bdede10346add0 /src/preprocessing | |
parent | 4c1f67446ad59f1c5efe7230b96b0d3ccac0e692 (diff) |
Cleanup some includes (#5847)
In particular, theory_engine.h is included many places spuriously.
A few blocks of code changed indentation, updated to guidelines.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/extended_rewriter_pass.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/int_to_bv.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/theory_preprocess.cpp | 1 |
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" |