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

bug fixes

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-01-05 17:00:54 -10:00 committed by Lev Nachmanson
parent 5158797233
commit 0027ae21e8
2 changed files with 17 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/math/lp/dioph_eq.cpp
View file

@ -292,14 +292,14 @@ namespace lp {
TRACE("dioph_eq", m_s.lra.print_term(*m_t, tout); tout << ", m_t->j() =" << m_t->j() << std::endl;);
if (!contains(m_s.m_active_terms, m_t)) {
for (int i = m_s.m_added_terms.size() - 1; i >= 0; --i) {
if (m_s.m_added_terms[i] == m_t) // the address is the same
if (i != m_s.m_added_terms.size() -1) m_s.m_added_terms[i] = m_s.m_added_terms.back();
m_s.m_added_terms.pop_back();
break;
if (m_s.m_added_terms[i] != m_t) continue;
// the address is the same
if (i != m_s.m_added_terms.size() -1) m_s.m_added_terms[i] = m_s.m_added_terms.back();
m_s.m_added_terms.pop_back();
return; // all is done since the term has not made it to entries, etc
}
return;
}
NOT_IMPLEMENTED_YET();
// deregister the term that has been activated
for (const auto & p: m_t->ext_coeffs()) {
auto it = m_s.m_columns_to_terms.find(p.var());
SASSERT(it != m_s.m_columns_to_terms.end());
@ -309,6 +309,15 @@ namespace lp {
}
}
TRACE("dioph_eq",
tout << "the deleted term column in m_l_matrix" << std::endl;
for (auto p: m_s.m_l_matrix.column(m_t->j())) {
tout << p.coeff()<< ", row " << p.var() << std::endl;
}
tout << "m_l_matrix has " << m_s.m_l_matrix.column_count() << std::endl;
tout << "and" << m_s.m_l_matrix.row_count() << " rows" << std::endl;
);
NOT_IMPLEMENTED_YET();
}
};

7
src/math/lp/lar_term.h
View file

@ -36,7 +36,7 @@ public:
lpvar j() const { return m_j; }
void set_j(unsigned j) {
m_j = j;
}
}
void add_monomial(const mpq& c, unsigned j) {
if (c.is_zero())
return;
@ -275,10 +275,7 @@ public:
const_iterator(u_map<mpq>::iterator it) : m_it(it) {}
bool operator==(const const_iterator &other) const { return m_it == other.m_it; }
bool operator!=(const const_iterator &other) const { return !(*this == other); }
// Return a pointer to the same object returned by operator*.
const ival* operator->() const {
return &(**this);
}
};
bool is_normalized() const {