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

diff --git a/src/options/options.h b/src/options/options.h
new file mode 100644
index 000000000..a3abdd54b
--- /dev/null
+++ b/src/options/options.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file options.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: taking, cconway
+ ** Minor contributors (to current version): dejan
+ ** 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 Global (command-line, set-option, ...) parameters for SMT.
+ **
+ ** Global (command-line, set-option, ...) parameters for SMT.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__OPTIONS__OPTIONS_H
+#define __CVC4__OPTIONS__OPTIONS_H
+
+#include <iostream>
+#include <fstream>
+#include <string>
+
+#include "util/exception.h"
+#include "util/language.h"
+#include "util/tls.h"
+
+namespace CVC4 {
+
+namespace options {
+  class OptionsHolder;
+}/* CVC4::options namespace */
+
+class ExprStream;
+class NodeManager;
+class NodeManagerScope;
+class SmtEngine;
+
+/** Class representing an option-parsing exception. */
+class CVC4_PUBLIC OptionException : public CVC4::Exception {
+public:
+  OptionException(const std::string& s) throw() :
+    CVC4::Exception("Error in option parsing: " + s) {
+  }
+};/* class OptionException */
+
+class CVC4_PUBLIC Options {
+  /** The struct that holds all option values. */
+  options::OptionsHolder* d_holder;
+
+  /** The current Options in effect */
+  static CVC4_THREADLOCAL(Options*) s_current;
+
+  /** Low-level assignment function for options */
+  template <class T>
+  void assign(T, std::string option, std::string value, SmtEngine* smt);
+  /** Low-level assignment function for bool-valued options */
+  template <class T>
+  void assignBool(T, std::string option, bool value, SmtEngine* smt);
+
+  friend class NodeManager;
+  friend class NodeManagerScope;
+  friend class SmtEngine;
+
+public:
+
+  /** Get the current Options in effect */
+  static inline Options& current() {
+    return *s_current;
+  }
+
+  Options();
+  Options(const Options& options);
+  ~Options();
+
+  /**
+   * Set the value of the given option.  Use of this default
+   * implementation causes a compile-time error; write-able
+   * options specialize this template with a real implementation.
+   */
+  template <class T>
+  void set(T, const typename T::type&) {
+    // Flag a compile-time error.  Write-able options specialize
+    // this template to provide an implementation.
+    T::you_are_trying_to_assign_to_a_read_only_option;
+  }
+
+  /** Get the value of the given option.  Const access only. */
+  template <class T>
+  const typename T::type& operator[](T) const;
+
+  /**
+   * Returns true iff the value of the given option was set
+   * by the user via a command-line option or SmtEngine::setOption().
+   * (Options::set() is low-level and doesn't count.)  Returns false
+   * otherwise.
+   */
+  template <class T>
+  bool wasSetByUser(T) const;
+
+  /**
+   * Get a description of the command-line flags accepted by
+   * parseOptions.  The returned string will be escaped so that it is
+   * suitable as an argument to printf. */
+  std::string getDescription() const;
+
+  /**
+   * Print overall command-line option usage message, prefixed by
+   * "msg"---which could be an error message causing the usage
+   * output in the first place, e.g. "no such option --foo"
+   */
+  static void printUsage(const std::string msg, std::ostream& out);
+
+  /**
+   * Print command-line option usage message for only the most-commonly
+   * used options.  The message is prefixed by "msg"---which could be
+   * an error message causing the usage output in the first place, e.g.
+   * "no such option --foo"
+   */
+  static void printShortUsage(const std::string msg, std::ostream& out);
+
+  /** Print help for the --lang command line option */
+  static void printLanguageHelp(std::ostream& out);
+
+  /**
+   * Initialize the options based on the given command-line arguments.
+   */
+  int parseOptions(int argc, char* argv[]) throw(OptionException);
+
+  /**
+   * Set the output language based on the given string.
+   */
+  void setOutputLanguage(const char* str) throw(OptionException);
+
+  /**
+   * Set the input language based on the given string.
+   */
+  void setInputLanguage(const char* str) throw(OptionException);
+
+};/* class Options */
+
+}/* CVC4 namespace */
+
+#include "options/base_options.h"
+
+#endif /* __CVC4__OPTIONS__OPTIONS_H */