feat: Strict Ackermannization tactic (bv_ac_eager) for QF_UFBV #5657

bollu · 2024-10-09T04:10:59Z

We implement strict Ackermannization,
which is an algorithmic technique to convert 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.

leanprover-community-bot · 2024-10-09T04:37:48Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git 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-mathlib branch. Try git 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-mathlib branch. Try git 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-mathlib branch. Try git rebase 2a891a3889a2cf1ac9e0499b4d11b596bfd9d410 --onto cb600ed9b436e4290b819b0529f8454490bffeb6. (2024-12-03 19:24:56)

src/Lean/Elab/Tactic/BVAckermannize.lean

alexkeizer

I did a partial pass, so far I'm missing some documentation to explain what's what, have not attempted to grok the correctness of the code yet

src/Lean/Elab/Tactic/BVAckermannize.lean

src/Std/Tactic/BVAckermannize.lean

tobiasgrosser · 2024-10-19T18:55:05Z

src/Std/Tactic/BVAckermannize/Syntax.lean

+example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
+  intros
+  bv_decide
+```


I don't see an uninterpreted function here.

src/Lean/Elab/Tactic/BVAckermannize.lean

hargoniX · 2024-11-22T22:11:27Z

src/Lean/Elab/Tactic/BVAckermannize.lean

+a `BVTy` into an App.
+-/
+def reifyAp (f : Expr) : OptionT MetaM (Function × Array Argument) := do
+  let xs := f.getAppArgs


what if we are working on a function like

f : Nat -> Bool -> Bool

applied to something like f 1 b. In this situation you would fully give up on reification even though it is very much possible to do this by using (f 1) as the function instead. Do we want this? And if so, how far do we want to push it? In theory we could even support things like f : Nat -> Bool -> Nat -> Bool.

Yes, that's a fair point, I do indeed bail out. I added a comment describing that it's currently very conservative, and that we can extend to handle a larger fragment.

src/Lean/Elab/Tactic/BVAckermannize.lean

hargoniX · 2024-11-22T22:27:53Z

src/Lean/Elab/Tactic/BVAckermannize.lean

+    return (mkAppN f args, g) -- NOTE: is there some way to use update to update this?
+
+
+partial def introAckForExpr (g : MVarId) (e : Expr) : AckM (Expr × MVarId) := do


Going directly under binders violates the invariant that we don't deal with loose bvars in MetaM, all important functions like isDefEq, whnf etc. rely on the fact that you do not do this. Is there a particular reason that you break the invariant here.

Furthermore despite being some of the larger functions in this file these are one of the only ones without a doc string.

src/Lean/Elab/Tactic/BVAckermannize.lean

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.

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 9, 2024