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, 7 insertions, 10 deletions

diff --git a/src/prop/sat.h b/src/prop/sat.h
index f9e135c0d..e583f4da0 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -131,9 +131,6 @@ class SatSolver : public SatInputInterface {
   /** Context we will be using to synchronzie the sat solver */
   context::Context* d_context;
 
-  /** Remember the options */
-  // Options* d_options;
-
   /* Pointer to the concrete SAT solver. Including this via the
      preprocessor saves us a level of indirection vs, e.g., defining a
      sub-class for each solver. */
@@ -208,9 +205,8 @@ public:
   };
 
   SatSolver(PropEngine* propEngine,
-                   TheoryEngine* theoryEngine,
-                   context::Context* context,
-                   const Options& options);
+            TheoryEngine* theoryEngine,
+            context::Context* context);
 
   ~SatSolver();
 
@@ -261,7 +257,7 @@ public:
 #ifdef __CVC4_USE_MINISAT
 
 inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
-                     context::Context* context, const Options& options) :
+                     context::Context* context) :
   d_propEngine(propEngine),
   d_cnfStream(NULL),
   d_theoryEngine(theoryEngine),
@@ -269,12 +265,13 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_statistics()
 {
   // Create the solver
-  d_minisat = new Minisat::SimpSolver(this, d_context, options.incrementalSolving);
+  d_minisat = new Minisat::SimpSolver(this, d_context,
+                                      Options::current()->incrementalSolving);
   // Setup the verbosity
-  d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1;
+  d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;
 
   // No random choices
-  if(Debug.isOn("no_rnd_decisions")){
+  if(Debug.isOn("no_rnd_decisions")) {
     d_minisat->random_var_freq = 0;
   }