feat: bv_decide grind integration

[hargoniX]

This PR adds support for bv_decide to make use of the grind state when used in sym/grind interactive mode. bv_decide now picks up on the (relevant) equivalence classes, encodes them into the SAT problem and then handles the problem as normally.

This allows us to solve problems such as:

example (a b d : UInt8) (h0 : d = a ||| b)
    (h1 : g d &&& 0xC0 = 0) :
    g (a ||| b) &&& 0x40 = 0 := by
  grind =>
    bv_decide

In this case grind informs bv_decide through congruence closure. Other things such as facts learned by theory solvers or e-matching are also available.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for b27ccc9 against e5a38df are in. There are significant results. @hargoniX

• 🟥 build//instructions: +16.6G (+0.14%)

Medium changes (6🟥)

• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.Basic//instructions: +2.2G (+26.61%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.Enums//instructions: +1.1G (+13.18%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.Rewrite//instructions: +1.4G (+34.27%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.Structures//instructions: +1.6G (+30.94%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.TypeAnalysis//instructions: +2.0G (+27.60%) (reduced significance based on absolute threshold)
• 🟥 elab/bv_decide_large_aig//task-clock: +319ms (+9.69%)

Small changes (12🟥)

• 🟥 build/module/Lean.Elab.Tactic.BVDecide//instructions: +3.4G (+323.56%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Main//instructions: +200.9M (+14.14%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.AC//instructions: +309.8M (+3.85%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.AndFlatten//instructions: +804.2M (+24.88%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.EmbeddedConstraint//instructions: +625.4M (+21.25%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.IntToBitVec//instructions: +285.8M (+10.94%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.Reduction//instructions: +54.1M (+5.11%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize.ShortCircuit//instructions: +54.9M (+3.32%)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Normalize//instructions: +4.4G (+48.11%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Reflect.ReifiedLemmas//instructions: +12.6M (+0.71%)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Reflect//instructions: +9.7M (+0.98%)
• 🟥 elab/bv_decide_large_aig//wall-clock: +332ms (+10.03%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e5a38df11cfe1e806b9f57b65b338117c33ed33e --onto bd97ed8e35639e17a11d1490cbc46d994e7b4513. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-07 12:30:07)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e5a38df11cfe1e806b9f57b65b338117c33ed33e --onto c4e6b62c3d955ef20da94310797072f7c4c5fa2b. You can force reference manual CI using the force-manual-ci label. (2026-08-07 12:30:08)