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

author	Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
	Tue, 9 Mar 2021 12:48:43 +0000 (13:48 +0100)
committer	GitHub <noreply@github.com>
	Tue, 9 Mar 2021 12:48:43 +0000 (13:48 +0100)
commit	540ef6910a2b7ffeb67bac18dfc489fb4a6115d6
tree	23b0c78b126cb5b1584b75eca14fe648624a023a	tree
parent	b302cb1f92aae1c0954c86065469e5c2b7206e74	commit \| diff

Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

239 files changed:

src/context/cdhashmap.h		diff \| blob \| history
src/context/cdlist.h		diff \| blob \| history
src/context/cdtrail_queue.h		diff \| blob \| history
src/context/context_mm.cpp		diff \| blob \| history
src/context/context_mm.h		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/preprocessing/assertion_pipeline.cpp		diff \| blob \| history
src/printer/let_binding.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/dump_manager.h		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/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/smt/unsat_core_manager.h		diff \| blob \| history
src/smt/witness_form.h		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.h		diff \| blob \| history
src/theory/arith/arith_preprocess.cpp		diff \| blob \| history
src/theory/arith/arith_preprocess.h		diff \| blob \| history
src/theory/arith/arith_static_learner.h		diff \| blob \| history
src/theory/arith/arith_utilities.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/callbacks.cpp		diff \| blob \| history
src/theory/arith/callbacks.h		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/cut_log.h		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/dio_solver.h		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/error_set.h		diff \| blob \| history
src/theory/arith/fc_simplex.h		diff \| blob \| history
src/theory/arith/infer_bounds.h		diff \| blob \| history
src/theory/arith/inference_manager.cpp		diff \| blob \| history
src/theory/arith/inference_manager.h		diff \| blob \| history
src/theory/arith/nl/cad/constraints.h		diff \| blob \| history
src/theory/arith/nl/cad/projections.h		diff \| blob \| history
src/theory/arith/nl/cad/proof_checker.h		diff \| blob \| history
src/theory/arith/nl/cad/proof_generator.cpp		diff \| blob \| history
src/theory/arith/nl/cad/proof_generator.h		diff \| blob \| history
src/theory/arith/nl/cad_solver.h		diff \| blob \| history
src/theory/arith/nl/ext/constraint.cpp		diff \| blob \| history
src/theory/arith/nl/ext/constraint.h		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.cpp		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.h		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/tangent_plane_check.h		diff \| blob \| history
src/theory/arith/nl/ext_theory_callback.h		diff \| blob \| history
src/theory/arith/nl/iand_solver.h		diff \| blob \| history
src/theory/arith/nl/iand_utils.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/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/transcendental_solver.cpp		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/normal_form.h		diff \| blob \| history
src/theory/arith/operator_elim.cpp		diff \| blob \| history
src/theory/arith/operator_elim.h		diff \| blob \| history
src/theory/arith/partial_model.h		diff \| blob \| history
src/theory/arith/proof_checker.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/soi_simplex.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/arrays/array_info.h		diff \| blob \| history
src/theory/arrays/proof_checker.h		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/atom_requests.h		diff \| blob \| history
src/theory/bags/bag_solver.cpp		diff \| blob \| history
src/theory/bags/bag_solver.h		diff \| blob \| history
src/theory/bags/bags_rewriter.h		diff \| blob \| history
src/theory/bags/bags_statistics.h		diff \| blob \| history
src/theory/bags/inference_generator.cpp		diff \| blob \| history
src/theory/bags/inference_generator.h		diff \| blob \| history
src/theory/bags/inference_manager.cpp		diff \| blob \| history
src/theory/bags/inference_manager.h		diff \| blob \| history
src/theory/bags/solver_state.h		diff \| blob \| history
src/theory/bags/term_registry.cpp		diff \| blob \| history
src/theory/bags/term_registry.h		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/bags/theory_bags.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/booleans/proof_checker.h		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.h		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.h		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/builtin/type_enumerator.cpp		diff \| blob \| history
src/theory/builtin/type_enumerator.h		diff \| blob \| history
src/theory/bv/bitblast/aig_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/aig_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_eager_solver.h		diff \| blob \| history
src/theory/bv/bv_inequality_graph.h		diff \| blob \| history
src/theory/bv/bv_solver_simple.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.h		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/slicer.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/combination_care_graph.cpp		diff \| blob \| history
src/theory/combination_engine.cpp		diff \| blob \| history
src/theory/combination_engine.h		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.h		diff \| blob \| history
src/theory/datatypes/inference.h		diff \| blob \| history
src/theory/datatypes/inference_manager.h		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.h		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/decision_strategy.h		diff \| blob \| history
src/theory/eager_proof_generator.cpp		diff \| blob \| history
src/theory/eager_proof_generator.h		diff \| blob \| history
src/theory/ee_manager_distributed.cpp		diff \| blob \| history
src/theory/ee_manager_distributed.h		diff \| blob \| history
src/theory/engine_output_channel.h		diff \| blob \| history
src/theory/ext_theory.h		diff \| blob \| history
src/theory/fp/fp_converter.cpp		diff \| blob \| history
src/theory/fp/fp_converter.h		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
src/theory/inference_manager_buffered.h		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
src/theory/model_manager.cpp		diff \| blob \| history
src/theory/model_manager.h		diff \| blob \| history
src/theory/model_manager_distributed.cpp		diff \| blob \| history
src/theory/model_manager_distributed.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.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/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.h		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.h		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.h		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/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/example_infer.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_qe_preproc.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.h		diff \| blob \| history
src/theory/quantifiers/sygus/transition_inference.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.h		diff \| blob \| history
src/theory/quantifiers/sygus/type_node_id_trie.h		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/relevance_manager.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/inference_manager.cpp		diff \| blob \| history
src/theory/sets/theory_sets.h		diff \| blob \| history
src/theory/shared_solver.cpp		diff \| blob \| history
src/theory/shared_solver.h		diff \| blob \| history
src/theory/smt_engine_subsolver.h		diff \| blob \| history
src/theory/sort_inference.h		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/solver_state.cpp		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_id.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.cpp		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/theory_preprocessor.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/proof_equality_engine.cpp		diff \| blob \| history
src/theory/uf/proof_equality_engine.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.h		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/theory/valuation.h		diff \| blob \| history

RSS Atom