From 2e784a6ba34708dab51b1871394992d01d658ddc Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 10 Mar 2026 18:10:16 +0000 Subject: [PATCH 1/2] Initial plan From d4b99730b98464cf548863c7e31956d9db7b0dac Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 10 Mar 2026 18:30:33 +0000 Subject: [PATCH 2/2] Fix build error: remove stale dep_tracker method definitions from seq_nielsen.cpp Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/seq/seq_nielsen.cpp | 52 ------------------------------------- 1 file changed, 52 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 0c3a6342c..6decb616d 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -203,58 +203,6 @@ namespace seq { } }; - // ----------------------------------------------- - // dep_tracker - // ----------------------------------------------- - - dep_tracker::dep_tracker(unsigned num_bits) { - unsigned words = (num_bits + 31) / 32; - m_bits.resize(words, 0); - } - - dep_tracker::dep_tracker(unsigned num_bits, unsigned set_bit) : dep_tracker(num_bits) { - if (set_bit < num_bits) { - unsigned word_idx = set_bit / 32; - unsigned bit_idx = set_bit % 32; - m_bits[word_idx] = 1u << bit_idx; - } - } - - void dep_tracker::merge(dep_tracker const& other) { - if (other.m_bits.empty()) - return; - if (m_bits.size() < other.m_bits.size()) - m_bits.resize(other.m_bits.size(), 0); - for (unsigned i = 0; i < other.m_bits.size(); ++i) - m_bits[i] |= other.m_bits[i]; - } - - bool dep_tracker::is_superset(dep_tracker const& other) const { - for (unsigned i = 0; i < other.m_bits.size(); ++i) { - unsigned my_bits = (i < m_bits.size()) ? m_bits[i] : 0; - if ((my_bits & other.m_bits[i]) != other.m_bits[i]) - return false; - } - return true; - } - - bool dep_tracker::empty() const { - for (unsigned b : m_bits) - if (b != 0) return false; - return true; - } - - void dep_tracker::get_set_bits(unsigned_vector& indices) const { - for (unsigned i = 0; i < m_bits.size(); ++i) { - unsigned word = m_bits[i]; - while (word != 0) { - unsigned bit = i * 32 + ntz_core(word); - indices.push_back(bit); - word &= word - 1; // clear lowest set bit - } - } - } - // ----------------------------------------------- // str_eq // -----------------------------------------------