feat: Strict Ackermannization for bitvector problems

We implement strict ackermannization,
which is an algorithmic technique to convert QF_BV+UF into QF_BV.

The implementation walks over the goals and the hypotheses.
When it encounters a function application `(f x1 x2 ... xn)`
where the type signature of `f` is `BitVec k1 -> BitVec k2 -> ... -> BitVec kn -> BitVec ko`,
it creates a new variable `fAppX : BitVec k0`, and an equation `fAppX = f x1 ... xn`.
Next, when it encounters another application of the same function `(f y1 y2 ... yn)`,
it creates a new variable `fAppY : BitVec k0`, and another equation `fAppY = f y1 ... yn`.

After the walk, we loop over all pairs of applications of the function `f` that we have abstracted.
In this case, we have `fAppX` and `fAppY`. For these, we build a extentionality equation, which says that if

```
hAppXAppYExt: x1 = x2 -> y1 = y2 -> ... xn = yn -> fAppX = fAppY
```

Intuitively, this is the only fact that they theory UF can propagate,
and we thus encode it directly as a SAT formula,
by abstracting out the actual function application into a new free variable.

This implementation creates the ackermann variables (`fAppX, fAppY`) first,
and then in a subsequent phase, adds all the ackermann equations (`hAppXAppYExt`).
This anticipates the next patches which will implement *incremental* ackermannization,
where we will use the counterexample from the model to selectively add ackerman equations.

src/Lean/Elab/Tactic.lean

@@ -44,3 +44,4 @@ import Lean.Elab.Tactic.DiscrTreeKey
 import Lean.Elab.Tactic.BVDecide
 import Lean.Elab.Tactic.BoolToPropSimps
 import Lean.Elab.Tactic.Classical
+import Lean.Elab.Tactic.BVAckermannize