From fbd3d445e28464cda5de89fd1eb125641ccc3ab8 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 2 Mar 2026 21:16:46 +0000 Subject: [PATCH] Add clarifying comments for hash matrix overflow safety and cache validity Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/euf/euf_sgraph.cpp | 5 +++++ src/ast/euf/euf_snode.h | 4 +++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index a080ab3fa..eff926004 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -289,6 +289,10 @@ namespace euf { static const unsigned HASH_BASE = 31; + // Compute a 2x2 polynomial hash matrix for associativity-respecting hashing. + // Unsigned overflow is intentional and well-defined (mod 2^32). + // M[0][0] tracks HASH_BASE^(num_leaves), which is always nonzero since + // HASH_BASE is odd. M[0][1] is the actual hash value. void sgraph::compute_hash_matrix(snode* n) { if (n->is_empty()) { // identity matrix: concat with empty is identity @@ -310,6 +314,7 @@ namespace euf { } else { // leaf/token: [[HASH_BASE, value], [0, 1]] + // +1 avoids zero hash values; wraps safely on unsigned overflow unsigned v = n->get_expr() ? n->get_expr()->get_id() + 1 : n->id() + 1; n->m_hash_matrix[0][0] = HASH_BASE; n->m_hash_matrix[0][1] = v; diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index bf9ce293e..955dd3788 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -109,7 +109,9 @@ namespace euf { unsigned level() const { return m_level; } unsigned length() const { return m_length; } - // associativity-respecting hash: cached if the 2x2 matrix is non-zero + // associativity-respecting hash: cached if the 2x2 matrix is non-zero. + // M[0][0] = HASH_BASE^(num_leaves) which is always nonzero since HASH_BASE + // is odd and gcd(odd, 2^32) = 1, so the check is safe. bool has_cached_hash() const { return m_hash_matrix[0][0] != 0; } unsigned assoc_hash() const { return m_hash_matrix[0][1]; }