This commit is a merge from the "betterstats" branch, which:

* Makes Options an "omnipresent thread-local global" (like the notion
  of the "current NodeManager" was already).  Options::current() accesses
  this structure.
* Removes Options from constructors and data structures everywhere
  (this cleans up a lot of things).
* No longer uses StatisticsRegistry statically.  An instance of the
  registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
  the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
  compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
  registry; this is needed by main() to reach in and get the registry,
  for flushing statistics at the end.

1 files changed, 38 insertions, 30 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 563fa472e..655562512 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -51,7 +51,8 @@ void doCommand(SmtEngine&, Command*);
 void printUsage();
 
 namespace CVC4 {
-  namespace main {/* Global options variable */
+  namespace main {
+    /** Global options variable */
     Options options;
 
     /** Full argv[0] */
@@ -59,6 +60,9 @@ namespace CVC4 {
 
     /** Just the basename component of argv[0] */
     const char *progName;
+
+    /** A pointer to the StatisticsRegistry (the signal handlers need it) */
+    CVC4::StatisticsRegistry* pStatistics;
   }
 }
 
@@ -104,8 +108,8 @@ int main(int argc, char* argv[]) {
     *options.out << "unknown" << endl;
 #endif
     *options.err << "CVC4 Error:" << endl << e << endl;
-    if(options.statistics) {
-      StatisticsRegistry::flushStatistics(*options.err);
+    if(options.statistics && pStatistics != NULL) {
+      pStatistics->flushStatistics(*options.err);
     }
     exit(1);
   } catch(bad_alloc) {
@@ -113,8 +117,8 @@ int main(int argc, char* argv[]) {
     *options.out << "unknown" << endl;
 #endif
     *options.err << "CVC4 ran out of memory." << endl;
-    if(options.statistics) {
-      StatisticsRegistry::flushStatistics(*options.err);
+    if(options.statistics && pStatistics != NULL) {
+      pStatistics->flushStatistics(*options.err);
     }
     exit(1);
   } catch(...) {
@@ -171,17 +175,41 @@ int runCvc4(int argc, char* argv[]) {
     options.interactive = inputFromStdin && isatty(fileno(stdin));
   }
 
+  // Determine which messages to show based on smtcomp_mode and verbosity
+  if(Configuration::isMuzzledBuild()) {
+    Debug.setStream(CVC4::null_os);
+    Trace.setStream(CVC4::null_os);
+    Notice.setStream(CVC4::null_os);
+    Chat.setStream(CVC4::null_os);
+    Message.setStream(CVC4::null_os);
+    Warning.setStream(CVC4::null_os);
+  } else {
+    if(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+  }
+
   // Create the expression manager
   ExprManager exprMgr(options);
 
   // Create the SmtEngine
-  SmtEngine smt(&exprMgr, options);
+  SmtEngine smt(&exprMgr);
+
+  // signal handlers need access
+  pStatistics = smt.getStatisticsRegistry();
 
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
   ReferenceStat< const char* > s_statFilename("filename", filename);
-  RegisterStatistic statFilenameReg(&s_statFilename);
+  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
 
   if(options.inputLanguage == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
@@ -200,26 +228,7 @@ int runCvc4(int argc, char* argv[]) {
     }
   }
 
-  // Determine which messages to show based on smtcomp_mode and verbosity
-  if(Configuration::isMuzzledBuild()) {
-    Debug.setStream(CVC4::null_os);
-    Trace.setStream(CVC4::null_os);
-    Notice.setStream(CVC4::null_os);
-    Chat.setStream(CVC4::null_os);
-    Message.setStream(CVC4::null_os);
-    Warning.setStream(CVC4::null_os);
-  } else {
-    if(options.verbosity < 2) {
-      Chat.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 1) {
-      Notice.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 0) {
-      Message.setStream(CVC4::null_os);
-      Warning.setStream(CVC4::null_os);
-    }
-
+  if(!Configuration::isMuzzledBuild()) {
     OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
     Debug.getStream() << Expr::setlanguage(language);
     Trace.getStream() << Expr::setlanguage(language);
@@ -229,7 +238,6 @@ int runCvc4(int argc, char* argv[]) {
     Warning.getStream() << Expr::setlanguage(language);
   }
 
-
   // Parse and execute commands until we are done
   Command* cmd;
   if( options.interactive ) {
@@ -273,10 +281,10 @@ int runCvc4(int argc, char* argv[]) {
 #endif
 
   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-  RegisterStatistic statSatResultReg(&s_statSatResult);
+  RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
 
   if(options.statistics) {
-    StatisticsRegistry::flushStatistics(*options.err);
+    smt.getStatisticsRegistry()->flushStatistics(*options.err);
   }
 
   return returnValue;