mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

Add vector::erase_if

Browse source 
(ended up unused but I didn't want to throw it away)
This commit is contained in:
Jakob Rath 2023-03-05 12:59:20 +01:00
parent e0db58c998
commit 1ef01c5042
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/util/vector.h
View file

@ -556,6 +556,7 @@ public:
*prev = std::move(*pos); *prev = std::move(*pos);
} }
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--; reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
// TODO: where is the destructor called?
} }
void erase(T const & elem) { 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) { void shrink(SZ s) {
if (m_data) { if (m_data) {
SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]); SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]);