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.
TreapMap.merge
is a very flexible way to merge twoTreapMap
s, but it has a couple of drawbacks:null
values to be added to the result map (becausemerge
treatsnull
as meaning "remove this entry")The first issue can be a major performance problem if you're merging two large maps with a relatively small key intersection, and you only need to apply custom merge logic to the keys in the intersection. This turns out to be very common.
To address this, we add new methods to
TreapMap
:These apply the
merger
function only to the intersection of the two maps' keys, and don't permitmerger
to discard entries.union
preserves all non-intersecting entries from both maps, whileintersect
discards them.We also add parallel versions of both functions, following the example of
merge
/parallelMerge
.See https://github.com/Certora/EVMVerifier/pull/6819 for an example of where this can be used to get some significant performance benefits.