perf: speed up reflection of if in bv_decide

[hargoniX]

This PR adds a slight performance improvement to reflection of if statements that I noticed by profiling Leanwuzla against SMTCOMP's non-incremental/QF_BV/fft/Sz256_6616.smt2.

In particular:

1. The profile showed about 4 percent of the total run time were spent constructing these decidable instances in reflection of if statements. We can construct them much quicker by hand as they always have the same structure
2. This delays construction of these statements until we actually generate the reflection proof that we wish to submit to the kernel. Thus if we encounter a SAT instad of an UNSAT problem we will not spend time generating these expressions anymore.

baseline
  Time (mean ± σ):     31.236 s ±  0.258 s
  Range (min … max):   30.899 s … 31.661 s    10 runs

after
  Time (mean ± σ):     30.671 s ±  0.288 s
  Range (min … max):   30.350 s … 31.156 s    10 runs

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6162 has successfully built against this PR. (2024-11-21 20:24:06) View Log