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, 23 insertions, 21 deletions

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 756c7d7a9..523486f80 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -28,10 +28,12 @@
 #include "util/Assert.h"
 #include "util/exception.h"
 #include "options/options.h"
-#include "util/stats.h"
+#include "util/statistics.h"
+#include "smt/smt_engine.h"
 
 #include "cvc4autoconfig.h"
 #include "main/main.h"
+#include "main/command_executor.h"
 
 using CVC4::Exception;
 using namespace std;
@@ -52,8 +54,8 @@ bool segvNoSpin = false;
 /** Handler for SIGXCPU, i.e., timeout. */
 void timeout_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by timeout.\n");
-  if((*pOptions)[options::statistics] && pStatistics != NULL) {
-    pStatistics->flushInformation(cerr);
+  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pExecutor->flushStatistics(cerr);
   }
   abort();
 }
@@ -61,8 +63,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
 /** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
-  if((*pOptions)[options::statistics] && pStatistics != NULL) {
-    pStatistics->flushInformation(cerr);
+  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pExecutor->flushStatistics(cerr);
   }
   abort();
 }
@@ -86,8 +88,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if((*pOptions)[options::statistics] && pStatistics != NULL) {
-      pStatistics->flushInformation(cerr);
+    if((*pOptions)[options::statistics] && pExecutor != NULL) {
+      pExecutor->flushStatistics(cerr);
     }
     abort();
   } else {
@@ -106,8 +108,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
   } else if(addr < 10*1024) {
     cerr << "Looks like a NULL pointer was dereferenced." << endl;
   }
-  if((*pOptions)[options::statistics] && pStatistics != NULL) {
-    pStatistics->flushInformation(cerr);
+  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pExecutor->flushStatistics(cerr);
   }
   abort();
 #endif /* CVC4_DEBUG */
@@ -119,8 +121,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if((*pOptions)[options::statistics] && pStatistics != NULL) {
-      pStatistics->flushInformation(cerr);
+    if((*pOptions)[options::statistics] && pExecutor != NULL) {
+      pExecutor->flushStatistics(cerr);
     }
     abort();
   } else {
@@ -132,8 +134,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
-  if((*pOptions)[options::statistics] && pStatistics != NULL) {
-    pStatistics->flushInformation(cerr);
+  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pExecutor->flushStatistics(cerr);
   }
   abort();
 #endif /* CVC4_DEBUG */
@@ -156,8 +158,8 @@ void cvc4unexpected() {
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
-    if((*pOptions)[options::statistics] && pStatistics != NULL) {
-      pStatistics->flushInformation(cerr);
+    if((*pOptions)[options::statistics] && pExecutor != NULL) {
+      pExecutor->flushStatistics(cerr);
     }
     set_terminate(default_terminator);
   } else {
@@ -169,8 +171,8 @@ void cvc4unexpected() {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
-  if((*pOptions)[options::statistics] && pStatistics != NULL) {
-    pStatistics->flushInformation(cerr);
+  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pExecutor->flushStatistics(cerr);
   }
   set_terminate(default_terminator);
 #endif /* CVC4_DEBUG */
@@ -182,16 +184,16 @@ void cvc4terminate() {
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.  "
           "(Don't do that.)\n");
-  if((*pOptions)[options::statistics] && pStatistics != NULL) {
-    pStatistics->flushInformation(cerr);
+  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pExecutor->flushStatistics(cerr);
   }
   default_terminator();
 #else /* CVC4_DEBUG */
   fprintf(stderr,
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
-  if((*pOptions)[options::statistics] && pStatistics != NULL) {
-    pStatistics->flushInformation(cerr);
+  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pExecutor->flushStatistics(cerr);
   }
   default_terminator();
 #endif /* CVC4_DEBUG */