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

1 files changed, 7 insertions, 3 deletions

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 8e0f23c6a..8c964a5eb 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -27,7 +27,8 @@
 #include "expr/type.h"
 #include "expr/expr.h"
 #include "util/subrange_bound.h"
-#include "util/stats.h"
+#include "util/statistics.h"
+#include "util/sexpr.h"
 
 ${includes}
 
@@ -35,7 +36,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 39 "${template}"
+#line 40 "${template}"
 
 namespace CVC4 {
 
@@ -454,7 +455,10 @@ public:
   Expr mkBoundVar(Type type);
 
   /** Get a reference to the statistics registry for this ExprManager */
-  StatisticsRegistry* getStatisticsRegistry() const throw();
+  Statistics getStatistics() const throw();
+
+  /** Get a reference to the statistics registry for this ExprManager */
+  SExpr getStatistic(const std::string& name) const throw();
 
   /** Export an expr to a different ExprManager */
   //static Expr exportExpr(const Expr& e, ExprManager* em);