Separate public-facing and internal-facing interfaces to Statistics.
authorMorgan Deters <mdeters@gmail.com>
Sat, 22 Sep 2012 21:10:51 +0000 (21:10 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 22 Sep 2012 21:10:51 +0000 (21:10 +0000)
commite2611a54c5479086df0c4a80f56597aae80b5c4e
treeb0d98600bd70147f28197883d3481614b87d76f6
parent8b106b77c11d12d16abac845ed704845ef888bd2
Separate public-facing and internal-facing interfaces to Statistics.

The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).

The StatisticsRegistry is now internal-only.  However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).

This is part of the ongoing effort to clean up the public interface.

(this commit was certified error- and warning-free by the test-and-commit script.)
67 files changed:
AUTHORS
README
src/Makefile.am
src/compat/cvc3_compat.cpp
src/compat/cvc3_compat.h
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/node_manager.cpp
src/include/cvc4_private.h
src/include/cvc4_private_library.h [new file with mode: 0644]
src/main/Makefile.am
src/main/command_executor.cpp
src/main/command_executor.h
src/main/command_executor_portfolio.cpp
src/main/command_executor_portfolio.h
src/main/driver_unified.cpp
src/main/main.cpp
src/main/main.h
src/main/util.cpp
src/printer/printer.cpp
src/prop/bvminisat/simp/SimpSolver.h
src/prop/sat_solver.h
src/prop/theory_proxy.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/arith/arith_priority_queue.h
src/theory/arith/arith_static_learner.h
src/theory/arith/congruence_manager.h
src/theory/arith/dio_solver.h
src/theory/arith/linear_equality.h
src/theory/arith/simplex.h
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_instantiator.h
src/theory/arrays/array_info.h
src/theory/arrays/theory_arrays.h
src/theory/bv/bitblaster.h
src/theory/bv/theory_bv.h
src/theory/bv/theory_bv_rewrite_rules.h
src/theory/bv/theory_bv_rewriter.h
src/theory/datatypes/theory_datatypes_instantiator.h
src/theory/ite_simplifier.h
src/theory/quantifiers/theory_quantifiers.h
src/theory/quantifiers/theory_quantifiers_instantiator.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/rewriterules/theory_rewriterules.h
src/theory/shared_terms_database.h
src/theory/theory.h
src/theory/theory_engine.h
src/theory/uf/equality_engine.h
src/theory/uf/inst_strategy.h
src/theory/uf/symmetry_breaker.h
src/theory/uf/theory_uf_instantiator.h
src/theory/uf/theory_uf_strong_solver.h
src/util/Makefile.am
src/util/sexpr.h
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]
src/util/stats.cpp [deleted file]
src/util/stats.h [deleted file]
src/util/stats.i [deleted file]
test/system/Makefile.am
test/system/statistics.cpp [new file with mode: 0644]
test/unit/util/stats_black.h