mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 03:46:17 +00:00
Code Activity

fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-10 13:17:25 -07:00
parent 805443c8ab
commit 2928cc261c
1 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,21 +34,25 @@ namespace simplex {
for (unsigned v = 0; v < m; ++v) for (unsigned v = 0; v < m; ++v)
c.push_back(0); c.push_back(0);
unsigned nullity = 0, rank = 0;
for (auto const& row : M.get_rows()) { for (auto const& row : M.get_rows()) {
// scan for non-zero variable in row // scan for non-zero variable in row
bool found = false; bool found = false;
d.push_back(0); d.push_back(0);
++nullity;
for (auto& [coeff1, v] : M.get_row(row)) { for (auto& [coeff1, v] : M.get_row(row)) {
if (mpq_manager<false>::is_zero(coeff1)) if (mpq_manager<false>::is_zero(coeff1))
continue; continue;
if (c[v] != 0) if (c[v] != 0)
continue; continue;
--nullity;
++rank;
d.back() = v + 1; d.back() = v + 1;
c[v] = row.id() + 1; c[v] = row.id() + 1;
D = 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& [row2, row_entry2] : M.get_rows(v)) { for (auto [row2, row_entry2] : M.get_rows(v)) {
if (row.id() >= row2.id()) if (row.id() >= row2.id())
continue; continue;
mpq & m_js = row_entry2->m_coeff; mpq & m_js = row_entry2->m_coeff;
@ -59,7 +63,7 @@ namespace simplex {
continue; continue;
D = m_ik; D = m_ik;
mgr.set(m_ik, mpq(0)); mgr.set(m_ik, mpq(0));
for (auto& [row2, row_entry2] : M.get_rows(w)) { for (auto [row2, row_entry2] : M.get_rows(w)) {
if (row.id() >= row2.id()) if (row.id() >= row2.id())
continue; continue;
auto& m_js = M.get_coeff(row2, v); auto& m_js = M.get_coeff(row2, v);
@ -73,6 +77,13 @@ namespace simplex {
mgr.del(coeff); mgr.del(coeff);
std::cout << "nullity " << nullity << "\n";
std::cout << "rank " << rank << "\n";
unsigned_vector pivots(rank, 0u);
unsigned_vector nonpivots(nullity, 0u);
// TODO: extract kernel using d // TODO: extract kernel using d
for (unsigned k = 0; k < d.size(); ++k) { for (unsigned k = 0; k < d.size(); ++k) {
if (d[k] != 0) if (d[k] != 0)