feat: allow bv_decide users to configure the SAT solver

[hargoniX]

This PR adds a new solverMode field to bv_decide's configuration, allowing users to configure
the SAT solver for different kinds of workloads.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for bd1d227 against bba35e4 are in! @hargoniX

Small changes (5🟥)

• 🟥 build/module/Lean.Elab.Tactic.BVDecide.External//instructions: +43.8M (+1.7%)
• 🟥 build/module/Std.Tactic.BVDecide.Syntax//bytes .ilean: +1kiB (+17.1%)
• 🟥 build/module/Std.Tactic.BVDecide.Syntax//bytes .olean: +27kiB (+21.5%) (reduced significance based on *//lines)
• 🟥 build/module/Std.Tactic.BVDecide.Syntax//bytes .olean.server: +2kiB (+20.7%) (reduced significance based on *//lines)
• 🟥 build/module/Std.Tactic.BVDecide.Syntax//instructions: +88.1M (+5.7%) (reduced significance based on *//lines)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-30 13:05:21)

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-11847 has successfully built against this PR. (2025-12-30 13:11:41) View Log
• 🟡 Reference manual branch lean-pr-testing-11847 build against this PR didn't complete normally. (2025-12-30 13:12:41) View Log