`TreapMap.keys` as `TreapSet` #20

ericeil · 2024-12-21T17:31:26Z

Currently it is quite expensive to do operations like this:

set2 = map1.keys intersect set1

This is because the keys property on TreapMap is an ImmuableSet, not a TreapSet, so the intersection operation must convert it to a TreapSet first, using the generic Set->TreapSet conversion, which is rather expensive.

This is a shame, because a TreapMap<K, V> of course is already structured the same way as a TreapSet<K>, so the conversion to TreapSet should be very cheap.

This PR redefines the keys property as a TreapSet, and defines efficient implementations of this. Depending on usage, we can sometimes avoid the conversion to TreapSet altogether; if not, we can do the conversion as a straightforward projection of the existing TreapMap structure, avoiding most of the overhead of the generic conversion.

We also add single and singleOrNull methods to TreapMap, which are useful in their own right, and can be used to avoid the conversion to TreapSet in some cases.

Currently it is quite expensive to do operations like this: ``` set2 = map1.keys intersect set1 ``` This is because the `keys` property on `TreapMap` is an `ImmuableSet`, not a `TreapSet`, so the intersection operation must convert it to a `TreapSet` first, using the generic `Set`->`TreapSet` conversion, which is rather expensive. This is a shame, because a `TreapMap<K, V>` of course is already structured the same way as a `TreapSet<K>`, so the conversion to `TreapSet` should be very cheap. This PR redefines the `keys` property as a `TreapSet`, and defines efficient implementations of this. Depending on usage, we may be able to avoid the conversion to `TreapSet` altogether; if not, we can do the conversion as a straightforward projection of the existing `TreapMap` structure, avoiding most of the overhead of the generic conversion. We also add `single` and `singleOrNull` methods to `TreapMap`, which are useful in their own right, and can be used to avoid the conversion to `TreapSet` in some cases.

yoav-rodeh

some questions

yoav-rodeh · 2025-01-07T01:36:14Z

collect/src/main/kotlin/com/certora/collect/SortedTreapSet.kt

-    override fun shallowGetSingleElement(): E = treapKey
+    override fun singleOrNull(): E? = treapKey.takeIf { left == null && right == null }
+    override fun single(): E = treapKey.also {
+        if (left != null || right != null) { throw IllegalArgumentException("Set contains more than one element") }


any reason not to do (here and also in the hash version)

override fun single(): E = singleOrNull() ?: throw ...

E might be nullable, so singleOrNull doesn't give the correct behavior.

yoav-rodeh · 2025-01-07T01:46:14Z

collect/src/main/kotlin/com/certora/collect/AbstractKeySet.kt

+    override fun singleOrNull() = map.singleOrNull()?.key
+    override fun arbitraryOrNull() = map.arbitraryOrNull()?.key
+
+    override fun containsAny(elements: Iterable<K>) = keys.value.containsAny(elements)


why do you create the keys set for containsAny and containsAll?
is it because if elements happens to be a TreapSet it's more efficient?

but then if elements is not then then can be pretty costly. I'm especially thinking of the case where keys is very large and elements is tiny. You'll run in time O(|keys|).

maybe you can check here if elements is a TreapSet or not, and according to that choose what to do?

Yes, I'm opting for simplicity here. The problem you point out (large map, small elements) is still a problem even if everything's a treap. Optimizing that is tricky, since getting the size of a Treap (as you point out elsewhere) is surprisingly expensive.

We could have different cases here:

Empty elements

Single Treap element

Non-treap (maybe broken down further by size?)

...but I'd much rather just keep this simple for now. It's possible we will never even use this method. :)

alright, I agree it's likely that calling these will be pretty rare.

yoav-rodeh · 2025-01-07T01:47:50Z

collect/src/main/kotlin/com/certora/collect/AbstractKeySet.kt

+    Presents the keys of a [TreapMap] as a [TreapSet].
+
+    The idea here is that a `TreapMap<K, *>` is stored with the same Treap structure as a `TreapSet<K>`, so we can very
+    quickly create the corresponding `TreapSet<K>` when needed, in O(1) time.


I think it's O(n) time, instead of the naive algorithm to create the set, which would take O(n log(n)), no?

Haha yes, this was really wishful thinking. :)

(At one point I thought I could do this in O(1) time, by having the maps actually implement TreapSet, but that idea didn't pan out)

yoav-rodeh · 2025-01-07T01:51:36Z

collect/src/main/kotlin/com/certora/collect/AbstractKeySet.kt

+    override fun toString() = keys.value.toString()
+
+    override val size get() = map.size
+    override fun isEmpty() = map.isEmpty()


i always find it very unintuitive that size for treaps is an expensive operation. No avoiding it really I guess...

Well, we could store the size in the treap nodes, but of course that increases memory usage. So far this still seems like the right tradeoff.

yoav-rodeh · 2025-01-07T01:55:33Z

collect/src/main/kotlin/com/certora/collect/SortedTreapSet.kt

@@ -27,6 +27,7 @@ internal class SortedTreapSet<@Treapable E>(
    override fun Iterable<E>.toTreapSetOrNull(): SortedTreapSet<E>? =
        (this as? SortedTreapSet<E>)
        ?: (this as? PersistentSet.Builder<E>)?.build() as? SortedTreapSet<E>


a question about line 29, how come you check if it is a PresistentSet.Builder and not SortedTreapSet.Builder?

There is no SortedTreapSet.Builder.

yoav-rodeh · 2025-01-07T01:56:02Z

collect/src/main/kotlin/com/certora/collect/SortedTreapMap.kt

+    private fun treapSetFromKeys(): SortedTreapSet<K> =
+        SortedTreapSet(treapKey, left?.treapSetFromKeys(), right?.treapSetFromKeys())
+
+    @Suppress("Treapability")


why do you suppress here?

The treapability analysis doesn't see that the superclass's hashCode implementation is stable. I'll fix this a different way.

yoav-rodeh · 2025-01-07T01:58:37Z

collect/src/main/kotlin/com/certora/collect/SortedTreapMap.kt

+
+    @Suppress("Treapability")
+    class KeySet<@Treapable K>(
+        override val map: SortedTreapMap<K, *>,


is there no avoiding the * here?
can't KeySet be an inner class, and then you get K and V for free?

It didn't occur to me to make this an inner class! That's a good idea (though you'll see the * pop up elsewhere after this change :) )

… mapKeys

jtoman · 2025-01-07T19:09:44Z

collect/src/main/kotlin/com/certora/collect/HashTreapSet.kt

+    override fun single(): E = element.also {
+        if (next != null || left != null || right != null) { throw IllegalArgumentException("Set contains more than one element") }
+    }


just because you can write something as a one liner, doesn't mean you should.

This "post fixing" conditional stuff sucks in ruby, let's not bring it into kotlin :)

jtoman · 2025-01-07T19:15:00Z

collect/src/main/kotlin/com/certora/collect/SortedTreapSet.kt

-    override fun shallowGetSingleElement(): E = treapKey
+    override fun singleOrNull(): E? = treapKey.takeIf { left == null && right == null }
+    override fun single(): E = treapKey.also {
+        if (left != null || right != null) { throw IllegalArgumentException("Set contains more than one element") }


same objection as above. Just use a block body

jtoman · 2025-01-07T19:19:17Z

collect/src/main/kotlin/com/certora/collect/HashTreapMap.kt

@@ -31,6 +31,7 @@ internal class HashTreapMap<@Treapable K, V>(
        this as? HashTreapMap<K, V>
        ?: (this as? PersistentMap.Builder<K, V>)?.build() as? HashTreapMap<K, V>

+    override fun singleOrNull() = MapEntry(key, value).takeIf { next == null && left == null && right == null }


you might wonder why I don't object to this, where I am objecting to the also nonsense. I confess I don't have a great rule of thumb, except this looks more idiomatic, and the takeIf is clearly indicating what's happening, whereas using also to exceptionally abort is pretty surprising

yoav-rodeh

lgtm!

ericeil force-pushed the mapKeys branch from e342176 to 7d71fc3 Compare January 2, 2025 20:00

ericeil changed the title ~~TreapMap.keys as TreapSet~~ TreapMap.keys as TreapSet Jan 2, 2025

ericeil marked this pull request as ready for review January 2, 2025 20:02

ericeil requested review from jtoman and yoav-rodeh January 2, 2025 20:03

Remove potentially misleading comment

fb82689

yoav-rodeh reviewed Jan 7, 2025

View reviewed changes

ericeil added 2 commits January 7, 2025 08:17

Yoav's CR

19cd783

Merge branch 'mapKeys' of github.com:ericeil/certora-collections into…

fe1c6d9

… mapKeys

ericeil requested a review from yoav-rodeh January 7, 2025 16:18

jtoman requested changes Jan 7, 2025

View reviewed changes

John's feedback

861593a

ericeil requested a review from jtoman January 7, 2025 19:25

yoav-rodeh approved these changes Jan 7, 2025

View reviewed changes

jtoman approved these changes Jan 7, 2025

View reviewed changes

Merge branch 'main' into mapKeys

d77f633

ericeil enabled auto-merge (squash) January 7, 2025 20:48

ericeil merged commit e2d8c8e into Certora:main Jan 7, 2025
1 check passed

ericeil deleted the mapKeys branch January 7, 2025 20:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`TreapMap.keys` as `TreapSet` #20

`TreapMap.keys` as `TreapSet` #20

ericeil commented Dec 21, 2024 •

edited

Loading

yoav-rodeh left a comment

yoav-rodeh Jan 7, 2025

ericeil Jan 7, 2025

yoav-rodeh Jan 7, 2025

ericeil Jan 7, 2025 •

edited

Loading

yoav-rodeh Jan 7, 2025

yoav-rodeh Jan 7, 2025

ericeil Jan 7, 2025

yoav-rodeh Jan 7, 2025

ericeil Jan 7, 2025

yoav-rodeh Jan 7, 2025

ericeil Jan 7, 2025

yoav-rodeh Jan 7, 2025

ericeil Jan 7, 2025

yoav-rodeh Jan 7, 2025

ericeil Jan 7, 2025

jtoman Jan 7, 2025

ericeil Jan 7, 2025

jtoman Jan 7, 2025

jtoman Jan 7, 2025

yoav-rodeh left a comment

TreapMap.keys as TreapSet #20

TreapMap.keys as TreapSet #20

Conversation

ericeil commented Dec 21, 2024 • edited Loading

yoav-rodeh left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ericeil Jan 7, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

yoav-rodeh left a comment

Choose a reason for hiding this comment

`TreapMap.keys` as `TreapSet` #20

`TreapMap.keys` as `TreapSet` #20

ericeil commented Dec 21, 2024 •

edited

Loading

ericeil Jan 7, 2025 •

edited

Loading