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, 4 insertions, 85 deletions

diff --git a/doc/cvc4.1.in b/doc/cvc4.1_template.in
index 6c6a9768c..23eff6110 100644
--- a/doc/cvc4.1.in
+++ b/doc/cvc4.1_template.in
@@ -44,91 +44,10 @@ is unspecified and
 .B CVC4
 is connected to a terminal, interactive mode is assumed.
 
-.SH OPTIONS
-.IP "\-\-lang=LANG | \-L LANG"
-force input language (default is \(lqauto\(rq; see \-\-lang help)
-.IP \-\-output\-lang=LANG
-force output language (default is \(lqauto\(rq; see \-\-output\-lang help)
-.IP "\-\-version | \-V"
-identify this CVC4 binary
-.IP "\-\-help | \-h"
-this command line reference
-.IP \-\-parse\-only
-exit after parsing input
-.IP \-\-preprocess\-only
-exit after preprocessing (useful with \-\-stats or \-\-dump)
-.IP \-\-dump=MODE
-dump preprocessed assertions, T\-propagations, etc., see \-\-dump=help
-.IP \-\-dump\-to=FILE
-all dumping goes to FILE (instead of stdout)
-.IP \-\-mmap
-memory map file input
-.IP \-\-show\-config
-show CVC4 static configuration
-.IP \-\-segv\-nospin
-don't spin on segfault waiting for gdb
-.IP \-\-lazy\-type\-checking
-type check expressions only when necessary (default)
-.IP \-\-eager\-type\-checking
-type check expressions immediately on creation (debug builds only)
-.IP \-\-no\-type\-checking
-never type check expressions
-.IP \-\-no\-checking
-disable ALL semantic checks, including type checks
-.IP \-\-no\-theory\-registration
-disable theory reg (not safe for some theories)
-.IP \-\-strict\-parsing
-fail on non\-conformant inputs (SMT2 only)
-.IP "\-\-verbose | \-v"
-increase verbosity (may be repeated)
-.IP "\-\-quiet | \-q"
-decrease verbosity (may be repeated)
-.IP "\-\-trace=FLAG | \-t FLAG"
-trace something (e.g. \-t pushpop), can repeat
-.IP "\-\-debug=FLAG | \-d FLAG"
-debug something (e.g. \-d arith), can repeat
-.IP \-\-stats
-give statistics on exit
-.IP \-\-default\-expr\-depth=N
-print exprs to depth N (0 == default, \-1 == no limit)
-.IP \-\-print\-expr\-types
-print types with variables when printing exprs
-.IP \-\-interactive
-run interactively
-.IP \-\-no\-interactive
-do not run interactively
-.IP \-\-produce\-models
-support the get\-value command
-.IP \-\-produce\-assignments
-support the get\-assignment command
-.IP \-\-lazy\-definition\-expansion
-expand define\-fun lazily
-.IP \-\-simplification=MODE
-choose simplification mode, see \-\-simplification=help
-.IP \-\-no\-static\-learning
-turn off static learning (e.g. diamond\-breaking)
-.IP \-\-replay=file
-replay decisions from file
-.IP \-\-replay\-log=file
-log decisions and propagations to file
-.IP \-\-pivot\-rule=RULE
-change the pivot rule (see \-\-pivot\-rule help)
-.IP \-\-pivot\-threshold=N
-sets the number of heuristic pivots per variable per simplex instance
-.IP \-\-prop\-row\-length=N
-sets the maximum row length to be used in propagation
-.IP \-\-random\-freq=P
-sets the frequency of random decisions in the sat solver(P=0.0 by default)
-.IP \-\-random\-seed=S
-sets the random seed for the sat solver
-.IP \-\-disable\-variable\-removal
-enable permanent removal of variables in arithmetic (UNSAFE! experts only)
-.IP \-\-disable\-arithmetic\-propagation
-turns on arithmetic propagation
-.IP \-\-disable\-symmetry\-breaker
-turns off UF symmetry breaker (Deharbe et al., CADE 2011)
-.IP \-\-incremental
-enable incremental solving
+.SH COMMON OPTIONS
+${common_manpage_documentation}
+
+${remaining_manpage_documentation}
 
 .\".SH FILES
 .\".SH ENVIRONMENT