mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

get rid of m_resize_buffer

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-23 20:02:05 -07:00
parent 2975873b91
commit 98dfb1ba86
1 changed files with 7 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/lp/int_set.h
View file

@ -25,7 +25,6 @@ namespace lp {
// serves at a set of non-negative integers smaller than the set size // serves at a set of non-negative integers smaller than the set size
class int_set { class int_set {
svector<int> m_data; svector<int> m_data;
svector<int> m_resize_buffer;
unsigned_vector m_index; unsigned_vector m_index;
public: public:
@ -33,7 +32,6 @@ public:
int_set() {} int_set() {}
int_set(int_set const& other): int_set(int_set const& other):
m_data(other.m_data), m_data(other.m_data),
m_resize_buffer(other.m_resize_buffer),
m_index(other.m_index) {} m_index(other.m_index) {}
bool contains(unsigned j) const { bool contains(unsigned j) const {
@ -65,13 +63,14 @@ public:
void resize(unsigned size) { void resize(unsigned size) {
if (size < data_size()) { if (size < data_size()) {
for (unsigned j: m_index) { unsigned i = 0;
if (j > size) for (unsigned j : m_index) {
m_resize_buffer.push_back(j); if (j < size) {
m_data[j] = i;
m_index[i++] = j;
}
} }
for (unsigned j : m_resize_buffer) m_index.shrink(i);
erase(j);
m_resize_buffer.clear();
} }
m_data.resize(size, -1); m_data.resize(size, -1);
} }