diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index f231dc0a9..f72f86438 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -174,8 +174,6 @@ namespace lp { else if (val != numeric_traits::one()) out << T_to_string(val); out << "x"; - if (is_fresh_var(j)) - out << "~"; out << j; } @@ -374,7 +372,7 @@ namespace lp { void register_columns_to_term(const lar_term& t) { TRACE("dioph_eq", tout << "register term:"; lra.print_term(t, tout);); - for (const auto &p: t) { + for (const auto &p: t.ext_coeffs()) { auto it = m_columns_to_terms.find(p.var()); if (it != m_columns_to_terms.end()) { it->second.insert(t.j()); @@ -405,7 +403,7 @@ namespace lp { m_e_matrix.add_row(); SASSERT(m_e_matrix.row_count() == m_entries.size()); - for (const auto& p : t) { + for (const auto& p : t.ext_coeffs()) { SASSERT(p.coeff().is_int()); if (is_fixed(p.var())) e.m_c += p.coeff() * lia.lower_bound(p.var()).x; @@ -415,13 +413,6 @@ namespace lp { m_e_matrix.add_new_element(entry_index, lj, p.coeff()); } } - if (is_fixed(t.j())) { - e.m_c -= lia.lower_bound(t.j()).x; - } else { - unsigned lj = add_var(t.j()); - m_e_matrix.add_columns_up_to(lj); - m_e_matrix.add_new_element(entry_index, lj, -mpq(1)); - } SASSERT(entry_invariant(entry_index)); } @@ -866,7 +857,7 @@ namespace lp { print_lar_term_L(term_to_tighten, tout) << std::endl; tout << "m_tmp_l:"; print_lar_term_L(m_tmp_l, tout) << std::endl; tout << "open_ml:"; - print_term_o(open_ml(m_tmp_l), tout) << std::endl; + print_lar_term_L(open_ml(m_tmp_l), tout) << std::endl; tout << "term_to_tighten + open_ml:"; print_term_o(term_to_tighten + open_ml(m_tmp_l), tout) << std::endl; @@ -1307,7 +1298,7 @@ namespace lp { for (unsigned k = 0; k < lra.terms().size(); k ++ ) { const lar_term* t = lra.terms()[k]; if (!all_vars_are_int(*t)) continue; - for (const auto& p: *t) { + for (const auto& p: (*t).ext_coeffs()) { unsigned j = p.var(); auto it = c2t.find(j); if (it == c2t.end()) { @@ -1317,7 +1308,8 @@ namespace lp { } else { it->second.insert(t->j()); } - + + } } for (const auto & p : c2t) { @@ -1502,14 +1494,14 @@ namespace lp { { tout << "get_term_from_entry(" << ei << "):"; print_term_o(get_term_from_entry(ei), tout) << std::endl; - tout << "remove_fresh_vars:"; + tout << "ls:"; print_term_o(remove_fresh_vars(get_term_from_entry(ei)), tout) << std::endl; tout << "e.m_l:"; print_lar_term_L(l_term_from_row(ei), tout) << std::endl; tout << "open_ml(e.m_l):"; - print_term_o(open_ml(l_term_from_row(ei)), tout) << std::endl; - tout << "fix_vars(open_ml(e.m_l)):"; - print_term_o(fix_vars(open_ml(l_term_from_row(ei))), tout) << std::endl; + print_lar_term_L(open_ml(l_term_from_row(ei)), tout) << std::endl; + tout << "rs:"; + print_term_o(fix_vars(open_ml(m_l_matrix.m_rows[ei])), tout) << std::endl; } ); return ret; @@ -1544,7 +1536,7 @@ namespace lp { std::ostream& print_ml(const lar_term& ml, std::ostream& out) { term_o opened_ml = open_ml(ml); - return print_term_o(opened_ml, out); + return print_lar_term_L(opened_ml, out); } template term_o open_ml(const T& ml) const { @@ -1564,7 +1556,7 @@ namespace lp { m_indexed_work_vector.clear(); for (const auto & p: m_l_matrix.m_rows[ei]) { const lar_term& t = lra.get_term(p.var()); - for (const auto & q: t) { + for (const auto & q: t.ext_coeffs()) { if (is_fixed(q.var())) { c += p.coeff()*q.coeff()*lia.lower_bound(q.var()).x; } else { @@ -1572,13 +1564,6 @@ namespace lp { m_indexed_work_vector.add_value_at_index(q.var(), p.coeff() * q.coeff()); } } - if (is_fixed(t.j())) { - c -= lia.lower_bound(t.j()).x; - } - else { - make_space_in_work_vector(t.j()); - m_indexed_work_vector.add_value_at_index(t.j(), -p.coeff()); - } } } diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index ad4f2eba5..0fc376a71 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -30,6 +30,8 @@ protected: // the column index related to the term lpvar m_j = -1; public: + + // the column index related to the term lpvar j() const { return m_j; } void set_j(unsigned j) { @@ -92,8 +94,6 @@ public: } // constructors lar_term() = default; -<<<<<<< HEAD -======= lar_term(lar_term&& other) noexcept = default; // copy assignment operator lar_term& operator=(const lar_term& other) = default; @@ -106,7 +106,6 @@ public: } } ->>>>>>> 956229fb6 (test that pivoting is correct in dioph_eq.cpp) lar_term(const vector>& coeffs) { for (auto const& p : coeffs) { add_monomial(p.first, p.second); @@ -257,10 +256,9 @@ public: m_coeffs.reset(); } - class ival { + struct ival { lpvar m_var; const mpq & m_coeff; - public: ival(lpvar var, const mpq & val) : m_var(var), m_coeff(val) { } lpvar j() const { return m_var; } lpvar var() const { return m_var; } @@ -274,7 +272,12 @@ public: const_iterator operator++() { const_iterator i = *this; m_it++; return i; } const_iterator operator++(int) { m_it++; return *this; } const_iterator(u_map::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 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 { @@ -316,5 +319,101 @@ public: } const_iterator begin() const { return m_coeffs.begin();} const_iterator end() const { return m_coeffs.end(); } + // This iterator yields all (coefficient, variable) pairs + // plus one final pair: (mpq(-1), j()). + class ext_const_iterator { + // We'll store a reference to the lar_term, and an + // iterator into m_coeffs. Once we reach end of m_coeffs, + // we'll yield exactly one extra pair, then we are done. + const lar_term& m_term; + lar_term::const_iterator m_it; + bool m_done; // Have we gone past m_coeffs? + + public: + // Construct either a "begin" iterator (end=false) or "end" iterator (end=true). + ext_const_iterator(const lar_term& t, bool is_end) + : m_term(t) + , m_it(is_end ? t.end() : t.begin()) + , m_done(false) + { + // If it is_end == true, we represent a genuine end-iterator. + if (is_end) { + m_done = true; + } + } + + // Compare iterators. Two iterators are equal if both are "done" or hold the same internal iterator. + bool operator==(ext_const_iterator const &other) const { + // They are equal if they are both at the special extra pair or both at the same spot in m_coeffs. + if (m_done && other.m_done) { + return true; + } + return (!m_done && !other.m_done && m_it == other.m_it); + } + + bool operator!=(ext_const_iterator const &other) const { + return !(*this == other); + } + + // Return the element we point to: + // 1) If we haven't finished m_coeffs, yield (coefficient, var). + // 2) If we've iterated past m_coeffs exactly once, return (mpq(-1), j()). + auto operator*() const { + if (!m_done && m_it != m_term.end()) { + // Normal monomial from m_coeffs + // Each entry is of type { m_value, m_key } in this context + return *m_it; + } + else { + // We've gone past normal entries, so return the extra pair + // (mpq(-1), j()). + return ival(m_term.j(), rational::minus_one()); + } + } + + // Pre-increment + ext_const_iterator& operator++() { + if (!m_done && m_it != m_term.end()) { + ++m_it; + } + else { + // We were about to return that extra pair: + // after we move once more, we are done. + m_done = true; + } + return *this; + } + + // Post-increment + ext_const_iterator operator++(int) { + ext_const_iterator temp(*this); + ++(*this); + return temp; + } + }; + + // Return the begin/end of our extended iteration. + // begin: starts at first real monomial + // end: marks a finalized end of iteration + ext_const_iterator ext_coeffs_begin() const { + return ext_const_iterator(*this, /*is_end=*/false); + } + ext_const_iterator ext_coeffs_end() const { + return ext_const_iterator(*this, /*is_end=*/true); + } + + // Provide a small helper for "range-based for": + // for (auto & [coef, var] : myTerm.ext_coeffs()) { ... } + struct ext_range { + ext_const_iterator b, e; + ext_const_iterator begin() const { return b; } + ext_const_iterator end() const { return e; } + }; + + // return an object that can be used in range-based for loops + ext_range ext_coeffs() const { + return { ext_coeffs_begin(), ext_coeffs_end() }; + } + }; }