Feature request: making delegates available when solving from a Yices context

[disteph]

So far, external SAT-solvers are only available through yices_check_formula / yices_check_formulas which don't use any Yices context; the assertions are just passed as arguments. At the moment if I have a Yices context containing some bitvector constraints, I have no choice but to make bitblasting target the built-in SAT-solver.

Level 1 of this feature would be to have the choice of the backend SAT-solver when doing check-sat on a context with only QF_BV constraints and that only allows a single call to check-sat (mimicking what happens with yices_check_formula / yices_check_formulas).

Level 2 of this feature would be to have the choice of the backend SAT-solver when doing check-sat on a context with only QF_BV constraints but that allows incremental checks and push-pop, relying on the incrementality of the backend SAT-solver or using assumptions.

Level 3 of this feature would be to have the choice of the backend SAT-solver when the context's constraints combine the bitvector theory with other theories, and when the context allows incremental checks and push-pop.