mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-08 06:14:52 +00:00
Code Activity

Address code review: add comments for collect_leaves, find_assoc_equal, and display

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-01 23:24:59 +00:00
parent 5c14edf030
commit b8656d4fbe
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/euf/euf_sgraph.cpp
View file

@ -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<snode const>& 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;
}