Added support for proof production in Equality Engine.  Cleaned up existing proof signatures and added proof signature for theory of arrays.  Added new MBQI technique based on interval abstraction.  Cleaned up option names.  Improved symmetry breaking for uf strong solver.  Other minor cleanup.
Removing and consolidating options for uf-ss and quantifiers.  Bug fix for inst gen-style MBQI.
string contain changes
minor fix, bring back the assertion.
remove a warning in strings
Fix LogicInfo parsing for string logics
Fix LogicInfo parsing for string logics
clean some code
Cache apt packages on Travis.
Switch license default back to BSD, and add --best and --enable-gpl options.
Merge branch '1.3.x'

Conflicts:
	COPYING
	NEWS
	config/cvc4.m4
Another way to handle negative contain
gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)
Merge branch '1.3.x'
add constant replace, indexof
add constant replace, indexof
Merge branch 'master' of github.com:tiliang/CVC4
move new functions under exp options
Add new method --quant-cf for finding conflicts eagerly for quantified formulas.  This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation.  Clean up the rewriter, other minor cleanup.
Add stats to quantifiers conflict find.  Added option for qcf.  Working on handling non-APPLY_UF terms.