From dc764ce250f0d63714dab76f98bc556f00afb9f0 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 25 Mar 2021 18:34:39 +0100 Subject: [PATCH] Add missing includes. (#6207) This PR adds includes that are missing from source files, but currently provided by other includes. This mostly concerns which is currently included by the statistics, which will change in the future. --- src/expr/proof_node_manager.cpp | 2 ++ src/expr/term_conversion_proof_generator.cpp | 2 ++ src/preprocessing/passes/ho_elim.cpp | 2 ++ src/smt/preprocess_proof_generator.cpp | 2 ++ src/smt/set_defaults.cpp | 2 ++ src/smt/sygus_solver.cpp | 2 ++ src/theory/arith/arith_rewriter.cpp | 1 + src/theory/arith/cut_log.cpp | 1 + src/theory/arith/operator_elim.cpp | 2 ++ src/theory/quantifiers/extended_rewrite.cpp | 2 ++ src/theory/quantifiers/query_generator.cpp | 1 + src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 1 + src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 2 ++ src/theory/quantifiers/sygus/sygus_process_conj.cpp | 1 + src/theory/quantifiers/sygus/term_database_sygus.cpp | 2 ++ src/theory/quantifiers/sygus_sampler.cpp | 2 ++ src/theory/sort_inference.cpp | 1 + 17 files changed, 28 insertions(+) diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 6d8b05c0a..a018db4c0 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -14,6 +14,8 @@ #include "expr/proof_node_manager.h" +#include + #include "expr/proof.h" #include "expr/proof_checker.h" #include "expr/proof_node.h" diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index d15776c3f..470b8c9f8 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -14,6 +14,8 @@ #include "expr/term_conversion_proof_generator.h" +#include + #include "expr/proof_checker.h" #include "expr/proof_node.h" #include "expr/term_context.h" diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index dfe7da87d..284fbc72b 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -16,6 +16,8 @@ #include "preprocessing/passes/ho_elim.h" +#include + #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "preprocessing/assertion_pipeline.h" diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index ee2b12827..9ee01b2ef 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -15,6 +15,8 @@ #include "smt/preprocess_proof_generator.h" +#include + #include "expr/proof.h" #include "expr/proof_checker.h" #include "expr/proof_node.h" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 535c14560..f8476b734 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -14,6 +14,8 @@ #include "smt/set_defaults.h" +#include + #include "base/output.h" #include "options/arith_options.h" #include "options/arrays_options.h" diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 6cb6a499f..ea74f7a1e 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -14,6 +14,8 @@ #include "smt/sygus_solver.h" +#include + #include "expr/dtype.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 170e2d0f4..2de8cf66b 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -16,6 +16,7 @@ **/ #include +#include #include #include diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp index 89165b45e..426e10956 100644 --- a/src/theory/arith/cut_log.cpp +++ b/src/theory/arith/cut_log.cpp @@ -16,6 +16,7 @@ **/ #include +#include #include #include #include diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index ab01960dd..ee15e0f11 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -14,6 +14,8 @@ #include "theory/arith/operator_elim.h" +#include + #include "expr/attribute.h" #include "expr/bound_var_manager.h" #include "expr/skolem_manager.h" diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index c201c9ffc..9c6dd3964 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/extended_rewrite.h" +#include + #include "theory/arith/arith_msum.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/datatypes_rewriter.h" diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 1c34cc2f4..61ad4b87f 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/query_generator.h" #include +#include #include "options/quantifiers_options.h" #include "smt/smt_engine.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 1e58a1f24..7645cc237 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -14,6 +14,7 @@ **/ #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include #include #include "expr/dtype_cons.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index c72ad20d9..964d64655 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/sygus/sygus_grammar_norm.h" +#include + #include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 66e322efe..93474b4ae 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -14,6 +14,7 @@ **/ #include "theory/quantifiers/sygus/sygus_process_conj.h" +#include #include #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 50c522d95..e7bbc947a 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" +#include + #include "base/check.h" #include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index e5bb7b300..ea530da67 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/sygus_sampler.h" +#include + #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 18f07703c..e9e788160 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -21,6 +21,7 @@ #include "theory/sort_inference.h" +#include #include #include "options/quantifiers_options.h" -- 2.30.2