From b8656d4fbe5d5e4d33874fb965d7c8939b6897a5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 1 Mar 2026 23:24:59 +0000 Subject: [PATCH] Address code review: add comments for collect_leaves, find_assoc_equal, and display Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/euf/euf_seq_plugin.cpp | 2 ++ src/ast/euf/euf_sgraph.cpp | 8 ++++++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/euf/euf_seq_plugin.cpp b/src/ast/euf/euf_seq_plugin.cpp index e249a317a..eba855861 100644 --- a/src/ast/euf/euf_seq_plugin.cpp +++ b/src/ast/euf/euf_seq_plugin.cpp @@ -237,6 +237,8 @@ namespace euf { } std::ostream& seq_plugin::display(std::ostream& out) const { + // sgraph contents are displayed by sgraph::display, not here, + // since sgraph owns the seq_plugin (not the other way around) out << "seq-plugin\n"; return out; } diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index ee1b5745f..a31eb74d2 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -25,6 +25,9 @@ namespace euf { // Associativity-respecting hash: flattens concat into leaf sequence // concat(concat(a, b), c) and concat(a, concat(b, c)) hash identically + // Recursively flatten a concatenation tree into a sequence of leaf nodes. + // This produces the same leaf order regardless of tree associativity, + // so concat(concat(a,b),c) and concat(a,concat(b,c)) yield [a,b,c]. static void collect_leaves(snode const* n, ptr_vector& leaves) { if (n->is_concat()) { collect_leaves(n->arg(0), leaves); @@ -353,9 +356,10 @@ namespace euf { if (!n || !n->is_concat()) return nullptr; snode* existing = nullptr; - if (m_concat_table.find(n, existing) && existing != n) { + // find returns true when a matching entry exists, + // check that it is a different node to report a genuine match + if (m_concat_table.find(n, existing) && existing != n) return existing; - } return nullptr; }