feat: Strict Ackermannization (bv_ac_eager) tactic for QF_UFBV

[bollu]

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.

[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 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)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2a891a3889a2cf1ac9e0499b4d11b596bfd9d410 --onto c5181569f959e4a0d9586954212125adcb6e44d0. (2024-12-05 09:14:01)

[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

[bollu]

changelog-library

[bollu]

awaiting-review

[bollu]

CC @hargoniX :)

[bollu]

awaiting-author

[bollu]

awaiting-review

[alexkeizer]

Suggested change

	| .bool => m!"bool"
	| .bitVec w => m!"BitVec {w}"
	| .bool => m!"bool"
	| .bitVec w => m!"bitVec {w}"

Consistently capitalize these, please!

[alexkeizer]

You might want to give this an actual descriptive docstring, and move the NOTE to a non-doc comment.

[alexkeizer]

Check your whitespace, I think this is indented one level too much

[alexkeizer]

Suggested change

	end CallInfo
	structure State where
	end CallInfo
	structure State where

[alexkeizer]

Suggested change

	def State.init : State where
	def State.init : State := {}

The where without anything after reads a bit weird to me, I'd prefer something more explicit, but this is pure aesthethics/taste, so feel free to ignore

[alexkeizer]

This seems like they were notes for the implementation, but do we want to keep them around?

[alexkeizer]

To me, "ack" means acknowledge. In the context of this file, the abbrevation makes sense, but for the namespace we might want to spell out Ackermannize fully

[alexkeizer]

Suggested change

	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.
	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.

[alexkeizer]

Suggested change

	This directory contains the lazy ackermannization tactic.
	This directory contains the eager ackermannization tactic.

[alexkeizer]

Does it actually integrate bv_decide into the tactic? I thought it rather reduces uninterpreted functions + bitvectors to bitvectors (which bv_decide can then solve by reduction to SAT)