From 1ef01c5042ac52e35be5df1a51c10d7a0ebcfd33 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Sun, 5 Mar 2023 12:59:20 +0100
Subject: [PATCH] Add vector::erase_if

(ended up unused but I didn't want to throw it away)
---
 src/util/vector.h | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/util/vector.h b/src/util/vector.h
index 5b7eaa1c2..d575c8304 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -556,6 +556,7 @@ public:
             *prev = std::move(*pos);
         }
         reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
+        // TODO: where is the destructor called?
     }
 
     void erase(T const & elem) {
@@ -565,6 +566,20 @@ public:
         }
     }
 
+    /** Erase all elements that satisfy the given predicate. Returns the number of erased elements. */
+    template <typename UnaryPredicate>
+    SZ erase_if(UnaryPredicate should_erase) {
+        iterator i = begin();
+        iterator const e = end();
+        for (iterator j = begin(); j != e; ++j)
+            if (!should_erase(std::as_const(*j)))
+                *(i++) = std::move(*j);
+        SZ const count = e - i;
+        SASSERT_EQ(i - begin(), size() - count);
+        shrink(size() - count);
+        return count;
+    }
+
     void shrink(SZ s) {
         if (m_data) {
             SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]);