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

diff --git a/src/options/base_options b/src/options/base_options
new file mode 100644
index 000000000..10ad564e6
--- /dev/null
+++ b/src/options/base_options
@@ -0,0 +1,110 @@
+#
+# Option specification file for CVC4
+#
+# This is essentially a shell script interpreted with special commands.
+#
+# Lines starting with whitespace are special.  They are passed in their entirety (minus
+# the first whitespace char) to the "doc" command.  Lines starting with a single slash
+# are stripped of this initial character and interpreted by the "doc-alt" command.  A period
+# "." in the first column of a line, followed optionally by whitespace but without any other
+# content on the line, is interpreted as an empty string passed to doc.  (This allows
+# multi-paragraph documentation for options.)  Lines may be continued with a backslash (\)
+# at the end of a line.
+#
+# commands are:
+#
+#   module ID "include-file" name
+#
+#     Identifies the module.  Must be the first command in the file.  ID is a suitable
+#     identifier for a preprocessor definition, and should be unique; name is a "pretty"
+#     name used for the benefit of the end CVC4 user in, e.g., option listings.
+#
+#   common-option SPECIFICATION
+#   option SPECIFICATION
+#   expert-option SPECIFICATION
+#   undocumented-option SPECIFICATION
+#
+#     These commands declare (respectively) common options presented first to the user,
+#     standard options that the user might want to see with "--help" documentation,
+#     expert options that should be marked as expert-only, and options that should not
+#     appear in normal option documentation (even if documentation is included here).
+#
+#     SPECIFICATIONs take this form:
+#
+#       SPECIFICATION ::= (internal-name | -) [-short-option/-alternate-short-option] [--long-option/--alternate-long-option] [smt-option-name] C++-type [ATTRIBUTEs...]
+#       ATTRIBUTE ::=   :include include-files..
+#                     | :default C++-expression
+#                     | :handler custom-option-handlers..
+#                     | :handler-include include-files..
+#                     | :read-only
+#                     | :read-write
+#                     | :link linked-options..
+#
+#   alias smt-option-name = (smt-option-name[=argument])+
+#   alias (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+
+#
+#     The alias command creates a new SmtEngine option name, or short option, or long option,
+#     and binds it to act the same way as if the options to the right of "=" were passed.
+#     For example, if there are options to --disable-warning-1 and --disable-warning-2, etc.,
+#     a useful alias might be:
+#
+#       alias --disable-all-warnings = --disable-warning-1 --disable-warning-2
+#
+#     Aliases cannot take arguments, and command-line aliases cannot set SmtEngine properties,
+#     and SmtEngine aliases cannot set command-line properties.  For these things, you need a
+#     custom handler.
+#
+#   warning message
+#
+#     Warn about something during processing (like a FIXME).
+#
+#   endmodule
+#
+#     This file should end with the "endmodule" command, and nothing should follow it.
+#
+
+module BASE "options/base_options.h" Base
+
+option binary_name std::string
+
+option in std::istream* :default &std::cin :include <iostream>
+option out std::ostream* :default &std::cout :include <iostream>
+option err std::ostream* :default &std::cerr :include <iostream>
+
+common-option inputLanguage -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write
+ force input language (default is "auto"; see --lang help)
+common-option outputLanguage --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write
+ force input language (default is "auto"; see --lang help)
+option languageHelp bool
+
+option verbosity verbosity int :read-write :default 0
+ the verbosity level of CVC4
+common-option - -v --verbose void :handler CVC4::options::increaseVerbosity
+ increase verbosity (may be repeated)
+common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity
+ decrease verbosity (may be repeated)
+
+common-option statistics stats --stats bool
+ give statistics on exit
+
+common-option parseOnly parse-only --parse-only bool :read-write
+ exit after parsing input
+
+common-option preprocessOnly preprocess-only --preprocess-only bool
+ exit after preprocessing input
+
+option segvNoSpin --segv-nospin bool
+ don't spin on segfault waiting for gdb
+
+option - -t --trace=TAG argument :handler CVC4::options::addTraceTag
+ trace something (e.g. -t pushpop), can repeat
+option - -d --debug=TAG argument :handler CVC4::options::addDebugTag
+ debug something (e.g. -d arith), can repeat
+
+option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h"
+ print the "success" output required of SMT-LIBv2
+
+alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success
+ SMT-LIBv2 compliance mode (implies other options)
+
+endmodule