Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h
for faster compilation
Revert Clark's last commit, at his request; there are some bugs.

This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
Re-enable predicate subtyping, reversing commit 8f9f549 (needed for Kind integration)
fix for lambdas in relation to subtypes
fixup for miplib trick (related to lambda fix for subtypes)
subrange-related fix
new --tear-down-incremental mode
new --force-logic option that overrides what the input says
more ITE rewrites
some of the minisat markers/assumption framework
Revert "subrange-related fix"

This reverts commit 771943753d540defa4e708667f70fee131462367.
some speculative rewriting/solving in BOOL and UF theories
crazy hack impl
more crazy hack