From e34217656ebb74cf42915d7a185a3112b580972f Mon Sep 17 00:00:00 2001 From: Eric Eilebrecht Date: Thu, 2 Jan 2025 08:12:05 -0800 Subject: [PATCH] Comments --- .../com/certora/collect/AbstractKeySet.kt | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/collect/src/main/kotlin/com/certora/collect/AbstractKeySet.kt b/collect/src/main/kotlin/com/certora/collect/AbstractKeySet.kt index f67719b..8748786 100644 --- a/collect/src/main/kotlin/com/certora/collect/AbstractKeySet.kt +++ b/collect/src/main/kotlin/com/certora/collect/AbstractKeySet.kt @@ -1,7 +1,28 @@ package com.certora.collect +/** + Presents the keys of a [TreapMap] as a [TreapSet]. + + The idea here is that a `TreapMap` is stored with the same Treap structure as a `TreapSet`, so we can very + quickly create the corresponding `TreapSet` when needed, in O(1) time. + + We lazily initialize the set, so that we don't create it until we need it. For many operations, we can avoid + creating the set entirely, and just use the map directly. However, many operations, e.g. [addAll]/[union] and + [retainAll/intersect], are much more efficient when we have a [TreapSet], so we create it when needed. + + Note: It would be really nice if we could just treat the [TreapMap] objects themselves as [TreapSet] objects, but + this presents some problems. The most fundamental problem is that the [TreapMap] and [TreapSet] interfaces have + methods that are not compatible; for example, they both implement [Iterable], but with different element types. + */ internal abstract class AbstractKeySet<@Treapable K, S : TreapSet> : TreapSet { + /** + The map whose keys we are presenting as a set. We prefer to use the map directly when possible, so we don't + need to create the set. + */ abstract val map: AbstractTreapMap + /** + The set of keys. This is a lazy property so that we don't create the set until we need it. + */ abstract val keys: Lazy @Suppress("Treapability")