Merge pull request #59 from kbansal/sets3

sets type enumerator
Minor cleanup in datatypes.
Fixed bug 590, added regression test
Fixed bug 589
Fix bug590 regression distcheck failure from last night.
Fixed inefficiency in bit-vector rewrite rule.
Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.

* support for new commands meta-info, declare-const, echo, get-model,
  reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
  this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
  in 2.0 mode)

What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
  Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
  (Currently :incremental and maybe others get "stuck" due to late driver
  integration.)
Add --user-pat=resort.  Minor cleanup of options.
Minor parser performance fix.
Fix typo.
Minor fix for --user-pat=resort
Improve stats in conjecture generator, minor cleanup.
Initial infrastructure for function definition quantifiers, internal parsing format for Smt2.
Preprocessing step for finding finite runs of well-defined function definitions using FMF.
Added new, much faster, care graph computation for arrays
Force split on true first in combineTheories
Fix bugs in getModelValue in bit-vectors
Be more lazy about generating array lemmas
Do not allow duplication of function definitions.  Set incomplete flag in model builder.
Fix some mistakes in datatypes theory combination, disable two regressions.  Minor fix for fun defs.
Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemmas being rewritten).  Minor improvement to dt care graph.  Reenable regressions.
Simplify which lemmas to communicate in dt.