mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

bug fixes

Browse source 
values cannot change on basic variables from inequalities
arithmetic modulo can produce 0 coefficients
This commit is contained in:
Nikolaj Bjorner 2021-08-31 11:26:44 -07:00
parent d1118cb178
commit 05d564e828
3 changed files with 33 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -844,9 +844,8 @@ namespace polysat {
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));
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));
}
SASSERT(well_formed());
@ -1345,7 +1344,7 @@ namespace polysat {
if (m_vars[v].max() >= m_vars[w].max() && !new_bound(i, v, 0, m_vars[w].max(), vlo, vhi, wlo, whi))
return false;
if (value(v) >= value(w) && value(v) + 1 != 0 && m_vars[w].contains(value(v) + 1))
if (!is_base(w) && value(v) >= value(w) && value(v) + 1 != 0 && m_vars[w].contains(value(v) + 1))
update_value(w, value(v) - value(w) + 1);
return true;
@ -1364,7 +1363,7 @@ namespace polysat {
if (m_vars[v].max() > m_vars[w].max() && !new_bound(i, v, 0, m_vars[w].max() + 1, vlo, vhi, wlo, whi))
return false;
if (value(v) > value(w) && m_vars[w].contains(value(v)))
if (value(v) > value(w) && !is_base(w) && m_vars[w].contains(value(v)))
update_value(w, value(v) - value(w));
return true;
@ -1475,6 +1474,7 @@ namespace polysat {
if (s == null_var)
continue;
SASSERT(i == base2row(s).id());
VERIFY(well_formed_row(r));
}
for (unsigned i = 0; i < m_vars.size(); ++i) {

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

@ -289,7 +289,7 @@ namespace simplex {
col_entries_t col_entries(int v) { return col_entries_t(*this, v); }
void display(std::ostream& out);
void display_row(std::ostream& out, row const& r);
void display_row(std::ostream& out, row const& r) const;
bool well_formed() const;
void collect_statistics(::statistics & st) const;

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

@ -339,6 +339,10 @@ 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); \
@ -415,11 +419,25 @@ 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);
}
}
}
@ -492,7 +510,7 @@ namespace simplex {
if (e.is_dead()) {
dead.insert(i);
continue;
}
}
DEBUG_CODE(
SASSERT(!vars.contains(e.var()));
SASSERT(!m.is_zero(e.m_coeff));
@ -558,17 +576,18 @@ namespace simplex {
template<typename Ext>
void sparse_matrix<Ext>::display(std::ostream& out) {
for (unsigned i = 0; i < m_rows.size(); ++i) {
if (m_rows[i].size() == 0) continue;
display_row(out, row(i));
if (m_rows[i].size() != 0)
display_row(out, row(i));
}
}
template<typename Ext>
void sparse_matrix<Ext>::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->coeff());
out << "*v" << it->var() << " ";
void sparse_matrix<Ext>::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() << " ";
}
}
out << "\n";
}