From b347117cf3a8a9143ab20d081cc198439d7fff76 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Jun 2014 10:02:54 -0700
Subject: [PATCH] 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 | 32 ++++++++++++++++++++++++++++++++
 src/util/scoped_map.h         | 12 ++++++++++++
 2 files changed, 44 insertions(+)

diff --git a/src/tests/util/scoped_map.cpp b/src/tests/util/scoped_map.cpp
index a97443e65..127df0a51 100644
--- a/src/tests/util/scoped_map.cpp
+++ b/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;
 }
diff --git a/src/util/scoped_map.h b/src/util/scoped_map.h
index 478856258..a5e976e4a 100644
--- a/src/util/scoped_map.h
+++ b/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 << "{";