mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

sparse_matrix iterators

Browse source
This commit is contained in:
Jakob Rath 2022-08-01 12:17:21 +02:00 • committed by Nikolaj Bjorner
parent 6eae27ffad
commit 9275d1e57a
4 changed files with 22 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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;

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

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

2
src/smt/theory_dense_diff_logic_def.h
View file

@ -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;

2
src/smt/theory_diff_logic_def.h
View file

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