Options merge. This commit:

1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)

The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:

* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important.  If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***

Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).

Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double).  For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).

Benefits of the new options system include:

1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose

I've taken lots of care not to break anything.  Hopefully, I've succeeded in that.

1 files changed, 136 insertions, 126 deletions

diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index d93e9f872..648c6c9f9 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -40,7 +40,11 @@
 #include "expr/command.h"
 #include "util/Assert.h"
 #include "util/configuration.h"
-#include "util/options.h"
+#include "options/options.h"
+#include "main/options.h"
+#include "smt/options.h"
+#include "prop/options.h"
+#include "theory/uf/options.h"
 #include "util/output.h"
 #include "util/dump.h"
 #include "util/result.h"
@@ -78,7 +82,7 @@ static bool doCommand(SmtEngine&, Command*, Options&);
 Result doSmt(SmtEngine &smt, Command *cmd, Options &options);
 
 template<typename T>
-void sharingManager(int numThreads,
+void sharingManager(unsigned numThreads,
                     SharedChannel<T>* channelsOut[],
                     SharedChannel<T>* channelsIn[],
                     SmtEngine* smts[]);
@@ -122,23 +126,25 @@ public:
   {}
 
   void notifyNewLemma(Expr lemma) {
-    if(Debug.isOn("disable-lemma-sharing")) return;
-    const Options *options = Options::current();
-    if(options->sharingFilterByLength >= 0) { // 0 would mean no-sharing effectively
-      if( int(lemma.getNumChildren()) > options->sharingFilterByLength)
+    if(Debug.isOn("disable-lemma-sharing")) {
+      return;
+    }
+    if(options::sharingFilterByLength() >= 0) { // 0 would mean no-sharing effectively
+      if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) {
         return;
+      }
     }
     ++cnt;
-    Trace("sharing") << d_tag << ": " << lemma << std::endl;
+    Trace("sharing") << d_tag << ": " << lemma << endl;
     expr::pickle::Pickle pkl;
-    try{
+    try {
       d_pickler.toPickle(lemma, pkl);
       d_sharedChannel->push(pkl);
-      if(Trace.isOn("showSharing") and options->thread_id == 0) {
-        *(Options::current()->out) << "thread #0: notifyNewLemma: " << lemma << endl;
+      if(Trace.isOn("showSharing") && options::thread_id() == 0) {
+        *options::out() << "thread #0: notifyNewLemma: " << lemma << endl;
       }
-    }catch(expr::pickle::PicklingException& p){
-      Trace("sharing::blocked") << lemma << std::endl;
+    } catch(expr::pickle::PicklingException& p){
+      Trace("sharing::blocked") << lemma << endl;
     }
   }
 
@@ -172,8 +178,8 @@ public:
     expr::pickle::Pickle pkl = d_sharedChannel->pop();
 
     Expr e = d_pickler.fromPickle(pkl);
-    if(Trace.isOn("showSharing") and Options::current()->thread_id == 0) {
-      *(Options::current()->out) << "thread #0: getNewLemma: " << e << endl;
+    if(Trace.isOn("showSharing") && options::thread_id() == 0) {
+      *options::out() << "thread #0: getNewLemma: " << e << endl;
     }
     return e;
   }
@@ -182,7 +188,7 @@ public:
 
 
 
-int runCvc4(int argc, char *argv[], Options& options) {
+int runCvc4(int argc, char *argv[], Options& opts) {
 
 #ifdef CVC4_CLN_IMP
   Warning() << "WARNING:" << endl
@@ -211,7 +217,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
   s_beforePortfolioTime.start();
 
   // For the signal handlers' benefit
-  pOptions = &options;
+  pOptions = &opts;
 
   // Initialize the signal handlers
   cvc4_init();
@@ -222,36 +228,36 @@ int runCvc4(int argc, char *argv[], Options& options) {
   /****************************** Options Processing ************************/
 
   // Parse the options
-  int firstArgIndex = options.parseOptions(argc, argv);
+  int firstArgIndex = opts.parseOptions(argc, argv);
 
-  progName = options.binary_name.c_str();
+  progName = opts[options::binary_name].c_str();
 
-  if( options.help ) {
-    printUsage(options, true);
+  if( opts[options::help] ) {
+    printUsage(opts, true);
     exit(1);
-  } else if( options.languageHelp ) {
-    Options::printLanguageHelp(*options.out);
+  } else if( opts[options::languageHelp] ) {
+    Options::printLanguageHelp(*opts[options::out]);
     exit(1);
-  } else if( options.version ) {
-    *options.out << Configuration::about().c_str() << flush;
+  } else if( opts[options::version] ) {
+    *opts[options::out] << Configuration::about().c_str() << flush;
     exit(0);
   }
 
-  int numThreads = options.threads;
+  unsigned numThreads = opts[options::threads];
 
-  if(options.threadArgv.size() > size_t(numThreads)) {
+  if(opts[options::threadArgv].size() > size_t(numThreads)) {
     stringstream ss;
-    ss << "--thread" << (options.threadArgv.size() - 1)
+    ss << "--thread" << (opts[options::threadArgv].size() - 1)
        << " configuration string seen but this portfolio will only contain "
        << numThreads << " thread(s)!";
     throw OptionException(ss.str());
   }
 
-  segvNoSpin = options.segvNoSpin;
+  segvNoSpin = opts[options::segvNoSpin];
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC4_COMPETITION_MODE
-  *options.out << unitbuf;
+  *opts[options::out] << unitbuf;
 #endif /* CVC4_COMPETITION_MODE */
 
   // We only accept one input file
@@ -264,29 +270,29 @@ int runCvc4(int argc, char *argv[], Options& options) {
     firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
 
   // if we're reading from stdin on a TTY, default to interactive mode
-  if(!options.interactiveSetByUser) {
-    options.interactive = inputFromStdin && isatty(fileno(stdin));
+  if(!opts.wasSetByUser(options::interactive)) {
+    opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin)));
   }
 
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 
-  if(options.inputLanguage == language::input::LANG_AUTO) {
+  if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      options.inputLanguage = language::input::LANG_CVC4;
+      opts.set(options::inputLanguage, language::input::LANG_CVC4);
     } else {
       unsigned len = strlen(filename);
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        options.inputLanguage = language::input::LANG_SMTLIB_V2;
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        options.inputLanguage = language::input::LANG_SMTLIB;
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB);
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        options.inputLanguage = language::input::LANG_TPTP;
+        opts.set(options::inputLanguage, language::input::LANG_TPTP);
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        options.inputLanguage = language::input::LANG_CVC4;
+        opts.set(options::inputLanguage, language::input::LANG_CVC4);
       }
     }
   }
@@ -301,54 +307,55 @@ int runCvc4(int argc, char *argv[], Options& options) {
     Warning.setStream(CVC4::null_os);
     Dump.setStream(CVC4::null_os);
   } else {
-    if(options.verbosity < 2) {
+    if(opts[options::verbosity] < 2) {
       Chat.setStream(CVC4::null_os);
     }
-    if(options.verbosity < 1) {
+    if(opts[options::verbosity] < 1) {
       Notice.setStream(CVC4::null_os);
     }
-    if(options.verbosity < 0) {
+    if(opts[options::verbosity] < 0) {
       Message.setStream(CVC4::null_os);
       Warning.setStream(CVC4::null_os);
     }
 
-    OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
+    OutputLanguage language = language::toOutputLanguage(opts[options::inputLanguage]);
     Debug.getStream() << Expr::setlanguage(language);
     Trace.getStream() << Expr::setlanguage(language);
     Notice.getStream() << Expr::setlanguage(language);
     Chat.getStream() << Expr::setlanguage(language);
     Message.getStream() << Expr::setlanguage(language);
     Warning.getStream() << Expr::setlanguage(language);
-    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+    Dump.getStream() << Expr::setlanguage(language)
                      << Expr::setdepth(-1)
                      << Expr::printtypes(false);
   }
 
   // important even for muzzled builds (to get result output right)
-  *options.out << Expr::setlanguage(options.outputLanguage);
+  *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
 
   vector<Options> threadOptions;
-  for(int i = 0; i < numThreads; ++i) {
-    threadOptions.push_back(options);
-    Options& opts = threadOptions.back();
+  for(unsigned i = 0; i < numThreads; ++i) {
+    threadOptions.push_back(opts);
+    Options& tOpts = threadOptions.back();
 
     // Set thread identifier
-    opts.thread_id = i;
+    tOpts.set(options::thread_id, i);
 
     // If the random-seed is negative, pick a random seed randomly
-    if(options.satRandomSeed < 0)
-      opts.satRandomSeed = (double)rand();
+    if(opts[options::satRandomSeed] < 0) {
+      tOpts.set(options::satRandomSeed, (double)rand());
+    }
 
-    if(i < (int)options.threadArgv.size() && !options.threadArgv[i].empty()) {
+    if(i < opts[options::threadArgv].size() && !opts[options::threadArgv][i].empty()) {
       // separate out the thread's individual configuration string
       stringstream optidss;
       optidss << "--thread" << i;
       string optid = optidss.str();
       int targc = 1;
-      char* tbuf = strdup(options.threadArgv[i].c_str());
+      char* tbuf = strdup(opts[options::threadArgv][i].c_str());
       char* p = tbuf;
       // string length is certainly an upper bound on size needed
-      char** targv = new char*[options.threadArgv[i].size()];
+      char** targv = new char*[opts[options::threadArgv][i].size()];
       char** vp = targv;
       *vp++ = strdup(optid.c_str());
       p = strtok(p, " ");
@@ -360,7 +367,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
       *vp++ = NULL;
       if(targc > 1) { // this is necessary in case you do e.g. --thread0="  "
         try {
-          opts.parseOptions(targc, targv);
+          tOpts.parseOptions(targc, targv);
         } catch(OptionException& e) {
           stringstream ss;
           ss << optid << ": " << e.getMessage();
@@ -372,7 +379,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
              << "' in thread configuration " << optid << " !";
           throw OptionException(ss.str());
         }
-        if(opts.threads != numThreads || opts.threadArgv != options.threadArgv) {
+        if(tOpts[options::threads] != numThreads || tOpts[options::threadArgv] != opts[options::threadArgv]) {
           stringstream ss;
           ss << "not allowed to set thread options in " << optid << " !";
           throw OptionException(ss.str());
@@ -387,16 +394,16 @@ int runCvc4(int argc, char *argv[], Options& options) {
   // Some more options related stuff
 
   /* Use satRandomSeed for generating random numbers, in particular satRandomSeed-s */
-  srand((unsigned int)(-options.satRandomSeed));
+  srand((unsigned int)(-opts[options::satRandomSeed]));
 
   assert(numThreads >= 1);      //do we need this?
 
   /* Output to string stream  */
   vector<stringstream*> ss_out(numThreads);
-  if(options.verbosity == 0 or options.separateOutput) {
-    for(int i = 0;i <numThreads; ++i) {
+  if(opts[options::verbosity] == 0 || opts[options::separateOutput]) {
+    for(unsigned i = 0; i < numThreads; ++i) {
       ss_out[i] = new stringstream;
-      threadOptions[i].out = ss_out[i];
+      threadOptions[i].set(options::out, ss_out[i]);
     }
   }
 
@@ -431,8 +438,8 @@ int runCvc4(int argc, char *argv[], Options& options) {
   Command* cmd;
   // bool status = true;           // Doesn't seem to be use right now: commenting it out
   CommandSequence* seq = new CommandSequence();
-  if( options.interactive ) {
-    InteractiveShell shell(*exprMgr, options);
+  if( opts[options::interactive] ) {
+    InteractiveShell shell(*exprMgr, opts);
     Message() << Configuration::getPackageName()
               << " " << Configuration::getVersionString();
     if(Configuration::isSubversionBuild()) {
@@ -452,7 +459,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
   } else {
     ParserBuilder parserBuilder =
       ParserBuilder(exprMgr, filename).
-        withOptions(options);
+        withOptions(opts);
 
     if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -465,15 +472,16 @@ int runCvc4(int argc, char *argv[], Options& options) {
     Parser *parser = parserBuilder.build();
     while((cmd = parser->nextCommand())) {
       seq->addCommand(cmd);
-      // doCommand(smt, cmd, options);
+      // doCommand(smt, cmd, opts);
       // delete cmd;
     }
     // Remove the parser
     delete parser;
   }
 
-  if(options.parseOnly)
+  if(opts[options::parseOnly]) {
     return 0;
+  }
 
   exprMgr = NULL;               // don't want to use that variable
                                 // after this point
@@ -482,7 +490,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
   ExprManagerMapCollection* vmaps[numThreads]; // vmaps[0] is generally empty
   Command *seqs[numThreads];
   seqs[0] = seq;   seq = NULL;
-  for(int i = 1; i < numThreads; ++i) {
+  for(unsigned i = 1; i < numThreads; ++i) {
     vmaps[i] = new ExprManagerMapCollection();
     exprMgrs[i] = new ExprManager(threadOptions[i]);
     seqs[i] = seqs[0]->exportTo(exprMgrs[i], *(vmaps[i]) );
@@ -515,14 +523,16 @@ int runCvc4(int argc, char *argv[], Options& options) {
 
   // Create the SmtEngine(s)
   SmtEngine *smts[numThreads];
-  for(int i = 0; i < numThreads; ++i) {
+  for(unsigned i = 0; i < numThreads; ++i) {
     smts[i] = new SmtEngine(exprMgrs[i]);
 
     // Register the statistics registry of the thread
-    string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
-    smts[i]->getStatisticsRegistry()->setName(tag);
-    theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() );
+    string emTag = "ExprManager thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
+    string smtTag = "SmtEngine thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
+    exprMgrs[i]->getStatisticsRegistry()->setName(emTag);
+    smts[i]->getStatisticsRegistry()->setName(smtTag);
     theStatisticsRegistry.registerStat_( exprMgrs[i]->getStatisticsRegistry() );
+    theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() );
   }
 
   /************************* Lemma sharing init ************************/
@@ -532,12 +542,12 @@ int runCvc4(int argc, char *argv[], Options& options) {
 
   if(numThreads == 1) {
     // Disable sharing
-    threadOptions[0].sharingFilterByLength = 0;
+    threadOptions[0].set(options::sharingFilterByLength, 0);
   } else {
     // Setup sharing channels
     const unsigned int sharingChannelSize = 1000000;
 
-    for(int i = 0; i<numThreads; ++i){
+    for(unsigned i = 0; i < numThreads; ++i){
       if(Debug.isOn("channel-empty")) {
         channelsOut[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
         channelsIn[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
@@ -548,14 +558,14 @@ int runCvc4(int argc, char *argv[], Options& options) {
     }
 
     /* Lemma output channel */
-    for(int i = 0; i<numThreads; ++i) {
-      string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
-      threadOptions[i].lemmaOutputChannel =
+    for(unsigned i = 0; i < numThreads; ++i) {
+      string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
+      threadOptions[i].set(options::lemmaOutputChannel,
         new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i],
-                                        vmaps[i]->d_from, vmaps[i]->d_to);
-      threadOptions[i].lemmaInputChannel =
+                                        vmaps[i]->d_from, vmaps[i]->d_to));
+      threadOptions[i].set(options::lemmaInputChannel,
         new PortfolioLemmaInputChannel(tag, channelsIn[i], exprMgrs[i],
-                                       vmaps[i]->d_from, vmaps[i]->d_to);
+                                       vmaps[i]->d_from, vmaps[i]->d_to));
     }
   }
 
@@ -564,7 +574,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
   /* Portfolio */
   boost::function<Result()> fns[numThreads];
 
-  for(int i = 0; i < numThreads; ++i) {
+  for(unsigned i = 0; i < numThreads; ++i) {
     fns[i] = boost::bind(doSmt, boost::ref(*smts[i]), seqs[i], boost::ref(threadOptions[i]));
   }
 
@@ -580,7 +590,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
 
   /************************* Post printing answer ***********************/
 
-  if(options.printWinner){
+  if(opts[options::printWinner]){
     cout << "The winner is #" << winner << endl;
   }
 
@@ -606,29 +616,29 @@ int runCvc4(int argc, char *argv[], Options& options) {
   // Stop timers, enough work done
   s_totalTime.stop();
 
-  if(options.statistics) {
-    pStatistics->flushInformation(*options.err);
+  if(opts[options::statistics]) {
+    pStatistics->flushInformation(*opts[options::err]);
   }
 
-  if(options.separateOutput) {
-    for(int i = 0; i < numThreads; ++i) {
-      *options.out << "--- Output from thread #" << i << " ---" << endl;
-      *options.out << ss_out[i]->str();
+  if(opts[options::separateOutput]) {
+    for(unsigned i = 0; i < numThreads; ++i) {
+      *opts[options::out] << "--- Output from thread #" << i << " ---" << endl;
+      *opts[options::out] << ss_out[i]->str();
     }
   }
 
-  /*if(options.statistics) {
+  /*if(opts[options::statistics]) {
     double totalTime = double(s_totalTime.getData().tv_sec) +
         double(s_totalTime.getData().tv_nsec)/1000000000.0;
     cout.precision(6);
-    *options.err << "real time: " << totalTime << "s\n";
-    int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(options.lemmaOutputChannel)).cnt;
+    *opts[options::err] << "real time: " << totalTime << "s\n";
+    int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(opts[options::lemmaOutputChannel])).cnt;
     int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(threadOptions[1].lemmaOutputChannel)).cnt;
-    *options.err << "lemmas shared by thread #0: " << th0_lemcnt << endl;
-    *options.err << "lemmas shared by thread #1: " << th1_lemcnt << endl;
-    *options.err << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime)
+    *opts[options::err] << "lemmas shared by thread #0: " << th0_lemcnt << endl;
+    *opts[options::err] << "lemmas shared by thread #1: " << th1_lemcnt << endl;
+    *opts[options::err] << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime)
                  << " lem/sec" << endl;
-    *options.err << "winner: #" << (winner == 0 ? 0 : 1) << endl;
+    *opts[options::err] << "winner: #" << (winner == 0 ? 0 : 1) << endl;
   }*/
 
   // destruction is causing segfaults, let us just exit
@@ -663,23 +673,23 @@ namespace CVC4 {
   }
 }
 
-void printUsage(Options& options, bool full) {
+void printUsage(Options& opts, bool full) {
   stringstream ss;
-  ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
+  ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl
       << endl
       << "Without an input file, or with `-', CVC4 reads from standard input." << endl
       << endl
       << "CVC4 options:" << endl;
   if(full) {
-    Options::printUsage( ss.str(), *options.out );
+    Options::printUsage( ss.str(), *opts[options::out] );
   } else {
-    Options::printShortUsage( ss.str(), *options.out );
+    Options::printShortUsage( ss.str(), *opts[options::out] );
   }
 }
 
 /** Executes a command. Deletes the command after execution. */
-static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
-  if( options.parseOnly ) {
+static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) {
+  if( opts[options::parseOnly] ) {
     return true;
   }
 
@@ -691,15 +701,15 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
     for(CommandSequence::iterator subcmd = seq->begin();
         subcmd != seq->end();
         ++subcmd) {
-      status = doCommand(smt, *subcmd, options) && status;
+      status = doCommand(smt, *subcmd, opts) && status;
     }
   } else {
-    if(options.verbosity > 0) {
-      *options.out << "Invoking: " << *cmd << endl;
+    if(opts[options::verbosity] > 0) {
+      *opts[options::out] << "Invoking: " << *cmd << endl;
     }
 
-    if(options.verbosity >= 0) {
-      cmd->invoke(&smt, *options.out);
+    if(opts[options::verbosity] >= 0) {
+      cmd->invoke(&smt, *opts[options::out]);
     } else {
       cmd->invoke(&smt);
     }
@@ -712,48 +722,48 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
 /**** End of code shared with driver.cpp ****/
 
 /** Create the SMT engine and execute the commands */
-Result doSmt(SmtEngine &smt, Command *cmd, Options &options) {
+Result doSmt(SmtEngine &smt, Command *cmd, Options &opts) {
 
   try {
     // For the signal handlers' benefit
-    pOptions = &options;
+    pOptions = &opts;
 
     // Execute the commands
-    bool status = doCommand(smt, cmd, options);
+    bool status = doCommand(smt, cmd, opts);
 
-    // if(options.statistics) {
-    //   smt.getStatisticsRegistry()->flushInformation(*options.err);
-    //   *options.err << "Statistics printing of my thread complete " << endl;
+    // if(opts[options::statistics]) {
+    //   smt.getStatisticsRegistry()->flushInformation(*opts[options::err]);
+    //   *opts[options::err] << "Statistics printing of my thread complete " << endl;
     // }
 
     return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN;
   } catch(OptionException& e) {
-    *pOptions->out << "unknown" << endl;
+    *(*pOptions)[options::out] << "unknown" << endl;
     cerr << "CVC4 Error:" << endl << e << endl;
     printUsage(*pOptions);
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
-    *pOptions->out << "unknown" << endl;
+    *(*pOptions)[options::out] << "unknown" << endl;
 #endif
-    *pOptions->err << "CVC4 Error:" << endl << e << endl;
-    if(pOptions->statistics) {
-      pStatistics->flushInformation(*pOptions->err);
+    *(*pOptions)[options::err] << "CVC4 Error:" << endl << e << endl;
+    if((*pOptions)[options::statistics]) {
+      pStatistics->flushInformation(*(*pOptions)[options::err]);
     }
   }
   return Result::SAT_UNKNOWN;
 }
 
 template<typename T>
-void sharingManager(int numThreads,
+void sharingManager(unsigned numThreads,
                     SharedChannel<T> *channelsOut[], // out and in with respect
                     SharedChannel<T> *channelsIn[],
                     SmtEngine *smts[])  // to smt engines
 {
-  Trace("sharing") << "sharing: thread started " << std::endl;
+  Trace("sharing") << "sharing: thread started " << endl;
   vector <int> cnt(numThreads); // Debug("sharing")
 
   vector< queue<T> > queues;
-  for(int i = 0; i < numThreads; ++i){
+  for(unsigned i = 0; i < numThreads; ++i){
     queues.push_back(queue<T>());
   }
 
@@ -768,7 +778,7 @@ void sharingManager(int numThreads,
 
     boost::this_thread::sleep(boost::posix_time::milliseconds(sharingBroadcastInterval));
 
-    for(int t = 0; t < numThreads; ++t) {
+    for(unsigned t = 0; t < numThreads; ++t) {
 
       if(channelsOut[t]->empty()) continue;      /* No activity on this channel */
 
@@ -784,22 +794,22 @@ void sharingManager(int numThreads,
                          << ". Chunk " << cnt[t] << std :: endl;
       }
 
-      for(int u = 0; u < numThreads; ++u) {
+      for(unsigned u = 0; u < numThreads; ++u) {
         if(u != t){
-          Trace("sharing") << "sharing: adding to queue " << u << std::endl;
+          Trace("sharing") << "sharing: adding to queue " << u << endl;
           queues[u].push(data);
         }
       }/* end of inner for: broadcast activity */
 
     } /* end of outer for: look for activity */
 
-    for(int t = 0; t < numThreads; ++t){
+    for(unsigned t = 0; t < numThreads; ++t){
       /* Alert if channel full, so that we increase sharingChannelSize
          or decrease sharingBroadcastInterval */
       Assert(not channelsIn[t]->full());
 
       while(!queues[t].empty() && !channelsIn[t]->full()){
-        Trace("sharing") << "sharing: pushing on channel " << t << std::endl;
+        Trace("sharing") << "sharing: pushing on channel " << t << endl;
         T data = queues[t].front();
         channelsIn[t]->push(data);
         queues[t].pop();
@@ -807,17 +817,17 @@ void sharingManager(int numThreads,
     }
   } /* end of infinite while */
 
-  Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << std::endl;
+  Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << endl;
 
-  for(int t = 0; t < numThreads; ++t) {
-    Trace("interrupt") << "Interrupting thread #" << t << std::endl;
+  for(unsigned t = 0; t < numThreads; ++t) {
+    Trace("interrupt") << "Interrupting thread #" << t << endl;
     try{
       smts[t]->interrupt();
     }catch(ModalException &e){
       // It's fine, the thread is probably not there.
-      Trace("interrupt") << "Could not interrupt thread #" << t << std::endl;
+      Trace("interrupt") << "Could not interrupt thread #" << t << endl;
     }
   }
 
-  Trace("sharing") << "sharing: Interrupted, exiting." << std::endl;
+  Trace("sharing") << "sharing: Interrupted, exiting." << endl;
 }