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.
fixup