git.libre-soc.org Git - cvc5.git/commit

author	Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
	Tue, 2 Mar 2021 00:58:20 +0000 (01:58 +0100)
committer	GitHub <noreply@github.com>
	Tue, 2 Mar 2021 00:58:20 +0000 (00:58 +0000)
commit	b5073e16ea49ce9214fcc5318ce080724719c809
tree	1073858c57a3590b67ae7fd8e6fa2d46872f9114	tree
parent	822ae21e0b26e9a98b3a5585dbcd2694bbbce685	commit \| 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.

210 files changed:

src/api/cvc4cpp.cpp		diff \| blob \| history
src/base/exception.cpp		diff \| blob \| history
src/base/exception.h		diff \| blob \| history
src/base/listener.h		diff \| blob \| history
src/base/output.h		diff \| blob \| history
src/context/cdlist.h		diff \| blob \| history
src/context/context.cpp		diff \| blob \| history
src/context/context.h		diff \| blob \| history
src/expr/buffered_proof_generator.cpp		diff \| blob \| history
src/expr/buffered_proof_generator.h		diff \| blob \| history
src/expr/datatype_index.cpp		diff \| blob \| history
src/expr/datatype_index.h		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/dtype.h		diff \| blob \| history
src/expr/lazy_proof.cpp		diff \| blob \| history
src/expr/lazy_proof.h		diff \| blob \| history
src/expr/lazy_proof_chain.cpp		diff \| blob \| history
src/expr/lazy_proof_chain.h		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_traversal.cpp		diff \| blob \| history
src/expr/node_traversal.h		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/proof.cpp		diff \| blob \| history
src/expr/proof.h		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/dump.cpp		diff \| blob \| history
src/smt/listeners.cpp		diff \| blob \| history
src/smt/logic_request.h		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/arith/arith_preprocess.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.h		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.h		diff \| blob \| history
src/theory/arith/nl/cad/cdcac.cpp		diff \| blob \| history
src/theory/arith/nl/cad/cdcac.h		diff \| blob \| history
src/theory/arith/nl/cad_solver.cpp		diff \| blob \| history
src/theory/arith/nl/cad_solver.h		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.cpp		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.h		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.h		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.h		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext_theory_callback.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.h		diff \| blob \| history
src/theory/arith/nl/iand_utils.cpp		diff \| blob \| history
src/theory/arith/nl/iand_utils.h		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.cpp		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.h		diff \| blob \| history
src/theory/arith/nl/icp/intersection.cpp		diff \| blob \| history
src/theory/arith/nl/icp/intersection.h		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/nl/poly_conversion.cpp		diff \| blob \| history
src/theory/arith/nl/poly_conversion.h		diff \| blob \| history
src/theory/arith/nl/stats.h		diff \| blob \| history
src/theory/arith/nl/strategy.h		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/taylor_generator.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/taylor_generator.h		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.h		diff \| blob \| history
src/theory/arith/simplex.cpp		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/arrays/inference_manager.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/bags/bag_solver.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/bv/bitblast/simple_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bv_inequality_graph.h		diff \| blob \| history
src/theory/bv/bv_solver_lazy.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/care_graph.h		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.cpp		diff \| blob \| history
src/theory/datatypes/inference_manager.cpp		diff \| blob \| history
src/theory/datatypes/inference_manager.h		diff \| blob \| history
src/theory/datatypes/proof_checker.cpp		diff \| blob \| history
src/theory/datatypes/sygus_datatype_utils.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_utils.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/ext_theory.cpp		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/fp/theory_fp.h		diff \| blob \| history
src/theory/inference_manager_buffered.cpp		diff \| blob \| history
src/theory/model_manager.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/vts_term_cache.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.h		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_rep_bound_ext.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_state.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.h		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_red.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_strat.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.h		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep.h		diff \| blob \| history
src/theory/sets/rels_utils.h		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_inference_manager.cpp		diff \| blob \| history
src/theory/theory_inference_manager.h		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/trust_node.h		diff \| blob \| history
src/theory/uf/eq_proof.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/util/bitvector.cpp		diff \| blob \| history
src/util/bitvector.h		diff \| blob \| history
src/util/cardinality.cpp		diff \| blob \| history
src/util/cardinality.h		diff \| blob \| history
src/util/divisible.h		diff \| blob \| history
src/util/ostream_util.cpp		diff \| blob \| history
src/util/ostream_util.h		diff \| blob \| history
src/util/resource_manager.cpp		diff \| blob \| history
src/util/resource_manager.h		diff \| blob \| history
src/util/statistics.cpp		diff \| blob \| history
src/util/statistics_registry.h		diff \| blob \| history
src/util/tuple.h		diff \| blob \| history
src/util/utility.cpp		diff \| blob \| history
src/util/utility.h		diff \| blob \| history
test/unit/expr/node_black.cpp		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history
test/unit/theory/theory_arith_white.cpp		diff \| blob \| history
test/unit/util/datatype_black.cpp		diff \| blob \| history

RSS Atom