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, 251 insertions, 0 deletions

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
new file mode 100644
index 000000000..f111f512b
--- /dev/null
+++ b/src/smt/options_handlers.h
@@ -0,0 +1,251 @@
+/*********************                                                        */
+/*! \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 SmtEngine options
+ **
+ ** Custom handlers and predicates for SmtEngine options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__SMT__OPTIONS_HANDLERS_H
+#define __CVC4__SMT__OPTIONS_HANDLERS_H
+
+#include "util/dump.h"
+
+namespace CVC4 {
+namespace smt {
+
+static const std::string dumpHelp = "\
+Dump modes currently supported by the --dump option:\n\
+\n\
+benchmark\n\
++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
+  does not include any declarations or assertions.  Implied by all following\n\
+  modes.\n\
+\n\
+declarations\n\
++ Dump declarations.  Implied by all following modes.\n\
+\n\
+assertions\n\
++ Output the assertions after non-clausal simplification and static\n\
+  learning phases, but before presolve-time T-lemmas arrive.  If\n\
+  non-clausal simplification and static learning are off\n\
+  (--simplification=none --no-static-learning), the output\n\
+  will closely resemble the input (with term-level ITEs removed).\n\
+\n\
+learned\n\
++ Output the assertions after non-clausal simplification, static\n\
+  learning, and presolve-time T-lemmas.  This should include all eager\n\
+  T-lemmas (in the form provided by the theory, which my or may not be\n\
+  clausal).  Also includes level-0 BCP done by Minisat.\n\
+\n\
+clauses\n\
++ Do all the preprocessing outlined above, and dump the CNF-converted\n\
+  output\n\
+\n\
+state\n\
++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
+  Implied by all \"stateful\" modes below and conflicts with all\n\
+  non-stateful modes below.\n\
+\n\
+t-conflicts [non-stateful]\n\
++ Output correctness queries for all theory conflicts\n\
+\n\
+missed-t-conflicts [stateful]\n\
++ Output completeness queries for theory conflicts\n\
+\n\
+t-propagations [stateful]\n\
++ Output correctness queries for all theory propagations\n\
+\n\
+missed-t-propagations [stateful]\n\
++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
+\n\
+t-lemmas [non-stateful]\n\
++ Output correctness queries for all theory lemmas\n\
+\n\
+t-explanations [non-stateful]\n\
++ Output correctness queries for all theory explanations\n\
+\n\
+bv-rewrites [non-stateful]\n\
++ Output correctness queries for all bitvector rewrites\n\
+\n\
+theory::fullcheck [non-stateful]\n\
++ Output completeness queries for all full-check effort-level theory checks\n\
+\n\
+Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
+one from the assertions category (either assertions, learned, or clauses), and\n\
+perhaps one or more stateful or non-stateful modes for checking correctness\n\
+and completeness of decision procedure implementations.  Stateful modes dump\n\
+the contextual assertions made by the core solver (all decisions and\n\
+propagations as assertions; that affects the validity of the resulting\n\
+correctness and completeness queries, so of course stateful and non-stateful\n\
+modes cannot be mixed in the same run.\n\
+\n\
+The --output-language option controls the language used for dumping, and\n\
+this allows you to connect CVC4 to another solver implementation via a UNIX\n\
+pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
+to a file.\n\
+";
+
+static const std::string simplificationHelp = "\
+Simplification modes currently supported by the --simplification option:\n\
+\n\
+batch (default) \n\
++ save up all ASSERTions; run nonclausal simplification and clausal\n\
+  (MiniSat) propagation for all of them only after reaching a querying command\n\
+  (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
+\n\
+incremental\n\
++ run nonclausal simplification and clausal propagation at each ASSERT\n\
+  (and at CHECKSAT/QUERY/SUBTYPE)\n\
+\n\
+none\n\
++ do not perform nonclausal simplification\n\
+";
+
+inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_DUMPING
+  char* optargPtr = strdup(optarg.c_str());
+  char* tokstr = optargPtr;
+  char* toksave;
+  while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
+    tokstr = NULL;
+    if(!strcmp(optargPtr, "benchmark")) {
+    } else if(!strcmp(optargPtr, "declarations")) {
+    } else if(!strcmp(optargPtr, "assertions")) {
+    } else if(!strcmp(optargPtr, "learned")) {
+    } else if(!strcmp(optargPtr, "clauses")) {
+    } else if(!strcmp(optargPtr, "t-conflicts") ||
+              !strcmp(optargPtr, "t-lemmas") ||
+              !strcmp(optargPtr, "t-explanations") ||
+              !strcmp(optargPtr, "bv-rewrites") ||
+              !strcmp(optargPtr, "theory::fullcheck")) {
+      // These are "non-state-dumping" modes.  If state (SAT decisions,
+      // propagations, etc.) is dumped, it will interfere with the validity
+      // of these generated queries.
+      if(Dump.isOn("state")) {
+        throw OptionException(std::string("dump option `") + optargPtr +
+                              "' conflicts with a previous, "
+                              "state-dumping dump option.  You cannot "
+                              "mix stateful and non-stateful dumping modes; "
+                              "see --dump help.");
+      } else {
+        Dump.on("no-permit-state");
+      }
+    } else if(!strcmp(optargPtr, "state") ||
+              !strcmp(optargPtr, "missed-t-conflicts") ||
+              !strcmp(optargPtr, "t-propagations") ||
+              !strcmp(optargPtr, "missed-t-propagations")) {
+      // These are "state-dumping" modes.  If state (SAT decisions,
+      // propagations, etc.) is not dumped, it will interfere with the
+      // validity of these generated queries.
+      if(Dump.isOn("no-permit-state")) {
+        throw OptionException(std::string("dump option `") + optargPtr +
+                              "' conflicts with a previous, "
+                              "non-state-dumping dump option.  You cannot "
+                              "mix stateful and non-stateful dumping modes; "
+                              "see --dump help.");
+      } else {
+        Dump.on("state");
+      }
+    } else if(!strcmp(optargPtr, "help")) {
+      puts(dumpHelp.c_str());
+      exit(1);
+    } else {
+      throw OptionException(std::string("unknown option for --dump: `") +
+                            optargPtr + "'.  Try --dump help.");
+    }
+
+    Dump.on(optargPtr);
+    Dump.on("benchmark");
+    if(strcmp(optargPtr, "benchmark")) {
+      Dump.on("declarations");
+    }
+  }
+  free(optargPtr);
+#else /* CVC4_DUMPING */
+  throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_DUMPING
+  size_t dagSetting = expr::ExprDag::getDag(Dump.getStream());
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name for --dump-to"));
+  } else if(optarg == "-") {
+    Dump.setStream(DumpOutC::dump_cout);
+  } else {
+    std::ostream* dumpTo = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+    if(!*dumpTo) {
+      throw OptionException(std::string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
+    }
+    Dump.setStream(*dumpTo);
+  }
+  expr::ExprDag::setDag(Dump.getStream(), dagSetting);
+#else /* CVC4_DUMPING */
+  throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "batch") {
+    return SIMPLIFICATION_MODE_BATCH;
+  } else if(optarg == "incremental") {
+    return SIMPLIFICATION_MODE_INCREMENTAL;
+  } else if(optarg == "none") {
+    return SIMPLIFICATION_MODE_NONE;
+  } else if(optarg == "help") {
+    puts(simplificationHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --simplification: `") +
+                          optarg + "'.  Try --simplification help.");
+  }
+}
+
+inline std::string checkReplayFilename(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_REPLAY
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name for --replay"));
+  } else {
+    return optarg;
+  }
+#else /* CVC4_REPLAY */
+  throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+inline std::ostream* checkReplayLogFilename(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_REPLAY
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name for --replay-log"));
+  } else if(optarg == "-") {
+    return &std::cout;
+  } else {
+    std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+    if(!*replayLog) {
+      throw OptionException(std::string("Cannot open replay-log file: `") + optarg + "'");
+    }
+    return replayLog;
+  }
+#else /* CVC4_REPLAY */
+  throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__OPTIONS_HANDLERS_H */