From 7c8f2d93bbc5eb870fef95a5b0fbb69d9e38e7e0 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 3 Mar 2026 00:07:53 +0000
Subject: [PATCH] Change seq_plugin m_sg to sgraph& reference,
 enode_concat_hash takes sgraph& directly

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/euf/euf_seq_plugin.cpp | 19 +++++++------------
 src/ast/euf/euf_seq_plugin.h   | 10 ++++------
 2 files changed, 11 insertions(+), 18 deletions(-)

diff --git a/src/ast/euf/euf_seq_plugin.cpp b/src/ast/euf/euf_seq_plugin.cpp
index 2a711a765..618b1699a 100644
--- a/src/ast/euf/euf_seq_plugin.cpp
+++ b/src/ast/euf/euf_seq_plugin.cpp
@@ -47,12 +47,9 @@ namespace euf {
     }
 
     unsigned enode_concat_hash::operator()(enode* n) const {
-        sgraph* sg = sg_ptr ? *sg_ptr : nullptr;
-        if (sg) {
-            snode* sn = sg->find(n->get_expr());
-            if (sn && sn->has_cached_hash())
-                return sn->assoc_hash();
-        }
+        snode* sn = sg.find(n->get_expr());
+        if (sn && sn->has_cached_hash())
+            return sn->assoc_hash();
         if (!is_any_concat(n, seq))
             return n->get_id();
         enode_vector leaves;
@@ -82,18 +79,16 @@ namespace euf {
         plugin(g),
         m_seq(g.get_manager()),
         m_rewriter(g.get_manager()),
-        m_sg(sg),
+        m_sg(sg ? *sg : *alloc(sgraph, g.get_manager(), g, false)),
         m_sg_owned(sg == nullptr),
-        m_concat_hash(m_seq, &m_sg),
+        m_concat_hash(m_seq, m_sg),
         m_concat_eq(m_seq),
         m_concat_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_concat_hash, m_concat_eq) {
-        if (!m_sg)
-            m_sg = alloc(sgraph, g.get_manager(), g, false);
     }
 
     seq_plugin::~seq_plugin() {
-        if (m_sg_owned && m_sg)
-            dealloc(m_sg);
+        if (m_sg_owned)
+            dealloc(&m_sg);
     }
 
     void seq_plugin::register_node(enode* n) {
diff --git a/src/ast/euf/euf_seq_plugin.h b/src/ast/euf/euf_seq_plugin.h
index b6f2637ba..8f72a6837 100644
--- a/src/ast/euf/euf_seq_plugin.h
+++ b/src/ast/euf/euf_seq_plugin.h
@@ -50,14 +50,12 @@ namespace euf {
     class sgraph;
 
     // Associativity-respecting hash for enode concat trees.
-    // Flattens concat(concat(a,b),c) and concat(a,concat(b,c))
-    // to the same leaf sequence [a,b,c] before hashing.
+    // Uses cached snode hash matrices from the sgraph for O(1) hashing.
     // Handles both str.++ (OP_SEQ_CONCAT) and re.++ (OP_RE_CONCAT).
-    // When an sgraph is available, uses cached snode hash matrices.
     struct enode_concat_hash {
         seq_util const& seq;
-        sgraph* const* sg_ptr;  // pointer to the sgraph* member in seq_plugin
-        enode_concat_hash(seq_util const& s, sgraph* const* sg = nullptr) : seq(s), sg_ptr(sg) {}
+        sgraph& sg;
+        enode_concat_hash(seq_util const& s, sgraph& sg) : seq(s), sg(sg) {}
         unsigned operator()(enode* n) const;
     };
 
@@ -78,7 +76,7 @@ namespace euf {
 
         seq_util         m_seq;
         seq_rewriter     m_rewriter;
-        sgraph*          m_sg = nullptr;   // sgraph (may or may not be owned)
+        sgraph&          m_sg;
         bool             m_sg_owned = false; // whether we own the sgraph
         svector<undo_kind> m_undo;