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

diff --git a/src/smt/options b/src/smt/options
new file mode 100644
index 000000000..5ee65e50a
--- /dev/null
+++ b/src/smt/options
@@ -0,0 +1,81 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+# FIXME: need to add support for SMT-LIBv2-required options:
+#
+#   expand-definitions
+#   regular-output-channel
+#   diagnostic-output-channel
+#   produce-unsat-cores
+#
+
+module SMT "smt/options.h" SMT layer
+
+common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
+ dump preprocessed assertions, etc., see --dump=help
+common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
+ all dumping goes to FILE (instead of stdout)
+
+expert-option lazyDefinitionExpansion --lazy-definition-expansion bool
+ expand define-funs/LAMBDAs lazily
+
+option simplificationMode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
+ choose simplification mode, see --simplification=help
+alias --no-simplification = --simplification=none
+ turn off all simplification (same as --simplification=none)
+
+option doStaticLearning static-learning /--no-static-learning bool :default true
+ use static learning (on by default)
+/turn off static learning (e.g. diamond-breaking)
+
+common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
+ support the get-value and get-model commands
+common-option produceAssignments produce-assignments --produce-assignments bool
+ support the get-assignment command
+
+# This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
+# is a mode in which the assertion list must be kept.  So it belongs here.
+common-option interactive interactive-mode --interactive bool :read-write
+ force interactive mode
+
+option doITESimp --ite-simp bool :read-write
+ turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
+/turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)
+
+option unconstrainedSimp --unconstrained-simp bool :default false :read-write
+ turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
+/turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
+
+option repeatSimp --repeat-simp bool :read-write
+ make multiple passes with nonclausal simplifier
+/do not make multiple passes with nonclausal simplifier
+
+common-option incrementalSolving incremental -i --incremental bool
+ enable incremental solving
+
+common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long"
+ enable time limiting (give milliseconds)
+common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long"
+ enable time limiting per query (give milliseconds)
+common-option cumulativeResourceLimit --rlimit=N "unsigned long"
+ enable resource limiting
+common-option perCallResourceLimit --rlimit-per=N "unsigned long"
+ enable resource limiting per query
+
+option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
+ replay decisions from file
+option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h"
+ log decisions and propagations to file
+option replayStream ExprStream*
+
+# portfolio options
+option threads --threads=N unsigned :default 2
+ Total number of threads
+option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h"
+ The input channel to receive notfication events for new lemmas
+option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
+ The output channel to receive notfication events for new lemmas
+
+endmodule