T-entailment work, and QCF (quant conflict find) work that uses it.

This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
decision engine: cache start index for and/or nodes

This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.

This was triggerred by a benchmark sent by andy/viktor.

performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex
Merge remote-tracking branch 'upstream/master' into sets
Minor optimizations to datatypes, revert to checkClash not mod eq.  Minor clean up.
More minor optimizations for datatypes.
Add option --dt-stc-ind for strengthening skolemization.  Refactor skolemization.
Fix assertion from previous commit.
Simplification of EqualityEngine::areDisequal.  Comparison for production : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5.  Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.
Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.
Valuation::entailmentCheck() proxy for TheoryEngine version.  Signature and contract is the same as for TheoryEngine version.
Improving documentation for glpk-cut-log switch.
add constant regular expression check for intersection.
fix a bug in replace and contains
First draft of ambqi_builder (new implementation of MBQI based on disjoint sets).
minor
Fix INSTALL docs.