perf: add a bitblasting cache for bv_decide's boolean substructure

[hargoniX]

This PR adds a bitblasting cache for the boolean substructure of problems that bv_decide works on in addition to the one used for bvexpr.

Unfortunately this is currently causing a regression on QF_BV/sage/app1/bench_1967.smt2 so probably shouldn't merge yet.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-04-21 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-04-21 10:33:06)

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 54d38720218fb6d777434ec6437648bf90418120. There were significant changes against commit 02f7a1dd41f034939acf49a5c2c590076cb26d8e:

  Benchmark                         Metric                  Change
  ==========================================================================
+ Init.Data.BitVec.Lemmas re-elab   branch-misses            -1.9% (-24.6 σ)
+ big_do                            task-clock               -4.4% (-13.7 σ)
+ big_do                            wall-clock               -4.5% (-45.7 σ)
- bv_decide_mul                     maxrss                    1.5%  (30.7 σ)
- channel.lean                      bounded0_spsc            14.7%  (30.4 σ)
+ deriv                             task-clock               -1.7% (-12.8 σ)
+ deriv                             wall-clock               -1.7% (-12.6 σ)
+ ilean roundtrip                   parse                    -7.5% (-11.2 σ)
+ lake build clean                  task-clock               -1.9% (-15.2 σ)
+ lake config tree                  task-clock               -4.3% (-11.9 σ)
+ lake config tree                  wall-clock               -4.1% (-11.0 σ)
+ liasolver                         task-clock               -8.2% (-33.8 σ)
+ liasolver                         wall-clock               -8.2% (-33.8 σ)
+ stdlib                            blocked                  -2.8% (-12.3 σ)
+ stdlib                            blocked (unaccounted)    -3.1% (-44.4 σ)
- stdlib                            instructions              1.1% (166.2 σ)
- stdlib                            maxrss                    3.7%  (21.1 σ)
+ stdlib                            task-clock               -2.1% (-11.8 σ)