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.)

2 files changed, 5 insertions, 5 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 4e884a9ab..2c5bc0170 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -2335,12 +2335,12 @@ void ValidityChecker::loadFile(std::istream& is,
   delete p;
 }
 
-Statistics& ValidityChecker::getStatistics() {
-  return *d_smt->getStatisticsRegistry();
+Statistics ValidityChecker::getStatistics() {
+  return d_smt->getStatistics();
 }
 
 void ValidityChecker::printStatistics() {
-  Message() << d_smt->getStatisticsRegistry();
+  d_smt->getStatistics().flushInformation(Message.getStream());
 }
 
 int compare(const Expr& e1, const Expr& e2) {
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 39f6658ad..c140d2994 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -469,7 +469,7 @@ public:
   InputLanguage getOutputLang() const;
 };/* class CVC3::ExprManager */
 
-typedef CVC4::StatisticsRegistry Statistics;
+typedef CVC4::Statistics Statistics;
 
 #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4
 #define SMTLIB_LANG ::CVC4::language::input::LANG_SMTLIB
@@ -1553,7 +1553,7 @@ public:
   /***************************************************************************/
 
   //! Get statistics object
-  virtual Statistics& getStatistics();
+  virtual Statistics getStatistics();
 
   //! Print collected statistics to stdout
   virtual void printStatistics();