sparse_matrix iterators

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;

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());

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;

src/smt/theory_diff_logic_def.h

@@ -1283,7 +1283,7 @@ theory_diff_logic<Ext>::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);