Fix enode_concat_eq leaf comparison, simplify is_str/re_concat, update sgraph summary

Address remaining review feedback from PR #8820:
- Use pointer comparison instead of ID comparison in enode_concat_eq
- Remove redundant num_args() == 2 check from is_str_concat/is_re_concat
- Update euf_sgraph.h abstract to detail seq_plugin features

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/ast/euf/euf_seq_plugin.cpp

@@ -66,7 +66,7 @@ namespace euf {
         if (la.size() != lb.size())
             return false;
         for (unsigned i = 0; i < la.size(); ++i)
-            if (la[i]->get_id() != lb[i]->get_id())
+            if (la[i] != lb[i])
                 return false;
         return true;
     }

src/ast/euf/euf_seq_plugin.h

@@ -93,18 +93,22 @@ namespace euf {
         bool is_str_concat(enode* n) const { return m_seq.str.is_concat(n->get_expr()); }
         bool is_str_concat(enode* n, enode*& a, enode*& b) {
             expr* ea = nullptr, *eb = nullptr;
-            return m_seq.str.is_concat(n->get_expr(), ea, eb) &&
-                   n->num_args() == 2 &&
-                   (a = n->get_arg(0), b = n->get_arg(1), true);
+            if (!m_seq.str.is_concat(n->get_expr(), ea, eb))
+                return false;
+            a = n->get_arg(0);
+            b = n->get_arg(1);
+            return true;
         }
 
         // regex concat predicates
         bool is_re_concat(enode* n) const { return m_seq.re.is_concat(n->get_expr()); }
         bool is_re_concat(enode* n, enode*& a, enode*& b) {
             expr* ea = nullptr, *eb = nullptr;
-            return m_seq.re.is_concat(n->get_expr(), ea, eb) &&
-                   n->num_args() == 2 &&
-                   (a = n->get_arg(0), b = n->get_arg(1), true);
+            if (!m_seq.re.is_concat(n->get_expr(), ea, eb))
+                return false;
+            a = n->get_arg(0);
+            b = n->get_arg(1);
+            return true;
         }
 
         // any concat, string or regex

src/ast/euf/euf_sgraph.h

@@ -9,21 +9,24 @@ Abstract:
 
     Sequence/string graph layer
 
-    Encapsulates string expressions in the style of euf_egraph.h.
+    Encapsulates string and regex expressions for the string solver.
     The sgraph maps Z3 sequence/regex AST expressions to snode structures
     organized as binary concatenation trees with metadata, and owns an
     egraph with a seq_plugin for congruence closure.
 
-    Implemented:
     -- snode classification: empty, char, variable, unit, concat, power,
        star, loop, union, intersection, complement, fail, full_char,
        full_seq, to_re, in_re, other.
     -- Metadata computation: ground, regex_free, nullable, level, length.
-    -- Expression registration via mk, lookup via find.
+    -- Expression registration via mk(expr*), lookup via find(expr*).
     -- Scope management: push/pop with backtracking.
-    -- egraph ownership with seq_plugin for concat associativity,
-       Kleene star merging, and nullable absorption.
-    -- enode registration via mk_enode.
+    -- egraph ownership with seq_plugin for:
+       * concat associativity via associativity-respecting hash table,
+       * Kleene star merging (u.v*.v*.w = u.v*.w),
+       * nullable absorption next to .* (u.*.v.w = u.*.w when v nullable),
+       * str.++ identity elimination (concat(a, ε) = a),
+       * re.++ identity/absorption (concat(a, epsilon) = a, concat(a, ∅) = ∅).
+    -- enode registration via mk_enode(expr*).
 
     ZIPT features not yet ported: