From 98dfb1ba8665e030656a24f867385d59cf86c9dd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 23 Mar 2020 20:02:05 -0700 Subject: [PATCH] get rid of m_resize_buffer Signed-off-by: Lev Nachmanson --- src/math/lp/int_set.h | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/math/lp/int_set.h b/src/math/lp/int_set.h index be45714bf..8f047dd2e 100644 --- a/src/math/lp/int_set.h +++ b/src/math/lp/int_set.h @@ -25,7 +25,6 @@ namespace lp { // serves at a set of non-negative integers smaller than the set size class int_set { svector m_data; - svector m_resize_buffer; unsigned_vector m_index; public: @@ -33,7 +32,6 @@ public: int_set() {} int_set(int_set const& other): m_data(other.m_data), - m_resize_buffer(other.m_resize_buffer), m_index(other.m_index) {} bool contains(unsigned j) const { @@ -65,13 +63,14 @@ public: void resize(unsigned size) { if (size < data_size()) { - for (unsigned j: m_index) { - if (j > size) - m_resize_buffer.push_back(j); + unsigned i = 0; + for (unsigned j : m_index) { + if (j < size) { + m_data[j] = i; + m_index[i++] = j; + } } - for (unsigned j : m_resize_buffer) - erase(j); - m_resize_buffer.clear(); + m_index.shrink(i); } m_data.resize(size, -1); }