mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

Vector updates from polysat branch (#7066)

Browse source 
* vector: add erase_if

* vector: generalize operator<<

* vector: fix missing destructor call
This commit is contained in:
Jakob Rath 2023-12-19 17:58:55 +01:00 committed by GitHub
parent 4c9f705cd1
commit 97d450868e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 18 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/util/vector.h
View file

@ -30,6 +30,7 @@ Revision History:
#include <functional>
#include <memory>
#include <type_traits>
#include <utility>
#include "util/memory_manager.h"
#include "util/hash.h"
#include "util/z3_exception.h"
@ -558,7 +559,7 @@ public:
for(; pos != e; ++pos, ++prev) {
*prev = std::move(*pos);
}
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
pop_back();
}
void erase(T const & elem) {
@ -568,6 +569,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]);
@ -756,7 +771,8 @@ using bool_vector = svector<bool>;
template<typename T>
inline std::ostream& operator<<(std::ostream& out, svector<T> const& v) {
for (unsigned u : v) out << u << " ";
for (auto const& x : v)
out << x << " ";
return out;
}