mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

fix merge

Browse source
This commit is contained in:
Jakob Rath 2022-07-01 17:16:40 +02:00
parent e5e79c1d4b
commit 003896991d
6 changed files with 129 additions and 141 deletions
Download patch file Download diff file Expand all files Collapse all files

2
CMakeLists.txt
View file

@ -2,7 +2,7 @@
cmake_minimum_required(VERSION 3.4) cmake_minimum_required(VERSION 3.4)
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") 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 # Project version

1
src/math/polysat/constraint.h
View file

@ -18,6 +18,7 @@ Author:
#include "math/polysat/interval.h" #include "math/polysat/interval.h"
#include "math/polysat/search_state.h" #include "math/polysat/search_state.h"
#include "math/polysat/univariate/univariate_solver.h" #include "math/polysat/univariate/univariate_solver.h"
#include <iostream>
namespace polysat { namespace polysat {

64
src/math/polysat/fixplex_def.h
View file

@ -226,7 +226,7 @@ namespace polysat {
numeral base_coeff = 0; numeral base_coeff = 0;
numeral value = 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(); var_t v = e.var();
if (v == base_var) if (v == base_var)
base_coeff = e.coeff(); base_coeff = e.coeff();
@ -281,11 +281,13 @@ namespace polysat {
row r = base2row(v); row r = base2row(v);
numeral b = row2base_coeff(r); numeral b = row2base_coeff(r);
unsigned tz_b = m.trailing_zeros(b); unsigned tz_b = m.trailing_zeros(b);
for (auto col : M.col_entries(v)) { auto col_it = M.col_begin(v);
if (r.id() == col.get_row().id()) auto const col_end = M.col_end(v);
for (; col_it != col_end; ++col_it) {
if (r.id() == col_it.get_row().id())
continue; continue;
numeral value_v = value(v); 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 false;
} }
return true; return true;
@ -315,12 +317,12 @@ namespace polysat {
else { else {
unsigned tz = UINT_MAX; unsigned tz = UINT_MAX;
numeral coeff; numeral coeff;
for (auto c : M.col_entries(var)) { for (auto [r2, r2_entry] : M.get_col(var)) {
unsigned tzc = m.trailing_zeros(c.get_row_entry().coeff()); unsigned tzc = m.trailing_zeros(r2_entry->coeff());
if (tzc < tz) { if (tzc < tz) {
r = c.get_row(); r = r2;
tz = tzc; tz = tzc;
coeff = c.get_row_entry().coeff(); coeff = r2_entry->coeff();
if (tz == 0) if (tz == 0)
break; break;
} }
@ -362,11 +364,10 @@ namespace polysat {
// R.value += delta*v_coeff // R.value += delta*v_coeff
// s.value = - R.value / s_coeff // s.value = - R.value / s_coeff
// //
for (auto c : M.col_entries(v)) { for (auto [r, r_entry] : M.get_col(v)) {
row r = c.get_row();
row_info& ri = m_rows[r.id()]; row_info& ri = m_rows[r.id()];
var_t s = ri.m_base; 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); set_base_value(s);
add_patch(s); add_patch(s);
} }
@ -432,7 +433,7 @@ namespace polysat {
numeral delta_best = 0; numeral delta_best = 0;
bool best_in_bounds = false; 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(); var_t y = r.var();
numeral const& b = r.coeff(); numeral const& b = r.coeff();
if (x == y) if (x == y)
@ -497,7 +498,7 @@ namespace polysat {
unsigned max = get_num_vars(); unsigned max = get_num_vars();
var_t result = max; var_t result = max;
row r = base2row(x); 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(); var_t y = c.var();
if (x == y || y >= result) if (x == y || y >= result)
continue; continue;
@ -710,8 +711,8 @@ namespace polysat {
unsigned tz1 = m.trailing_zeros(b); unsigned tz1 = m.trailing_zeros(b);
if (tz1 == 0) if (tz1 == 0)
return true; return true;
for (auto col : M.col_entries(y)) { for (auto [_, r_entry] : M.get_col(y)) {
numeral c = col.get_row_entry().coeff(); numeral c = r_entry->coeff();
unsigned tz2 = m.trailing_zeros(c); unsigned tz2 = m.trailing_zeros(c);
if (tz1 > tz2) if (tz1 > tz2)
return false; return false;
@ -739,7 +740,7 @@ namespace polysat {
SASSERT(is_base(x)); SASSERT(is_base(x));
auto r = base2row(x); auto r = base2row(x);
mod_interval<numeral> range(0, 1); mod_interval<numeral> range(0, 1);
for (auto const& e : M.row_entries(r)) { for (auto const& e : M.get_row(r)) {
var_t v = e.var(); var_t v = e.var();
numeral const& c = e.coeff(); numeral const& c = e.coeff();
range += m_vars[v] * c; range += m_vars[v] * c;
@ -767,7 +768,7 @@ namespace polysat {
return false; return false;
numeral fixed = 0; numeral fixed = 0;
unsigned parity = UINT_MAX; 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(); var_t v = e.var();
auto c = e.coeff(); auto c = e.coeff();
if (is_fixed(v)) if (is_fixed(v))
@ -841,13 +842,15 @@ namespace polysat {
unsigned tz_b = m.trailing_zeros(b); unsigned tz_b = m.trailing_zeros(b);
for (auto const& col : M.col_entries(y)) { auto col_it = M.col_begin(y);
row r_z = col.get_row(); 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(); unsigned rz = r_z.id();
if (rz == rx) if (rz == rx)
continue; continue;
TRACE("fixplex", display_row(tout << "eliminate ", r_z, false) << "\n";); 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";); TRACE("fixplex", display_row(tout << "eliminated ", r_z, false) << "\n";);
add_patch(row2base(r_z)); add_patch(row2base(r_z));
} }
@ -904,7 +907,7 @@ namespace polysat {
SASSERT(is_base(v)); SASSERT(is_base(v));
auto row = base2row(v); auto row = base2row(v);
ptr_vector<u_dependency> todo; ptr_vector<u_dependency> todo;
for (auto const& e : M.row_entries(row)) { for (auto const& e : M.get_row(row)) {
var_t v = e.var(); var_t v = e.var();
todo.push_back(m_vars[v].m_lo_dep); todo.push_back(m_vars[v].m_lo_dep);
todo.push_back(m_vars[v].m_hi_dep); todo.push_back(m_vars[v].m_hi_dep);
@ -926,8 +929,8 @@ namespace polysat {
template<typename Ext> template<typename Ext>
int fixplex<Ext>::get_num_non_free_dep_vars(var_t x_j, int best_so_far) { int fixplex<Ext>::get_num_non_free_dep_vars(var_t x_j, int best_so_far) {
int result = is_non_free(x_j); int result = is_non_free(x_j);
for (auto const& col : M.col_entries(x_j)) { for (auto [r, _] : M.get_col(x_j)) {
var_t s = row2base(col.get_row()); var_t s = row2base(r);
result += is_non_free(s); result += is_non_free(s);
if (result > best_so_far) if (result > best_so_far)
return result; return result;
@ -1104,7 +1107,7 @@ namespace polysat {
y = null_var; y = null_var;
if (!row_is_integral(r)) if (!row_is_integral(r))
return false; return false;
for (auto const& e : M.row_entries(r)) { for (auto const& e : M.get_row(r)) {
var_t v = e.var(); var_t v = e.var();
if (is_fixed(v)) if (is_fixed(v))
continue; continue;
@ -1130,8 +1133,7 @@ namespace polysat {
return; return;
var_t z, u; var_t z, u;
numeral cz, cu; numeral cz, cu;
for (auto c : M.col_entries(x)) { for (auto [r2, _] : M.get_col(x)) {
auto r2 = c.get_row();
if (r1.id() == r2.id()) if (r1.id() == r2.id())
continue; continue;
if (!is_offset_row(r2, cz, z, cu, u)) if (!is_offset_row(r2, cz, z, cu, u))
@ -1299,7 +1301,7 @@ namespace polysat {
mod_interval<numeral> range(0, 1); mod_interval<numeral> range(0, 1);
numeral free_c = 0; numeral free_c = 0;
var_t free_v = null_var; 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(); var_t v = e.var();
numeral const& c = e.coeff(); numeral const& c = e.coeff();
if (is_free(v)) { if (is_free(v)) {
@ -1320,7 +1322,7 @@ namespace polysat {
SASSERT(in_bounds(free_v)); SASSERT(in_bounds(free_v));
return res; return res;
} }
for (auto const& e : M.row_entries(r)) { for (auto const& e : M.get_row(r)) {
var_t v = e.var(); var_t v = e.var();
SASSERT(!is_free(v)); SASSERT(!is_free(v));
auto range1 = range - m_vars[v] * e.coeff(); auto range1 = range - m_vars[v] * e.coeff();
@ -1406,7 +1408,7 @@ namespace polysat {
template<typename Ext> template<typename Ext>
u_dependency* fixplex<Ext>::row2dep(row const& r) { u_dependency* fixplex<Ext>::row2dep(row const& r) {
u_dependency* d = nullptr; 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(); 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_lo_dep, d);
d = m_deps.mk_join(m_vars[v].m_hi_dep, d); d = m_deps.mk_join(m_vars[v].m_hi_dep, d);
@ -1461,7 +1463,7 @@ namespace polysat {
template<typename Ext> template<typename Ext>
std::ostream& fixplex<Ext>::display_row(std::ostream& out, row const& r, bool values) const { std::ostream& fixplex<Ext>::display_row(std::ostream& out, row const& r, bool values) const {
out << r.id() << " := " << pp(row2value(r)) << " : "; 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(); var_t v = e.var();
if (e.coeff() != 1) if (e.coeff() != 1)
out << pp(e.coeff()) << " * "; out << pp(e.coeff()) << " * ";
@ -1502,7 +1504,7 @@ namespace polysat {
VERIFY(m_vars[s].m_is_base); VERIFY(m_vars[s].m_is_base);
numeral sum = 0; numeral sum = 0;
numeral base_coeff = row2base_coeff(r); 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(); sum += value(e.var()) * e.coeff();
SASSERT(s != e.var() || base_coeff == e.coeff()); SASSERT(s != e.var() || base_coeff == e.coeff());
} }

42
src/math/simplex/simplex_def.h
View file

@ -76,13 +76,13 @@ namespace simplex {
scoped_eps_numeral value(em), tmp(em); scoped_eps_numeral value(em), tmp(em);
row_iterator it = M.row_begin(r), end = M.row_end(r); row_iterator it = M.row_begin(r), end = M.row_end(r);
for (; it != end; ++it) { for (; it != end; ++it) {
var_t v = it->var(); var_t v = it->m_var;
if (v == base_var) { if (v == base_var) {
m.set(base_coeff, it->coeff()); m.set(base_coeff, it->m_coeff);
} }
else { else {
SASSERT(!is_base(v)); 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); em.add(value, tmp, value);
} }
} }
@ -97,8 +97,8 @@ namespace simplex {
bool first = true; bool first = true;
for (; it2 != end; ++it2) { for (; it2 != end; ++it2) {
if (!first) tout << " + "; if (!first) tout << " + ";
tout << "v" << it2->var() << " * "; tout << "v" << it2->m_var << " * ";
m.display(tout, it2->coeff()); tout << " "; m.display(tout, it2->m_coeff); tout << " ";
first = false; first = false;
} }
tout << "\n"; tout << "\n";
@ -176,7 +176,7 @@ namespace simplex {
new_value = vi.m_value; new_value = vi.m_value;
} }
// need to move var such that old_base comes in bound. // 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(is_base(var));
SASSERT(m_vars[var].m_base2row == r.id()); SASSERT(m_vars[var].m_base2row == r.id());
SASSERT(!below_lower(old_base) && !above_upper(old_base)); SASSERT(!below_lower(old_base) && !above_upper(old_base));
@ -285,10 +285,10 @@ namespace simplex {
void simplex<Ext>::display_row(std::ostream& out, row const& r, bool values) { void simplex<Ext>::display_row(std::ostream& out, row const& r, bool values) {
row_iterator it = M.row_begin(r), end = M.row_end(r); row_iterator it = M.row_begin(r), end = M.row_end(r);
for (; it != end; ++it) { for (; it != end; ++it) {
m.display(out, it->coeff()); m.display(out, it->m_coeff);
out << "*v" << it->var() << " "; out << "*v" << it->m_var << " ";
if (values) { 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 << em.to_string(vi.m_value);
out << " ["; out << " [";
if (vi.m_lower_valid) out << em.to_string(vi.m_lower); else out << "-oo"; 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) { for (; it != end; ++it) {
row r_k = it.get_row(); row r_k = it.get_row();
if (r_k.id() != r_i) { if (r_k.id() != r_i) {
a_kj = it.get_row_entry().coeff(); a_kj = it.get_row_entry().m_coeff;
a_kj.neg(); a_kj.neg();
M.mul(r_k, a_ij); M.mul(r_k, a_ij);
M.add(r_k, a_kj, row(r_i)); M.add(r_k, a_kj, row(r_i));
@ -439,7 +439,7 @@ namespace simplex {
var_t s = m_row2base[r.id()]; var_t s = m_row2base[r.id()];
var_info& si = m_vars[s]; var_info& si = m_vars[s];
scoped_eps_numeral delta2(em); 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.mul(delta, coeff, delta2);
em.div(delta2, si.m_base_coeff, delta2); em.div(delta2, si.m_base_coeff, delta2);
delta2.neg(); delta2.neg();
@ -555,9 +555,9 @@ namespace simplex {
row_iterator it = M.row_begin(r), end = M.row_end(r); row_iterator it = M.row_begin(r), end = M.row_end(r);
for (; it != end; ++it) { for (; it != end; ++it) {
var_t x_j = it->var(); var_t x_j = it->m_var;
if (x_i == x_j) continue; 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_neg = is_below ? m.is_neg(a_ij) : m.is_pos(a_ij);
bool is_pos = !is_neg; bool is_pos = !is_neg;
@ -618,8 +618,8 @@ namespace simplex {
row r(m_vars[x_i].m_base2row); row r(m_vars[x_i].m_base2row);
row_iterator it = M.row_begin(r), end = M.row_end(r); row_iterator it = M.row_begin(r), end = M.row_end(r);
for (; it != end; ++it) { for (; it != end; ++it) {
var_t x_j = it->var(); var_t x_j = it->m_var;
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_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)))) { if (x_i != x_j && ((!is_neg && above_lower(x_j)) || (is_neg && below_upper(x_j)))) {
SASSERT(!is_base(x_j)); SASSERT(!is_base(x_j));
@ -749,7 +749,7 @@ namespace simplex {
// //
var_t s = m_row2base[it.get_row().id()]; var_t s = m_row2base[it.get_row().id()];
var_info& vs = m_vars[s]; 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; numeral const& base_coeff = vs.m_base_coeff;
SASSERT(!m.is_zero(coeff)); SASSERT(!m.is_zero(coeff));
bool base_to_lower = (m.is_pos(coeff) != m.is_pos(base_coeff)) == to_lower; 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; bool inc_y = false;
for (; it != end; ++it) { for (; it != end; ++it) {
var_t x = it->var(); var_t x = it->m_var;
if (x == v) continue; 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))) { if ((inc_x && at_upper(x)) || (!inc_x && at_lower(x))) {
TRACE("simplex", tout << "v" << x << " pos: " << inc_x TRACE("simplex", tout << "v" << x << " pos: " << inc_x
<< " at upper: " << at_upper(x) << " at upper: " << at_upper(x)
@ -867,7 +867,7 @@ namespace simplex {
row r = it.get_row(); row r = it.get_row();
var_t s = m_row2base[r.id()]; var_t s = m_row2base[r.id()];
var_info& vi = m_vars[s]; 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; numeral const& a_ii = vi.m_base_coeff;
bool sign_eq = (m.is_pos(a_ii) == m.is_pos(a_ij)); bool sign_eq = (m.is_pos(a_ii) == m.is_pos(a_ij));
bool inc_s = sign_eq != inc_x_j; 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); row_iterator it = M.row_begin(r), end = M.row_end(r);
scoped_eps_numeral sum(em), tmp(em); scoped_eps_numeral sum(em), tmp(em);
for (; it != end; ++it) { 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; 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 (!em.is_zero(sum)) {
IF_VERBOSE(0, M.display_row(verbose_stream(), r);); IF_VERBOSE(0, M.display_row(verbose_stream(), r););

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

@ -32,19 +32,15 @@ namespace simplex {
typedef typename Ext::manager manager; typedef typename Ext::manager manager;
typedef unsigned var_t; typedef unsigned var_t;
struct row_entry {
class row_entry {
friend class sparse_matrix;
numeral m_coeff; numeral m_coeff;
var_t m_var; var_t m_var;
public:
row_entry(numeral && c, var_t v) : m_coeff(std::move(c)), m_var(v) {} row_entry(numeral && c, var_t v) : m_coeff(std::move(c)), m_var(v) {}
inline numeral const& coeff() const { return m_coeff; } inline numeral const& coeff() const { return m_coeff; }
inline var_t var() const { return m_var; } inline var_t var() const { return m_var; }
}; };
private: private:
struct column;
struct stats { struct stats {
unsigned m_add_rows; 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(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) {} _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; }
}; };
/** /**
@ -88,6 +84,7 @@ namespace simplex {
bool is_dead() const { return (unsigned) m_row_id == dead_id; } bool is_dead() const { return (unsigned) m_row_id == dead_id; }
}; };
struct column;
/** /**
\brief A row contains a base variable and set of \brief A row contains a base variable and set of
@ -111,7 +108,6 @@ namespace simplex {
int get_idx_of(var_t v) const; int get_idx_of(var_t v) const;
}; };
/** /**
\brief A column stores in which rows a variable occurs. \brief A column stores in which rows a variable occurs.
The column may have free/dead entries. The field m_first_free_idx The column may have free/dead entries. The field m_first_free_idx
@ -135,7 +131,6 @@ namespace simplex {
void del_col_entry(unsigned idx); void del_col_entry(unsigned idx);
}; };
manager& m; manager& m;
vector<_row> m_rows; vector<_row> m_rows;
svector<unsigned> m_dead_rows; // rows to recycle svector<unsigned> 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_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); } 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; friend class sparse_matrix;
sparse_matrix& s; sparse_matrix& s;
row r; 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: public:
row_iterator begin() { return s.row_begin(r); } row_iterator begin() { return s.row_begin(r); }
row_iterator end() { return s.row_end(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(); } unsigned column_size(var_t v) const { return m_columns[v].size(); }
@ -232,40 +227,33 @@ namespace simplex {
column const& m_col; column const& m_col;
vector<_row>& m_rows; vector<_row>& m_rows;
void move_to_used() { 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; ++m_curr;
} }
} }
col_iterator(column const& c, vector<_row>& r, bool begin): col_iterator(column const& c, vector<_row>& r, bool begin):
m_curr(0), m_col(c), m_rows(r) { m_curr(0), m_col(c), m_rows(r) {
++m_col.m_refs; ++m_col.m_refs;
if (begin) if (begin) {
move_to_used(); move_to_used();
else }
else {
m_curr = m_col.num_entries(); m_curr = m_col.num_entries();
} }
public:
~col_iterator() {
--col().m_refs;
} }
public:
col_iterator(col_iterator const& other): ~col_iterator() {
m_curr(other.m_curr), --m_col.m_refs;
m_var(other.m_var),
m_sm(other.m_sm) {
++m_col.m_refs;
} }
row get_row() const { 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]; col_entry const& c = m_col.m_entries[m_curr];
int row_id = c.m_row_id; 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<row, row_entry*> operator*() { return std::make_pair(get_row(), &get_row_entry()); } std::pair<row, row_entry*> operator*() { return std::make_pair(get_row(), &get_row_entry()); }
@ -273,12 +261,23 @@ namespace simplex {
col_iterator operator++(int) { col_iterator tmp = *this; ++*this; return tmp; } 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; }
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; }
}; };
col_iterator col_begin(int v) { return col_iterator(m_columns[v], m_rows, true); } 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); } 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 { class var_rows {
friend class sparse_matrix; friend class sparse_matrix;
sparse_matrix& s; sparse_matrix& s;
@ -331,8 +330,9 @@ namespace simplex {
return m_zero; return m_zero;
} }
void display(std::ostream& out); 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; bool well_formed() const;
manager& get_manager() { return m; } manager& get_manager() { return m; }
@ -357,4 +357,4 @@ namespace simplex {
typedef unsynch_mpq_inf_manager eps_manager; typedef unsynch_mpq_inf_manager eps_manager;
}; };
} };

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

@ -99,10 +99,10 @@ namespace simplex {
if (i != j) { if (i != j) {
_row_entry & t2 = m_entries[j]; _row_entry & t2 = m_entries[j];
m.swap(t2.m_coeff, t1.m_coeff); 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; t2.m_col_idx = t1.m_col_idx;
SASSERT(!t2.is_dead()); 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; col.m_entries[t2.m_col_idx].m_row_idx = j;
} }
j++; j++;
@ -138,8 +138,8 @@ namespace simplex {
unsigned idx = 0; unsigned idx = 0;
for (auto const& e : m_entries) { for (auto const& e : m_entries) {
if (!e.is_dead()) { if (!e.is_dead()) {
result_map[e.var()] = idx; result_map[e.m_var] = idx;
idxs.push_back(e.var()); idxs.push_back(e.m_var);
} }
++idx; ++idx;
} }
@ -150,7 +150,7 @@ namespace simplex {
int sparse_matrix<Ext>::_row::get_idx_of(var_t v) const { int sparse_matrix<Ext>::_row::get_idx_of(var_t v) const {
unsigned idx = 0; unsigned idx = 0;
for (auto const& e : m_entries) { for (auto const& e : m_entries) {
if (!e.is_dead() && e.var() == v) if (!e.is_dead() && e.m_var == v)
return idx; return idx;
++idx; ++idx;
} }
@ -199,9 +199,10 @@ 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>
const typename sparse_matrix<Ext>::col_entry * const typename sparse_matrix<Ext>::col_entry *
@ -344,10 +345,6 @@ namespace simplex {
r_entry.m_var = v; \ r_entry.m_var = v; \
m.set(r_entry.m_coeff, it->m_coeff); \ m.set(r_entry.m_coeff, it->m_coeff); \
_SET_COEFF_; \ _SET_COEFF_; \
if (m.is_zero(r_entry.m_coeff)) { \
r1.del_row_entry(row_idx); \
continue; \
} \
column & c = m_columns[v]; \ column & c = m_columns[v]; \
int col_idx; \ int col_idx; \
col_entry & c_entry = c.add_col_entry(col_idx); \ col_entry & c_entry = c.add_col_entry(col_idx); \
@ -358,7 +355,7 @@ namespace simplex {
else { \ else { \
/* variable v is in row1 */ \ /* variable v is in row1 */ \
_row_entry & r_entry = r1.m_entries[pos]; \ _row_entry & r_entry = r1.m_entries[pos]; \
SASSERT(r_entry.var() == v); \ SASSERT(r_entry.m_var == v); \
_ADD_COEFF_; \ _ADD_COEFF_; \
if (m.is_zero(r_entry.m_coeff)) { \ if (m.is_zero(r_entry.m_coeff)) { \
del_row_entry(r1, pos); \ del_row_entry(r1, pos); \
@ -394,7 +391,7 @@ namespace simplex {
template<typename Ext> template<typename Ext>
void sparse_matrix<Ext>::del_row_entry(_row& r, unsigned pos) { void sparse_matrix<Ext>::del_row_entry(_row& r, unsigned pos) {
_row_entry & r_entry = r.m_entries[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; 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];
@ -407,8 +404,11 @@ namespace simplex {
*/ */
template<typename Ext> template<typename Ext>
void sparse_matrix<Ext>::neg(row r) { void sparse_matrix<Ext>::neg(row r) {
for (auto& r : row_entries(r)) row_iterator it = row_begin(r);
m.neg(r.m_coeff); row_iterator end = row_end(r);
for (; it != end; ++it) {
m.neg(it->m_coeff);
}
} }
/** /**
@ -424,24 +424,10 @@ namespace simplex {
neg(r); neg(r);
} }
else { else {
bool has0 = false;
row_iterator it = row_begin(r); row_iterator it = row_begin(r);
row_iterator end = row_end(r); row_iterator end = row_end(r);
for (; it != end; ++it) { for (; it != end; ++it) {
m.mul(it->m_coeff, n, it->m_coeff); 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(); g.reset();
row_iterator it = row_begin(r), end = row_end(r); row_iterator it = row_begin(r), end = row_end(r);
for (; it != end && !m.is_one(g); ++it) { for (; it != end && !m.is_one(g); ++it) {
if (!m.is_int(it->coeff())) { if (!m.is_int(it->m_coeff)) {
g = numeral(1); g = numeral(1);
break; break;
} }
if (m.is_zero(g)) g = it->m_coeff; 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)) { if (m.is_zero(g)) {
g = numeral(1); g = numeral(1);
@ -517,13 +503,13 @@ namespace simplex {
continue; continue;
} }
DEBUG_CODE( DEBUG_CODE(
SASSERT(!vars.contains(e.var())); SASSERT(!vars.contains(e.m_var));
SASSERT(!m.is_zero(e.m_coeff)); SASSERT(!m.is_zero(e.m_coeff));
SASSERT(e.var() != dead_id); SASSERT(e.m_var != dead_id);
col_entry const& c = m_columns[e.var()].m_entries[e.m_col_idx]; 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_id == row_id);
SASSERT((unsigned)c.m_row_idx == i);); SASSERT((unsigned)c.m_row_idx == i););
vars.insert(e.var()); vars.insert(e.m_var);
} }
int idx = r.m_first_free_idx; int idx = r.m_first_free_idx;
while (idx != -1) { while (idx != -1) {
@ -552,7 +538,7 @@ namespace simplex {
DEBUG_CODE( DEBUG_CODE(
_row const& row = m_rows[c.m_row_id]; _row const& row = m_rows[c.m_row_id];
_row_entry const& r = row.m_entries[c.m_row_idx]; _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);); SASSERT((unsigned)r.m_col_idx == i););
rows.insert(c.m_row_id); rows.insert(c.m_row_id);
} }
@ -581,18 +567,17 @@ namespace simplex {
template<typename Ext> template<typename Ext>
void sparse_matrix<Ext>::display(std::ostream& out) { void sparse_matrix<Ext>::display(std::ostream& out) {
for (unsigned i = 0; i < m_rows.size(); ++i) { for (unsigned i = 0; i < m_rows.size(); ++i) {
if (m_rows[i].size() != 0) if (m_rows[i].size() == 0) continue;
display_row(out, row(i)); display_row(out, row(i));
} }
} }
template<typename Ext> template<typename Ext>
void sparse_matrix<Ext>::display_row(std::ostream& out, row const& r) const { void sparse_matrix<Ext>::display_row(std::ostream& out, row const& r) {
for (auto const& e : m_rows[r.id()].m_entries) { row_iterator it = row_begin(r), end = row_end(r);
if (!e.is_dead()) { for (; it != end; ++it) {
m.display(out, e.coeff()); m.display(out, it->m_coeff);
out << "*v" << e.var() << " "; out << "*v" << it->m_var << " ";
}
} }
out << "\n"; out << "\n";
} }