Minor fixes post-merge of RR.
Work on array pf signature, add working example.  Add quantifiers proof signature. Ignore terms not in current master EE for QCF.  Minor refactoring.  Make --rewrite-rules true by default.
Add working example of LFSC proof with quantifiers.  Update quantifiers signature to avoid dependent types in side condition.
Add ability to provide theory-specific proof rules to EqualityEngine, extends enumeration of MergeReasonType.  Add initial use in TheoryArrays.
dos2unix on the proof signatures, and fix the makefile.
SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff).  Thanks to David Cok for the bug report.
Fix for ite of >=64bit wide bitvectors with unconstrained condition.
hot fix for pre-reg term caching in strings
hot fix for pre-reg term caching in strings
Merge branch 'master' of github.com:tiliang/CVC4
Fix a memory leak in LFSC proof checker.  Largest QF_UF proof from Morgan (problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory.  Add example test proof.
Minor documentation fixups.
Fix proof signatures makefile
Minor usability fixes related to SMT-LIB compliance.
Appease compilers from latest XCode release (v5.1).
Move the translator binary from src/main to examples, no longer built by default.
Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.
Set dumping options from (set-option..) and API more directly.
Refactor the theory specific parts of definition expansion into the theory solvers.

In the process of doing this I may have fixed some bugs or some potential bugs so there
may be some user visible results of this refactoring.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Fix documentation for Theory::preRegisterTerm().