mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

adding K

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-09 16:47:26 -07:00
parent ad2445e423
commit 6a8ac5f9b1
4 changed files with 25 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,22 +25,25 @@ namespace simplex {
class sparse_matrix_ops {
public:
static void gauss_jordan(sparse_matrix<mpq_ext>& M) {
static void kernel(sparse_matrix<mpq_ext>& M, vector<vector<mpq>>& K) {
mpq_ext::numeral coeff;
vector<unsigned> c, d;
vector<unsigned> d;
bool_vector c;
unsigned m = M.num_vars();
for (unsigned v = 0; v < m; ++v)
c.push_back(0);
c.push_back(false);
for (auto const& row : M.get_rows()) {
// scan for non-zero variable in row
bool found = false;
d.push_back(0);
for (auto const& [coeff1, v] : M.get_row(row)) {
if (mpq_manager<false>::is_zero(coeff1))
continue;
found = true;
d.push_back(v);
c[v] = row.id() + 1;
if (c[v])
continue;
d.back() = v + 1;
c[v] = true;
// eliminate v from other rows.
for (auto const& [row2, row_entry2] : M.get_rows(v)) {
if (row.id() == row2.id())
@ -51,15 +54,21 @@ namespace simplex {
M.add(row2, coeff, row);
}
break;
}
if (!found)
d.push_back(0);
}
}
M.get_manager().del(coeff);
// TODO: do something with c and d
// TODO: extract kernel using d
for (unsigned k = 0; k < d.size(); ++k) {
if (d[k] != 0)
continue;
K.push_back(vector<mpq>());
for (unsigned i = 0; i < d.size(); ++i) {
// K.back().push_back(d[i] > 0 ? M[d[i]-1][k] : (i == k) ? 1 : 0);
}
}
}
};