Removing StatisticsRegistry's static functions current() and registerStat().
authorTim King <taking@google.com>
Sat, 9 Jan 2016 00:44:57 +0000 (16:44 -0800)
committerTim King <taking@google.com>
Sat, 9 Jan 2016 00:44:57 +0000 (16:44 -0800)
commitf4ef7af0a2295691f281ee1604dfeb4082fe229c
tree995e512e5669cec6bbc9447d00ec912d5e4c19e3
parentdef0a07f9676a292a849d7fc8269ffd0901ce156
Removing StatisticsRegistry's static functions current() and registerStat().
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.
123 files changed:
src/Makefile.am
src/cvc4.i
src/decision/justification_heuristic.cpp
src/expr/Makefile.am
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/node_manager.cpp
src/expr/statistics.cpp [deleted file]
src/expr/statistics.h [deleted file]
src/expr/statistics.i [deleted file]
src/expr/statistics_registry.cpp [deleted file]
src/expr/statistics_registry.h [deleted file]
src/main/command_executor.h
src/main/command_executor_portfolio.cpp
src/main/driver_unified.cpp
src/main/main.cpp
src/main/main.h
src/main/portfolio.cpp
src/main/portfolio.h
src/main/util.cpp
src/prop/bvminisat/bvminisat.cpp
src/prop/bvminisat/bvminisat.h
src/prop/bvminisat/simp/SimpSolver.h
src/prop/minisat/minisat.cpp
src/prop/minisat/minisat.h
src/prop/prop_engine.cpp
src/prop/sat_solver.h
src/prop/sat_solver_factory.cpp
src/prop/sat_solver_factory.h
src/prop/theory_proxy.cpp
src/prop/theory_proxy.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/smt_engine_check_proof.cpp
src/smt/smt_engine_scope.h
src/smt/smt_statistics_registry.cpp [new file with mode: 0644]
src/smt/smt_statistics_registry.h [new file with mode: 0644]
src/theory/arith/approx_simplex.cpp
src/theory/arith/approx_simplex.h
src/theory/arith/arith_static_learner.cpp
src/theory/arith/arith_static_learner.h
src/theory/arith/attempt_solution_simplex.cpp
src/theory/arith/attempt_solution_simplex.h
src/theory/arith/congruence_manager.cpp
src/theory/arith/congruence_manager.h
src/theory/arith/constraint.cpp
src/theory/arith/cut_log.h
src/theory/arith/dio_solver.cpp
src/theory/arith/dio_solver.h
src/theory/arith/dual_simplex.cpp
src/theory/arith/dual_simplex.h
src/theory/arith/error_set.cpp
src/theory/arith/error_set.h
src/theory/arith/fc_simplex.cpp
src/theory/arith/fc_simplex.h
src/theory/arith/linear_equality.cpp
src/theory/arith/linear_equality.h
src/theory/arith/soi_simplex.cpp
src/theory/arith/soi_simplex.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
src/theory/arith/theory_arith_private.h
src/theory/arrays/array_info.cpp
src/theory/arrays/array_info.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/bv/abstraction.cpp
src/theory/bv/abstraction.h
src/theory/bv/aig_bitblaster.cpp
src/theory/bv/bv_quick_check.cpp
src/theory/bv/bv_quick_check.h
src/theory/bv/bv_subtheory_algebraic.cpp
src/theory/bv/bv_subtheory_bitblast.cpp
src/theory/bv/bv_subtheory_core.cpp
src/theory/bv/bv_subtheory_inequality.cpp
src/theory/bv/bv_to_bool.cpp
src/theory/bv/bv_to_bool.h
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/bv/slicer.cpp
src/theory/bv/slicer.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/bv/theory_bv_rewrite_rules.h
src/theory/bv/theory_bv_rewriter.cpp
src/theory/bv/theory_bv_rewriter.h
src/theory/ite_utilities.cpp
src/theory/ite_utilities.h
src/theory/quantifiers/ce_guided_instantiation.cpp
src/theory/quantifiers/ceg_instantiator.h
src/theory/quantifiers/inst_strategy_cbqi.h
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/rewriter.cpp
src/theory/sets/theory_sets_private.cpp
src/theory/shared_terms_database.cpp
src/theory/shared_terms_database.h
src/theory/strings/theory_strings.cpp
src/theory/theory.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
src/theory/uf/equality_engine.h
src/theory/uf/symmetry_breaker.h
src/theory/uf/theory_uf_strong_solver.cpp
src/theory/uf/theory_uf_strong_solver.h
src/theory/unconstrained_simplifier.cpp
src/theory/unconstrained_simplifier.h
src/util/Makefile.am
src/util/statistics.cpp [new file with mode: 0644]
src/util/statistics.h [new file with mode: 0644]
src/util/statistics.i [new file with mode: 0644]
src/util/statistics_registry.cpp [new file with mode: 0644]
src/util/statistics_registry.h [new file with mode: 0644]
test/system/statistics.cpp
test/unit/util/stats_black.h