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.

12 files changed, 387 insertions, 227 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 594751358..730afa32d 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -65,6 +65,9 @@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g
 tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@
 
+EXTRA_DIST = \
+	options_handlers.h
+
 clean-local:
 	rm -f $(BUILT_SOURCES)
 
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index f24526e6c..ca5dfad93 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -36,7 +36,10 @@
 #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 "theory/uf/options.h"
 #include "util/output.h"
 #include "util/dump.h"
 #include "util/result.h"
@@ -66,28 +69,28 @@ 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] );
   }
 }
 
-int runCvc4(int argc, char* argv[], Options& options) {
+int runCvc4(int argc, char* argv[], Options& opts) {
 
   // Timer statistic
   TimerStat s_totalTime("totalTime");
   s_totalTime.start();
 
   // For the signal handlers' benefit
-  pOptions = &options;
+  pOptions = &opts;
 
   // Initialize the signal handlers
   cvc4_init();
@@ -95,26 +98,26 @@ int runCvc4(int argc, char* argv[], Options& options) {
   progPath = argv[0];
 
   // 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);
   }
 
-  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
@@ -127,8 +130,8 @@ 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)));
   }
 
   // Determine which messages to show based on smtcomp_mode and verbosity
@@ -141,13 +144,13 @@ 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);
     }
@@ -156,28 +159,28 @@ int runCvc4(int argc, char* argv[], Options& options) {
   // 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);
       }
     }
   }
 
-  if(options.outputLanguage == language::output::LANG_AUTO) {
-    options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
+  if(opts[options::outputLanguage] == language::output::LANG_AUTO) {
+    opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage]));
   }
 
   // Determine which messages to show based on smtcomp_mode and verbosity
@@ -190,70 +193,73 @@ 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);
     }
 
-    Debug.getStream() << Expr::setlanguage(options.outputLanguage);
-    Trace.getStream() << Expr::setlanguage(options.outputLanguage);
-    Notice.getStream() << Expr::setlanguage(options.outputLanguage);
-    Chat.getStream() << Expr::setlanguage(options.outputLanguage);
-    Message.getStream() << Expr::setlanguage(options.outputLanguage);
-    Warning.getStream() << Expr::setlanguage(options.outputLanguage);
-    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+    Debug.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+    Trace.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+    Notice.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+    Chat.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+    Message.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+    Warning.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
+    Dump.getStream() << Expr::setlanguage(opts[options::outputLanguage])
                      << 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]);
 
   // Create the expression manager
-  ExprManager exprMgr(options);
+  ExprManager exprMgr(opts);
 
   // Create the SmtEngine
+  StatisticsRegistry driverStats("driver");
   SmtEngine smt(&exprMgr);
 
   Parser* replayParser = NULL;
-  if( options.replayFilename != "" ) {
-    ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
+  if( opts[options::replayFilename] != "" ) {
+    ParserBuilder replayParserBuilder(&exprMgr, opts[options::replayFilename], opts);
 
-    if( options.replayFilename == "-") {
+    if( opts[options::replayFilename] == "-") {
       if( inputFromStdin ) {
         throw OptionException("Replay file and input file can't both be stdin.");
       }
       replayParserBuilder.withStreamInput(cin);
     }
     replayParser = replayParserBuilder.build();
-    options.replayStream = new Parser::ExprStream(replayParser);
+    opts.set(options::replayStream, new Parser::ExprStream(replayParser));
   }
-  if( options.replayLog != NULL ) {
-    *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
+  if( opts[options::replayLog] != NULL ) {
+    *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
   }
 
   // signal handlers need access
   pStatistics = smt.getStatisticsRegistry();
+  exprMgr.getStatisticsRegistry()->setName("ExprManager");
   pStatistics->registerStat_(exprMgr.getStatisticsRegistry());
+  pStatistics->registerStat_(&driverStats);
 
   // Timer statistic
-  RegisterStatistic statTotalTime(exprMgr, &s_totalTime);
+  RegisterStatistic statTotalTime(&driverStats, &s_totalTime);
 
   // Filename statistics
   ReferenceStat< const char* > s_statFilename("filename", filename);
-  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
+  RegisterStatistic statFilenameReg(&driverStats, &s_statFilename);
 
   // Parse and execute commands until we are done
   Command* cmd;
   bool status = true;
-  if( options.interactive ) {
-    InteractiveShell shell(exprMgr, options);
+  if( opts[options::interactive] ) {
+    InteractiveShell shell(exprMgr, opts);
     Message() << Configuration::getPackageName()
               << " " << Configuration::getVersionString();
     if(Configuration::isSubversionBuild()) {
@@ -268,11 +274,11 @@ int runCvc4(int argc, char* argv[], Options& options) {
       replayParser->useDeclarationsFrom(shell.getParser());
     }
     while((cmd = shell.readCommand())) {
-      status = doCommand(smt,cmd, options) && status;
+      status = doCommand(smt,cmd, opts) && status;
       delete cmd;
     }
   } else {
-    ParserBuilder parserBuilder(&exprMgr, filename, options);
+    ParserBuilder parserBuilder(&exprMgr, filename, opts);
 
     if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -292,23 +298,23 @@ int runCvc4(int argc, char* argv[], Options& options) {
         delete cmd;
         break;
       }
-      status = doCommand(smt, cmd, options) && status;
+      status = doCommand(smt, cmd, opts) && status;
       delete cmd;
     }
     // Remove the parser
     delete parser;
   }
 
-  if( options.replayStream != NULL ) {
+  if( opts[options::replayStream] != NULL ) {
     // this deletes the expression parser too
-    delete options.replayStream;
-    options.replayStream = NULL;
+    delete opts[options::replayStream];
+    opts.set(options::replayStream, NULL);
   }
 
   int returnValue;
   string result = "unknown";
   if(status) {
-    result = smt.getInfo(":status").getValue();
+    result = smt.getInfo("status").getValue();
 
     if(result == "sat") {
       returnValue = 10;
@@ -329,20 +335,20 @@ int runCvc4(int argc, char* argv[], Options& options) {
 #endif /* CVC4_COMPETITION_MODE */
 
   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-  RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
+  RegisterStatistic statSatResultReg(&driverStats, &s_statSatResult);
 
   s_totalTime.stop();
 
-  if(options.statistics) {
-    pStatistics->flushInformation(*options.err);
+  if(opts[options::statistics]) {
+    pStatistics->flushInformation(*opts[options::err]);
   }
 
   return returnValue;
 }
 
 /** 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;
   }
 
@@ -354,15 +360,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);
     }
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;
 }
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 03a3a0ae3..443404384 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -33,7 +33,7 @@
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/language.h"
 
 #include <string.h>
@@ -85,8 +85,8 @@ static set<string> s_declarations;
 
 InteractiveShell::InteractiveShell(ExprManager& exprManager,
                                    const Options& options) :
-  d_in(*options.in),
-  d_out(*options.out),
+  d_in(*options[options::in]),
+  d_out(*options[options::out]),
   d_options(options),
   d_quit(false) {
   ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
@@ -99,7 +99,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
     ::rl_completion_entry_function = commandGenerator;
     ::using_history();
 
-    switch(OutputLanguage lang = toOutputLanguage(d_options.inputLanguage)) {
+    switch(OutputLanguage lang = toOutputLanguage(d_options[options::inputLanguage])) {
     case output::LANG_CVC4:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
       commandsBegin = cvc_commands;
@@ -174,7 +174,7 @@ Command* InteractiveShell::readCommand() {
   /* Prompt the user for input. */
   if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-    lineBuf = ::readline(d_options.verbosity >= 0 ? "CVC4> " : "");
+    lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "CVC4> " : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
       ::add_history(lineBuf);
     }
@@ -182,7 +182,7 @@ Command* InteractiveShell::readCommand() {
     free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
   } else {
-    if(d_options.verbosity >= 0) {
+    if(d_options[options::verbosity] >= 0) {
       d_out << "CVC4> " << flush;
     }
 
@@ -239,7 +239,7 @@ Command* InteractiveShell::readCommand() {
       input[n] = '\n';
       if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-        lineBuf = ::readline(d_options.verbosity >= 0 ? "... > " : "");
+        lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "... > " : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -247,7 +247,7 @@ Command* InteractiveShell::readCommand() {
         free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
       } else {
-        if(d_options.verbosity >= 0) {
+        if(d_options[options::verbosity] >= 0) {
           d_out << "... > " << flush;
         }
 
@@ -262,7 +262,7 @@ Command* InteractiveShell::readCommand() {
     }
   }
 
-  d_parser->setInput(Input::newStringInput(d_options.inputLanguage, input, INPUT_FILENAME));
+  d_parser->setInput(Input::newStringInput(d_options[options::inputLanguage], input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 7f17b88d7..214ae0d02 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -21,6 +21,7 @@
 #include <string>
 
 #include "util/language.h"
+#include "options/options.h"
 
 namespace CVC4 {
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index b90ab433a..70f2783a5 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -34,7 +34,8 @@
 #include "expr/command.h"
 #include "util/Assert.h"
 #include "util/configuration.h"
-#include "util/options.h"
+#include "main/options.h"
+#include "theory/uf/options.h"
 #include "util/output.h"
 #include "util/result.h"
 #include "util/stats.h"
@@ -51,22 +52,22 @@ using namespace CVC4::main;
  * Put everything in runCvc4().
  */
 int main(int argc, char* argv[]) {
-  Options options;
+  Options opts;
   try {
-    return runCvc4(argc, argv, options);
+    return runCvc4(argc, argv, opts);
   } catch(OptionException& e) {
 #ifdef CVC4_COMPETITION_MODE
-    *options.out << "unknown" << endl;
+    *opts[options::out] << "unknown" << endl;
 #endif
     cerr << "CVC4 Error:" << endl << e << endl;
-    printUsage(options);
+    printUsage(opts);
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
-    *options.out << "unknown" << endl;
+    *opts[options::out] << "unknown" << endl;
 #endif
-    *options.err << "CVC4 Error:" << endl << e << endl;
-    if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushInformation(*options.err);
+    *opts[options::err] << "CVC4 Error:" << endl << e << endl;
+    if(opts[options::statistics] && pStatistics != NULL) {
+      pStatistics->flushInformation(*opts[options::err]);
     }
   }
   exit(1);
diff --git a/src/main/main.h b/src/main/main.h
index 4df5ccc49..09ba60c94 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -19,7 +19,7 @@
 #include <exception>
 #include <string>
 
-#include "util/options.h"
+#include "options/options.h"
 #include "util/exception.h"
 #include "util/stats.h"
 #include "util/tls.h"
diff --git a/src/main/options b/src/main/options
new file mode 100644
index 000000000..6defc8642
--- /dev/null
+++ b/src/main/options
@@ -0,0 +1,38 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module DRIVER "main/options.h" Driver
+
+common-option version -V --version/ bool
+ identify this CVC4 binary
+
+common-option help -h --help/ bool
+ full command line reference
+
+common-option - --show-config void :handler CVC4::main::showConfiguration :handler-include "main/options_handlers.h"
+ show CVC4 static configuration
+
+option - --show-debug-tags void :handler CVC4::main::showDebugTags :handler-include "main/options_handlers.h"
+ show all available tags for debugging
+option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-include "main/options_handlers.h"
+ show all available tags for tracing
+
+# portfolio options
+option printWinner bool
+ enable printing the winning thread (pcvc4 only)
+option - --threadN=string void
+ configures thread N (0..#threads-1)
+option threadArgv std::vector<std::string>
+#:includes <vector> <string>
+ Thread configuration (a string to be passed to parseOptions)
+option thread_id int :default -1
+ Thread ID, for internal use in case of multi-threaded run
+option separateOutput bool :default false
+ In multi-threaded setting print output of each thread at the
+ end of run, separated by a divider ("----").
+option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
+ don't share lemmas strictly longer than N
+
+endmodule
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
new file mode 100644
index 000000000..e607e13ce
--- /dev/null
+++ b/src/main/options_handlers.h
@@ -0,0 +1,101 @@
+/*********************                                                        */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Custom handlers and predicates for main driver options
+ **
+ ** Custom handlers and predicates for main driver options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MAIN__OPTIONS_HANDLERS_H
+#define __CVC4__MAIN__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace main {
+
+inline void showConfiguration(std::string option, SmtEngine* smt) {
+  fputs(Configuration::about().c_str(), stdout);
+  printf("\n");
+  printf("version    : %s\n", Configuration::getVersionString().c_str());
+  if(Configuration::isSubversionBuild()) {
+    printf("subversion : yes [%s r%u%s]\n",
+           Configuration::getSubversionBranchName(),
+           Configuration::getSubversionRevision(),
+           Configuration::hasSubversionModifications() ?
+             " (with modifications)" : "");
+  } else {
+    printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
+  }
+  printf("\n");
+  printf("library    : %u.%u.%u\n",
+         Configuration::getVersionMajor(),
+         Configuration::getVersionMinor(),
+         Configuration::getVersionRelease());
+  printf("\n");
+  printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
+  printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
+  printf("replay     : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
+  printf("tracing    : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
+  printf("dumping    : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
+  printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
+  printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
+  printf("proof      : %s\n", Configuration::isProofBuild() ? "yes" : "no");
+  printf("coverage   : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
+  printf("profiling  : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
+  printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
+  printf("\n");
+  printf("cudd       : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
+  printf("cln        : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
+  printf("gmp        : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
+  printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
+  exit(0);
+}
+
+inline void showDebugTags(std::string option, SmtEngine* smt) {
+  if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
+    printf("available tags:");
+    unsigned ntags = Configuration::getNumDebugTags();
+    char const* const* tags = Configuration::getDebugTags();
+    for(unsigned i = 0; i < ntags; ++ i) {
+      printf(" %s", tags[i]);
+    }
+    printf("\n");
+  } else if(! Configuration::isDebugBuild()) {
+    throw OptionException("debug tags not available in non-debug builds");
+  } else {
+    throw OptionException("debug tags not available in non-tracing builds");
+  }
+  exit(0);
+}
+
+inline void showTraceTags(std::string option, SmtEngine* smt) {
+  if(Configuration::isTracingBuild()) {
+    printf("available tags:");
+    unsigned ntags = Configuration::getNumTraceTags();
+    char const* const* tags = Configuration::getTraceTags();
+    for (unsigned i = 0; i < ntags; ++ i) {
+      printf(" %s", tags[i]);
+    }
+    printf("\n");
+  } else {
+    throw OptionException("trace tags not available in non-tracing build");
+  }
+  exit(0);
+}
+
+
+}/* CVC4::main namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MAIN__OPTIONS_HANDLERS_H */
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index fc22374cf..10c387b14 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -25,7 +25,7 @@
 
 #include "smt/smt_engine.h"
 #include "util/result.h"
-#include "util/options.h"
+#include "options/options.h"
 
 using namespace boost;
 
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
index 9bc911be3..1a82d651b 100644
--- a/src/main/portfolio.h
+++ b/src/main/portfolio.h
@@ -25,7 +25,7 @@
 
 #include "smt/smt_engine.h"
 #include "expr/command.h"
-#include "util/options.h"
+#include "options/options.h"
 
 namespace CVC4 {
 
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 5877704ae..756c7d7a9 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -27,7 +27,7 @@
 
 #include "util/Assert.h"
 #include "util/exception.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/stats.h"
 
 #include "cvc4autoconfig.h"
@@ -52,7 +52,7 @@ bool segvNoSpin = false;
 /** Handler for SIGXCPU, i.e., timeout. */
 void timeout_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by timeout.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   abort();
@@ -61,7 +61,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->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   abort();
@@ -86,7 +86,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(pOptions->statistics && pStatistics != NULL) {
+    if((*pOptions)[options::statistics] && pStatistics != NULL) {
       pStatistics->flushInformation(cerr);
     }
     abort();
@@ -106,7 +106,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->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   abort();
@@ -119,7 +119,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(pOptions->statistics && pStatistics != NULL) {
+    if((*pOptions)[options::statistics] && pStatistics != NULL) {
       pStatistics->flushInformation(cerr);
     }
     abort();
@@ -132,7 +132,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   abort();
@@ -156,7 +156,7 @@ void cvc4unexpected() {
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
-    if(pOptions->statistics && pStatistics != NULL) {
+    if((*pOptions)[options::statistics] && pStatistics != NULL) {
       pStatistics->flushInformation(cerr);
     }
     set_terminate(default_terminator);
@@ -169,7 +169,7 @@ void cvc4unexpected() {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   set_terminate(default_terminator);
@@ -182,7 +182,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->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   default_terminator();
@@ -190,7 +190,7 @@ void cvc4terminate() {
   fprintf(stderr,
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
-  if(pOptions->statistics && pStatistics != NULL) {
+  if((*pOptions)[options::statistics] && pStatistics != NULL) {
     pStatistics->flushInformation(cerr);
   }
   default_terminator();