Adding listeners to Options.

- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

10 files changed, 399 insertions, 336 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index aa43cff0f..b2dbaf39b 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -22,10 +22,6 @@
 #include <string>
 
 #include "main/main.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
-#include "options/printer_options.h"
-#include "options/smt_options.h"
 #include "smt_util/command.h"
 
 
@@ -55,12 +51,19 @@ CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
   d_smtEngine(new SmtEngine(&exprMgr)),
   d_options(options),
   d_stats("driver"),
-  d_result() {
+  d_result(),
+  d_replayStream(NULL)
+{}
+
+void CommandExecutor::setReplayStream(ExprStream* replayStream) {
+  assert(d_replayStream == NULL);
+  d_replayStream = replayStream;
+  d_smtEngine->setReplayStream(d_replayStream);
 }
 
 bool CommandExecutor::doCommand(Command* cmd)
 {
-  if( d_options[options::parseOnly] ) {
+  if( d_options.getParseOnly() ) {
     return true;
   }
 
@@ -70,15 +73,15 @@ bool CommandExecutor::doCommand(Command* cmd)
     bool status = true;
 
     for(CommandSequence::iterator subcmd = seq->begin();
-        (status || d_options[options::continuedExecution]) && subcmd != seq->end();
+        (status || d_options.getContinuedExecution()) && subcmd != seq->end();
         ++subcmd) {
       status = doCommand(*subcmd);
     }
 
     return status;
   } else {
-    if(d_options[options::verbosity] > 2) {
-      *d_options[options::out] << "Invoking: " << *cmd << std::endl;
+    if(d_options.getVerbosity() > 2) {
+      *d_options.getOut() << "Invoking: " << *cmd << std::endl;
     }
 
     return doCommandSingleton(cmd);
@@ -87,8 +90,8 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  if(d_options[options::statistics]) {
-    flushStatistics(*d_options[options::err]);
+  if(d_options.getStatistics()) {
+    flushStatistics(*d_options.getErr());
   }
   delete d_smtEngine;
   d_smtEngine = new SmtEngine(&d_exprMgr);
@@ -97,8 +100,8 @@ void CommandExecutor::reset()
 bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
-  if(d_options[options::verbosity] >= -1) {
-    status = smtEngineInvoke(d_smtEngine, cmd, d_options[options::out]);
+  if(d_options.getVerbosity() >= -1) {
+    status = smtEngineInvoke(d_smtEngine, cmd, d_options.getOut());
   } else {
     status = smtEngineInvoke(d_smtEngine, cmd, NULL);
   }
@@ -113,42 +116,53 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_result = res = q->getResult();
   }
 
-  if((cs != NULL || q != NULL) && d_options[options::statsEveryQuery]) {
+  if((cs != NULL || q != NULL) && d_options.getStatsEveryQuery()) {
     std::ostringstream ossCurStats;
     flushStatistics(ossCurStats);
-    printStatsIncremental(*d_options[options::err], d_lastStatistics, ossCurStats.str());
+    std::ostream& err = *d_options.getErr();
+    printStatsIncremental(err, d_lastStatistics, ossCurStats.str());
     d_lastStatistics = ossCurStats.str();
   }
 
   // dump the model/proof/unsat core if option is set
   if(status) {
     Command* g = NULL;
-    if( d_options[options::produceModels] &&
-        d_options[options::dumpModels] &&
+    if( d_options.getProduceModels() &&
+        d_options.getDumpModels() &&
         ( res.asSatisfiabilityResult() == Result::SAT ||
           (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
       g = new GetModelCommand();
     }
-    if( d_options[options::proof] &&
-        d_options[options::dumpProofs] &&
+    if( d_options.getProof() &&
+        d_options.getDumpProofs() &&
         res.asSatisfiabilityResult() == Result::UNSAT ) {
       g = new GetProofCommand();
     }
-    if( d_options[options::dumpInstantiations] &&
-        ( ( d_options[options::instFormatMode] != INST_FORMAT_MODE_SZS &&
-            ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) ||
-          res.asSatisfiabilityResult() == Result::UNSAT ) ) {
+
+    if( d_options.getDumpInstantiations() &&
+        ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS &&
+            ( res.asSatisfiabilityResult() == Result::SAT ||
+              (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) ||
+          res.asSatisfiabilityResult() == Result::UNSAT ) )
+    {
       g = new GetInstantiationsCommand();
     }
-    if( d_options[options::dumpSynth] && res.asSatisfiabilityResult() == Result::UNSAT ){
+
+    if( d_options.getDumpSynth() &&
+        res.asSatisfiabilityResult() == Result::UNSAT )
+    {
       g = new GetSynthSolutionCommand();
     }
-    if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) {
+
+    if( d_options.getDumpUnsatCores() &&
+        res.asSatisfiabilityResult() == Result::UNSAT )
+    {
       g = new GetUnsatCoreCommand();
     }
+
     if(g != NULL) {
       // set no time limit during dumping if applicable
-      if( d_options[options::forceNoLimitCpuWhileDump] ){
+      if( d_options.getForceNoLimitCpuWhileDump() ){
         setNoLimitCPU();
       }
       status = doCommandSingleton(g);
@@ -165,7 +179,9 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
     cmd->invoke(smt, *out);
   }
   // ignore the error if the command-verbosity is 0 for this command
-  if(smt->getOption(std::string("command-verbosity:") + cmd->getCommandName()).getIntegerValue() == 0) {
+  std::string commandName =
+      std::string("command-verbosity:") + cmd->getCommandName();
+  if(smt->getOption(commandName).getIntegerValue() == 0) {
     return true;
   }
   return !cmd->fail();
@@ -223,5 +239,51 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
   }
 }
 
+void CommandExecutor::printStatsFilterZeros(std::ostream& out,
+                                            const std::string& statsString) {
+  // read each line, if a number, check zero and skip if so
+  // Stat are assumed to one-per line: "<statName>, <statValue>"
+
+  std::istringstream iss(statsString);
+  std::string statName, statValue;
+
+  std::getline(iss, statName, ',');
+
+  while( !iss.eof() ) {
+
+    std::getline(iss, statValue, '\n');
+
+    double curFloat;
+    bool isFloat = (std::istringstream(statValue) >> curFloat);
+
+    if( (isFloat && curFloat == 0) ||
+        statValue == " \"0\"" ||
+        statValue == " \"[]\"") {
+      // skip
+    } else {
+      out << statName << "," << statValue << std::endl;
+    }
+
+    std::getline(iss, statName, ',');
+  }
+
+}
+
+void CommandExecutor::flushOutputStreams() {
+  if(d_options.getStatistics()) {
+    if(d_options.getStatsHideZeros() == false) {
+      flushStatistics(*(d_options.getErr()));
+    } else {
+      std::ostringstream ossStats;
+      flushStatistics(ossStats);
+      printStatsFilterZeros(*(d_options.getErr()), ossStats.str());
+    }
+  }
+
+  // make sure out and err streams are flushed too
+  d_options.flushOut();
+  d_options.flushErr();
+}
+
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 7b6c2fab5..03bbe661b 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -37,12 +37,16 @@ protected:
   Options& d_options;
   StatisticsRegistry d_stats;
   Result d_result;
+  ExprStream* d_replayStream;
 
 public:
   CommandExecutor(ExprManager &exprMgr, Options &options);
 
   virtual ~CommandExecutor() {
     delete d_smtEngine;
+    if(d_replayStream != NULL){
+      delete d_replayStream;
+    }
   }
 
   /**
@@ -65,7 +69,13 @@ public:
     d_stats.flushInformation(out);
   }
 
-  SmtGlobals* globals() { return d_smtEngine->globals(); }
+  static void printStatsFilterZeros(std::ostream& out,
+                                    const std::string& statsString);
+
+  LemmaChannels* channels() { return d_smtEngine->channels(); }
+  void flushOutputStreams();
+
+  void setReplayStream(ExprStream* replayStream);
 
 protected:
   /** Executes treating cmd as a singleton */
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 9d0042694..bf1143647 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -31,12 +31,8 @@
 #include "expr/pickler.h"
 #include "main/main.h"
 #include "main/portfolio.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
 #include "options/options.h"
-#include "options/printer_options.h"
 #include "options/set_language.h"
-#include "options/smt_options.h"
 #include "smt_util/command.h"
 
 
@@ -45,25 +41,26 @@ using namespace std;
 namespace CVC4 {
 namespace main {
 
-CommandExecutorPortfolio::CommandExecutorPortfolio
-(ExprManager &exprMgr, Options &options, vector<Options>& tOpts):
-  CommandExecutor(exprMgr, options),
-  d_numThreads(options[options::threads]),
-  d_smts(),
-  d_seq(new CommandSequence()),
-  d_threadOptions(tOpts),
-  d_vmaps(),
-  d_lastWinner(0),
-  d_channelsOut(),
-  d_channelsIn(),
-  d_ostringstreams(),
-  d_statLastWinner("portfolio::lastWinner"),
-  d_statWaitTime("portfolio::waitTime")
+CommandExecutorPortfolio::CommandExecutorPortfolio(
+    ExprManager &exprMgr, Options &options, OptionsList& tOpts)
+    : CommandExecutor(exprMgr, options),
+      d_numThreads(options.getThreads()),
+      d_smts(),
+      d_seq(new CommandSequence()),
+      d_threadOptions(tOpts),
+      d_vmaps(),
+      d_lastWinner(0),
+      d_channelsOut(),
+      d_channelsIn(),
+      d_ostringstreams(),
+      d_statLastWinner("portfolio::lastWinner"),
+      d_statWaitTime("portfolio::waitTime")
 {
   assert(d_threadOptions.size() == d_numThreads);
 
   d_statLastWinner.setData(d_lastWinner);
   d_stats.registerStat(&d_statLastWinner);
+
   d_stats.registerStat(&d_statWaitTime);
 
   /* Duplication, individualization */
@@ -111,7 +108,7 @@ void CommandExecutorPortfolio::lemmaSharingInit()
 
   if(d_numThreads == 1) {
     // Disable sharing
-    d_threadOptions[0].set(options::sharingFilterByLength, 0);
+    d_threadOptions[0].setSharingFilterByLength(0);
   } else {
     // Setup sharing channels
     const unsigned int sharingChannelSize = 1000000;
@@ -125,34 +122,34 @@ void CommandExecutorPortfolio::lemmaSharingInit()
 
     /* Lemma I/O channels */
     for(unsigned i = 0; i < d_numThreads; ++i) {
-      string tag = "thread #" +
-        boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+      int thread_id = d_threadOptions[i].getThreadId();
+      string tag = "thread #" + boost::lexical_cast<string>(thread_id);
       LemmaOutputChannel* outputChannel =
           new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i],
                                           d_vmaps[i]->d_from, d_vmaps[i]->d_to);
       LemmaInputChannel* inputChannel =
           new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i],
                                          d_vmaps[i]->d_from, d_vmaps[i]->d_to);
-      d_smts[i]->globals()->setLemmaInputChannel(inputChannel);
-      d_smts[i]->globals()->setLemmaOutputChannel(outputChannel);
+      d_smts[i]->channels()->setLemmaInputChannel(inputChannel);
+      d_smts[i]->channels()->setLemmaOutputChannel(outputChannel);
     }
 
     /* Output to string stream  */
     assert(d_ostringstreams.size() == 0);
     for(unsigned i = 0; i < d_numThreads; ++i) {
       d_ostringstreams.push_back(new ostringstream);
-      d_threadOptions[i].set(options::out, d_ostringstreams[i]);
+      d_threadOptions[i].setOut(d_ostringstreams[i]);
 
+      OutputLanguage outputLanguage = d_threadOptions[i].getOutputLanguage();
       // important even for muzzled builds (to get result output right)
-      *d_threadOptions[i][options::out]
-        << language::SetLanguage(d_threadOptions[i][options::outputLanguage]);
+      *(d_threadOptions[i].getOut()) << language::SetLanguage(outputLanguage);
     }
   }
 }/* CommandExecutorPortfolio::lemmaSharingInit() */
 
 void CommandExecutorPortfolio::lemmaSharingCleanup()
 {
-  assert(d_numThreads == d_options[options::threads]);
+  assert(d_numThreads == d_options.getThreads());
 
   if(d_numThreads == 1)
     return;
@@ -163,10 +160,10 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
   for(unsigned i = 0; i < d_numThreads; ++i) {
     delete d_channelsIn[i];
     delete d_channelsOut[i];
-    delete d_smts[i]->globals()->getLemmaInputChannel();
-    d_smts[i]->globals()->setLemmaInputChannel(NULL);
-    delete d_smts[i]->globals()->getLemmaOutputChannel();
-    d_smts[i]->globals()->setLemmaOutputChannel(NULL);
+    delete d_smts[i]->channels()->getLemmaInputChannel();
+    d_smts[i]->channels()->setLemmaInputChannel(NULL);
+    delete d_smts[i]->channels()->getLemmaOutputChannel();
+    d_smts[i]->channels()->setLemmaOutputChannel(NULL);
   }
   d_channelsIn.clear();
   d_channelsOut.clear();
@@ -175,7 +172,7 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
   if(d_ostringstreams.size() != 0) {
     assert(d_ostringstreams.size() == d_numThreads);
     for(unsigned i = 0; i < d_numThreads; ++i) {
-      d_threadOptions[i].set(options::out, d_options[options::out]);
+      d_threadOptions[i].setOut(d_options.getOut());
       delete d_ostringstreams[i];
     }
     d_ostringstreams.clear();
@@ -225,9 +222,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     Command* cmdExported =
       d_lastWinner == 0 ?
       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
-    bool ret = smtEngineInvoke(d_smts[d_lastWinner],
-                               cmdExported,
-                               d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
+    std::ostream* winnersOut =  d_options.getVerbosity() >= -1 ?
+        (d_threadOptions[d_lastWinner]).getOut() : NULL;
+    bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, winnersOut);
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else if(mode == 1) {               // portfolio
@@ -260,13 +257,15 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
           cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) :
           d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
       } catch(ExportUnsupportedException& e) {
-        if(d_options[options::fallbackSequential]) {
-          Notice() << "Unsupported theory encountered, switching to sequential mode.";
+        if(d_options.getFallbackSequential()) {
+          Notice() << "Unsupported theory encountered."
+                   << "Switching to sequential mode.";
           return CommandExecutor::doCommandSingleton(cmd);
         }
         else
-          throw Exception("Certain theories (e.g., datatypes) are (currently) unsupported in portfolio\n"
-                          "mode. Please see option --fallback-sequential to make this a soft error.");
+          throw Exception("Certain theories (e.g., datatypes) are (currently)"
+                          " unsupported in portfolio\n mode. Please see option"
+                          " --fallback-sequential to make this a soft error.");
       }
     }
 
@@ -289,11 +288,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     /* Portfolio */
     boost::function<bool()>* fns = new boost::function<bool()>[d_numThreads];
     for(unsigned i = 0; i < d_numThreads; ++i) {
-      fns[i] = boost::bind(smtEngineInvoke,
-                           d_smts[i],
-                           seqs[i],
-                           d_options[options::verbosity] >= -1 ? d_threadOptions[i][options::out] : NULL
-                           );
+      std::ostream* current_out_or_null = d_options.getVerbosity() >= -1 ?
+          d_threadOptions[i].getOut() : NULL;
+
+      fns[i] = boost::bind(smtEngineInvoke, d_smts[i], seqs[i],
+                           current_out_or_null);
     }
 
     assert(d_channelsIn.size() == d_numThreads
@@ -311,12 +310,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
                          &d_channelsIn[0],
                          &d_smts[0]);
 
-    size_t threadStackSize = d_options[options::threadStackSize];
+    size_t threadStackSize = d_options.getThreadStackSize();
     threadStackSize *= 1024 * 1024;
 
     pair<int, bool> portfolioReturn =
         runPortfolio(d_numThreads, smFn, fns, threadStackSize,
-                     d_options[options::waitToJoin], d_statWaitTime);
+                     d_options.getWaitToJoin(), d_statWaitTime);
 
 #ifdef CVC4_STATISTICS_ON
     assert( d_statWaitTime.running() );
@@ -327,25 +326,24 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     d_result = d_smts[d_lastWinner]->getStatusOfLastCommand();
 
     if(d_ostringstreams.size() != 0) {
-      assert(d_numThreads == d_options[options::threads]);
+      assert(d_numThreads == d_options.getThreads());
       assert(portfolioReturn.first >= 0);
       assert(unsigned(portfolioReturn.first) < d_numThreads);
 
+      std::ostream& out = *d_options.getOut();
       if(Debug.isOn("treat-unknown-error")) {
         if(d_ostringstreams[portfolioReturn.first]->str() == "unknown\n") {
-          *d_options[options::out]
-            << "portfolioReturn = (" << portfolioReturn.first << ", " << portfolioReturn.second
-            << ")\n";
+          out << "portfolioReturn = (" << portfolioReturn.first << ", "
+              << portfolioReturn.second << ")\n";
           for(unsigned i = 0; i < d_numThreads; ++i)
-            *d_options[options::out]
-              << "thread " << i << ": " << d_ostringstreams[i]->str() << std::endl;
+            out << "thread " << i << ": " << d_ostringstreams[i]->str()
+                << std::endl;
           throw Exception("unknown encountered");
         }
       }
 
-      *d_options[options::out]
-        << d_ostringstreams[portfolioReturn.first]->str()
-        << std::flush;
+      out << d_ostringstreams[portfolioReturn.first]->str()
+          << std::flush;
 
 #ifdef CVC4_COMPETITION_MODE
       // We use CVC4 in competition with --no-wait-to-join. If
@@ -366,27 +364,32 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     // dump the model/proof/unsat core if option is set
     if(status) {
-      if( d_options[options::produceModels] &&
-          d_options[options::dumpModels] &&
+      if( d_options.getProduceModels() &&
+          d_options.getDumpModels() &&
           ( d_result.asSatisfiabilityResult() == Result::SAT ||
-            (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) {
+            (d_result.isUnknown() &&
+             d_result.whyUnknown() == Result::INCOMPLETE) ) )
+      {
         Command* gm = new GetModelCommand();
         status = doCommandSingleton(gm);
-      } else if( d_options[options::proof] &&
-                 d_options[options::dumpProofs] &&
+      } else if( d_options.getProof() &&
+                 d_options.getDumpProofs() &&
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
         Command* gp = new GetProofCommand();
         status = doCommandSingleton(gp);
-      } else if( d_options[options::dumpInstantiations] &&
-                 ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && 
-                   ( d_result.asSatisfiabilityResult() == Result::SAT || (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) || 
-                 d_result.asSatisfiabilityResult() == Result::UNSAT ) ) {
+      } else if( d_options.getDumpInstantiations() &&
+                 ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS &&
+                   ( d_result.asSatisfiabilityResult() == Result::SAT ||
+                     (d_result.isUnknown() &&
+                      d_result.whyUnknown() == Result::INCOMPLETE) ) ) ||
+                   d_result.asSatisfiabilityResult() == Result::UNSAT ) ) {
         Command* gi = new GetInstantiationsCommand();
         status = doCommandSingleton(gi);
-      } else if( d_options[options::dumpSynth] && d_result.asSatisfiabilityResult() == Result::UNSAT ){
+      } else if( d_options.getDumpSynth() &&
+                 d_result.asSatisfiabilityResult() == Result::UNSAT ){
         Command* gi = new GetSynthSolutionCommand();
         status = doCommandSingleton(gi);
-      } else if( d_options[options::dumpUnsatCores] &&
+      } else if( d_options.getDumpUnsatCores() &&
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
         Command* guc = new GetUnsatCoreCommand();
         status = doCommandSingleton(guc);
@@ -395,13 +398,15 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     return status;
   } else if(mode == 2) {
-    Command* cmdExported =
-      d_lastWinner == 0 ?
-      cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
-    bool ret = smtEngineInvoke(d_smts[d_lastWinner],
-                               cmdExported,
-                               d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
-    if(d_lastWinner != 0) delete cmdExported;
+    Command* cmdExported = d_lastWinner == 0 ?
+        cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]));
+    std::ostream* winner_out_if_verbose = d_options.getVerbosity() >= -1 ?
+        d_threadOptions[d_lastWinner].getOut() : NULL;
+    bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported,
+                               winner_out_if_verbose);
+    if(d_lastWinner != 0){
+      delete cmdExported;
+    }
     return ret;
   } else {
     // Unreachable();
@@ -412,16 +417,17 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 }/* CommandExecutorPortfolio::doCommandSingleton() */
 
 void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
-  assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
+  assert(d_numThreads == d_exprMgrs.size() &&
+         d_exprMgrs.size() == d_smts.size());
   for(size_t i = 0; i < d_numThreads; ++i) {
     string emTag = "thread#"
-      + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+        + boost::lexical_cast<string>(d_threadOptions[i].getThreadId());
     Statistics stats = d_exprMgrs[i]->getStatistics();
     stats.setPrefix(emTag);
     stats.flushInformation(out);
 
     string smtTag = "thread#"
-      + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+        + boost::lexical_cast<string>(d_threadOptions[i].getThreadId());
     stats = d_smts[i]->getStatistics();
     stats.setPrefix(smtTag);
     stats.flushInformation(out);
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index ee2b270fb..ce9a80a4e 100644
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -40,7 +40,7 @@ class CommandExecutorPortfolio : public CommandExecutor {
                                  // not too hard to support this changing
   std::vector<SmtEngine*> d_smts;
   CommandSequence* d_seq;
-  std::vector<Options>& d_threadOptions;
+  OptionsList& d_threadOptions;
   std::vector<ExprManagerMapCollection*> d_vmaps;
 
   int d_lastWinner;
@@ -57,7 +57,7 @@ class CommandExecutorPortfolio : public CommandExecutor {
 public:
   CommandExecutorPortfolio(ExprManager &exprMgr,
                            Options &options,
-                           std::vector<Options>& tOpts);
+                           OptionsList& tOpts);
 
   ~CommandExecutorPortfolio();
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 71f47906d..83b85c170 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -25,6 +25,7 @@
 // This must come before PORTFOLIO_BUILD.
 #include "cvc4autoconfig.h"
 
+#include "base/configuration.h"
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
 #include "expr/expr_manager.h"
@@ -36,18 +37,12 @@
 
 #include "main/interactive_shell.h"
 #include "main/main.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
 #include "options/options.h"
-#include "options/quantifiers_options.h"
 #include "options/set_language.h"
-#include "options/smt_options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
-#include "smt/smt_options_handler.h"
 #include "smt_util/command.h"
-#include "util/configuration.h"
 #include "util/result.h"
 #include "util/statistics_registry.h"
 
@@ -79,47 +74,18 @@ namespace CVC4 {
 
 void printUsage(Options& opts, bool full) {
   stringstream ss;
-  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;
+  ss << "usage: " << opts.getBinaryName() << " [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(), *opts[options::out] );
+    Options::printUsage( ss.str(), *(opts.getOut()) );
   } else {
-    Options::printShortUsage( ss.str(), *opts[options::out] );
+    Options::printShortUsage( ss.str(), *(opts.getOut()) );
   }
 }
 
-void printStatsFilterZeros(std::ostream& out, const std::string& statsString) {
-  // read each line, if a number, check zero and skip if so
-  // Stat are assumed to one-per line: "<statName>, <statValue>"
-
-  std::istringstream iss(statsString);
-  std::string statName, statValue;
-
-  std::getline(iss, statName, ',');
-
-  while( !iss.eof() ) {
-
-    std::getline(iss, statValue, '\n');
-
-    double curFloat;
-    bool isFloat = (std::istringstream(statValue) >> curFloat);
-
-    if( (isFloat && curFloat == 0) ||
-        statValue == " \"0\"" ||
-        statValue == " \"[]\"") {
-      // skip
-    } else {
-      out << statName << "," << statValue << std::endl;
-    }
-
-    std::getline(iss, statName, ',');
-  }
-
-}
-
 int runCvc4(int argc, char* argv[], Options& opts) {
 
   // Timer statistic
@@ -134,38 +100,35 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   progPath = argv[0];
 
-#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij."
-  smt::SmtOptionsHandler optionsHandler(NULL);
-
   // Parse the options
-  vector<string> filenames = opts.parseOptions(argc, argv, &optionsHandler);
+  vector<string> filenames = opts.parseOptions(argc, argv);
 
 # ifndef PORTFOLIO_BUILD
-  if( opts.wasSetByUser(options::threads) ||
-      opts.wasSetByUser(options::threadStackSize) ||
-      ! opts[options::threadArgv].empty() ) {
+  if( opts.wasSetByUserThreads() ||
+      opts.wasSetByUserThreadStackSize() ||
+      (! opts.getThreadArgv().empty()) ) {
     throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
   }
 # endif
 
-  progName = opts[options::binary_name].c_str();
+  progName = opts.getBinaryName().c_str();
 
-  if( opts[options::help] ) {
+  if( opts.getHelp() ) {
     printUsage(opts, true);
     exit(1);
-  } else if( opts[options::languageHelp] ) {
-    Options::printLanguageHelp(*opts[options::out]);
+  } else if( opts.getLanguageHelp() ) {
+    Options::printLanguageHelp(*(opts.getOut()));
     exit(1);
-  } else if( opts[options::version] ) {
-    *opts[options::out] << Configuration::about().c_str() << flush;
+  } else if( opts.getVersion() ) {
+    *(opts.getOut()) << Configuration::about().c_str() << flush;
     exit(0);
   }
 
-  segvSpin = opts[options::segvSpin];
+  segvSpin = opts.getSegvSpin();
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC4_COMPETITION_MODE
-  *opts[options::out] << unitbuf;
+  *(opts.getOut()) << unitbuf;
 #endif /* CVC4_COMPETITION_MODE */
 
   // We only accept one input file
@@ -177,66 +140,66 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 
   // if we're reading from stdin on a TTY, default to interactive mode
-  if(!opts.wasSetByUser(options::interactive)) {
-    opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin)));
+  if(!opts.wasSetByUserInteractive()) {
+    opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
   }
 
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str();
 
-  if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
+  if(opts.getInputLanguage() == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      opts.set(options::inputLanguage, language::input::LANG_CVC4);
+      opts.setInputLanguage(language::input::LANG_CVC4);
     } else {
       unsigned len = strlen(filename);
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2_0);
+        opts.setInputLanguage(language::input::LANG_SMTLIB_V2_0);
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
+        opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
       } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
+        opts.setInputLanguage(language::input::LANG_SMTLIB_V1);
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        opts.set(options::inputLanguage, language::input::LANG_TPTP);
+        opts.setInputLanguage(language::input::LANG_TPTP);
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        opts.set(options::inputLanguage, language::input::LANG_CVC4);
+        opts.setInputLanguage(language::input::LANG_CVC4);
       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
-        opts.set(options::inputLanguage, language::input::LANG_SYGUS);
+        opts.setInputLanguage(language::input::LANG_SYGUS);
         //since there is no sygus output language, set this to SMT lib 2
-        //opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2_0);
+        //opts.setOutputLanguage(language::output::LANG_SMTLIB_V2_0);
       }
     }
   }
 
-  if(opts[options::outputLanguage] == language::output::LANG_AUTO) {
-    opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage]));
+  if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
+    opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
   }
 
   // if doing sygus, turn on CEGQI by default
-  if(opts[options::inputLanguage] == language::input::LANG_SYGUS ){
-    if( !opts.wasSetByUser(options::ceGuidedInst)) {
-      opts.set(options::ceGuidedInst, true);
+  if(opts.getInputLanguage() == language::input::LANG_SYGUS ){
+    if( !opts.wasSetByUserCeGuidedInst()) {
+      opts.setCeGuidedInst(true);
     }
-    if( !opts.wasSetByUser(options::dumpSynth)) {
-      opts.set(options::dumpSynth, true);
+    if( !opts.wasSetByUserDumpSynth()) {
+      opts.setDumpSynth(true);
     }
   }
 
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
-    DebugChannel.setStream(CVC4::null_os);
-    TraceChannel.setStream(CVC4::null_os);
-    NoticeChannel.setStream(CVC4::null_os);
-    ChatChannel.setStream(CVC4::null_os);
-    MessageChannel.setStream(CVC4::null_os);
-    WarningChannel.setStream(CVC4::null_os);
+    DebugChannel.setStream(&CVC4::null_os);
+    TraceChannel.setStream(&CVC4::null_os);
+    NoticeChannel.setStream(&CVC4::null_os);
+    ChatChannel.setStream(&CVC4::null_os);
+    MessageChannel.setStream(&CVC4::null_os);
+    WarningChannel.setStream(&CVC4::null_os);
   }
 
   // important even for muzzled builds (to get result output right)
-  *opts[options::out] << language::SetLanguage(opts[options::outputLanguage]);
+  (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 
   // Create the expression manager using appropriate options
   ExprManager* exprMgr;
@@ -244,20 +207,24 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   exprMgr = new ExprManager(opts);
   pExecutor = new CommandExecutor(*exprMgr, opts);
 # else
-  vector<Options> threadOpts = parseThreadSpecificOptions(opts);
+  OptionsList threadOpts;
+  parseThreadSpecificOptions(threadOpts, opts);
+
   bool useParallelExecutor = true;
   // incremental?
-  if(opts.wasSetByUser(options::incrementalSolving) &&
-     opts[options::incrementalSolving] &&
-     !opts[options::incrementalParallel]) {
-    Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n"
+  if(opts.wasSetByUserIncrementalSolving() &&
+     opts.getIncrementalSolving() &&
+     (! opts.getIncrementalParallel()) ) {
+    Notice() << "Notice: In --incremental mode, using the sequential solver"
+             << " unless forced by...\n"
              << "Notice: ...the experimental --incremental-parallel option.\n";
     useParallelExecutor = false;
   }
   // proofs?
-  if(opts[options::checkProofs]) {
-    if(opts[options::fallbackSequential]) {
-      Warning() << "Warning: Falling back to sequential mode, as cannot run portfolio in check-proofs mode.\n";
+  if(opts.getCheckProofs()) {
+    if(opts.getFallbackSequential()) {
+      Warning() << "Warning: Falling back to sequential mode, as cannot run"
+                << " portfolio in check-proofs mode.\n";
       useParallelExecutor = false;
     }
     else {
@@ -275,41 +242,41 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 # endif
 
   Parser* replayParser = NULL;
-  if( opts[options::replayFilename] != "" ) {
-    ParserBuilder replayParserBuilder(exprMgr, opts[options::replayFilename], opts);
+  if( opts.getReplayInputFilename() != "" ) {
+    std::string replayFilename = opts.getReplayInputFilename();
+    ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts);
 
-    if( opts[options::replayFilename] == "-") {
+    if( replayFilename == "-") {
       if( inputFromStdin ) {
         throw OptionException("Replay file and input file can't both be stdin.");
       }
       replayParserBuilder.withStreamInput(cin);
     }
     replayParser = replayParserBuilder.build();
-    pExecutor->globals()->setReplayStream(new Parser::ExprStream(replayParser));
-  }
-  if( pExecutor->globals()->getReplayLog() != NULL ) {
-    *(pExecutor->globals()->getReplayLog()) <<
-        language::SetLanguage(opts[options::outputLanguage]) << expr::ExprSetDepth(-1);
+    pExecutor->setReplayStream(new Parser::ExprStream(replayParser));
   }
 
   int returnValue = 0;
   {
     // Timer statistic
-    RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), pTotalTime);
+    RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(),
+                                    pTotalTime);
 
     // Filename statistics
     ReferenceStat< const char* > s_statFilename("filename", filename);
-    RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename);
+    RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
+                                      &s_statFilename);
 
     // Parse and execute commands until we are done
     Command* cmd;
     bool status = true;
-    if(opts[options::interactive] && inputFromStdin) {
-      if(opts[options::tearDownIncremental] > 0) {
-        throw OptionException("--tear-down-incremental doesn't work in interactive mode");
+    if(opts.getInteractive() && inputFromStdin) {
+      if(opts.getTearDownIncremental() > 0) {
+        throw OptionException(
+            "--tear-down-incremental doesn't work in interactive mode");
       }
 #ifndef PORTFOLIO_BUILD
-      if(!opts.wasSetByUser(options::incrementalSolving)) {
+      if(!opts.wasSetByUserIncrementalSolving()) {
         cmd = new SetOptionCommand("incremental", SExpr(true));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
@@ -317,7 +284,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       }
 #endif /* PORTFOLIO_BUILD */
       InteractiveShell shell(*exprMgr, opts);
-      if(opts[options::interactivePrompt]) {
+      if(opts.getInteractivePrompt()) {
         Message() << Configuration::getPackageName()
                   << " " << Configuration::getVersionString();
         if(Configuration::isGitBuild()) {
@@ -339,7 +306,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         try {
           cmd = shell.readCommand();
         } catch(UnsafeInterruptException& e) {
-          *opts[options::out] << CommandInterrupted();
+          (*opts.getOut()) << CommandInterrupted();
           break;
         }
         if (cmd == NULL)
@@ -351,14 +318,15 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         }
         delete cmd;
       }
-    } else if(opts[options::tearDownIncremental] > 0) {
-      if(!opts[options::incrementalSolving]) {
+    } else if( opts.getTearDownIncremental() > 0) {
+      if(!opts.getIncrementalSolving()) {
         cmd = new SetOptionCommand("incremental", SExpr(true));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
         delete cmd;
-        // if(opts.wasSetByUser(options::incrementalSolving)) {
-        //   throw OptionException("--tear-down-incremental incompatible with --incremental");
+        // if(opts.wasSetByUserIncrementalSolving()) {
+        //   throw OptionException(
+        //     "--tear-down-incremental incompatible with --incremental");
         // }
 
         // cmd = new SetOptionCommand("incremental", SExpr(false));
@@ -387,9 +355,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       int needReset = 0;
       // true if one of the commands was interrupted
       bool interrupted = false;
-      while (status || opts[options::continuedExecution]) {
+      while (status || opts.getContinuedExecution()) {
         if (interrupted) {
-          *opts[options::out] << CommandInterrupted();
+          (*opts.getOut()) << CommandInterrupted();
           break;
         }
 
@@ -402,11 +370,12 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         }
 
         if(dynamic_cast<PushCommand*>(cmd) != NULL) {
-          if(needReset >= opts[options::tearDownIncremental]) {
+          if(needReset >= opts.getTearDownIncremental()) {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
               if (interrupted) break;
-              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
+              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
+              {
                 Command* cmd = allCommands[i][j]->clone();
                 cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
@@ -428,10 +397,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           }
         } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
           allCommands.pop_back(); // fixme leaks cmds here
-          if (needReset >= opts[options::tearDownIncremental]) {
+          if (needReset >= opts.getTearDownIncremental()) {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
-              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
+              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
+              {
                 Command* cmd = allCommands[i][j]->clone();
                 cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
@@ -442,7 +412,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
               }
             }
             if (interrupted) continue;
-            *opts[options::out] << CommandSuccess();
+            (*opts.getOut()) << CommandSuccess();
             needReset = 0;
           } else {
             status = pExecutor->doCommand(cmd);
@@ -453,10 +423,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           }
         } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
                   dynamic_cast<QueryCommand*>(cmd) != NULL) {
-          if(needReset >= opts[options::tearDownIncremental]) {
+          if(needReset >= opts.getTearDownIncremental()) {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
-              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
+              for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
+              {
                 Command* cmd = allCommands[i][j]->clone();
                 cmd->setMuted(true);
                 pExecutor->doCommand(cmd);
@@ -516,7 +487,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       // Remove the parser
       delete parser;
     } else {
-      if(!opts.wasSetByUser(options::incrementalSolving)) {
+      if(!opts.wasSetByUserIncrementalSolving()) {
         cmd = new SetOptionCommand("incremental", SExpr(false));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
@@ -539,9 +510,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         replayParser->useDeclarationsFrom(parser);
       }
       bool interrupted = false;
-      while(status || opts[options::continuedExecution]) {
+      while(status || opts.getContinuedExecution()) {
         if (interrupted) {
-          *opts[options::out] << CommandInterrupted();
+          (*opts.getOut()) << CommandInterrupted();
           pExecutor->reset();
           break;
         }
@@ -569,13 +540,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       delete parser;
     }
 
-    if( pExecutor->globals()->getReplayStream() != NULL ) {
-      ExprStream* replayStream = pExecutor->globals()->getReplayStream();
-      pExecutor->globals()->setReplayStream(NULL);
-      // this deletes the expression parser too
-      delete replayStream;
-    }
-
     Result result;
     if(status) {
       result = pExecutor->getResult();
@@ -586,7 +550,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     }
 
 #ifdef CVC4_COMPETITION_MODE
-    *opts[options::out] << flush;
+    opts.flushOut();
     // exit, don't return (don't want destructors to run)
     // _exit() from unistd.h doesn't run global destructors
     // or other on_exit/atexit stuff.
@@ -594,37 +558,22 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 #endif /* CVC4_COMPETITION_MODE */
 
     ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-    RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult);
+    RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(),
+                                       &s_statSatResult);
 
     pTotalTime->stop();
 
+    // Tim: I think that following comment is out of date?
     // Set the global executor pointer to NULL first.  If we get a
     // signal while dumping statistics, we don't want to try again.
-    if(opts[options::statistics]) {
-      if(opts[options::statsHideZeros] == false) {
-        pExecutor->flushStatistics(*opts[options::err]);
-      } else {
-        std::ostringstream ossStats;
-        pExecutor->flushStatistics(ossStats);
-        printStatsFilterZeros(*opts[options::err], ossStats.str());
-      }
-    }
-
-    // make sure to flush replay output log before early-exit
-    if( pExecutor->globals()->getReplayLog() != NULL ) {
-      *(pExecutor->globals()->getReplayLog()) << flush;
-    }
-
-    // make sure out and err streams are flushed too
-    *opts[options::out] << flush;
-    *opts[options::err] << flush;
+    pExecutor->flushOutputStreams();
 
 #ifdef CVC4_DEBUG
-    if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
+    if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) {
       _exit(returnValue);
     }
 #else /* CVC4_DEBUG */
-    if(opts[options::earlyExit]) {
+    if(opts.getEarlyExit()) {
       _exit(returnValue);
     }
 #endif /* CVC4_DEBUG */
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 6888d3af5..19e4859b0 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -40,10 +40,7 @@
 
 #include "base/output.h"
 #include "options/language.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
 #include "options/options.h"
-#include "options/smt_options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -92,16 +89,18 @@ static set<string> s_declarations;
 #endif /* HAVE_LIBREADLINE */
 
 InteractiveShell::InteractiveShell(ExprManager& exprManager,
-                                   const Options& options) :
-  d_in(*options[options::in]),
-  d_out(*options[options::out]),
-  d_options(options),
-  d_quit(false) {
+                                   const Options& options)
+    : d_in(*options.getIn()),
+      d_out(*options.getOutConst()),
+      d_options(options),
+      d_quit(false)
+{
   ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
-  if(d_options.wasSetByUser(options::forceLogic)) {
-    d_parser->forceLogic(d_options[options::forceLogic]->getLogicString());
+  if(d_options.wasSetByUserForceLogicString()) {
+    LogicInfo tmp(d_options.getForceLogicString());
+    d_parser->forceLogic(tmp.getLogicString());
   }
 
 #if HAVE_LIBREADLINE
@@ -114,7 +113,8 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
 #endif /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
-    switch(OutputLanguage lang = toOutputLanguage(d_options[options::inputLanguage])) {
+    OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
+    switch(lang) {
     case output::LANG_CVC4:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
       commandsBegin = cvc_commands;
@@ -195,7 +195,8 @@ restart:
   /* Prompt the user for input. */
   if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-    lineBuf = ::readline(d_options[options::interactivePrompt] ? (line == "" ? "CVC4> " : "... > ") : "");
+    lineBuf = ::readline(d_options.getInteractivePrompt()
+                         ? (line == "" ? "CVC4> " : "... > ") : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
       ::add_history(lineBuf);
     }
@@ -203,7 +204,7 @@ restart:
     free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
   } else {
-    if(d_options[options::interactivePrompt]) {
+    if(d_options.getInteractivePrompt()) {
       if(line == "") {
         d_out << "CVC4> " << flush;
       } else {
@@ -219,7 +220,8 @@ restart:
 
   string input = "";
   while(true) {
-    Debug("interactive") << "Input now '" << input << line << "'" << endl << flush;
+    Debug("interactive") << "Input now '" << input << line << "'" << endl
+                         << flush;
 
     assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
 
@@ -260,7 +262,8 @@ restart:
       /* Extract the newline delimiter from the stream too */
       int c CVC4_UNUSED = d_in.get();
       assert(c == '\n');
-      Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush;
+      Debug("interactive") << "Next char is '" << (char)c << "'" << endl
+                           << flush;
     }
 
     input += line;
@@ -271,7 +274,7 @@ restart:
       input[n] = '\n';
       if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-        lineBuf = ::readline(d_options[options::interactivePrompt] ? "... > " : "");
+        lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -279,7 +282,7 @@ restart:
         free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
       } else {
-        if(d_options[options::interactivePrompt]) {
+        if(d_options.getInteractivePrompt()) {
           d_out << "... > " << flush;
         }
 
@@ -295,7 +298,8 @@ restart:
     }
   }
 
-  d_parser->setInput(Input::newStringInput(d_options[options::inputLanguage], input, INPUT_FILENAME));
+  d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(),
+                                           input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */
@@ -326,8 +330,8 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_0 ||
-       d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_5) {
+    if(d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
+       d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5) {
       d_out << "(error \"" << pe << "\")" << endl;
     } else {
       d_out << pe << endl;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 92902ac11..9151d8bf7 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -22,19 +22,18 @@
 #include <stdio.h>
 #include <unistd.h>
 
+#include "base/configuration.h"
 #include "base/output.h"
 #include "expr/expr_manager.h"
 #include "main/command_executor.h"
 #include "main/interactive_shell.h"
-#include "options/base_options.h"
 #include "options/language.h"
-#include "options/main_options.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
 #include "smt/smt_engine.h"
 #include "smt_util/command.h"
-#include "util/configuration.h"
 #include "util/result.h"
 #include "util/statistics.h"
 
@@ -56,24 +55,24 @@ int main(int argc, char* argv[]) {
     return runCvc4(argc, argv, opts);
   } catch(OptionException& e) {
 #ifdef CVC4_COMPETITION_MODE
-    *opts[options::out] << "unknown" << endl;
+    *opts.getOut() << "unknown" << endl;
 #endif
     cerr << "CVC4 Error:" << endl << e << endl << endl
          << "Please use --help to get help on command-line options."
          << endl;
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
-    *opts[options::out] << "unknown" << endl;
+    *opts.getOut() << "unknown" << endl;
 #endif
-    if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2_0 ||
-       opts[options::outputLanguage] == output::LANG_SMTLIB_V2_5) {
-      *opts[options::out] << "(error \"" << e << "\")" << endl;
+    if(opts.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
+       opts.getOutputLanguage() == output::LANG_SMTLIB_V2_5) {
+      *opts.getOut() << "(error \"" << e << "\")" << endl;
     } else {
-      *opts[options::err] << "CVC4 Error:" << endl << e << endl;
+      *opts.getErr() << "CVC4 Error:" << endl << e << endl;
     }
-    if(opts[options::statistics] && pExecutor != NULL) {
+    if(opts.getStatistics() && pExecutor != NULL) {
       pTotalTime->stop();
-      pExecutor->flushStatistics(*opts[options::err]);
+      pExecutor->flushStatistics(*opts.getErr());
     }
   }
   exit(1);
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
index 1ec0b961c..e42787fea 100644
--- a/src/main/portfolio_util.cpp
+++ b/src/main/portfolio_util.cpp
@@ -19,45 +19,68 @@
 #include <cassert>
 #include <vector>
 
-#include "options/base_options.h"
-#include "options/main_options.h"
 #include "options/options.h"
-#include "options/prop_options.h"
-#include "options/smt_options.h"
-#include "smt/smt_options_handler.h"
 
 using namespace std;
 
 namespace CVC4 {
 
-vector<Options> parseThreadSpecificOptions(Options opts)
-{
-  vector<Options> threadOptions;
+OptionsList::OptionsList() : d_options() {}
+
+OptionsList::~OptionsList(){
+  for(std::vector<Options*>::iterator i = d_options.begin(),
+          iend = d_options.end(); i != iend; ++i)
+  {
+    Options* current = *i;
+    delete current;
+  }
+  d_options.clear();
+}
+
+void OptionsList::push_back_copy(const Options& opts) {
+  Options* copy = new Options;
+  copy->copyValues(opts);
+  d_options.push_back(copy);
+}
+
+Options& OptionsList::operator[](size_t position){
+  return *(d_options[position]);
+}
+
+const Options& OptionsList::operator[](size_t position) const {
+  return *(d_options[position]);
+}
 
-#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij."
-  smt::SmtOptionsHandler optionsHandler(NULL);
+Options& OptionsList::back() {
+  return *(d_options.back());
+}
 
-  unsigned numThreads = opts[options::threads];
+size_t OptionsList::size() const {
+  return d_options.size();
+}
+
+void parseThreadSpecificOptions(OptionsList& threadOptions, const Options& opts)
+{
+
+  unsigned numThreads = opts.getThreads();
 
   for(unsigned i = 0; i < numThreads; ++i) {
-    threadOptions.push_back(opts);
+    threadOptions.push_back_copy(opts);
     Options& tOpts = threadOptions.back();
 
     // Set thread identifier
-    tOpts.set(options::thread_id, i);
-
-    if(i < opts[options::threadArgv].size() &&
-       !opts[options::threadArgv][i].empty()) {
-
+    tOpts.setThreadId(i);
+    const std::vector<std::string>& optThreadArgvs = opts.getThreadArgv();
+    if(i < optThreadArgvs.size() && (! optThreadArgvs[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(opts[options::threadArgv][i].c_str());
+      char* tbuf = strdup(optThreadArgvs[i].c_str());
       char* p = tbuf;
       // string length is certainly an upper bound on size needed
-      char** targv = new char*[opts[options::threadArgv][i].size()];
+      char** targv = new char*[optThreadArgvs[i].size()];
       char** vp = targv;
       *vp++ = strdup(optid.c_str());
       p = strtok(p, " ");
@@ -69,7 +92,7 @@ vector<Options> parseThreadSpecificOptions(Options opts)
       *vp++ = NULL;
       if(targc > 1) { // this is necessary in case you do e.g. --thread0="  "
         try {
-          tOpts.parseOptions(targc, targv, &optionsHandler);
+          tOpts.parseOptions(targc, targv);
         } catch(OptionException& e) {
           stringstream ss;
           ss << optid << ": " << e.getMessage();
@@ -81,8 +104,8 @@ vector<Options> parseThreadSpecificOptions(Options opts)
              << "' in thread configuration " << optid << " !";
           throw OptionException(ss.str());
         }
-        if(tOpts[options::threads] != numThreads
-           || tOpts[options::threadArgv] != opts[options::threadArgv]) {
+        if(tOpts.getThreads() != numThreads ||
+           tOpts.getThreadArgv() != opts.getThreadArgv()) {
           stringstream ss;
           ss << "not allowed to set thread options in " << optid << " !";
           throw OptionException(ss.str());
@@ -95,12 +118,10 @@ vector<Options> parseThreadSpecificOptions(Options opts)
   }
 
   assert(numThreads >= 1);      //do we need this?
-
-  return threadOptions;
 }
 
 void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) {
-  if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) {
+  if(int(lemma.getNumChildren()) > Options::currentGetSharingFilterByLength()) {
     return;
   }
   ++cnt;
@@ -109,9 +130,9 @@ void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) {
   try {
     d_pickler.toPickle(lemma, pkl);
     d_sharedChannel->push(pkl);
-    if(Trace.isOn("showSharing") && options::thread_id() == 0) {
-      *options::out() << "thread #0: notifyNewLemma: " << lemma
-                      << std::endl;
+    if(Trace.isOn("showSharing") && Options::currentGetThreadId() == 0) {
+      (*(Options::currentGetOut()))
+          << "thread #0: notifyNewLemma: " << lemma << std::endl;
     }
   } catch(expr::pickle::PicklingException& p){
     Trace("sharing::blocked") << lemma << std::endl;
@@ -137,8 +158,8 @@ Expr PortfolioLemmaInputChannel::getNewLemma() {
   expr::pickle::Pickle pkl = d_sharedChannel->pop();
 
   Expr e = d_pickler.fromPickle(pkl);
-  if(Trace.isOn("showSharing") && options::thread_id() == 0) {
-    *options::out() << "thread #0: getNewLemma: " << e << std::endl;
+  if(Trace.isOn("showSharing") && Options::currentGetThreadId() == 0) {
+    (*Options::currentGetOut()) << "thread #0: getNewLemma: " << e << std::endl;
   }
   return e;
 }
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index 2b1e22754..50cf0060a 100644
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -19,7 +19,6 @@
 
 #include "base/output.h"
 #include "expr/pickler.h"
-#include "options/main_options.h"
 #include "smt/smt_engine.h"
 #include "smt_util/lemma_input_channel.h"
 #include "smt_util/lemma_output_channel.h"
@@ -73,7 +72,26 @@ public:
 
 };/* class PortfolioLemmaInputChannel */
 
-std::vector<Options> parseThreadSpecificOptions(Options opts);
+class OptionsList {
+ public:
+  OptionsList();
+  ~OptionsList();
+
+  void push_back_copy(const Options& options);
+
+  Options& operator[](size_t position);
+  const Options& operator[](size_t position) const;
+
+  Options& back();
+
+  size_t size() const;
+ private:
+  OptionsList(const OptionsList&) CVC4_UNDEFINED;
+  OptionsList& operator=(const OptionsList&) CVC4_UNDEFINED;
+  std::vector<Options*> d_options;
+};
+
+void parseThreadSpecificOptions(OptionsList& list, const Options& opts);
 
 template<typename T>
 void sharingManager(unsigned numThreads,
diff --git a/src/main/util.cpp b/src/main/util.cpp
index abcdcc7c5..71b46e67a 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -33,7 +33,6 @@
 #include "cvc4autoconfig.h"
 #include "main/command_executor.h"
 #include "main/main.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "smt/smt_engine.h"
 #include "util/statistics.h"
@@ -42,11 +41,6 @@ using CVC4::Exception;
 using namespace std;
 
 namespace CVC4 {
-
-#ifdef CVC4_DEBUG
-//extern CVC4_THREADLOCAL(const char*) s_debugLastException;
-#endif /* CVC4_DEBUG */
-
 namespace main {
 
 /**
@@ -64,7 +58,7 @@ void* cvc4StackBase;
 /** 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] && pExecutor != NULL) {
+  if(pOptions->getStatistics() && pExecutor != NULL) {
     pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
@@ -74,7 +68,7 @@ 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] && pExecutor != NULL) {
+  if(pOptions->getStatistics() && pExecutor != NULL) {
     pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
@@ -99,7 +93,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
   }
 
   if(!segvSpin) {
-    if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    if(pOptions->getStatistics() && pExecutor != NULL) {
       pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
     }
@@ -121,7 +115,7 @@ 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] && pExecutor != NULL) {
+  if(pOptions->getStatistics() && pExecutor != NULL) {
     pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
@@ -134,7 +128,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
 #ifdef CVC4_DEBUG
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(!segvSpin) {
-    if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    if(pOptions->getStatistics() && pExecutor != NULL) {
       pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
     }
@@ -149,7 +143,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
-  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+  if(pOptions->getStatistics() && pExecutor != NULL) {
     pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
@@ -177,7 +171,7 @@ void cvc4unexpected() {
     fprintf(stderr, "The exception is:\n%s\n\n", lastContents);
   }
   if(!segvSpin) {
-    if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    if(pOptions->getStatistics() && pExecutor != NULL) {
       pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
     }
@@ -192,7 +186,7 @@ void cvc4unexpected() {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
-  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+  if(pOptions->getStatistics() && pExecutor != NULL) {
     pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
@@ -211,7 +205,7 @@ 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] && pExecutor != NULL) {
+  if(pOptions->getStatistics() && pExecutor != NULL) {
     pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
@@ -220,7 +214,7 @@ void cvc4terminate() {
   fprintf(stderr,
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
-  if((*pOptions)[options::statistics] && pExecutor != NULL) {
+  if(pOptions->getStatistics() && pExecutor != NULL) {
     pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }