Apply three ZIPT code review improvements to euf_seq_plugin

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/da8647c4-ddff-47ce-9364-2eee3810c38d

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

src/ast/euf/euf_seq_plugin.cpp

@@ -64,6 +64,15 @@ namespace euf {
         if (a == b) return true;
         if (!is_any_concat(a, seq) || !is_any_concat(b, seq))
             return false;
+        // fast-path: snode length check (O(1), avoids leaf allocation)
+        snode* sa = sg.find(a->get_expr());
+        snode* sb = sg.find(b->get_expr());
+        if (sa && sb && sa->length() != sb->length())
+            return false;
+        // fast-path: cached associativity hash (O(1))
+        if (sa && sa->has_cached_hash() && sb && sb->has_cached_hash() &&
+            sa->assoc_hash() != sb->assoc_hash())
+            return false;
         enode_vector la, lb;
         collect_enode_leaves(a, seq, la);
         collect_enode_leaves(b, seq, lb);
@@ -82,7 +91,7 @@ namespace euf {
         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_eq(m_seq),
+        m_concat_eq(m_seq, m_sg),
         m_concat_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_concat_hash, m_concat_eq) {
     }
 
@@ -168,6 +177,17 @@ namespace euf {
             if (is_concat(n))
                 propagate_simplify(n);
         }
+
+        // Re-simplify concat nodes when a child's root has just become full_seq.
+        // This handles nullable absorption through nested concats:
+        // concat(.*, concat(v, w)) = concat(.*, w) when v is nullable but w is not.
+        for (enode* n : m_concats) {
+            enode *na, *nb;
+            if (is_re_concat(n, na, nb)) {
+                if (is_full_seq(na->get_root()) || is_full_seq(nb->get_root()))
+                    propagate_simplify(n);
+            }
+        }
     }
 
     //
@@ -236,6 +256,20 @@ namespace euf {
 
         // concat(concat(u, v), .*) = concat(u, .*) when v nullable
         // handled by associativity + nullable absorption on sub-concats
+
+        // Rule 3: Loop merging
+        // concat(v{l1,h1}, v{l2,h2}) = v{l1+l2,h1+h2}
+        unsigned lo1, hi1, lo2, hi2;
+        if (same_loop_body(a, b, lo1, hi1, lo2, hi2)) {
+            ast_manager& m = g.get_manager();
+            enode* body_n = a->get_arg(0);
+            // saturating add: prevent silent unsigned wrap-around on large bounds
+            unsigned lo_merged = (lo2 > UINT_MAX - lo1) ? UINT_MAX : lo1 + lo2;
+            unsigned hi_merged = (hi2 > UINT_MAX - hi1) ? UINT_MAX : hi1 + hi2;
+            expr_ref merged(m_seq.re.mk_loop(body_n->get_expr(), lo_merged, hi_merged), m);
+            enode* merged_n = mk(merged, 1, &body_n);
+            push_merge(n, merged_n);
+        }
     }
 
     bool seq_plugin::is_nullable(expr* e) {

src/ast/euf/euf_seq_plugin.h

@@ -63,7 +63,8 @@ namespace euf {
     // Handles both str.++ (OP_SEQ_CONCAT) and re.++ (OP_RE_CONCAT).
     struct enode_concat_eq {
         seq_util const& seq;
-        enode_concat_eq(seq_util const& s) : seq(s) {}
+        sgraph& sg;
+        enode_concat_eq(seq_util const& s, sgraph& sg) : seq(s), sg(sg) {}
         bool operator()(enode* a, enode* b) const;
     };