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

author	Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
	Wed, 3 Mar 2021 16:50:45 +0000 (17:50 +0100)
committer	GitHub <noreply@github.com>
	Wed, 3 Mar 2021 16:50:45 +0000 (16:50 +0000)
commit	a02a794c383ae2381e1210f53174cefb8d94e615
tree	0eac511c22ba9eeba1925e3afa4f0542edf5cf60	tree
parent	6db84f6e373f9651af48df7b654e3992f68472ac	commit \| diff

More cleanup of includes to reduce compilation times (#6037)

Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.

214 files changed:

src/base/exception.cpp		diff \| blob \| history
src/base/exception.h		diff \| blob \| history
src/base/listener.cpp		diff \| blob \| history
src/decision/decision_engine.cpp		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/decision/justification_heuristic.h		diff \| blob \| history
src/expr/buffered_proof_generator.h		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/kind_template.cpp		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/proof.cpp		diff \| blob \| history
src/expr/proof.h		diff \| blob \| history
src/expr/proof_checker.cpp		diff \| blob \| history
src/expr/proof_checker.h		diff \| blob \| history
src/expr/proof_ensure_closed.cpp		diff \| blob \| history
src/expr/proof_ensure_closed.h		diff \| blob \| history
src/expr/proof_generator.cpp		diff \| blob \| history
src/expr/proof_generator.h		diff \| blob \| history
src/expr/proof_node_algorithm.cpp		diff \| blob \| history
src/expr/proof_node_algorithm.h		diff \| blob \| history
src/expr/proof_node_manager.cpp		diff \| blob \| history
src/expr/proof_node_manager.h		diff \| blob \| history
src/expr/proof_node_to_sexpr.cpp		diff \| blob \| history
src/expr/proof_node_to_sexpr.h		diff \| blob \| history
src/expr/proof_node_updater.cpp		diff \| blob \| history
src/expr/proof_node_updater.h		diff \| blob \| history
src/expr/proof_step_buffer.cpp		diff \| blob \| history
src/expr/proof_step_buffer.h		diff \| blob \| history
src/expr/record.h		diff \| blob \| history
src/expr/sequence.cpp		diff \| blob \| history
src/expr/subs.cpp		diff \| blob \| history
src/expr/sygus_datatype.cpp		diff \| blob \| history
src/expr/symbol_manager.h		diff \| blob \| history
src/expr/tconv_seq_proof_generator.cpp		diff \| blob \| history
src/expr/tconv_seq_proof_generator.h		diff \| blob \| history
src/expr/term_canonize.cpp		diff \| blob \| history
src/expr/term_context_node.h		diff \| blob \| history
src/expr/term_context_stack.cpp		diff \| blob \| history
src/expr/term_conversion_proof_generator.cpp		diff \| blob \| history
src/expr/term_conversion_proof_generator.h		diff \| blob \| history
src/expr/type.cpp		diff \| blob \| history
src/expr/type_checker_template.cpp		diff \| blob \| history
src/expr/type_checker_util.h		diff \| blob \| history
src/expr/type_matcher.h		diff \| blob \| history
src/options/language.cpp		diff \| blob \| history
src/options/language.h		diff \| blob \| history
src/options/open_ostream.h		diff \| blob \| history
src/options/options_handler.h		diff \| blob \| history
src/preprocessing/assertion_pipeline.cpp		diff \| blob \| history
src/preprocessing/assertion_pipeline.h		diff \| blob \| history
src/preprocessing/passes/ackermann.cpp		diff \| blob \| history
src/preprocessing/passes/ackermann.h		diff \| blob \| history
src/preprocessing/passes/apply_substs.cpp		diff \| blob \| history
src/preprocessing/passes/apply_substs.h		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.h		diff \| blob \| history
src/preprocessing/passes/bv_abstraction.cpp		diff \| blob \| history
src/preprocessing/passes/bv_abstraction.h		diff \| blob \| history
src/preprocessing/passes/bv_eager_atoms.cpp		diff \| blob \| history
src/preprocessing/passes/bv_eager_atoms.h		diff \| blob \| history
src/preprocessing/passes/bv_gauss.cpp		diff \| blob \| history
src/preprocessing/passes/bv_gauss.h		diff \| blob \| history
src/preprocessing/passes/bv_intro_pow2.cpp		diff \| blob \| history
src/preprocessing/passes/bv_intro_pow2.h		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.h		diff \| blob \| history
src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_int.h		diff \| blob \| history
src/preprocessing/passes/extended_rewriter_pass.cpp		diff \| blob \| history
src/preprocessing/passes/extended_rewriter_pass.h		diff \| blob \| history
src/preprocessing/passes/foreign_theory_rewrite.cpp		diff \| blob \| history
src/preprocessing/passes/foreign_theory_rewrite.h		diff \| blob \| history
src/preprocessing/passes/fun_def_fmf.cpp		diff \| blob \| history
src/preprocessing/passes/fun_def_fmf.h		diff \| blob \| history
src/preprocessing/passes/global_negate.cpp		diff \| blob \| history
src/preprocessing/passes/global_negate.h		diff \| blob \| history
src/preprocessing/passes/ho_elim.cpp		diff \| blob \| history
src/preprocessing/passes/ho_elim.h		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/int_to_bv.h		diff \| blob \| history
src/preprocessing/passes/ite_removal.cpp		diff \| blob \| history
src/preprocessing/passes/ite_removal.h		diff \| blob \| history
src/preprocessing/passes/ite_simp.cpp		diff \| blob \| history
src/preprocessing/passes/ite_simp.h		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.h		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.cpp		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.h		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.h		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.cpp		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.h		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.cpp		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.h		diff \| blob \| history
src/preprocessing/passes/quantifiers_preprocess.cpp		diff \| blob \| history
src/preprocessing/passes/quantifiers_preprocess.h		diff \| blob \| history
src/preprocessing/passes/real_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/real_to_int.h		diff \| blob \| history
src/preprocessing/passes/rewrite.cpp		diff \| blob \| history
src/preprocessing/passes/rewrite.h		diff \| blob \| history
src/preprocessing/passes/sep_skolem_emp.cpp		diff \| blob \| history
src/preprocessing/passes/sep_skolem_emp.h		diff \| blob \| history
src/preprocessing/passes/sort_infer.cpp		diff \| blob \| history
src/preprocessing/passes/sort_infer.h		diff \| blob \| history
src/preprocessing/passes/static_learning.cpp		diff \| blob \| history
src/preprocessing/passes/static_learning.h		diff \| blob \| history
src/preprocessing/passes/strings_eager_pp.cpp		diff \| blob \| history
src/preprocessing/passes/strings_eager_pp.h		diff \| blob \| history
src/preprocessing/passes/sygus_inference.cpp		diff \| blob \| history
src/preprocessing/passes/sygus_inference.h		diff \| blob \| history
src/preprocessing/passes/synth_rew_rules.cpp		diff \| blob \| history
src/preprocessing/passes/synth_rew_rules.h		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.cpp		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.h		diff \| blob \| history
src/preprocessing/passes/theory_rewrite_eq.cpp		diff \| blob \| history
src/preprocessing/passes/theory_rewrite_eq.h		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.h		diff \| blob \| history
src/preprocessing/preprocessing_pass.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass.h		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.h		diff \| blob \| history
src/preprocessing/preprocessing_pass_registry.h		diff \| blob \| history
src/preprocessing/util/ite_utilities.cpp		diff \| blob \| history
src/preprocessing/util/ite_utilities.h		diff \| blob \| history
src/printer/let_binding.h		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.h		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/prop_proof_manager.cpp		diff \| blob \| history
src/prop/prop_proof_manager.h		diff \| blob \| history
src/prop/sat_proof_manager.h		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/abduction_solver.cpp		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/assertions.h		diff \| blob \| history
src/smt/check_models.cpp		diff \| blob \| history
src/smt/check_models.h		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/dump_manager.h		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/expand_definitions.h		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/managed_ostreams.h		diff \| blob \| history
src/smt/model.h		diff \| blob \| history
src/smt/model_blocker.cpp		diff \| blob \| history
src/smt/model_blocker.h		diff \| blob \| history
src/smt/node_command.cpp		diff \| blob \| history
src/smt/options_manager.h		diff \| blob \| history
src/smt/preprocess_proof_generator.cpp		diff \| blob \| history
src/smt/preprocess_proof_generator.h		diff \| blob \| history
src/smt/preprocessor.cpp		diff \| blob \| history
src/smt/preprocessor.h		diff \| blob \| history
src/smt/process_assertions.cpp		diff \| blob \| history
src/smt/process_assertions.h		diff \| blob \| history
src/smt/proof_manager.cpp		diff \| blob \| history
src/smt/proof_manager.h		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/proof_post_processor.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/term_formula_removal.h		diff \| blob \| history
src/theory/arith/delta_rational.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.cpp		diff \| blob \| history
src/theory/bv/bitblast/bitblaster.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.h		diff \| blob \| history
src/theory/datatypes/sygus_datatype_utils.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/lazy_tree_proof_generator.cpp		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_abduct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_utils.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine_proof_generator.cpp		diff \| blob \| history
src/theory/theory_id.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/eq_proof.cpp		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/util/bitvector.h		diff \| blob \| history
src/util/cardinality.cpp		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
src/util/poly_util.cpp		diff \| blob \| history
src/util/rational_gmp_imp.h		diff \| blob \| history
src/util/result.cpp		diff \| blob \| history
src/util/result.h		diff \| blob \| history
src/util/safe_print.cpp		diff \| blob \| history
src/util/safe_print.h		diff \| blob \| history
src/util/sampler.cpp		diff \| blob \| history
src/util/sampler.h		diff \| blob \| history
src/util/sexpr.h		diff \| blob \| history
src/util/string.h		diff \| blob \| history
test/unit/preprocessing/pass_bv_gauss_white.cpp		diff \| blob \| history
test/unit/prop/cnf_stream_white.cpp		diff \| blob \| history
test/unit/util/cardinality_black.cpp		diff \| blob \| history
test/unit/util/integer_black.cpp		diff \| blob \| history

RSS Atom