From fc1c8c4cc42907e6820801ef204f6dfb7dd4e131 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 18 Mar 2025 09:54:02 -0700 Subject: [PATCH] add public access to bijection key_val iterator Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index d875c9369..5ab075964 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -60,10 +60,23 @@ namespace lp { iv(const mpq& v, unsigned j) : m_coeff(v), m_j(j) {} }; - struct bijection { + class bijection { std::unordered_map m_map; std::unordered_map m_rev_map; + public: + auto map_begin() const { return m_map.begin(); } + auto map_end() const { return m_map.end(); } + + // Iterator helper + struct map_it { + const bijection& m_bij; + auto begin() const { return m_bij.map_begin(); } + auto end() const { return m_bij.map_end(); } + }; + + // Add a method to get iterators over the key->val map (complementing key_val) + map_it key_val_pairs() const { return {*this}; } void add(unsigned a, unsigned b) { SASSERT(!contains(m_map, a) && !contains(m_rev_map, b)); m_map[a] = b; @@ -968,8 +981,8 @@ namespace lp { void remove_irrelevant_fresh_defs() { std_vector xt_to_remove; std_vector rows_to_remove_the_defs_from; - for (const auto& p : m_fresh_k2xt_terms.m_bij.m_rev_map) { - unsigned xt = p.first; + for (const auto& p : m_fresh_k2xt_terms.m_bij.key_val_pairs()) { + unsigned xt = p.second; if (xt >= m_e_matrix.column_count()) { xt_to_remove.push_back(xt); rows_to_remove_the_defs_from.push_back(m_fresh_k2xt_terms.get_by_val(xt).second);