perf: bv_decide inline all lets once at the beginning of preprocessing

[hargoniX]

This PR changes bv_decide's preprocessing to inline all let at the beginning of the pipeline once. This makes sure that when we actually start to rewrite in the fixed point pipeline, no let are there anymore. As DiscrTree matching in the rewriting steps involves traversing and instantiating the lets over and over again this can bring some drastic speedups:

baseline:
lake exe leanwuzla --maxRecDepth=8000 --maxHeartbeats=2000000 --disableEmbeddedConstraintSubst ../../smt/non-incremental/QF_BV/fft/Sz256_6616.smt2   30.02s

after this:
lake exe leanwuzla --maxRecDepth=8000 --maxHeartbeats=2000000 --disableEmbeddedConstraintSubst ../../smt/non-incremental/QF_BV/fft/Sz256_6616.smt2   4.15s

[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 4e885be96d82c522af4acb9ce9afe77e5aea7feb --onto 884a9ea2ff70bb4d0c6da4a1c23ffc26c3a974ee. (2024-11-24 11:47:01)

[hargoniX]

Obsoleted by the proper fix https://github.com/leanprover/lean4/pull/6220/