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

author	Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
	Wed, 14 Apr 2021 19:37:12 +0000 (21:37 +0200)
committer	GitHub <noreply@github.com>
	Wed, 14 Apr 2021 19:37:12 +0000 (19:37 +0000)
commit	9f14a0d6feca8d8ba727f88ef7dda5268183bb56
tree	54d1500f368312ade8abb1fb9962976ae61bedfc	tree
parent	e5c26181dab76704ad9a47126585fe2ec9d6cac2	commit \| diff

Refactor / reimplement statistics (#6162)

This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.

185 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/decision/justification_heuristic.h		diff \| blob \| history
src/expr/proof_checker.cpp		diff \| blob \| history
src/expr/proof_checker.h		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/command_executor.h		diff \| blob \| history
src/options/base_options.toml		diff \| blob \| history
src/options/options.h		diff \| blob \| history
src/options/options_public_functions.cpp		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_to_bool.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.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/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.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/util/ite_utilities.cpp		diff \| blob \| history
src/preprocessing/util/ite_utilities.h		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/sat_proof.h		diff \| blob \| history
src/proof/sat_proof_implementation.h		diff \| blob \| history
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.h		diff \| blob \| history
src/prop/cadical.cpp		diff \| blob \| history
src/prop/cadical.h		diff \| blob \| history
src/prop/cryptominisat.cpp		diff \| blob \| history
src/prop/cryptominisat.h		diff \| blob \| history
src/prop/kissat.cpp		diff \| blob \| history
src/prop/kissat.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/minisat.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/sat_solver_factory.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/env.cpp		diff \| blob \| history
src/smt/env.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_engine_scope.cpp		diff \| blob \| history
src/smt/smt_engine_scope.h		diff \| blob \| history
src/smt/smt_engine_stats.cpp		diff \| blob \| history
src/smt/smt_engine_stats.h		diff \| blob \| history
src/smt/smt_statistics_registry.cpp		diff \| blob \| history
src/smt/smt_statistics_registry.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_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.h		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.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/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/dual_simplex.h		diff \| blob \| history
src/theory/arith/error_set.cpp		diff \| blob \| history
src/theory/arith/error_set.h		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.h		diff \| blob \| history
src/theory/arith/inference_manager.cpp		diff \| blob \| history
src/theory/arith/linear_equality.cpp		diff \| blob \| history
src/theory/arith/linear_equality.h		diff \| blob \| history
src/theory/arith/nl/stats.cpp		diff \| blob \| history
src/theory/arith/nl/stats.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_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/arrays/array_info.cpp		diff \| blob \| history
src/theory/arrays/array_info.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/bags_rewriter.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.h		diff \| blob \| history
src/theory/bags/bags_statistics.cpp		diff \| blob \| history
src/theory/bags/bags_statistics.h		diff \| blob \| history
src/theory/bags/inference_manager.cpp		diff \| blob \| history
src/theory/bv/abstraction.cpp		diff \| blob \| history
src/theory/bv/abstraction.h		diff \| blob \| history
src/theory/bv/bitblast/aig_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_quick_check.cpp		diff \| blob \| history
src/theory/bv/bv_quick_check.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_solver_lazy.cpp		diff \| blob \| history
src/theory/bv/bv_solver_lazy.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/bv_subtheory_core.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/bv_subtheory_inequality.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/datatypes/inference_manager.cpp		diff \| blob \| history
src/theory/engine_output_channel.cpp		diff \| blob \| history
src/theory/engine_output_channel.h		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/inference_manager_buffered.cpp		diff \| blob \| history
src/theory/inference_manager_buffered.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.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/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_inference_manager.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_statistics.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_statistics.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_stats.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_stats.h		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep.h		diff \| blob \| history
src/theory/sets/inference_manager.cpp		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.cpp		diff \| blob \| history
src/theory/strings/inference_manager.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.h		diff \| blob \| history
src/theory/strings/sequences_stats.cpp		diff \| blob \| history
src/theory/strings/sequences_stats.h		diff \| blob \| history
src/theory/strings/strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/strings_rewriter.h		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.h		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_id.cpp		diff \| blob \| history
src/theory/theory_inference_manager.cpp		diff \| blob \| history
src/theory/theory_inference_manager.h		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/symmetry_breaker.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/util/CMakeLists.txt		diff \| blob \| history
src/util/resource_manager.cpp		diff \| blob \| history
src/util/statistics.cpp	[deleted file]	blob \| history
src/util/statistics.h	[deleted file]	blob \| history
src/util/statistics_public.cpp		diff \| blob \| history
src/util/statistics_reg.cpp	[deleted file]	blob \| history
src/util/statistics_reg.h	[deleted file]	blob \| history
src/util/statistics_registry.cpp		diff \| blob \| history
src/util/statistics_registry.h		diff \| blob \| history
src/util/statistics_value.cpp		diff \| blob \| history
src/util/statistics_value.h		diff \| blob \| history
src/util/stats_base.cpp	[deleted file]	blob \| history
src/util/stats_base.h	[deleted file]	blob \| history
src/util/stats_histogram.h	[deleted file]	blob \| history
src/util/stats_timer.cpp	[deleted file]	blob \| history
src/util/stats_timer.h	[deleted file]	blob \| history
src/util/stats_utils.cpp	[deleted file]	blob \| history
src/util/stats_utils.h	[deleted file]	blob \| history
test/unit/util/stats_black.cpp		diff \| blob \| history

RSS Atom