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

diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in
new file mode 100644
index 000000000..23eff6110
--- /dev/null
+++ b/doc/cvc4.1_template.in
@@ -0,0 +1,127 @@
+.\" Process this file with
+.\" groff -man -Tascii cvc4.1
+.\"
+.TH CVC4 1 "@MAN_DATE@" "CVC4 release @VERSION@" "User Manuals"
+.SH NAME
+cvc4, pcvc4 \- an automated theorem prover
+.SH SYNOPSIS
+.B cvc4 [
+.I options
+.B ] [
+.I file
+.B ]
+.P
+.B pcvc4 [
+.I options
+.B ] [
+.I file
+.B ]
+.SH DESCRIPTION
+.B cvc4
+is an automated theorem prover for first-order formulas with respect
+to background theories of interest.
+.B pcvc4
+is CVC4's "portfolio" variant, which is capable of running multiple
+CVC4 instances in parallel, configured differently.
+
+With
+.I file
+, commands are read from
+.I file
+and executed.  CVC4 supports the SMT-LIB (versions 1.2 and 2.0) input
+format, as well as its own native \(lqpresentation language\(rq (see
+.BR cvc4 (5)
+), which is similar in many respects to CVC3's presentation language,
+but not identical.
+
+If
+.I file
+is unspecified, standard input is read (and the
+.B CVC4
+presentation language is assumed).  If
+.I file
+is unspecified and
+.B CVC4
+is connected to a terminal, interactive mode is assumed.
+
+.SH COMMON OPTIONS
+${common_manpage_documentation}
+
+${remaining_manpage_documentation}
+
+.\".SH FILES
+.\".SH ENVIRONMENT
+.SH DIAGNOSTICS
+.B CVC4
+reports all syntactic and semantic errors on standard error.
+.SH HISTORY
+The
+.B CVC4
+effort is the culmination of fifteen years of theorem proving
+research, starting with the
+.I Stanford Validity Checker (SVC)
+in 1996.
+
+SVC's successor, the
+.I Cooperating Validity Checker (CVC),
+had a more optimized internal design, produced proofs, used the
+.I Chaff
+SAT solver, and featured a number of usability
+enhancements.  Its name comes from the cooperative nature of
+decision procedures in Nelson-Oppen theory combination,
+which share amongst each other equalities between shared terms.
+
+CVC Lite, first made available in 2003, was a rewrite of CVC
+that attempted to make CVC
+more flexible (hence the \(lqlite\(rq) while extending the feature set:
+CVCLite supported quantifiers where its predecessors did not.
+CVC3 was a major overhaul of portions of CVC Lite: it added
+better decision procedure implementations, added support for using
+MiniSat in the core, and had generally better performance.
+
+CVC4 is the new version, the fifth generation of this validity
+checker line that is now celebrating fifteen years of heritage.
+It represents a complete re-evaluation of
+the core architecture to be both performant and to serve as a cutting-edge research vehicle
+for the next several years.  Rather than taking CVC3
+and redesigning problem parts, we've taken a clean-room approach,
+starting from scratch.  Before using any designs from CVC3, we have
+thoroughly scrutinized, vetted, and updated them.  Many parts of CVC4
+bear only a superficial resemblance, if any, to their correspondent in CVC3.
+
+However, CVC4 is fundamentally similar to CVC3 and many other
+modern SMT solvers: it is a DPLL(
+.I T
+) solver,
+with a SAT solver at its core and a delegation path to different decision
+procedure implementations, each in charge of solving formulas in some
+background theory.
+
+The re-evaluation and ground-up rewrite was necessitated, we felt, by
+the performance characteristics of CVC3.  CVC3 has many useful
+features, but some core aspects of the design led to high memory use, and
+the use of heavyweight computation (where more nimble engineering
+approaches could suffice) makes CVC3 a much slower prover than other tools.
+As these designs are central to CVC3, a new version was preferable to a
+selective re-engineering, which would have ballooned in short order.
+.SH VERSION
+This manual page refers to
+.B CVC4
+version @VERSION@.
+.SH BUGS
+A Bugzilla for the CVC4 project is maintained at
+.BR http://goedel.cs.nyu.edu/bugzilla3/ .
+.SH AUTHORS
+.B CVC4
+is developed by a team of researchers at New York University
+and the University of Iowa.
+See the AUTHORS file in the distribution for a full list of
+contributors.
+.SH "SEE ALSO"
+.BR libcvc4 (3),
+.BR libcvc4parser (3),
+.BR libcvc4compat (3)
+
+Additionally, the CVC4 wiki contains useful information about the
+design and internals of CVC4.  It is maintained at
+.BR http://goedel.cs.nyu.edu/wiki/ .