Add repack to hashmap (#117)

* add repack on hashmap * ci update
epfl-lara · Dec 16, 2024 · 156890f · 156890f
1 parent 3fadc81
commit 156890f
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala b/data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala
@@ -232,6 +232,11 @@ object MutableHashMap {
 
     }.ensuring (res => valid && (if (res) map.eq(old(this).map - key) else map.eq(old(this).map)))
 
+    def repack(): Boolean = {
+      require(valid)
+      this.underlying.v.repack()
+    }.ensuring (res => res == false || map == old(this).map)
+
     @ghost
     override  def valid: Boolean = underlying.v.valid &&
       underlying.v.map.toList.forall((k, v) => noDuplicateKeys(v)) &&