feat: lazy ackermannization for bv_decide #25
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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.
Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Alex Keizer <[email protected]>
Co-authored-by: Alex Keizer <[email protected]>
bollu
force-pushed
the
lazy-ackermannization
branch
from
a265977
to
7c1ee08
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.