Options merge. This commit:

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

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

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

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

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

Benefits of the new options system include:

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

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

1 files changed, 75 insertions, 69 deletions

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);
     }