leanprover
feat: Strict Ackermannization (bv_ac_eager) tactic for QF_UFBV
This PR implements strict Ackermannization, which is an algorithmic technique to reduce QF_UFBV 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 we have abstracted. In this case, we have fAppX and fAppY. For these, we build an extensionality equation, which says that if
hAppXAppYExt: x1 = x2 -> y1 = y2 -> ... xn = yn -> fAppX = fAppY
Intuitively, this is the only fact that the 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.
Mathlib CI status (docs):
- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase b814be6d6a5334784b172db15fd7fea39b4e3233 --onto 3e75d8f74297bc258352f8d89f71496aacefe7ae. (2024-10-09 04:37:48) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase fc4305ab15d7137f6bda64a557dc2ca9c6fc460f --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-21 19:15:57) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase fc4305ab15d7137f6bda64a557dc2ca9c6fc460f --onto cb600ed9b436e4290b819b0529f8454490bffeb6. (2024-12-03 15:24:30) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase 2a891a3889a2cf1ac9e0499b4d11b596bfd9d410 --onto cb600ed9b436e4290b819b0529f8454490bffeb6. (2024-12-03 19:24:56) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase 2a891a3889a2cf1ac9e0499b4d11b596bfd9d410 --onto c5181569f959e4a0d9586954212125adcb6e44d0. (2024-12-05 09:14:01)
