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

add copy constructor to handle reference count miss-match

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-12 17:56:09 -07:00
parent 0d776ecf88
commit cf8b3a0788
2 changed files with 34 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/math/simplex/sparse_matrix.h
View file

@ -220,35 +220,48 @@ namespace simplex {
class col_iterator { class col_iterator {
friend class sparse_matrix; friend class sparse_matrix;
unsigned m_curr; unsigned m_curr;
column const& m_col; int m_var;
vector<_row> const& m_rows; sparse_matrix const& m_sm;
column const& col() const {
return m_sm.m_columns[m_var];
}
void move_to_used() { void move_to_used() {
while (m_curr < m_col.num_entries() && m_col.m_entries[m_curr].is_dead()) { while (m_curr < col().num_entries() && col().m_entries[m_curr].is_dead()) {
++m_curr; ++m_curr;
} }
} }
col_iterator(column const& c, vector<_row> const& r, bool begin):
m_curr(0), m_col(c), m_rows(r) { col_iterator(int var, sparse_matrix const& sm, bool begin):
++m_col.m_refs; m_curr(0), m_var(var), m_sm(sm) {
if (begin) { ++col().m_refs;
if (begin)
move_to_used(); move_to_used();
} else
else { m_curr = col().num_entries();
m_curr = m_col.num_entries();
}
} }
public: public:
~col_iterator() { ~col_iterator() {
--m_col.m_refs; --col().m_refs;
}
col_iterator(col_iterator const& other):
m_curr(other.m_curr),
m_var(other.m_var),
m_sm(other.m_sm) {
++col().m_refs;
} }
row get_row() const { row get_row() const {
return row(m_col.m_entries[m_curr].m_row_id); return row(col().m_entries[m_curr].m_row_id);
} }
row_entry const& get_row_entry() { row_entry const& get_row_entry() {
col_entry const& c = m_col.m_entries[m_curr]; col_entry const& c = col().m_entries[m_curr];
int row_id = c.m_row_id; int row_id = c.m_row_id;
return m_rows[row_id].m_entries[c.m_row_idx]; return m_sm.m_rows[row_id].m_entries[c.m_row_idx];
} }
col_iterator & operator++() { ++m_curr; move_to_used(); return *this; } col_iterator & operator++() { ++m_curr; move_to_used(); return *this; }
@ -258,8 +271,8 @@ namespace simplex {
col_iterator& operator*() { return *this; } col_iterator& operator*() { return *this; }
}; };
col_iterator col_begin(int v) const { return col_iterator(m_columns[v], m_rows, true); } col_iterator col_begin(int v) const { return col_iterator(v, *this, true); }
col_iterator col_end(int v) const { return col_iterator(m_columns[v], m_rows, false); } col_iterator col_end(int v) const { return col_iterator(v, *this, false); }
class col_entries_t { class col_entries_t {
sparse_matrix const& m; sparse_matrix const& m;

12
src/math/simplex/sparse_matrix_def.h
View file

@ -199,9 +199,8 @@ namespace simplex {
*/ */
template<typename Ext> template<typename Ext>
inline void sparse_matrix<Ext>::column::compress_if_needed(vector<_row> & rows) { inline void sparse_matrix<Ext>::column::compress_if_needed(vector<_row> & rows) {
if (size() * 2 < num_entries() && m_refs == 0) { if (size() * 2 < num_entries() && m_refs == 0)
compress(rows); compress(rows);
}
} }
template<typename Ext> template<typename Ext>
@ -390,7 +389,7 @@ namespace simplex {
int col_idx = r_entry.m_col_idx; int col_idx = r_entry.m_col_idx;
r.del_row_entry(pos); r.del_row_entry(pos);
column & c = m_columns[v]; column & c = m_columns[v];
c.del_col_entry(col_idx); c.del_col_entry(col_idx);
c.compress_if_needed(m_rows); c.compress_if_needed(m_rows);
} }
@ -399,11 +398,8 @@ namespace simplex {
*/ */
template<typename Ext> template<typename Ext>
void sparse_matrix<Ext>::neg(row r) { void sparse_matrix<Ext>::neg(row r) {
row_iterator it = row_begin(r); for (auto& r : row_entries(r))
row_iterator end = row_end(r); m.neg(r.m_coeff);
for (; it != end; ++it) {
m.neg(it->m_coeff);
}
} }
/** /**