From 1d39b6d5d46039fcdb92507d44bb0853549eb82c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Nov 2015 17:29:30 -0800
Subject: [PATCH] feat(util/rb_map): add erase_min

---
 src/util/rb_map.h | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/util/rb_map.h b/src/util/rb_map.h
index fe959cc582..19446bcd2b 100644
--- a/src/util/rb_map.h
+++ b/src/util/rb_map.h
@@ -38,6 +38,13 @@ public:
 
     unsigned get_rc() const { return m_map.get_rc(); }
 
+    T erase_min() {
+        lean_assert(!empty());
+        T r = m_map.min()->second;
+        m_map.erase_min();
+        return r;
+    }
+
     class ref {
         rb_map & m_map;
         K const &   m_key;