diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index a33ea55bdbc..ecba27af5e2 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -36,6 +36,8 @@ namespace simplex { numeral m_coeff; var_t m_var; row_entry(numeral && c, var_t v) : m_coeff(std::move(c)), m_var(v) {} + inline numeral const& coeff() const { return m_coeff; } + inline var_t var() const { return m_var; } }; private: @@ -202,17 +204,17 @@ namespace simplex { row_iterator row_begin(row const& r) { return row_iterator(m_rows[r.id()], true); } row_iterator row_end(row const& r) { return row_iterator(m_rows[r.id()], false); } - class row_vars { + class row_entries_t { friend class sparse_matrix; sparse_matrix& s; row r; - row_vars(sparse_matrix& s, row r): s(s), r(r) {} + row_entries_t(sparse_matrix& s, row r): s(s), r(r) {} public: row_iterator begin() { return s.row_begin(r); } row_iterator end() { return s.row_end(r); } }; - row_vars get_row(row r) { return row_vars(*this, r); } + row_entries_t get_row(row r) { return row_entries_t(*this, r); } unsigned column_size(var_t v) const { return m_columns[v].size(); } @@ -247,7 +249,8 @@ namespace simplex { row get_row() const { return row(m_col.m_entries[m_curr].m_row_id); } - row_entry& get_row_entry() { + + row_entry& get_row_entry() const { col_entry const& c = m_col.m_entries[m_curr]; int row_id = c.m_row_id; return m_rows[row_id].m_entries[c.m_row_idx]; @@ -263,6 +266,18 @@ namespace simplex { col_iterator col_begin(int v) { return col_iterator(m_columns[v], m_rows, true); } col_iterator col_end(int v) { return col_iterator(m_columns[v], m_rows, false); } + class col_entries_t { + friend class sparse_matrix; + sparse_matrix& m; + int v; + col_entries_t(sparse_matrix& m, int v): m(m), v(v) {} + public: + col_iterator begin() { return m.col_begin(v); } + col_iterator end() { return m.col_end(v); } + }; + + col_entries_t get_col(int v) { return col_entries_t(*this, v); } + class var_rows { friend class sparse_matrix; sparse_matrix& s; diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index dc3700f2e1e..255e62f1185 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -98,7 +98,7 @@ namespace simplex { if (!t1.is_dead()) { if (i != j) { _row_entry & t2 = m_entries[j]; - t2.m_coeff.swap(t1.m_coeff); + m.swap(t2.m_coeff, t1.m_coeff); t2.m_var = t1.m_var; t2.m_col_idx = t1.m_col_idx; SASSERT(!t2.is_dead()); diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 3a19b1c19b7..b5abc7a2a9d 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -1011,7 +1011,7 @@ namespace smt { expr_ref tmp(m); core.reset(); for (; it != end; ++it) { - unsigned v = it->m_var; + unsigned v = it->var(); if (num_nodes <= v && v < num_nodes + num_edges) { unsigned edge_id = v - num_nodes; literal lit = m_edges[edge_id].m_justification; diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index e9747c4ae1d..80fbe402200 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1283,7 +1283,7 @@ theory_diff_logic::maximize(theory_var v, expr_ref& blocker, bool& has_shar expr_ref tmp(m); core.reset(); for (; it != end; ++it) { - unsigned v = it->m_var; + unsigned v = it->var(); if (is_simplex_edge(v)) { unsigned edge_id = simplex2edge(v); literal lit = m_graph.get_explanation(edge_id);