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.

4 files changed, 125 insertions, 54 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 1b73361c3..4bcc9a37d 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -40,6 +40,8 @@ using namespace CVC4;
 
 namespace CVC4 {
 
+CVC4_THREADLOCAL(const Options*) Options::s_current = NULL;
+
 #ifdef CVC4_DEBUG
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
 #else /* CVC4_DEBUG */
@@ -75,6 +77,7 @@ Options::Options() :
   typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
   earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
   incrementalSolving(false),
+  rewriteArithEqualities(false),
   pivotRule(MINIMUM)
 {
 }
@@ -88,9 +91,9 @@ static const string optionsDescription = "\
    --show-config          show CVC4 static configuration\n\
    --segv-nospin          don't spin on segfault waiting for gdb\n\
    --lazy-type-checking   type check expressions only when necessary (default)\n\
-   --eager-type-checking  type check expressions immediately on creation\n\
+   --eager-type-checking  type check expressions immediately on creation (debug builds only)\n\
    --no-type-checking     never type check expressions\n\
-   --no-checking          disable ALL semantic checks, including type checks \n\
+   --no-checking          disable ALL semantic checks, including type checks\n\
    --no-theory-registration disable theory reg (not safe for some theories)\n\
    --strict-parsing       fail on non-conformant inputs (SMT2 only)\n\
    --verbose | -v         increase verbosity (repeatable)\n\
@@ -106,7 +109,8 @@ static const string optionsDescription = "\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
    --lazy-definition-expansion expand define-fun lazily\n\
-   --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic \n\
+   --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
+   --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\
    --incremental          enable incremental solving\n";
 
 static const string languageDescription = "\
@@ -213,14 +217,14 @@ static struct option cmdlineOptions[] = {
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
-  { "produce-models", no_argument   , NULL, PRODUCE_MODELS},
-  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS},
-  { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING},
-  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING},
-  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
-  { "incremental", no_argument, NULL, INCREMENTAL},
+  { "produce-models", no_argument   , NULL, PRODUCE_MODELS },
+  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
+  { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING },
+  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
+  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
+  { "incremental", no_argument, NULL, INCREMENTAL },
   { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
-  { "rewrite-arithmetic-equalities" , no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES},
+  { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -484,8 +488,23 @@ throw(OptionException) {
   return optind;
 }
 
-bool Options::rewriteArithEqualities = false;
+std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) {
+  switch(rule) {
+  case Options::MINIMUM:
+    out << "MINIMUM";
+    break;
+  case Options::BREAK_TIES:
+    out << "BREAK_TIES";
+    break;
+  case Options::MAXIMUM:
+    out << "MAXIMUM";
+    break;
+  default:
+    out << "ArithPivotRule!UNKNOWN";
+  }
 
+  return out;
+}
 
 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
diff --git a/src/util/options.h b/src/util/options.h
index 32ce77a64..efbd48900 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -26,6 +26,7 @@
 
 #include "util/exception.h"
 #include "util/language.h"
+#include "util/tls.h"
 
 namespace CVC4 {
 
@@ -39,13 +40,23 @@ public:
 
 struct CVC4_PUBLIC Options {
 
+  /** The current Options in effect */
+  static CVC4_THREADLOCAL(const Options*) s_current;
+
+  /** Get the current Options in effect */
+  static inline const Options* current() {
+    return s_current;
+  }
+
+  /** The name of the binary (e.g. "cvc4") */
   std::string binary_name;
 
+  /** Whether to collect statistics during this run */
   bool statistics;
 
-  std::istream* in;
-  std::ostream* out;
-  std::ostream* err;
+  std::istream* in; /*< The input stream to use */
+  std::ostream* out; /*< The output stream to use */
+  std::ostream* err; /*< The error stream to use */
 
   /* -1 means no output */
   /* 0 is normal (and default) -- warnings only */
@@ -117,8 +128,10 @@ struct CVC4_PUBLIC Options {
   /** Whether incemental solving (push/pop) */
   bool incrementalSolving;
 
-  static bool rewriteArithEqualities;
+  /** Whether to rewrite equalities in arithmetic theory */
+  bool rewriteArithEqualities;
 
+  /** The pivot rule for arithmetic */
   typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
   ArithPivotRule pivotRule;
 
@@ -130,7 +143,14 @@ struct CVC4_PUBLIC Options {
    * suitable as an argument to printf. */
   std::string getDescription() const;
 
+  /**
+   * Print overall command-line option usage message, prefixed by
+   * "msg"---which could be an error message causing the usage
+   * output in the first place, e.g. "no such option --foo"
+   */
   static void printUsage(const std::string msg, std::ostream& out);
+
+  /** Print help for the --lang command line option */
   static void printLanguageHelp(std::ostream& out);
 
   /**
@@ -156,6 +176,8 @@ inline std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule);
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__OPTIONS_H */
diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 5be9525a9..428f051e0 100644
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -18,13 +18,33 @@
  **/
 
 #include "util/stats.h"
+#include "expr/node_manager.h"
+#include "expr/expr_manager_scope.h"
 
 using namespace CVC4;
 
-StatisticsRegistry::StatSet StatisticsRegistry::d_registeredStats;
-
 std::string Stat::s_delim(",");
 
+StatisticsRegistry* StatisticsRegistry::current() {
+  return NodeManager::currentNM()->getStatisticsRegistry();
+}
+
+void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
+#ifdef CVC4_STATISTICS_ON
+  StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+  AlwaysAssert(registeredStats.find(s) == registeredStats.end());
+  registeredStats.insert(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::registerStat() */
+
+void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
+#ifdef CVC4_STATISTICS_ON
+  StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats;
+  AlwaysAssert(registeredStats.find(s) != registeredStats.end());
+  registeredStats.erase(s);
+#endif /* CVC4_STATISTICS_ON */
+}/* StatisticsRegistry::unregisterStat() */
+
 void StatisticsRegistry::flushStatistics(std::ostream& out) {
 #ifdef CVC4_STATISTICS_ON
   for(StatSet::iterator i = d_registeredStats.begin();
@@ -34,5 +54,28 @@ void StatisticsRegistry::flushStatistics(std::ostream& out) {
     s->flushStat(out);
     out << std::endl;
   }
-#endif
+#endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::flushStatistics() */
+
+StatisticsRegistry::const_iterator StatisticsRegistry::begin() {
+  return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin();
+}/* StatisticsRegistry::begin() */
+
+StatisticsRegistry::const_iterator StatisticsRegistry::end() {
+  return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end();
+}/* StatisticsRegistry::end() */
+
+RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
+    d_em(&em), d_stat(stat) {
+  ExprManagerScope ems(*d_em);
+  StatisticsRegistry::registerStat(d_stat);
+}/* RegisterStatistic::RegisterStatistic(ExprManager&, Stat*) */
+
+RegisterStatistic::~RegisterStatistic() {
+  if(d_em != NULL) {
+    ExprManagerScope ems(*d_em);
+    StatisticsRegistry::unregisterStat(d_stat);
+  } else {
+    StatisticsRegistry::unregisterStat(d_stat);
+  }
+}/* RegisterStatistic::~RegisterStatistic() */
diff --git a/src/util/stats.h b/src/util/stats.h
index bf962d02b..53acc9b1b 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -42,6 +42,8 @@ namespace CVC4 {
 #  define __CVC4_USE_STATISTICS false
 #endif
 
+class ExprManager;
+
 class CVC4_PUBLIC Stat;
 
 inline std::ostream& operator<<(std::ostream& os, const ::timespec& t);
@@ -49,9 +51,6 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t);
 /**
  * The main statistics registry.  This registry maintains the list of
  * currently active statistics and is able to "flush" them all.
- *
- * The statistics registry is only used statically; one does not
- * construct a statistics registry.
  */
 class CVC4_PUBLIC StatisticsRegistry {
 private:
@@ -64,42 +63,42 @@ private:
   typedef std::set< Stat*, StatCmp > StatSet;
 
   /** The set of currently active statistics */
-  static StatSet d_registeredStats;
+  StatSet d_registeredStats;
 
-  /** Private default constructor undefined (no construction permitted). */
-  StatisticsRegistry() CVC4_UNDEFINED;
   /** Private copy constructor undefined (no copy permitted). */
   StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED;
 
 public:
 
+  /** Construct a statistics registry */
+  StatisticsRegistry() { }
+
   /** An iterator type over a set of statistics */
   typedef StatSet::const_iterator const_iterator;
 
+  /** Get a pointer to the current statistics registry */
+  static StatisticsRegistry* current();
+
   /** Flush all statistics to the given output stream. */
-  static void flushStatistics(std::ostream& out);
+  void flushStatistics(std::ostream& out);
 
   /** Register a new statistic, making it active. */
-  static inline void registerStat(Stat* s) throw(AssertionException);
+  static void registerStat(Stat* s) throw(AssertionException);
 
   /** Unregister an active statistic, making it inactive. */
-  static inline void unregisterStat(Stat* s) throw(AssertionException);
+  static void unregisterStat(Stat* s) throw(AssertionException);
 
   /**
    * Get an iterator to the beginning of the range of the set of active
    * (registered) statistics.
    */
-  static inline const_iterator begin() {
-    return d_registeredStats.begin();
-  }
+  static const_iterator begin();
 
   /**
    * Get an iterator to the end of the range of the set of active
    * (registered) statistics.
    */
-  static inline const_iterator end() {
-    return d_registeredStats.end();
-  }
+  static const_iterator end();
 
 };/* class StatisticsRegistry */
 
@@ -175,24 +174,6 @@ inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1,
   return s1->getName() < s2->getName();
 }
 
-inline void StatisticsRegistry::registerStat(Stat* s)
-  throw(AssertionException) {
-  if(__CVC4_USE_STATISTICS) {
-    AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
-    d_registeredStats.insert(s);
-  }
-}/* StatisticsRegistry::registerStat() */
-
-
-inline void StatisticsRegistry::unregisterStat(Stat* s)
-  throw(AssertionException) {
-  if(__CVC4_USE_STATISTICS) {
-    AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
-    d_registeredStats.erase(s);
-  }
-}/* StatisticsRegistry::unregisterStat() */
-
-
 /**
  * A class to represent a "read-only" data statistic of type T.  Adds to
  * the Stat base class the pure virtual function getData(), which returns
@@ -766,14 +747,20 @@ public:
  * registration and unregistration.
  */
 class RegisterStatistic {
+  ExprManager* d_em;
   Stat* d_stat;
 public:
   RegisterStatistic(Stat* stat) : d_stat(stat) {
+    Assert(StatisticsRegistry::current() != NULL,
+           "You need to specify an expression manager "
+           "on which to set the statistic");
     StatisticsRegistry::registerStat(d_stat);
   }
-  ~RegisterStatistic() {
-    StatisticsRegistry::unregisterStat(d_stat);
-  }
+
+  RegisterStatistic(ExprManager& em, Stat* stat);
+
+  ~RegisterStatistic();
+
 };/* class RegisterStatistic */
 
 #undef __CVC4_USE_STATISTICS