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

wip

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-10 11:17:34 -07:00
parent 0557d72d1c
commit 805443c8ab
2 changed files with 36 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -221,13 +221,13 @@ namespace simplex {
friend class sparse_matrix; friend class sparse_matrix;
unsigned m_curr; unsigned m_curr;
column const& m_col; column const& m_col;
vector<_row> const& m_rows; vector<_row>& m_rows;
void move_to_used() { void move_to_used() {
while (m_curr < m_col.num_entries() && m_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> const& 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) {
@ -245,21 +245,21 @@ namespace simplex {
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 const& get_row_entry() const { row_entry& get_row_entry() {
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_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 const*> 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()); }
col_iterator & operator++() { ++m_curr; move_to_used(); return *this; } col_iterator & operator++() { ++m_curr; move_to_used(); return *this; }
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 col_begin(int v) const { 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) const { 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 var_rows { class var_rows {
friend class sparse_matrix; friend class sparse_matrix;
@ -306,6 +306,13 @@ namespace simplex {
all_rows get_rows() { return all_rows(*this); } all_rows get_rows() { return all_rows(*this); }
numeral& get_coeff(row r, unsigned v) {
for (auto & [coeff, u] : get_row(r))
if (u == v)
return coeff;
throw default_exception("variable not in row");
}
void display(std::ostream& out); void display(std::ostream& out);
void display_row(std::ostream& out, row const& r); void display_row(std::ostream& out, row const& r);

38
src/math/simplex/sparse_matrix_ops.h
View file

@ -27,7 +27,7 @@ namespace simplex {
public: public:
static void kernel(sparse_matrix<mpq_ext>& M, vector<vector<rational>>& K) { static void kernel(sparse_matrix<mpq_ext>& M, vector<vector<rational>>& K) {
mpq_ext::numeral coeff; mpq_ext::numeral coeff;
rational D1, D2; rational D;
vector<unsigned> d, c; vector<unsigned> d, c;
unsigned m = M.num_vars(); unsigned m = M.num_vars();
auto& mgr = M.get_manager(); auto& mgr = M.get_manager();
@ -45,27 +45,26 @@ namespace simplex {
continue; continue;
d.back() = v + 1; d.back() = v + 1;
c[v] = row.id() + 1; c[v] = row.id() + 1;
D1 = rational(-1) / coeff1; D = rational(-1) / coeff1;
mgr.set(coeff1, mpq(-1)); mgr.set(coeff1, mpq(-1));
// eliminate v from other rows. // eliminate v from other rows.
for (auto const& [row2, row_entry2] : M.get_rows(v)) { for (auto& [row2, row_entry2] : M.get_rows(v)) {
if (row.id() >= row2.id() || row_entry2->m_coeff == 0) if (row.id() >= row2.id())
continue; continue;
for (auto& [coeff2, w] : M.get_row(row2)) { mpq & m_js = row_entry2->m_coeff;
if (v == w) mgr.set(m_js, (D * m_js).to_mpq());
mgr.set(coeff2, (D1*coeff2).to_mpq());
} }
} for (auto& [m_ik, w] : M.get_row(row)) {
for (auto& [coeff2, w] : M.get_row(row)) {
if (v == w) if (v == w)
continue; continue;
D2 = coeff2; D = m_ik;
mgr.set(coeff2, mpq(0)); mgr.set(m_ik, mpq(0));
for (auto const& [row2, row_entry2] : M.get_rows(w)) { for (auto& [row2, row_entry2] : M.get_rows(w)) {
if (row.id() >= row2.id() || row_entry2->m_coeff == 0 || row_entry2->m_var == v) if (row.id() >= row2.id())
continue; continue;
// mgr.set(row_entry2->m_coeff, row_entry2->m_coeff + D2*row2[v]); auto& m_js = M.get_coeff(row2, v);
auto & m_is = row_entry2->m_coeff;
mgr.set(m_is, (m_is + D * m_js).to_mpq());
} }
} }
break; break;
@ -80,7 +79,14 @@ namespace simplex {
continue; continue;
K.push_back(vector<rational>()); K.push_back(vector<rational>());
for (unsigned i = 0; i < d.size(); ++i) { for (unsigned i = 0; i < d.size(); ++i) {
// K.back().push_back(d[i] > 0 ? M[d[i]-1][k] : (i == k) ? 1 : 0); if (d[i] > 0) {
// row r = row(i);
// K.back().push_back(M[d[i]-1][k]);
}
else if (i == k)
K.back().push_back(rational(1));
else
K.back().push_back(rational(0));
} }
} }