feat(util/scoped_map): add 'keep' method for closing a scope without undoing operations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/tests/util/scoped_map.cpp

@@ -56,7 +56,39 @@ static void tst1() {
     lean_assert(s.find(30) == s.end());
 }
 
+static void tst2() {
+    scoped_map<int, int> s;
+    s.push();
+    s.insert(10, 20);
+    lean_assert(s.find(10)->second == 20);
+    lean_assert(s.contains(10));
+    s.pop();
+    lean_assert(!s.contains(10));
+    s.push();
+    s.insert(10, 30);
+    lean_assert(s.find(10)->second == 30);
+    lean_assert(s.num_scopes() == 1);
+    s.keep();
+    lean_assert(s.num_scopes() == 0);
+    lean_assert(s.find(10)->second == 30);
+    s.push();
+    s.push();
+    s.insert(1, 3);
+    lean_assert(s.num_scopes() == 2);
+    lean_assert(s.find(1)->second == 3);
+    s.keep();
+    lean_assert(s.find(1)->second == 3);
+    lean_assert(s.num_scopes() == 1);
+    lean_assert(s.size() == 2);
+    s.pop();
+    lean_assert(!s.contains(1));
+    lean_assert(s.num_scopes() == 0);
+    lean_assert(s.find(10)->second == 30);
+    lean_assert(s.size() == 1);
+}
+
 int main() {
     tst1();
+    tst2();
     return has_violations() ? 1 : 0;
 }

src/util/scoped_map.h

@@ -93,6 +93,14 @@ public:
         m_scopes.resize(num_scopes() - num);
     }
 
+    /** \brief Remove the top scope without 'undoing' the operations. */
+    void keep() {
+        lean_assert(num_scopes() > 0);
+        m_scopes.pop_back();
+        if (at_base_lvl())
+            m_actions.clear();
+    }
+
     /** \brief Return true iff the map is empty */
     bool empty() const {
         return m_map.empty();
@@ -151,6 +159,10 @@ public:
         return m_map.end();
     }
 
+    bool contains(Key const & k) const {
+        return find(k) != end();
+    }
+
     /** \brief (For debugging) Display the content of this scoped map. */
     friend std::ostream & operator<<(std::ostream & out, scoped_map const & m) {
         out << "{";