From 003896991d630679877bc1327ac72eb5da4313ef Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 1 Jul 2022 17:16:40 +0200 Subject: [PATCH] fix merge --- CMakeLists.txt | 2 +- src/math/polysat/constraint.h | 1 + src/math/polysat/fixplex_def.h | 64 +++++++++++---------- src/math/simplex/simplex_def.h | 42 +++++++------- src/math/simplex/sparse_matrix.h | 84 ++++++++++++++-------------- src/math/simplex/sparse_matrix_def.h | 77 ++++++++++--------------- 6 files changed, 129 insertions(+), 141 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9b0d111e6..2f3633f0f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.8.18.0 LANGUAGES CXX) +project(Z3 VERSION 4.8.18.0 LANGUAGES CXX C) ################################################################################ # Project version diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 1e34e90b7..d8bb5da8b 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -18,6 +18,7 @@ Author: #include "math/polysat/interval.h" #include "math/polysat/search_state.h" #include "math/polysat/univariate/univariate_solver.h" +#include namespace polysat { diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 1464811b7..c7eb5e1dd 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -226,7 +226,7 @@ namespace polysat { numeral base_coeff = 0; numeral value = 0; - for (auto const& e : M.row_entries(r)) { + for (auto const& e : M.get_row(r)) { var_t v = e.var(); if (v == base_var) base_coeff = e.coeff(); @@ -281,11 +281,13 @@ namespace polysat { row r = base2row(v); numeral b = row2base_coeff(r); unsigned tz_b = m.trailing_zeros(b); - for (auto col : M.col_entries(v)) { - if (r.id() == col.get_row().id()) + auto col_it = M.col_begin(v); + auto const col_end = M.col_end(v); + for (; col_it != col_end; ++col_it) { + if (r.id() == col_it.get_row().id()) continue; numeral value_v = value(v); - if (!eliminate_var(r, col, tz_b, value_v)) + if (!eliminate_var(r, col_it, tz_b, value_v)) return false; } return true; @@ -315,12 +317,12 @@ namespace polysat { else { unsigned tz = UINT_MAX; numeral coeff; - for (auto c : M.col_entries(var)) { - unsigned tzc = m.trailing_zeros(c.get_row_entry().coeff()); + for (auto [r2, r2_entry] : M.get_col(var)) { + unsigned tzc = m.trailing_zeros(r2_entry->coeff()); if (tzc < tz) { - r = c.get_row(); + r = r2; tz = tzc; - coeff = c.get_row_entry().coeff(); + coeff = r2_entry->coeff(); if (tz == 0) break; } @@ -362,11 +364,10 @@ namespace polysat { // R.value += delta*v_coeff // s.value = - R.value / s_coeff // - for (auto c : M.col_entries(v)) { - row r = c.get_row(); + for (auto [r, r_entry] : M.get_col(v)) { row_info& ri = m_rows[r.id()]; var_t s = ri.m_base; - ri.m_value += delta * c.get_row_entry().coeff(); + ri.m_value += delta * r_entry->coeff(); set_base_value(s); add_patch(s); } @@ -432,7 +433,7 @@ namespace polysat { numeral delta_best = 0; bool best_in_bounds = false; - for (auto const& r : M.row_entries(r)) { + for (auto const& r : M.get_row(r)) { var_t y = r.var(); numeral const& b = r.coeff(); if (x == y) @@ -497,7 +498,7 @@ namespace polysat { unsigned max = get_num_vars(); var_t result = max; row r = base2row(x); - for (auto const& c : M.col_entries(r)) { + for (auto const& c : M.get_col(r)) { var_t y = c.var(); if (x == y || y >= result) continue; @@ -710,8 +711,8 @@ namespace polysat { unsigned tz1 = m.trailing_zeros(b); if (tz1 == 0) return true; - for (auto col : M.col_entries(y)) { - numeral c = col.get_row_entry().coeff(); + for (auto [_, r_entry] : M.get_col(y)) { + numeral c = r_entry->coeff(); unsigned tz2 = m.trailing_zeros(c); if (tz1 > tz2) return false; @@ -739,7 +740,7 @@ namespace polysat { SASSERT(is_base(x)); auto r = base2row(x); mod_interval range(0, 1); - for (auto const& e : M.row_entries(r)) { + for (auto const& e : M.get_row(r)) { var_t v = e.var(); numeral const& c = e.coeff(); range += m_vars[v] * c; @@ -767,7 +768,7 @@ namespace polysat { return false; numeral fixed = 0; unsigned parity = UINT_MAX; - for (auto const& e : M.row_entries(row(r))) { + for (auto const& e : M.get_row(row(r))) { var_t v = e.var(); auto c = e.coeff(); if (is_fixed(v)) @@ -841,13 +842,15 @@ namespace polysat { unsigned tz_b = m.trailing_zeros(b); - for (auto const& col : M.col_entries(y)) { - row r_z = col.get_row(); + auto col_it = M.col_begin(y); + auto const col_end = M.col_end(y); + for (; col_it != col_end; ++col_it) { + auto r_z = col_it.get_row(); unsigned rz = r_z.id(); if (rz == rx) continue; TRACE("fixplex", display_row(tout << "eliminate ", r_z, false) << "\n";); - VERIFY(eliminate_var(r_x, col, tz_b, old_value_y)); + VERIFY(eliminate_var(r_x, col_it, tz_b, old_value_y)); TRACE("fixplex", display_row(tout << "eliminated ", r_z, false) << "\n";); add_patch(row2base(r_z)); } @@ -904,7 +907,7 @@ namespace polysat { SASSERT(is_base(v)); auto row = base2row(v); ptr_vector todo; - for (auto const& e : M.row_entries(row)) { + for (auto const& e : M.get_row(row)) { var_t v = e.var(); todo.push_back(m_vars[v].m_lo_dep); todo.push_back(m_vars[v].m_hi_dep); @@ -926,8 +929,8 @@ namespace polysat { template int fixplex::get_num_non_free_dep_vars(var_t x_j, int best_so_far) { int result = is_non_free(x_j); - for (auto const& col : M.col_entries(x_j)) { - var_t s = row2base(col.get_row()); + for (auto [r, _] : M.get_col(x_j)) { + var_t s = row2base(r); result += is_non_free(s); if (result > best_so_far) return result; @@ -1104,7 +1107,7 @@ namespace polysat { y = null_var; if (!row_is_integral(r)) return false; - for (auto const& e : M.row_entries(r)) { + for (auto const& e : M.get_row(r)) { var_t v = e.var(); if (is_fixed(v)) continue; @@ -1130,8 +1133,7 @@ namespace polysat { return; var_t z, u; numeral cz, cu; - for (auto c : M.col_entries(x)) { - auto r2 = c.get_row(); + for (auto [r2, _] : M.get_col(x)) { if (r1.id() == r2.id()) continue; if (!is_offset_row(r2, cz, z, cu, u)) @@ -1299,7 +1301,7 @@ namespace polysat { mod_interval range(0, 1); numeral free_c = 0; var_t free_v = null_var; - for (auto const& e : M.row_entries(r)) { + for (auto const& e : M.get_row(r)) { var_t v = e.var(); numeral const& c = e.coeff(); if (is_free(v)) { @@ -1320,7 +1322,7 @@ namespace polysat { SASSERT(in_bounds(free_v)); return res; } - for (auto const& e : M.row_entries(r)) { + for (auto const& e : M.get_row(r)) { var_t v = e.var(); SASSERT(!is_free(v)); auto range1 = range - m_vars[v] * e.coeff(); @@ -1406,7 +1408,7 @@ namespace polysat { template u_dependency* fixplex::row2dep(row const& r) { u_dependency* d = nullptr; - for (auto const& e : M.row_entries(r)) { + for (auto const& e : M.get_row(r)) { var_t v = e.var(); d = m_deps.mk_join(m_vars[v].m_lo_dep, d); d = m_deps.mk_join(m_vars[v].m_hi_dep, d); @@ -1461,7 +1463,7 @@ namespace polysat { template std::ostream& fixplex::display_row(std::ostream& out, row const& r, bool values) const { out << r.id() << " := " << pp(row2value(r)) << " : "; - for (auto const& e : M.row_entries(r)) { + for (auto const& e : M.get_row(r)) { var_t v = e.var(); if (e.coeff() != 1) out << pp(e.coeff()) << " * "; @@ -1502,7 +1504,7 @@ namespace polysat { VERIFY(m_vars[s].m_is_base); numeral sum = 0; numeral base_coeff = row2base_coeff(r); - for (auto const& e : M.row_entries(r)) { + for (auto const& e : M.get_row(r)) { sum += value(e.var()) * e.coeff(); SASSERT(s != e.var() || base_coeff == e.coeff()); } diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index 1d9ed1819..bc02ce5ef 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -76,13 +76,13 @@ namespace simplex { scoped_eps_numeral value(em), tmp(em); row_iterator it = M.row_begin(r), end = M.row_end(r); for (; it != end; ++it) { - var_t v = it->var(); + var_t v = it->m_var; if (v == base_var) { - m.set(base_coeff, it->coeff()); + m.set(base_coeff, it->m_coeff); } else { SASSERT(!is_base(v)); - em.mul(m_vars[v].m_value, it->coeff(), tmp); + em.mul(m_vars[v].m_value, it->m_coeff, tmp); em.add(value, tmp, value); } } @@ -97,8 +97,8 @@ namespace simplex { bool first = true; for (; it2 != end; ++it2) { if (!first) tout << " + "; - tout << "v" << it2->var() << " * "; - m.display(tout, it2->coeff()); tout << " "; + tout << "v" << it2->m_var << " * "; + m.display(tout, it2->m_coeff); tout << " "; first = false; } tout << "\n"; @@ -176,7 +176,7 @@ namespace simplex { new_value = vi.m_value; } // need to move var such that old_base comes in bound. - update_and_pivot(old_base, var, re.coeff(), new_value); + update_and_pivot(old_base, var, re.m_coeff, new_value); SASSERT(is_base(var)); SASSERT(m_vars[var].m_base2row == r.id()); SASSERT(!below_lower(old_base) && !above_upper(old_base)); @@ -285,10 +285,10 @@ namespace simplex { void simplex::display_row(std::ostream& out, row const& r, bool values) { row_iterator it = M.row_begin(r), end = M.row_end(r); for (; it != end; ++it) { - m.display(out, it->coeff()); - out << "*v" << it->var() << " "; + m.display(out, it->m_coeff); + out << "*v" << it->m_var << " "; if (values) { - var_info const& vi = m_vars[it->var()]; + var_info const& vi = m_vars[it->m_var]; out << em.to_string(vi.m_value); out << " ["; if (vi.m_lower_valid) out << em.to_string(vi.m_lower); else out << "-oo"; @@ -405,7 +405,7 @@ namespace simplex { for (; it != end; ++it) { row r_k = it.get_row(); if (r_k.id() != r_i) { - a_kj = it.get_row_entry().coeff(); + a_kj = it.get_row_entry().m_coeff; a_kj.neg(); M.mul(r_k, a_ij); M.add(r_k, a_kj, row(r_i)); @@ -439,7 +439,7 @@ namespace simplex { var_t s = m_row2base[r.id()]; var_info& si = m_vars[s]; scoped_eps_numeral delta2(em); - numeral const& coeff = it.get_row_entry().coeff(); + numeral const& coeff = it.get_row_entry().m_coeff; em.mul(delta, coeff, delta2); em.div(delta2, si.m_base_coeff, delta2); delta2.neg(); @@ -555,9 +555,9 @@ namespace simplex { row_iterator it = M.row_begin(r), end = M.row_end(r); for (; it != end; ++it) { - var_t x_j = it->var(); + var_t x_j = it->m_var; if (x_i == x_j) continue; - numeral const & a_ij = it->coeff(); + numeral const & a_ij = it->m_coeff; bool is_neg = is_below ? m.is_neg(a_ij) : m.is_pos(a_ij); bool is_pos = !is_neg; @@ -618,8 +618,8 @@ namespace simplex { row r(m_vars[x_i].m_base2row); row_iterator it = M.row_begin(r), end = M.row_end(r); for (; it != end; ++it) { - var_t x_j = it->var(); - numeral const & a_ij = it->coeff(); + var_t x_j = it->m_var; + numeral const & a_ij = it->m_coeff; bool is_neg = is_below ? m.is_neg(a_ij) : m.is_pos(a_ij); if (x_i != x_j && ((!is_neg && above_lower(x_j)) || (is_neg && below_upper(x_j)))) { SASSERT(!is_base(x_j)); @@ -749,7 +749,7 @@ namespace simplex { // var_t s = m_row2base[it.get_row().id()]; var_info& vs = m_vars[s]; - numeral const& coeff = it.get_row_entry().coeff(); + numeral const& coeff = it.get_row_entry().m_coeff; numeral const& base_coeff = vs.m_base_coeff; SASSERT(!m.is_zero(coeff)); bool base_to_lower = (m.is_pos(coeff) != m.is_pos(base_coeff)) == to_lower; @@ -801,9 +801,9 @@ namespace simplex { bool inc_y = false; for (; it != end; ++it) { - var_t x = it->var(); + var_t x = it->m_var; if (x == v) continue; - bool inc_x = m.is_pos(it->coeff()) == m.is_pos(m_vars[v].m_base_coeff); + bool inc_x = m.is_pos(it->m_coeff) == m.is_pos(m_vars[v].m_base_coeff); if ((inc_x && at_upper(x)) || (!inc_x && at_lower(x))) { TRACE("simplex", tout << "v" << x << " pos: " << inc_x << " at upper: " << at_upper(x) @@ -867,7 +867,7 @@ namespace simplex { row r = it.get_row(); var_t s = m_row2base[r.id()]; var_info& vi = m_vars[s]; - numeral const& a_ij = it.get_row_entry().coeff(); + numeral const& a_ij = it.get_row_entry().m_coeff; numeral const& a_ii = vi.m_base_coeff; bool sign_eq = (m.is_pos(a_ii) == m.is_pos(a_ij)); bool inc_s = sign_eq != inc_x_j; @@ -1013,9 +1013,9 @@ namespace simplex { row_iterator it = M.row_begin(r), end = M.row_end(r); scoped_eps_numeral sum(em), tmp(em); for (; it != end; ++it) { - em.mul(m_vars[it->var()].m_value, it->coeff(), tmp); + em.mul(m_vars[it->m_var].m_value, it->m_coeff, tmp); sum += tmp; - SASSERT(s != it->var() || m.eq(m_vars[s].m_base_coeff, it->coeff())); + SASSERT(s != it->m_var || m.eq(m_vars[s].m_base_coeff, it->m_coeff)); } if (!em.is_zero(sum)) { IF_VERBOSE(0, M.display_row(verbose_stream(), r);); diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index d7c485719..ecba27af5 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -32,19 +32,15 @@ namespace simplex { typedef typename Ext::manager manager; typedef unsigned var_t; - - class row_entry { - friend class sparse_matrix; + struct row_entry { numeral m_coeff; var_t m_var; - public: 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: - struct column; struct stats { unsigned m_add_rows; @@ -69,7 +65,7 @@ namespace simplex { }; _row_entry(numeral && c, var_t v) : row_entry(std::move(c), v), m_col_idx(0) {} _row_entry() : row_entry(numeral(), dead_id), m_col_idx(0) {} - bool is_dead() const { return row_entry::var() == dead_id; } + bool is_dead() const { return row_entry::m_var == dead_id; } }; /** @@ -87,7 +83,8 @@ namespace simplex { col_entry(): m_row_id(0), m_row_idx(0) {} bool is_dead() const { return (unsigned) m_row_id == dead_id; } }; - + + struct column; /** \brief A row contains a base variable and set of @@ -111,31 +108,29 @@ namespace simplex { int get_idx_of(var_t v) const; }; - /** - \brief A column stores in which rows a variable occurs. - The column may have free/dead entries. The field m_first_free_idx - is a reference to the first free/dead entry. + \brief A column stores in which rows a variable occurs. + The column may have free/dead entries. The field m_first_free_idx + is a reference to the first free/dead entry. */ struct column { svector m_entries; - unsigned m_size; + unsigned m_size; int m_first_free_idx; mutable unsigned m_refs; - - column() :m_size(0), m_first_free_idx(-1), m_refs(0) {} + + column():m_size(0), m_first_free_idx(-1), m_refs(0) {} unsigned size() const { return m_size; } unsigned num_entries() const { return m_entries.size(); } void reset(); - void compress(vector<_row>& rows); - void compress_if_needed(vector<_row>& rows); + void compress(vector<_row> & rows); + void compress_if_needed(vector<_row> & rows); //void compress_singleton(vector<_row> & rows, unsigned singleton_pos); - col_entry const* get_first_col_entry() const; - col_entry& add_col_entry(int& pos_idx); + col_entry const * get_first_col_entry() const; + col_entry & add_col_entry(int & pos_idx); void del_col_entry(unsigned idx); }; - manager& m; vector<_row> m_rows; svector m_dead_rows; // rows to recycle @@ -209,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(); } @@ -232,53 +227,57 @@ namespace simplex { column const& m_col; vector<_row>& m_rows; void move_to_used() { - while (m_curr < col().num_entries() && col().m_entries[m_curr].is_dead()) { + while (m_curr < m_col.num_entries() && m_col.m_entries[m_curr].is_dead()) { ++m_curr; } } col_iterator(column const& c, vector<_row>& r, bool begin): m_curr(0), m_col(c), m_rows(r) { ++m_col.m_refs; - if (begin) + if (begin) { move_to_used(); - else + } + else { m_curr = m_col.num_entries(); + } } - public: - ~col_iterator() { - --col().m_refs; - } - - col_iterator(col_iterator const& other): - m_curr(other.m_curr), - m_var(other.m_var), - m_sm(other.m_sm) { - ++m_col.m_refs; + --m_col.m_refs; } row get_row() const { - return row(m_col.m_entries[m_curr].m_row_id); + 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_sm.m_rows[row_id].m_entries[c.m_row_idx]; + return m_rows[row_id].m_entries[c.m_row_idx]; } std::pair operator*() { return std::make_pair(get_row(), &get_row_entry()); } col_iterator & operator++() { ++m_curr; move_to_used(); return *this; } col_iterator operator++(int) { col_iterator tmp = *this; ++*this; return tmp; } bool operator==(col_iterator const & it) const { return m_curr == it.m_curr; } - bool operator!=(col_iterator const & it) const { return m_curr != it.m_curr; } - col_iterator& operator*() { return *this; } + bool operator!=(col_iterator const & it) const { return m_curr != it.m_curr; } }; 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; @@ -330,9 +329,10 @@ namespace simplex { return row.m_coeff; return m_zero; } + void display(std::ostream& out); - void display_row(std::ostream& out, row const& r) const; + void display_row(std::ostream& out, row const& r); bool well_formed() const; manager& get_manager() { return m; } @@ -357,4 +357,4 @@ namespace simplex { typedef unsynch_mpq_inf_manager eps_manager; }; -} +}; diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index ab25d0de3..255e62f11 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -99,10 +99,10 @@ namespace simplex { if (i != j) { _row_entry & t2 = m_entries[j]; m.swap(t2.m_coeff, t1.m_coeff); - t2.m_var = t1.var(); + t2.m_var = t1.m_var; t2.m_col_idx = t1.m_col_idx; SASSERT(!t2.is_dead()); - column & col = cols[t2.var()]; + column & col = cols[t2.m_var]; col.m_entries[t2.m_col_idx].m_row_idx = j; } j++; @@ -138,8 +138,8 @@ namespace simplex { unsigned idx = 0; for (auto const& e : m_entries) { if (!e.is_dead()) { - result_map[e.var()] = idx; - idxs.push_back(e.var()); + result_map[e.m_var] = idx; + idxs.push_back(e.m_var); } ++idx; } @@ -150,7 +150,7 @@ namespace simplex { int sparse_matrix::_row::get_idx_of(var_t v) const { unsigned idx = 0; for (auto const& e : m_entries) { - if (!e.is_dead() && e.var() == v) + if (!e.is_dead() && e.m_var == v) return idx; ++idx; } @@ -199,8 +199,9 @@ namespace simplex { */ template inline void sparse_matrix::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); + } } template @@ -344,10 +345,6 @@ namespace simplex { r_entry.m_var = v; \ m.set(r_entry.m_coeff, it->m_coeff); \ _SET_COEFF_; \ - if (m.is_zero(r_entry.m_coeff)) { \ - r1.del_row_entry(row_idx); \ - continue; \ - } \ column & c = m_columns[v]; \ int col_idx; \ col_entry & c_entry = c.add_col_entry(col_idx); \ @@ -358,7 +355,7 @@ namespace simplex { else { \ /* variable v is in row1 */ \ _row_entry & r_entry = r1.m_entries[pos]; \ - SASSERT(r_entry.var() == v); \ + SASSERT(r_entry.m_var == v); \ _ADD_COEFF_; \ if (m.is_zero(r_entry.m_coeff)) { \ del_row_entry(r1, pos); \ @@ -394,11 +391,11 @@ namespace simplex { template void sparse_matrix::del_row_entry(_row& r, unsigned pos) { _row_entry & r_entry = r.m_entries[pos]; - var_t v = r_entry.var(); + var_t v = r_entry.m_var; int col_idx = r_entry.m_col_idx; r.del_row_entry(pos); column & c = m_columns[v]; - c.del_col_entry(col_idx); + c.del_col_entry(col_idx); c.compress_if_needed(m_rows); } @@ -407,8 +404,11 @@ namespace simplex { */ template void sparse_matrix::neg(row r) { - for (auto& r : row_entries(r)) - m.neg(r.m_coeff); + row_iterator it = row_begin(r); + row_iterator end = row_end(r); + for (; it != end; ++it) { + m.neg(it->m_coeff); + } } /** @@ -424,25 +424,11 @@ namespace simplex { neg(r); } else { - bool has0 = false; row_iterator it = row_begin(r); row_iterator end = row_end(r); for (; it != end; ++it) { m.mul(it->m_coeff, n, it->m_coeff); - has0 |= m.is_zero(it->m_coeff); - } - if (has0) { - unsigned idx = 0; - unsigned_vector idxs; - _row& row = m_rows[r.id()]; - for (auto const& e : row.m_entries) { - if (!e.is_dead() && m.is_zero(e.m_coeff)) - idxs.push_back(idx); - ++idx; - } - for (unsigned idx : idxs) - del_row_entry(row, idx); - } + } } } @@ -471,12 +457,12 @@ namespace simplex { g.reset(); row_iterator it = row_begin(r), end = row_end(r); for (; it != end && !m.is_one(g); ++it) { - if (!m.is_int(it->coeff())) { + if (!m.is_int(it->m_coeff)) { g = numeral(1); break; } if (m.is_zero(g)) g = it->m_coeff; - else m.gcd(g, it->coeff(), g); + else m.gcd(g, it->m_coeff, g); } if (m.is_zero(g)) { g = numeral(1); @@ -515,15 +501,15 @@ namespace simplex { if (e.is_dead()) { dead.insert(i); continue; - } + } DEBUG_CODE( - SASSERT(!vars.contains(e.var())); + SASSERT(!vars.contains(e.m_var)); SASSERT(!m.is_zero(e.m_coeff)); - SASSERT(e.var() != dead_id); - col_entry const& c = m_columns[e.var()].m_entries[e.m_col_idx]; + SASSERT(e.m_var != dead_id); + col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx]; SASSERT((unsigned)c.m_row_id == row_id); SASSERT((unsigned)c.m_row_idx == i);); - vars.insert(e.var()); + vars.insert(e.m_var); } int idx = r.m_first_free_idx; while (idx != -1) { @@ -552,7 +538,7 @@ namespace simplex { DEBUG_CODE( _row const& row = m_rows[c.m_row_id]; _row_entry const& r = row.m_entries[c.m_row_idx]; - SASSERT(r.var() == v); + SASSERT(r.m_var == v); SASSERT((unsigned)r.m_col_idx == i);); rows.insert(c.m_row_id); } @@ -581,18 +567,17 @@ namespace simplex { template void sparse_matrix::display(std::ostream& out) { for (unsigned i = 0; i < m_rows.size(); ++i) { - if (m_rows[i].size() != 0) - display_row(out, row(i)); + if (m_rows[i].size() == 0) continue; + display_row(out, row(i)); } } template - void sparse_matrix::display_row(std::ostream& out, row const& r) const { - for (auto const& e : m_rows[r.id()].m_entries) { - if (!e.is_dead()) { - m.display(out, e.coeff()); - out << "*v" << e.var() << " "; - } + void sparse_matrix::display_row(std::ostream& out, row const& r) { + row_iterator it = row_begin(r), end = row_end(r); + for (; it != end; ++it) { + m.display(out, it->m_coeff); + out << "*v" << it->m_var << " "; } out << "\n"; }