Enable model-based reduction technique for strings (#7680)

Enable model-based reduction technique for strings (#7680)

This changes our default strategy for deferring (some) reductions until after the model is constructed. It introduces the option `--strings-mbr` (model-based reduction) which is enabled by default.

When using model-based reductions, only *negatIve* contains and negative memberships are deferred for reduction/unfolding until LAST_CALL effort, where a candidate model is available. These steps are performed only if the constraints are not already satisfied in the model.  The intuition is that negative contains/membership are the *most* expensive constraints to process and are moreover the *least* likely to be false in the model.

It makes a few fixes to the extended/RE solvers:
- 2 kinds of inferences in `checkExtfEval` should not be performed for substitutions based on models
- The regular expression solver should not use inclusion tests to justify reduction of memberships when the basis for the reduction is an unfolded membership, due to the reasoning being potentially cyclic.  This led to a bogus model on a regression when the new strategy was enabled.

It also does minor refactoring of those solvers that was required for implementing the new policy.

This branch is +446-1 on SMT-LIB, with all gains coming on "sat" benchmarks, mostly from pyex.  It also solves 2 previously unsolved challenge Amazon benchmarks quickly.