merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding.  Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version
removing unecessary files
Minor cleanup after today's commits:

* change some uses of "std::cout" to "Message()"

* change some files to use Unix newlines instead of DOS newlines

* fix compiler warning
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.
fix some file documentation
Moving some instantiation-related stuff from src/theory to src/theory/quantifiers and src/theory/rewriterules.  This unclutters the src/theory directory somewhat.

The namespaces weren't changed, only the file locations.
fixes for portfolio
some fixes for Mac OS
fix for the SmtEngine::beforeSearch() option predicate
fixes to some *clean targets
a couple fixes to SmtEngine::setOption().  thanks Andy for the report!
add isFinished() to type enumerators (so we don't rely on exception-throwing after exhaustively enumerating finite types), also fix a standards-related FIXME in SmtEngine by clarifying the text of an error message
array-store-all class
fixes to paths in parser makefiles; if you've noticed strange SMT2 parser behavior the last couple days, this should fix it
better parser makefile fix
fix for proofs-enabled builds
fix uses of getMetaKind() from outside the expr package.  (they now use isConst() and isVar() as appropriate)

also some base infrastructure for the new ::isConst().
ArrayStoreAll infrastructure
Comparisons for LogicInfos, and associated tests
the array-store "construle" for isConst