Allow dynamic selection of the SAT solver with set-option

[bclement-ocp]

This patch adds support for (set-option :sat-solver) in the SMT-LIB frontend.

The patch mostly lifts SAT-independent bits out of Frontend.Make, allowing to use a first-class module stored on the Dolmen state to provide access to the frontend.

Changing solvers is only allowed in the initial state (before any assertions are made) as a forward-compatibility measure: it would currently be possible to switch solvers on the fly because we merely accumulate commands in the context and only call the solver on (check-sat), but allowing solver changes anywhere would make it harder to remove the command stack, which we will probably do at some point (see also #382).

The rationale behind this, as discussed offline, is to allow more flexibility in test files that require the use of a specific solver.

[Halbaroth]

LGTM :)

Thanks, it will be useful for non-regression tests :)

[Halbaroth]

Please run the linter before merging it ;)

[bclement-ocp]

Yes — I have also added "Check style" and "Check indentation" as required for merging in the repo settings.

(I usually only run check indent locally, not check style because it runs on all the files which makes it slow and incorrect)