Engine: prefix accelerated PikeVM #18
Merged
Conversation
This file contains hidden or 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
shilangyu
commented
Dec 5, 2025
shilangyu
force-pushed
the
mw/prefix-acc-pikevm
branch
from
0337e99 to
9178363
Compare
shilangyu
commented
Dec 11, 2025
shilangyu
commented
Dec 12, 2025
Collaborator
There was a problem hiding this comment.
Renamings Suggestions
-
lazy_treetolazy_iter: givent1andt2, what this describes is really just a single iteration -
.*_lazyprefix: how about.*_unanchored? These lemmas are only useful when doing unanchored matching. And againprefixhere has several meanings. (And I swear this is the last time I suggest "unanchored" for any renaming). -
nexttin PikeTree: how aboutfuture? It avoids the many meanings ofnext. And we had this conversation that it would also be nice to indicate that this only describes what happens if we try to match from the future positions onwards. Sofuturewould describe what happens if you try to start matching in the future. -
pvs_nextchar_generatehow aboutpvs_generate? Same forpvs_nextchar_filtertopvs_filter. -
pike_tree_accand associated lemmas: how abouttree_acceleration? We don't need thepikekeyword here, andaccelerationmight be easier to understand -
pike_tree_nextt_shapehow aboutfuture_tree_shape. Again I don't think thepikekeyword helps here
Collaborator
Author
To me the generate and filter steps are directly related to |
shilangyu
commented
Dec 17, 2025
Collaborator
Author
|
Rename commits to be |
They now support prefix acceleration with a simulation of the .*? prefix. This is optional, if the nextprefix is set to None, no acceleration and no .*? is used.
The only thing left to prove is the invariant_preservation. Then, Complexity might need a big overhaul to support the new algorithm.
WIP: prove restricted complexity
…s still one invariant missing about strictly advancing when accelerating
_lazyprefix -> _unanchored lazy_tree -> lazy_iter nextt -> future pike_tree_acc -> tree_acceleration
- remove empty lines in proofs or add a comment - remove large replaces - remove large asserts - remove eauto depth specifiers
shilangyu
force-pushed
the
mw/prefix-acc-pikevm
branch
from
84c3662 to
760478e
Compare
Collaborator
Author
|
I think everything is ready now! Once the CI passes and you give it a last look, feel free to merge @Aurele-Barriere! |
Collaborator
|
Amazing work! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.