feat: change bv_decide to an elaborated config

[hargoniX]

This PR changes bv_decide's configuration from lots of set_option to an elaborated config like simp or omega. The notable exception is sat.solver which is still a set_option such that users can configure a custom SAT solver globally for an entire project or file. Additionally it introduces the ability to set maxSteps for the simp preprocessing run through the new config.

The latter feature was requested by people using bv_decide on SMTLIB which has ginormous terms that exceed the default.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9b167e20512640afbee5777462fa50ddb2e778d5 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-08 11:09:59)