Merge pull request #8820 from Z3Prover/copilot/encapsulate-strings-in-euf-sgraph

Add string graph encapsulation (euf_sgraph/snode), OP_SEQ_POWER, and euf_seq_plugin

src/ast/euf/CMakeLists.txt

@@ -9,6 +9,8 @@ z3_add_component(euf
     euf_justification.cpp
     euf_mam.cpp
     euf_plugin.cpp
+    euf_seq_plugin.cpp
+    euf_sgraph.cpp
     euf_specrel_plugin.cpp
     ho_matcher.cpp
   COMPONENT_DEPENDENCIES

src/ast/euf/euf_seq_plugin.cpp

@@ -0,0 +1,280 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    euf_seq_plugin.cpp
+
+Abstract:
+
+    Plugin structure for sequences/strings.
+
+    Merges equivalence classes taking into account associativity
+    of concatenation and algebraic properties of strings and
+    regular expressions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-03-01
+    Clemens Eisenhofer 2026-03-01
+
+--*/
+
+#include "ast/euf/euf_seq_plugin.h"
+#include "ast/euf/euf_egraph.h"
+#include "ast/ast_pp.h"
+
+namespace euf {
+
+    // Check if enode is any kind of concat (str.++ or re.++)
+    static bool is_any_concat(enode* n, seq_util const& seq) {
+        expr* a = nullptr, *b = nullptr;
+        return seq.str.is_concat(n->get_expr(), a, b) || seq.re.is_concat(n->get_expr(), a, b);
+    }
+
+    // Collect leaves of a concat tree in left-to-right order.
+    // For non-concat nodes, the node itself is a leaf.
+    // Handles both str.++ and re.++.
+    static void collect_enode_leaves(enode* n, seq_util const& seq, enode_vector& leaves) {
+        if (is_any_concat(n, seq)) {
+            collect_enode_leaves(n->get_arg(0), seq, leaves);
+            collect_enode_leaves(n->get_arg(1), seq, leaves);
+        }
+        else {
+            leaves.push_back(n);
+        }
+    }
+
+    unsigned enode_concat_hash::operator()(enode* n) const {
+        if (!is_any_concat(n, seq))
+            return n->get_id();
+        enode_vector leaves;
+        collect_enode_leaves(n, seq, leaves);
+        unsigned h = 0;
+        for (enode* l : leaves)
+            h = combine_hash(h, l->get_id());
+        return h;
+    }
+
+    bool enode_concat_eq::operator()(enode* a, enode* b) const {
+        if (a == b) return true;
+        if (!is_any_concat(a, seq) || !is_any_concat(b, seq))
+            return false;
+        enode_vector la, lb;
+        collect_enode_leaves(a, seq, la);
+        collect_enode_leaves(b, seq, lb);
+        if (la.size() != lb.size())
+            return false;
+        for (unsigned i = 0; i < la.size(); ++i)
+            if (la[i]->get_id() != lb[i]->get_id())
+                return false;
+        return true;
+    }
+
+    seq_plugin::seq_plugin(egraph& g):
+        plugin(g),
+        m_seq(g.get_manager()),
+        m_rewriter(g.get_manager()),
+        m_concat_hash(m_seq),
+        m_concat_eq(m_seq),
+        m_concat_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_concat_hash, m_concat_eq) {
+    }
+
+    void seq_plugin::register_node(enode* n) {
+        m_queue.push_back(n);
+        push_undo(undo_kind::undo_add_concat);
+    }
+
+    void seq_plugin::merge_eh(enode* n1, enode* n2) {
+        m_queue.push_back(enode_pair(n1, n2));
+        push_undo(undo_kind::undo_add_concat);
+    }
+
+    void seq_plugin::push_undo(undo_kind k) {
+        m_undo.push_back(k);
+        push_plugin_undo(get_id());
+    }
+
+    void seq_plugin::propagate() {
+        if (m_qhead == m_queue.size())
+            return;
+        for (; m_qhead < m_queue.size(); ++m_qhead) {
+            if (g.inconsistent())
+                break;
+            if (std::holds_alternative<enode*>(m_queue[m_qhead])) {
+                auto n = std::get<enode*>(m_queue[m_qhead]);
+                propagate_register_node(n);
+            }
+            else {
+                auto [a, b] = std::get<enode_pair>(m_queue[m_qhead]);
+                propagate_merge(a, b);
+            }
+        }
+    }
+
+    void seq_plugin::propagate_register_node(enode* n) {
+        if (!m_seq.is_seq(n->get_expr()) && !m_seq.is_re(n->get_expr()))
+            return;
+
+        TRACE(seq, tout << "seq register " << g.bpp(n) << "\n");
+
+        if (is_concat(n)) {
+            propagate_assoc(n);
+            propagate_simplify(n);
+        }
+
+        // str.++ identity: concat(a, ε) = a, concat(ε, b) = b
+        enode* a, *b;
+        if (is_str_concat(n, a, b)) {
+            if (is_str_empty(a))
+                push_merge(n, b);
+            else if (is_str_empty(b))
+                push_merge(n, a);
+        }
+
+        // re.++ identity: concat(a, epsilon) = a, concat(epsilon, b) = b
+        // re.++ absorption: concat(a, ∅) = ∅, concat(∅, b) = ∅
+        if (is_re_concat(n, a, b)) {
+            if (is_re_epsilon(a))
+                push_merge(n, b);
+            else if (is_re_epsilon(b))
+                push_merge(n, a);
+            else if (is_re_empty(a))
+                push_merge(n, a);
+            else if (is_re_empty(b))
+                push_merge(n, b);
+        }
+    }
+
+    void seq_plugin::propagate_merge(enode* a, enode* b) {
+        if (!m_seq.is_seq(a->get_expr()) && !m_seq.is_re(a->get_expr()))
+            return;
+
+        TRACE(seq, tout << "seq merge " << g.bpp(a) << " == " << g.bpp(b) << "\n");
+
+        // when equivalence classes merge, re-check concat simplifications
+        for (enode* n : enode_class(a)) {
+            if (is_concat(n))
+                propagate_simplify(n);
+        }
+    }
+
+    //
+    // Concat associativity:
+    // Instead of creating new expressions, maintain a hash table
+    // that respects associativity. When a concat is registered,
+    // look up existing concats with the same leaf sequence.
+    // If found, merge the existing node with the new one.
+    //
+    void seq_plugin::propagate_assoc(enode* n) {
+        if (!is_concat(n))
+            return;
+
+        enode* existing = nullptr;
+        if (m_concat_table.find(n, existing)) {
+            if (existing != n)
+                push_merge(n, existing);
+        }
+        else {
+            m_concat_table.insert(n);
+            m_concats.push_back(n);
+            push_undo(undo_kind::undo_add_to_table);
+        }
+    }
+
+    //
+    // Concat simplification rules from ZIPT:
+    //
+    // 1. Kleene star merging: concat(u, v*, v*, w) = concat(u, v*, w)
+    //    when adjacent children in a concat chain have congruent star bodies.
+    //
+    // 2. Nullable absorption: concat(u, .*, v, w) = concat(u, .*, w)
+    //    when v is nullable and adjacent to full_seq (.*).
+    //
+    void seq_plugin::propagate_simplify(enode* n) {
+        enode* a, *b;
+        if (!is_concat(n, a, b))
+            return;
+
+        // Rule 1: Kleene star merging
+        // concat(v*, v*) = v*
+        if (same_star_body(a, b))
+            push_merge(n, a);
+
+        // Rule 1 extended: concat(v*, concat(v*, c)) = concat(v*, c)
+        enode* b1, *b2;
+        if (is_concat(b, b1, b2) && same_star_body(a, b1))
+            push_merge(n, b);
+
+        // Rule 2: Nullable absorption by .*
+        // concat(.*, v) = .* when v is nullable
+        if (is_full_seq(a) && is_nullable(b))
+            push_merge(n, a);
+
+        // concat(v, .*) = .* when v is nullable
+        if (is_nullable(a) && is_full_seq(b))
+            push_merge(n, b);
+
+        // concat(.*, concat(v, w)) = concat(.*, w) when v nullable
+        // handled by associativity + nullable absorption on sub-concats
+
+        // concat(concat(u, v), .*) = concat(u, .*) when v nullable
+        // handled by associativity + nullable absorption on sub-concats
+    }
+
+    bool seq_plugin::is_nullable(expr* e) {
+        expr_ref result = m_rewriter.is_nullable(e);
+        return g.get_manager().is_true(result);
+    }
+
+    bool seq_plugin::same_star_body(enode* a, enode* b) {
+        if (!is_star(a) || !is_star(b))
+            return false;
+        // re.star(x) and re.star(y) have congruent bodies if x ~ y
+        return a->get_arg(0)->get_root() == b->get_arg(0)->get_root();
+    }
+
+    bool seq_plugin::same_loop_body(enode* a, enode* b,
+                                    unsigned& lo1, unsigned& hi1,
+                                    unsigned& lo2, unsigned& hi2) {
+        if (!is_loop(a) || !is_loop(b))
+            return false;
+        expr* body_a, *body_b;
+        if (!m_seq.re.is_loop(a->get_expr(), body_a, lo1, hi1))
+            return false;
+        if (!m_seq.re.is_loop(b->get_expr(), body_b, lo2, hi2))
+            return false;
+        enode* na = g.find(body_a);
+        enode* nb = g.find(body_b);
+        if (!na || !nb)
+            return false;
+        return na->get_root() == nb->get_root();
+    }
+
+    void seq_plugin::undo() {
+        auto k = m_undo.back();
+        m_undo.pop_back();
+        switch (k) {
+        case undo_kind::undo_add_concat:
+            SASSERT(!m_queue.empty());
+            m_queue.pop_back();
+            if (m_qhead > m_queue.size())
+                m_qhead = m_queue.size();
+            break;
+        case undo_kind::undo_add_to_table:
+            SASSERT(!m_concats.empty());
+            m_concat_table.remove(m_concats.back());
+            m_concats.pop_back();
+            break;
+        }
+    }
+
+    std::ostream& seq_plugin::display(std::ostream& out) const {
+        out << "seq-plugin\n";
+        return out;
+    }
+
+    void seq_plugin::collect_statistics(statistics& st) const {
+        // statistics are collected by sgraph which owns us
+    }
+}

src/ast/euf/euf_seq_plugin.h

@@ -0,0 +1,171 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    euf_seq_plugin.h
+
+Abstract:
+
+    Plugin structure for sequences/strings.
+
+    Merges equivalence classes taking into account associativity
+    of concatenation and algebraic properties of strings and
+    regular expressions. Implements features from ZIPT:
+
+    -- Concat associativity: str.++ is associative, so
+       concat(a, concat(b, c)) = concat(concat(a, b), c).
+       Handled via an AC-style plugin for the concat operator.
+
+    -- Kleene star merging: adjacent identical Kleene stars
+       in a concatenation are collapsed, u.v*.v*.w = u.v*.w
+
+    -- Loop merging: adjacent loops over the same body are
+       merged, v{l1,h1}.v{l2,h2} = v{l1+l2,h1+h2}
+
+    -- Nullable absorption: a nullable token adjacent to .*
+       is absorbed, u.*.v.w = u.*.w when v is nullable.
+
+    The plugin integrates with euf_egraph for congruence closure.
+    Node registration in sgraph is handled by sgraph itself via
+    the egraph's on_make callback, not by the plugin.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-03-01
+    Clemens Eisenhofer 2026-03-01
+
+--*/
+
+#pragma once
+
+#include "ast/seq_decl_plugin.h"
+#include "ast/rewriter/seq_rewriter.h"
+#include "ast/euf/euf_plugin.h"
+#include "util/hashtable.h"
+
+namespace euf {
+
+    class egraph;
+
+    // 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.
+    // Handles both str.++ (OP_SEQ_CONCAT) and re.++ (OP_RE_CONCAT).
+    struct enode_concat_hash {
+        seq_util const& seq;
+        enode_concat_hash(seq_util const& s) : seq(s) {}
+        unsigned operator()(enode* n) const;
+    };
+
+    // Associativity-respecting equality for enode concat trees.
+    // 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) {}
+        bool operator()(enode* a, enode* b) const;
+    };
+
+    class seq_plugin : public plugin {
+
+        enum class undo_kind {
+            undo_add_concat,
+            undo_add_to_table,
+        };
+
+        seq_util         m_seq;
+        seq_rewriter     m_rewriter;
+        svector<undo_kind> m_undo;
+
+        // queue of merges and registrations to process
+        vector<std::variant<enode*, enode_pair>> m_queue;
+        unsigned         m_qhead = 0;
+
+        // track registered concat nodes for simplification
+        enode_vector     m_concats;
+
+        // associativity-respecting hash table for concat nodes
+        enode_concat_hash m_concat_hash;
+        enode_concat_eq   m_concat_eq;
+        hashtable<enode*, enode_concat_hash, enode_concat_eq> m_concat_table;
+
+        // string concat predicates
+        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);
+        }
+
+        // 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);
+        }
+
+        // any concat, string or regex
+        bool is_concat(enode* n) const { return is_str_concat(n) || is_re_concat(n); }
+        bool is_concat(enode* n, enode*& a, enode*& b) {
+            return is_str_concat(n, a, b) || is_re_concat(n, a, b);
+        }
+
+        bool is_star(enode* n) const { return m_seq.re.is_star(n->get_expr()); }
+        bool is_loop(enode* n) const { return m_seq.re.is_loop(n->get_expr()); }
+
+        // string empty: ε for str.++
+        bool is_str_empty(enode* n) const { return m_seq.str.is_empty(n->get_expr()); }
+        // regex empty set: ∅ for re.++ (absorbing element)
+        bool is_re_empty(enode* n) const { return m_seq.re.is_empty(n->get_expr()); }
+        // regex epsilon: to_re("") for re.++ (identity element)
+        bool is_re_epsilon(enode* n) const { return m_seq.re.is_epsilon(n->get_expr()); }
+
+        bool is_to_re(enode* n) const { return m_seq.re.is_to_re(n->get_expr()); }
+        bool is_full_seq(enode* n) const { return m_seq.re.is_full_seq(n->get_expr()); }
+
+        void push_undo(undo_kind k);
+
+        void propagate_register_node(enode* n);
+        void propagate_merge(enode* a, enode* b);
+
+        // concat associativity: maintain hash table of concat nodes,
+        // merge nodes that are equal modulo associativity
+        void propagate_assoc(enode* n);
+
+        // concat simplification:
+        // merging Kleene stars, merging loops, absorbing nullables
+        void propagate_simplify(enode* n);
+
+        // check if expression is nullable using existing seq_rewriter
+        bool is_nullable(expr* e);
+        bool is_nullable(enode* n) { return is_nullable(n->get_expr()); }
+
+        // check if two enodes have congruent star bodies
+        bool same_star_body(enode* a, enode* b);
+
+        // check if two enodes have congruent loop bodies and extract bounds
+        bool same_loop_body(enode* a, enode* b, unsigned& lo1, unsigned& hi1, unsigned& lo2, unsigned& hi2);
+
+    public:
+        seq_plugin(egraph& g);
+
+        theory_id get_id() const override { return m_seq.get_family_id(); }
+
+        void register_node(enode* n) override;
+
+        void merge_eh(enode* n1, enode* n2) override;
+
+        void diseq_eh(enode*) override {}
+
+        void propagate() override;
+
+        void undo() override;
+
+        std::ostream& display(std::ostream& out) const override;
+
+        void collect_statistics(statistics& st) const override;
+    };
+}

src/ast/euf/euf_sgraph.cpp

@@ -0,0 +1,412 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    euf_sgraph.cpp
+
+Abstract:
+
+    Sequence/string graph implementation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-03-01
+    Clemens Eisenhofer 2026-03-01
+
+--*/
+
+#include "ast/euf/euf_sgraph.h"
+#include "ast/euf/euf_seq_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/ast_pp.h"
+
+namespace euf {
+
+    sgraph::sgraph(ast_manager& m):
+        m(m),
+        m_seq(m),
+        m_egraph(m),
+        m_exprs(m) {
+        // create seq_plugin and register it with the egraph
+        m_egraph.add_plugin(alloc(seq_plugin, m_egraph));
+        // register on_make callback so sgraph creates snodes for new enodes
+        std::function<void(enode*)> on_make = [this](enode* n) {
+            expr* e = n->get_expr();
+            if (m_seq.is_seq(e) || m_seq.is_re(e))
+                mk(e);
+        };
+        m_egraph.set_on_make(on_make);
+    }
+
+    sgraph::~sgraph() {
+    }
+
+    snode_kind sgraph::classify(expr* e) const {
+        if (!is_app(e))
+            return snode_kind::s_other;
+
+        if (m_seq.str.is_empty(e))
+            return snode_kind::s_empty;
+
+        if (m_seq.str.is_string(e)) {
+            zstring s;
+            if (m_seq.str.is_string(e, s) && s.empty())
+                return snode_kind::s_empty;
+            return snode_kind::s_other;
+        }
+
+        if (m_seq.str.is_concat(e))
+            return snode_kind::s_concat;
+
+        if (m_seq.str.is_unit(e)) {
+            expr* ch = to_app(e)->get_arg(0);
+            if (m_seq.is_const_char(ch))
+                return snode_kind::s_char;
+            return snode_kind::s_unit;
+        }
+
+        if (m_seq.str.is_power(e))
+            return snode_kind::s_power;
+
+        if (m_seq.re.is_star(e))
+            return snode_kind::s_star;
+
+        if (m_seq.re.is_loop(e))
+            return snode_kind::s_loop;
+
+        if (m_seq.re.is_union(e))
+            return snode_kind::s_union;
+
+        if (m_seq.re.is_intersection(e))
+            return snode_kind::s_intersect;
+
+        if (m_seq.re.is_complement(e))
+            return snode_kind::s_complement;
+
+        if (m_seq.re.is_empty(e))
+            return snode_kind::s_fail;
+
+        if (m_seq.re.is_full_char(e))
+            return snode_kind::s_full_char;
+
+        if (m_seq.re.is_full_seq(e))
+            return snode_kind::s_full_seq;
+
+        if (m_seq.re.is_to_re(e))
+            return snode_kind::s_to_re;
+
+        if (m_seq.str.is_in_re(e))
+            return snode_kind::s_in_re;
+
+        // uninterpreted constants of string sort are variables
+        if (is_uninterp_const(e) && m_seq.is_seq(e->get_sort()))
+            return snode_kind::s_var;
+
+        return snode_kind::s_other;
+    }
+
+    void sgraph::compute_metadata(snode* n) {
+        switch (n->m_kind) {
+        case snode_kind::s_empty:
+            n->m_ground = true;
+            n->m_regex_free = true;
+            n->m_nullable = true;
+            n->m_level = 0;
+            n->m_length = 0;
+            break;
+
+        case snode_kind::s_char:
+            n->m_ground = true;
+            n->m_regex_free = true;
+            n->m_nullable = false;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_var:
+            n->m_ground = false;
+            n->m_regex_free = true;
+            n->m_nullable = false;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_unit:
+            n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true;
+            n->m_regex_free = true;
+            n->m_nullable = false;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_concat: {
+            SASSERT(n->num_args() == 2);
+            snode* l = n->arg(0);
+            snode* r = n->arg(1);
+            n->m_ground = l->is_ground() && r->is_ground();
+            n->m_regex_free = l->is_regex_free() && r->is_regex_free();
+            n->m_nullable = l->is_nullable() && r->is_nullable();
+            n->m_level = std::max(l->level(), r->level()) + 1;
+            n->m_length = l->length() + r->length();
+            ++m_stats.m_num_concat;
+            break;
+        }
+
+        case snode_kind::s_power: {
+            // s^n: nullable follows base, consistent with ZIPT's PowerToken
+            // the exponent n is assumed to be a symbolic integer, may or may not be zero
+            SASSERT(n->num_args() >= 1);
+            snode* base = n->arg(0);
+            n->m_ground = base->is_ground();
+            n->m_regex_free = base->is_regex_free();
+            n->m_nullable = base->is_nullable();
+            n->m_level = 1;
+            n->m_length = 1;
+            ++m_stats.m_num_power;
+            break;
+        }
+
+        case snode_kind::s_star:
+            SASSERT(n->num_args() == 1);
+            n->m_ground = n->arg(0)->is_ground();
+            n->m_regex_free = false;
+            n->m_nullable = true;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_loop:
+            n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true;
+            n->m_regex_free = false;
+            n->m_nullable = false; // depends on lower bound
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_union:
+            SASSERT(n->num_args() == 2);
+            n->m_ground = n->arg(0)->is_ground() && n->arg(1)->is_ground();
+            n->m_regex_free = false;
+            n->m_nullable = n->arg(0)->is_nullable() || n->arg(1)->is_nullable();
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_intersect:
+            SASSERT(n->num_args() == 2);
+            n->m_ground = n->arg(0)->is_ground() && n->arg(1)->is_ground();
+            n->m_regex_free = false;
+            n->m_nullable = n->arg(0)->is_nullable() && n->arg(1)->is_nullable();
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_complement:
+            SASSERT(n->num_args() == 1);
+            n->m_ground = n->arg(0)->is_ground();
+            n->m_regex_free = false;
+            n->m_nullable = !n->arg(0)->is_nullable();
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_fail:
+            n->m_ground = true;
+            n->m_regex_free = false;
+            n->m_nullable = false;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_full_char:
+            n->m_ground = true;
+            n->m_regex_free = false;
+            n->m_nullable = false;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_full_seq:
+            n->m_ground = true;
+            n->m_regex_free = false;
+            n->m_nullable = true;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_to_re:
+            SASSERT(n->num_args() == 1);
+            n->m_ground = n->arg(0)->is_ground();
+            n->m_regex_free = false;
+            n->m_nullable = n->arg(0)->is_nullable();
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        case snode_kind::s_in_re:
+            SASSERT(n->num_args() == 2);
+            n->m_ground = n->arg(0)->is_ground() && n->arg(1)->is_ground();
+            n->m_regex_free = false;
+            n->m_nullable = false;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
+        default:
+            n->m_ground = true;
+            n->m_regex_free = true;
+            n->m_nullable = false;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+        }
+    }
+
+    snode* sgraph::mk_snode(expr* e, snode_kind k, unsigned num_args, snode* const* args) {
+        unsigned id = m_nodes.size();
+        snode* n = snode::mk(m_region, e, k, id, num_args, args);
+        compute_metadata(n);
+        m_nodes.push_back(n);
+        m_exprs.push_back(e);
+        if (e) {
+            unsigned eid = e->get_id();
+            m_expr2snode.reserve(eid + 1, nullptr);
+            m_expr2snode[eid] = n;
+        }
+        ++m_stats.m_num_nodes;
+        return n;
+    }
+
+    snode* sgraph::mk(expr* e) {
+        SASSERT(e);
+        snode* n = find(e);
+        if (n)
+            return n;
+
+        snode_kind k = classify(e);
+
+        if (!is_app(e))
+            return mk_snode(e, k, 0, nullptr);
+
+        app* a = to_app(e);
+        unsigned arity = a->get_num_args();
+
+        // recursively register children
+        // for seq/re children, create classified snodes
+        // for other children (e.g. integer exponents), create s_other snodes
+        snode_vector child_nodes;
+        for (unsigned i = 0; i < arity; ++i) {
+            expr* ch = a->get_arg(i);
+            snode* cn = mk(ch);
+            child_nodes.push_back(cn);
+        }
+
+        return mk_snode(e, k, child_nodes.size(), child_nodes.data());
+    }
+
+    snode* sgraph::find(expr* e) const {
+        if (!e)
+            return nullptr;
+        unsigned eid = e->get_id();
+        if (eid < m_expr2snode.size())
+            return m_expr2snode[eid];
+        return nullptr;
+    }
+
+    enode* sgraph::mk_enode(expr* e) {
+        enode* n = m_egraph.find(e);
+        if (n) return n;
+        enode_vector args;
+        if (is_app(e)) {
+            for (expr* arg : *to_app(e)) {
+                enode* a = mk_enode(arg);
+                args.push_back(a);
+            }
+        }
+        return m_egraph.mk(e, 0, args.size(), args.data());
+    }
+
+    void sgraph::push() {
+        m_scopes.push_back(m_nodes.size());
+        ++m_num_scopes;
+        m_egraph.push();
+    }
+
+    void sgraph::pop(unsigned num_scopes) {
+        if (num_scopes == 0)
+            return;
+        SASSERT(num_scopes <= m_num_scopes);
+        unsigned new_lvl = m_num_scopes - num_scopes;
+        unsigned old_sz = m_scopes[new_lvl];
+        for (unsigned i = m_nodes.size(); i-- > old_sz; ) {
+            snode* n = m_nodes[i];
+            if (n->get_expr()) {
+                unsigned eid = n->get_expr()->get_id();
+                if (eid < m_expr2snode.size())
+                    m_expr2snode[eid] = nullptr;
+            }
+        }
+        m_nodes.shrink(old_sz);
+        m_exprs.shrink(old_sz);
+        m_scopes.shrink(new_lvl);
+        m_num_scopes = new_lvl;
+        m_egraph.pop(num_scopes);
+    }
+
+    std::ostream& sgraph::display(std::ostream& out) const {
+        auto kind_str = [](snode_kind k) -> char const* {
+            switch (k) {
+            case snode_kind::s_empty:      return "empty";
+            case snode_kind::s_char:       return "char";
+            case snode_kind::s_var:        return "var";
+            case snode_kind::s_unit:       return "unit";
+            case snode_kind::s_concat:     return "concat";
+            case snode_kind::s_power:      return "power";
+            case snode_kind::s_star:       return "star";
+            case snode_kind::s_loop:       return "loop";
+            case snode_kind::s_union:      return "union";
+            case snode_kind::s_intersect:  return "intersect";
+            case snode_kind::s_complement: return "complement";
+            case snode_kind::s_fail:       return "fail";
+            case snode_kind::s_full_char:  return "full_char";
+            case snode_kind::s_full_seq:   return "full_seq";
+            case snode_kind::s_to_re:      return "to_re";
+            case snode_kind::s_in_re:      return "in_re";
+            case snode_kind::s_other:      return "other";
+            }
+            return "?";
+        };
+        for (snode* n : m_nodes) {
+            out << "snode[" << n->id() << "] "
+                << kind_str(n->kind())
+                << " level=" << n->level()
+                << " len=" << n->length()
+                << " ground=" << n->is_ground()
+                << " rfree=" << n->is_regex_free()
+                << " nullable=" << n->is_nullable();
+            if (n->num_args() > 0) {
+                out << " args=(";
+                for (unsigned i = 0; i < n->num_args(); ++i) {
+                    if (i > 0) out << ", ";
+                    out << n->arg(i)->id();
+                }
+                out << ")";
+            }
+            if (n->get_expr())
+                out << " expr=" << mk_pp(n->get_expr(), m);
+            out << "\n";
+        }
+        return out;
+    }
+
+    void sgraph::collect_statistics(statistics& st) const {
+        st.update("seq-graph-nodes", m_stats.m_num_nodes);
+        st.update("seq-graph-concat", m_stats.m_num_concat);
+        st.update("seq-graph-power", m_stats.m_num_power);
+        st.update("seq-graph-hash-hits", m_stats.m_num_hash_hits);
+        m_egraph.collect_statistics(st);
+    }
+
+}
+

src/ast/euf/euf_sgraph.h

@@ -0,0 +1,127 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    euf_sgraph.h
+
+Abstract:
+
+    Sequence/string graph layer
+
+    Encapsulates string expressions in the style of euf_egraph.h.
+    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.
+    -- 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.
+
+    ZIPT features not yet ported:
+
+    -- Str operations: normalisation with union-find representatives and
+       cache migration, balanced tree maintenance, drop left/right with
+       caching, substitution, indexed access, iteration, ToList caching,
+       simplification, derivative computation, structural equality with
+       associative hashing, rotation equality, expression reconstruction,
+       Graphviz export.
+
+    -- StrToken subclasses: SymCharToken, StrAtToken, SubStrToken,
+       SetToken, PostToken/PreToken.
+
+    -- StrToken features: Nielsen-style GetDecomposition with side
+       constraints, NamedStrToken extension tracking for variable
+       splitting with PowerExtension, CollectSymbols for Parikh analysis,
+       MinTerms for character class analysis, token ordering, Derivable
+       and BasicRegex flags.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-03-01
+    Clemens Eisenhofer 2026-03-01
+
+--*/
+
+#pragma once
+
+#include "util/region.h"
+#include "util/statistics.h"
+#include "ast/ast.h"
+#include "ast/seq_decl_plugin.h"
+#include "ast/euf/euf_snode.h"
+#include "ast/euf/euf_egraph.h"
+
+namespace euf {
+
+    class seq_plugin;
+
+    class sgraph {
+
+        struct stats {
+            unsigned m_num_nodes;
+            unsigned m_num_concat;
+            unsigned m_num_power;
+            unsigned m_num_hash_hits;
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+
+        ast_manager&     m;
+        seq_util         m_seq;
+        egraph           m_egraph;
+        region           m_region;
+        snode_vector     m_nodes;
+        expr_ref_vector  m_exprs;       // pin expressions
+        unsigned_vector  m_scopes;
+        unsigned         m_num_scopes = 0;
+        stats            m_stats;
+
+        // maps expression id to snode
+        ptr_vector<snode> m_expr2snode;
+
+        snode* mk_snode(expr* e, snode_kind k, unsigned num_args, snode* const* args);
+        snode_kind classify(expr* e) const;
+        void compute_metadata(snode* n);
+
+    public:
+        sgraph(ast_manager& m);
+        ~sgraph();
+
+        ast_manager& get_manager() const { return m; }
+        seq_util& get_seq_util() { return m_seq; }
+        egraph& get_egraph() { return m_egraph; }
+        egraph const& get_egraph() const { return m_egraph; }
+
+        // register an expression and return its snode
+        snode* mk(expr* e);
+
+        // lookup an already-registered expression
+        snode* find(expr* e) const;
+
+        // register expression in both sgraph and egraph
+        enode* mk_enode(expr* e);
+
+        // scope management for backtracking
+        void push();
+        void pop(unsigned num_scopes);
+
+        // access
+        snode_vector const& nodes() const { return m_nodes; }
+        unsigned num_nodes() const { return m_nodes.size(); }
+
+        // display
+        std::ostream& display(std::ostream& out) const;
+
+        void collect_statistics(statistics& st) const;
+    };
+
+}
+

src/ast/euf/euf_snode.h

@@ -0,0 +1,163 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    euf_snode.h
+
+Abstract:
+
+    snode layer for sequence/string graph
+
+    Encapsulates strings in the style of euf_enode.h.
+    Maps Z3 sequence expressions to a ZIPT-style representation where
+    strings are composed of tokens (characters, variables, powers, regex, etc.)
+    organized as a binary tree of concatenations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-03-01
+    Clemens Eisenhofer 2026-03-01
+
+--*/
+
+#pragma once
+
+#include "util/vector.h"
+#include "util/region.h"
+#include "ast/ast.h"
+#include "ast/seq_decl_plugin.h"
+
+namespace euf {
+
+    class sgraph;
+    class snode;
+
+    typedef ptr_vector<snode> snode_vector;
+
+    enum class snode_kind {
+        s_empty,       // empty string (OP_SEQ_EMPTY or empty string constant)
+        s_char,        // concrete character unit (OP_SEQ_UNIT wrapping a char literal)
+        s_var,         // string variable (uninterpreted constant of string sort)
+        s_unit,        // generic unit (OP_SEQ_UNIT with non-literal character)
+        s_concat,      // concatenation of two snodes (OP_SEQ_CONCAT)
+        s_power,       // string exponentiation s^n (OP_SEQ_POWER)
+        s_star,        // Kleene star r* (OP_RE_STAR)
+        s_loop,        // bounded loop r{lo,hi} (OP_RE_LOOP)
+        s_union,       // union r1|r2 (OP_RE_UNION)
+        s_intersect,   // intersection r1&r2 (OP_RE_INTERSECT)
+        s_complement,  // complement ~r (OP_RE_COMPLEMENT)
+        s_fail,        // empty language (OP_RE_EMPTY_SET)
+        s_full_char,   // full character set (OP_RE_FULL_CHAR_SET)
+        s_full_seq,    // full sequence set r=.* (OP_RE_FULL_SEQ_SET)
+        s_to_re,       // string to regex (OP_SEQ_TO_RE)
+        s_in_re,       // regex membership (OP_SEQ_IN_RE)
+        s_other,       // other sequence expression not directly classified
+    };
+
+    class snode {
+        expr*       m_expr      = nullptr;
+        snode_kind  m_kind      = snode_kind::s_other;
+        unsigned    m_id        = UINT_MAX;
+        unsigned    m_num_args  = 0;
+
+        // metadata flags, analogous to ZIPT's Str/StrToken properties
+        bool        m_ground     = true;   // no uninterpreted string variables
+        bool        m_regex_free = true;   // no regex constructs
+        bool        m_nullable   = false;  // accepts the empty string
+        unsigned    m_level      = 0;      // tree depth/level (0 for empty, 1 for singletons)
+        unsigned    m_length     = 0;      // token count, number of leaf tokens in the tree
+
+        snode*      m_args[0]; // variable-length array, allocated via get_snode_size(num_args)
+
+        friend class sgraph;
+
+        static unsigned get_snode_size(unsigned num_args) {
+            return sizeof(snode) + num_args * sizeof(snode*);
+        }
+
+        static snode* mk(region& r, expr* e, snode_kind k, unsigned id, unsigned num_args, snode* const* args) {
+            void* mem = r.allocate(get_snode_size(num_args));
+            snode* n = new (mem) snode();
+            n->m_expr = e;
+            n->m_kind = k;
+            n->m_id = id;
+            n->m_num_args = num_args;
+            for (unsigned i = 0; i < num_args; ++i)
+                n->m_args[i] = args[i];
+            return n;
+        }
+
+    public:
+        expr*      get_expr() const { return m_expr; }
+        snode_kind kind()     const { return m_kind; }
+        unsigned   id()       const { return m_id; }
+        unsigned   num_args() const { return m_num_args; }
+        snode*     arg(unsigned i) const { SASSERT(i < m_num_args); return m_args[i]; }
+
+        bool is_ground()     const { return m_ground; }
+        bool is_regex_free() const { return m_regex_free; }
+        bool is_nullable()   const { return m_nullable; }
+        unsigned level()     const { return m_level; }
+        unsigned length()    const { return m_length; }
+
+        bool is_empty()   const { return m_kind == snode_kind::s_empty; }
+        bool is_char()    const { return m_kind == snode_kind::s_char; }
+        bool is_var()     const { return m_kind == snode_kind::s_var; }
+        bool is_unit()    const { return m_kind == snode_kind::s_unit; }
+        bool is_concat()  const { return m_kind == snode_kind::s_concat; }
+        bool is_power()   const { return m_kind == snode_kind::s_power; }
+        bool is_star()    const { return m_kind == snode_kind::s_star; }
+        bool is_loop()    const { return m_kind == snode_kind::s_loop; }
+        bool is_union()   const { return m_kind == snode_kind::s_union; }
+        bool is_intersect()  const { return m_kind == snode_kind::s_intersect; }
+        bool is_complement() const { return m_kind == snode_kind::s_complement; }
+        bool is_fail()       const { return m_kind == snode_kind::s_fail; }
+        bool is_full_char()  const { return m_kind == snode_kind::s_full_char; }
+        bool is_full_seq()   const { return m_kind == snode_kind::s_full_seq; }
+        bool is_to_re()      const { return m_kind == snode_kind::s_to_re; }
+        bool is_in_re()      const { return m_kind == snode_kind::s_in_re; }
+
+        // is this a leaf token (analogous to ZIPT's StrToken as opposed to Str)
+        bool is_token() const {
+            switch (m_kind) {
+            case snode_kind::s_empty:
+            case snode_kind::s_concat:
+                return false;
+            default:
+                return true;
+            }
+        }
+
+        // analogous to ZIPT's Str.First / Str.Last
+        snode const* first() const {
+            snode const* s = this;
+            while (s->is_concat())
+                s = s->arg(0);
+            return s;
+        }
+
+        snode const* last() const {
+            snode const* s = this;
+            while (s->is_concat())
+                s = s->arg(1);
+            return s;
+        }
+
+        snode* first() {
+            snode* s = this;
+            while (s->is_concat())
+                s = s->arg(0);
+            return s;
+        }
+
+        snode* last() {
+            snode* s = this;
+            while (s->is_concat())
+                s = s->arg(1);
+            return s;
+        }
+    };
+
+}
+

src/ast/seq_decl_plugin.cpp

@@ -222,6 +222,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_SEQ_NTH_I]     = alloc(psig, m, "seq.nth_i",    1, 2, seqAintT, A);
     m_sigs[OP_SEQ_NTH_U]     = alloc(psig, m, "seq.nth_u",    1, 2, seqAintT, A);
     m_sigs[OP_SEQ_LENGTH]    = alloc(psig, m, "seq.len",      1, 1, &seqA, intT);
+    m_sigs[OP_SEQ_POWER]     = alloc(psig, m, "seq.power",    1, 2, seqAintT, seqA);
     m_sigs[OP_RE_PLUS]       = alloc(psig, m, "re.+",         1, 1, &reA, reA);
     m_sigs[OP_RE_STAR]       = alloc(psig, m, "re.*",         1, 1, &reA, reA);
     m_sigs[OP_RE_OPTION]     = alloc(psig, m, "re.opt",       1, 1, &reA, reA);
@@ -591,6 +592,10 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         add_map_sig();
         return mk_str_fun(k, arity, domain, range, k);    
 
+    case OP_SEQ_POWER:
+        match(*m_sigs[k], arity, domain, range, rng);
+        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+
     case OP_SEQ_TO_RE:
         m_has_re = true;
         return mk_seq_fun(k, arity, domain, range, _OP_STRING_TO_REGEXP);

src/ast/seq_decl_plugin.h

@@ -59,6 +59,7 @@ enum seq_op_kind {
     OP_SEQ_MAPI,           // Array[Int,A,B] -> Int -> Seq[A] -> Seq[B]
     OP_SEQ_FOLDL,          // Array[B,A,B] -> B -> Seq[A] -> B
     OP_SEQ_FOLDLI,         // Array[Int,B,A,B] -> Int -> B -> Seq[A] -> B
+    OP_SEQ_POWER,          // Seq -> Int -> Seq, string exponentiation s^n
  
     OP_RE_PLUS,
     OP_RE_STAR,
@@ -307,6 +308,7 @@ public:
         app* mk_mapi(expr* f, expr* i, expr* s) const { expr* es[3] = { f, i, s }; return m.mk_app(m_fid, OP_SEQ_MAPI, 3, es); }
         app* mk_foldl(expr* f, expr* b, expr* s) const { expr* es[3] = { f, b, s }; return m.mk_app(m_fid, OP_SEQ_FOLDL, 3, es); }
         app* mk_foldli(expr* f, expr* i, expr* b, expr* s) const { expr* es[4] = { f, i, b, s }; return m.mk_app(m_fid, OP_SEQ_FOLDLI, 4, es); }
+        app* mk_power(expr* s, expr* n) const { expr* es[2] = { s, n }; return m.mk_app(m_fid, OP_SEQ_POWER, 2, es); }
 
         app* mk_substr(expr* a, expr* b, expr* c) const { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }
         app* mk_contains(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
@@ -348,6 +350,7 @@ public:
         bool is_mapi(expr const* n)      const { return is_app_of(n, m_fid, OP_SEQ_MAPI); }
         bool is_foldl(expr const* n)      const { return is_app_of(n, m_fid, OP_SEQ_FOLDL); }
         bool is_foldli(expr const* n)      const { return is_app_of(n, m_fid, OP_SEQ_FOLDLI); }
+        bool is_power(expr const* n)       const { return is_app_of(n, m_fid, OP_SEQ_POWER); }
         bool is_extract(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); }
         bool is_contains(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); }
         bool is_at(expr const* n)       const { return is_app_of(n, m_fid, OP_SEQ_AT); }
@@ -404,6 +407,7 @@ public:
         MATCH_TERNARY(is_mapi);
         MATCH_TERNARY(is_foldl);
         MATCH_QUATARY(is_foldli);
+        MATCH_BINARY(is_power);
         MATCH_BINARY(is_last_index);
         MATCH_TERNARY(is_replace);
         MATCH_TERNARY(is_replace_re);

src/test/CMakeLists.txt

@@ -51,6 +51,8 @@ add_executable(test-z3
   escaped.cpp
   euf_bv_plugin.cpp
   euf_arith_plugin.cpp
+  euf_sgraph.cpp
+  euf_seq_plugin.cpp
   ex.cpp
   expr_rand.cpp
   expr_substitution.cpp

src/test/euf_seq_plugin.cpp

@@ -0,0 +1,234 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+--*/
+
+#include "util/util.h"
+#include "ast/euf/euf_sgraph.h"
+#include "ast/euf/euf_seq_plugin.h"
+#include "ast/euf/euf_egraph.h"
+#include "ast/reg_decl_plugins.h"
+#include "ast/ast_pp.h"
+#include <iostream>
+
+static unsigned s_var = 0;
+
+static euf::enode* get_node(euf::egraph& g, seq_util& seq, expr* e) {
+    auto* n = g.find(e);
+    if (n) return n;
+    euf::enode_vector args;
+    if (is_app(e))
+        for (expr* arg : *to_app(e))
+            args.push_back(get_node(g, seq, arg));
+    n = g.mk(e, 0, args.size(), args.data());
+    if (seq.is_seq(e) || seq.is_re(e))
+        g.add_th_var(n, ++s_var, seq.get_family_id());
+    return n;
+}
+
+// test sgraph: basic classification and metadata
+static void test_sgraph_basic() {
+    std::cout << "test_sgraph_basic\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref y(m.mk_const("y", str_sort), m);
+    expr_ref empty(seq.str.mk_empty(str_sort), m);
+    expr_ref xy(seq.str.mk_concat(x, y), m);
+
+    euf::snode* sx = sg.mk(x);
+    SASSERT(sx);
+    SASSERT(sx->is_var());
+    SASSERT(!sx->is_ground());
+    SASSERT(sx->is_regex_free());
+    SASSERT(!sx->is_nullable());
+    SASSERT(sx->length() == 1);
+
+    euf::snode* se = sg.mk(empty);
+    SASSERT(se);
+    SASSERT(se->is_empty());
+    SASSERT(se->is_ground());
+    SASSERT(se->is_nullable());
+    SASSERT(se->length() == 0);
+
+    euf::snode* sxy = sg.mk(xy);
+    SASSERT(sxy);
+    SASSERT(sxy->is_concat());
+    SASSERT(!sxy->is_ground());
+    SASSERT(sxy->length() == 2);
+    SASSERT(sxy->num_args() == 2);
+
+    std::cout << "sgraph:\n";
+    sg.display(std::cout);
+    std::cout << "\n";
+}
+
+// test sgraph: backtracking with push/pop
+static void test_sgraph_backtrack() {
+    std::cout << "test_sgraph_backtrack\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref y(m.mk_const("y", str_sort), m);
+
+    sg.mk(x);
+    unsigned before = sg.num_nodes();
+
+    sg.push();
+
+    expr_ref xy(seq.str.mk_concat(x, y), m);
+    sg.mk(xy);
+    SASSERT(sg.num_nodes() > before);
+
+    sg.pop(1);
+    // y and xy were created inside the scope, so some nodes should be removed
+    // x was created before the scope, so it should persist
+    SASSERT(sg.find(x));
+}
+
+// test seq_plugin: concat associativity is normalized by the plugin
+static void test_seq_plugin_assoc() {
+    std::cout << "test_seq_plugin_assoc\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    euf::egraph& g = sg.get_egraph();
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref a(m.mk_const("a", str_sort), m);
+    expr_ref b(m.mk_const("b", str_sort), m);
+    expr_ref c(m.mk_const("c", str_sort), m);
+
+    // register nodes in egraph
+    // concat(concat(a,b),c) should be merged with concat(a,concat(b,c))
+    expr_ref ab(seq.str.mk_concat(a, b), m);
+    expr_ref ab_c(seq.str.mk_concat(ab, c), m);
+
+    euf::enode* nab_c = get_node(g, seq, ab_c);
+    g.propagate();
+
+    // the plugin should have created a right-associated form and merged
+    std::cout << g << "\n";
+}
+
+// test seq_plugin: empty string elimination
+static void test_seq_plugin_empty() {
+    std::cout << "test_seq_plugin_empty\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    euf::egraph& g = sg.get_egraph();
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref empty(seq.str.mk_empty(str_sort), m);
+    expr_ref xe(seq.str.mk_concat(x, empty), m);
+
+    auto* nxe = get_node(g, seq, xe);
+    auto* nx = g.find(x);
+    g.propagate();
+
+    // concat(x, empty) should be merged with x
+    SASSERT(nxe->get_root() == nx->get_root());
+    std::cout << g << "\n";
+}
+
+// test seq_plugin: Kleene star merging
+// The seq_plugin detects when star bodies are congruent
+// This tests the same_star_body logic at the regex level
+static void test_seq_plugin_star_merge() {
+    std::cout << "test_seq_plugin_star_merge\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    euf::egraph& g = sg.get_egraph();
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+    sort_ref re_sort(seq.re.mk_re(str_sort), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    // re.star(to_re(x))
+    expr_ref to_re_x(seq.re.mk_to_re(x), m);
+    expr_ref star_x(seq.re.mk_star(to_re_x), m);
+    // use regex concat for star * star
+    expr_ref star_star(seq.re.mk_concat(star_x, star_x), m);
+
+    // register in sgraph
+    sg.mk(star_star);
+    euf::snode* s = sg.find(star_x);
+    SASSERT(s && s->is_star());
+    SASSERT(s->is_nullable());
+
+    std::cout << g << "\n";
+}
+
+// test seq_plugin: nullable absorption by .*
+// concat(.*, nullable) should merge with .*
+static void test_seq_plugin_nullable_absorb() {
+    std::cout << "test_seq_plugin_nullable_absorb\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    euf::egraph& g = sg.get_egraph();
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref empty(seq.str.mk_empty(str_sort), m);
+    // concat(x, empty) = x (empty is nullable, exercises nullable check)
+    expr_ref xe(seq.str.mk_concat(x, empty), m);
+
+    auto* nxe = get_node(g, seq, xe);
+    auto* nx = g.find(x);
+    g.propagate();
+
+    // concat(x, empty) should be merged with x (empty elimination)
+    SASSERT(nxe->get_root() == nx->get_root());
+    std::cout << g << "\n";
+}
+
+// test sgraph owns egraph and syncs push/pop
+static void test_sgraph_egraph_sync() {
+    std::cout << "test_sgraph_egraph_sync\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    euf::egraph& g = sg.get_egraph();
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref y(m.mk_const("y", str_sort), m);
+    auto* nx = get_node(g, seq, x);
+    auto* ny = get_node(g, seq, y);
+
+    sg.push();
+
+    g.merge(nx, ny, nullptr);
+    g.propagate();
+    SASSERT(nx->get_root() == ny->get_root());
+
+    sg.pop(1);
+    // after pop, the merge should be undone
+    SASSERT(nx->get_root() != ny->get_root());
+}
+
+void tst_euf_seq_plugin() {
+    s_var = 0; test_sgraph_basic();
+    s_var = 0; test_sgraph_backtrack();
+    s_var = 0; test_seq_plugin_assoc();
+    s_var = 0; test_seq_plugin_empty();
+    s_var = 0; test_seq_plugin_star_merge();
+    s_var = 0; test_seq_plugin_nullable_absorb();
+    s_var = 0; test_sgraph_egraph_sync();
+}

src/test/euf_sgraph.cpp

@@ -0,0 +1,446 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    euf_sgraph.cpp
+
+Abstract:
+
+    Self-contained unit tests for the sgraph string graph layer.
+    Tests snode classification, metadata computation, push/pop
+    backtracking, associativity-respecting hash table, compound
+    node construction, and snode navigation.
+
+--*/
+
+#include "util/util.h"
+#include "ast/euf/euf_sgraph.h"
+#include "ast/reg_decl_plugins.h"
+#include "ast/ast_pp.h"
+#include "ast/arith_decl_plugin.h"
+#include <iostream>
+
+// test classification and metadata for basic string nodes:
+// variables, empty strings, characters, units, and concats
+static void test_sgraph_classify() {
+    std::cout << "test_sgraph_classify\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    // string variable
+    expr_ref x(m.mk_const("x", str_sort), m);
+    euf::snode* sx = sg.mk(x);
+    SASSERT(sx && sx->is_var());
+    SASSERT(!sx->is_ground());
+    SASSERT(sx->is_regex_free());
+    SASSERT(!sx->is_nullable());
+    SASSERT(sx->level() == 1);
+    SASSERT(sx->length() == 1);
+    SASSERT(sx->is_token());
+
+    // empty string
+    expr_ref empty(seq.str.mk_empty(str_sort), m);
+    euf::snode* se = sg.mk(empty);
+    SASSERT(se && se->is_empty());
+    SASSERT(se->is_ground());
+    SASSERT(se->is_nullable());
+    SASSERT(se->level() == 0);
+    SASSERT(se->length() == 0);
+    SASSERT(!se->is_token());
+
+    // character unit with literal char
+    expr_ref ch(seq.str.mk_char('A'), m);
+    expr_ref unit_a(seq.str.mk_unit(ch), m);
+    euf::snode* sca = sg.mk(unit_a);
+    SASSERT(sca && sca->is_char());
+    SASSERT(sca->is_ground());
+    SASSERT(!sca->is_nullable());
+    SASSERT(sca->level() == 1);
+    SASSERT(sca->length() == 1);
+    SASSERT(sca->is_token());
+
+    // concat of two variables
+    expr_ref y(m.mk_const("y", str_sort), m);
+    expr_ref xy(seq.str.mk_concat(x, y), m);
+    euf::snode* sxy = sg.mk(xy);
+    SASSERT(sxy && sxy->is_concat());
+    SASSERT(!sxy->is_ground());
+    SASSERT(sxy->is_regex_free());
+    SASSERT(!sxy->is_nullable());
+    SASSERT(sxy->level() == 2);
+    SASSERT(sxy->length() == 2);
+    SASSERT(sxy->num_args() == 2);
+    SASSERT(!sxy->is_token());
+
+    sg.display(std::cout);
+}
+
+// test classification for regex nodes:
+// star, union, intersection, complement, full_seq, full_char, fail, to_re, in_re
+static void test_sgraph_regex() {
+    std::cout << "test_sgraph_regex\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+
+    // to_re
+    expr_ref to_re_x(seq.re.mk_to_re(x), m);
+    euf::snode* str = sg.mk(to_re_x);
+    SASSERT(str && str->is_to_re());
+    SASSERT(!str->is_regex_free());
+    SASSERT(!str->is_nullable()); // to_re(x) nullable iff x nullable, x is var so not nullable
+    SASSERT(str->num_args() == 1);
+
+    // star
+    expr_ref star_x(seq.re.mk_star(to_re_x), m);
+    euf::snode* ss = sg.mk(star_x);
+    SASSERT(ss && ss->is_star());
+    SASSERT(!ss->is_regex_free());
+    SASSERT(ss->is_nullable()); // star is always nullable
+    SASSERT(ss->num_args() == 1);
+
+    // full_seq (.*)
+    expr_ref full_seq(seq.re.mk_full_seq(str_sort), m);
+    euf::snode* sfs = sg.mk(full_seq);
+    SASSERT(sfs && sfs->is_full_seq());
+    SASSERT(sfs->is_ground());
+    SASSERT(sfs->is_nullable());
+
+    // full_char (.)
+    expr_ref full_char(seq.re.mk_full_char(str_sort), m);
+    euf::snode* sfc = sg.mk(full_char);
+    SASSERT(sfc && sfc->is_full_char());
+    SASSERT(sfc->is_ground());
+    SASSERT(!sfc->is_nullable());
+
+    // empty set, fail
+    sort_ref re_sort(seq.re.mk_re(str_sort), m);
+    expr_ref empty_set(seq.re.mk_empty(re_sort), m);
+    euf::snode* sfail = sg.mk(empty_set);
+    SASSERT(sfail && sfail->is_fail());
+    SASSERT(!sfail->is_nullable());
+
+    // union: to_re(x) | star(to_re(x)), nullable because star is
+    expr_ref re_union(seq.re.mk_union(to_re_x, star_x), m);
+    euf::snode* su = sg.mk(re_union);
+    SASSERT(su && su->is_union());
+    SASSERT(su->is_nullable()); // star_x is nullable
+
+    // intersection: to_re(x) & star(to_re(x)), nullable only if both are
+    expr_ref re_inter(seq.re.mk_inter(to_re_x, star_x), m);
+    euf::snode* si = sg.mk(re_inter);
+    SASSERT(si && si->is_intersect());
+    SASSERT(!si->is_nullable()); // to_re(x) is not nullable
+
+    // complement of to_re(x): nullable because to_re(x) is not nullable
+    expr_ref re_comp(seq.re.mk_complement(to_re_x), m);
+    euf::snode* sc = sg.mk(re_comp);
+    SASSERT(sc && sc->is_complement());
+    SASSERT(sc->is_nullable()); // complement of non-nullable is nullable
+
+    // in_re
+    expr_ref in_re(seq.re.mk_in_re(x, star_x), m);
+    euf::snode* sir = sg.mk(in_re);
+    SASSERT(sir && sir->is_in_re());
+    SASSERT(!sir->is_regex_free());
+
+    sg.display(std::cout);
+}
+
+// test power node classification and metadata
+static void test_sgraph_power() {
+    std::cout << "test_sgraph_power\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    arith_util arith(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref n(arith.mk_int(3), m);
+    expr_ref xn(seq.str.mk_power(x, n), m);
+
+    euf::snode* sp = sg.mk(xn);
+    SASSERT(sp && sp->is_power());
+    SASSERT(!sp->is_ground()); // base x is not ground
+    SASSERT(sp->is_regex_free());
+    SASSERT(!sp->is_nullable()); // base x is not nullable
+    SASSERT(sp->num_args() >= 1);
+
+    sg.display(std::cout);
+}
+
+// test push/pop backtracking: nodes created inside a scope
+// are removed on pop, nodes before persist
+static void test_sgraph_push_pop() {
+    std::cout << "test_sgraph_push_pop\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref y(m.mk_const("y", str_sort), m);
+    expr_ref z(m.mk_const("z", str_sort), m);
+
+    // create x before any scope
+    sg.mk(x);
+    unsigned before = sg.num_nodes();
+    SASSERT(sg.find(x));
+
+    sg.push();
+
+    // create y and concat(x,y) inside scope
+    expr_ref xy(seq.str.mk_concat(x, y), m);
+    sg.mk(xy);
+    SASSERT(sg.num_nodes() > before);
+    SASSERT(sg.find(y));
+    SASSERT(sg.find(xy));
+
+    sg.pop(1);
+
+    // x persists, y and xy removed
+    SASSERT(sg.find(x));
+    SASSERT(!sg.find(y));
+    SASSERT(!sg.find(xy));
+    SASSERT(sg.num_nodes() == before);
+}
+
+// test nested push/pop with multiple scopes
+static void test_sgraph_nested_scopes() {
+    std::cout << "test_sgraph_nested_scopes\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref a(m.mk_const("a", str_sort), m);
+    expr_ref b(m.mk_const("b", str_sort), m);
+    expr_ref c(m.mk_const("c", str_sort), m);
+
+    sg.mk(a);
+    unsigned n0 = sg.num_nodes();
+
+    sg.push();
+    sg.mk(b);
+    unsigned n1 = sg.num_nodes();
+
+    sg.push();
+    sg.mk(c);
+    unsigned n2 = sg.num_nodes();
+    SASSERT(n2 > n1 && n1 > n0);
+
+    // pop inner scope, c goes away
+    sg.pop(1);
+    SASSERT(sg.num_nodes() == n1);
+    SASSERT(sg.find(a));
+    SASSERT(sg.find(b));
+    SASSERT(!sg.find(c));
+
+    // pop outer scope, b goes away
+    sg.pop(1);
+    SASSERT(sg.num_nodes() == n0);
+    SASSERT(sg.find(a));
+    SASSERT(!sg.find(b));
+}
+
+// test that find returns the same snode for the same expression
+static void test_sgraph_find_idempotent() {
+    std::cout << "test_sgraph_find_idempotent\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    euf::snode* s1 = sg.mk(x);
+    euf::snode* s2 = sg.mk(x);  // calling mk again returns same node
+    SASSERT(s1 == s2);
+    SASSERT(s1 == sg.find(x));
+}
+
+// test mk_concat: empty absorption, node construction via mk(concat_expr)
+static void test_sgraph_mk_concat() {
+    std::cout << "test_sgraph_mk_concat\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref y(m.mk_const("y", str_sort), m);
+    expr_ref empty(seq.str.mk_empty(str_sort), m);
+
+    euf::snode* sx = sg.mk(x);
+    euf::snode* sy = sg.mk(y);
+    euf::snode* se = sg.mk(empty);
+
+    // concat with empty yields the non-empty side at sgraph level
+    // (empty absorption is a property of the expression, checked via mk)
+    SASSERT(se && se->is_empty());
+
+    // normal concat via expression
+    expr_ref xy(seq.str.mk_concat(x, y), m);
+    euf::snode* sxy = sg.mk(xy);
+    SASSERT(sxy && sxy->is_concat());
+    SASSERT(sxy->num_args() == 2);
+    SASSERT(sxy->arg(0) == sx);
+    SASSERT(sxy->arg(1) == sy);
+
+    // calling mk again with same expr returns same node
+    euf::snode* sxy2 = sg.mk(xy);
+    SASSERT(sxy == sxy2);
+}
+
+// test power node construction via mk(power_expr)
+static void test_sgraph_mk_power() {
+    std::cout << "test_sgraph_mk_power\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    arith_util arith(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref n(arith.mk_int(5), m);
+    expr_ref xn(seq.str.mk_power(x, n), m);
+
+    euf::snode* sx = sg.mk(x);
+    euf::snode* sp = sg.mk(xn);
+    SASSERT(sp && sp->is_power());
+    SASSERT(sp->num_args() == 2);
+    SASSERT(sp->arg(0) == sx);
+
+    // calling mk again returns same node
+    euf::snode* sp2 = sg.mk(xn);
+    SASSERT(sp == sp2);
+}
+
+// test snode first/last navigation on concat trees
+static void test_sgraph_first_last() {
+    std::cout << "test_sgraph_first_last\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref a(m.mk_const("a", str_sort), m);
+    expr_ref b(m.mk_const("b", str_sort), m);
+    expr_ref c(m.mk_const("c", str_sort), m);
+
+    euf::snode* sa = sg.mk(a);
+    euf::snode* sb = sg.mk(b);
+    euf::snode* sc = sg.mk(c);
+
+    // concat(concat(a,b),c): first=a, last=c
+    expr_ref ab(seq.str.mk_concat(a, b), m);
+    expr_ref ab_c(seq.str.mk_concat(ab, c), m);
+    euf::snode* sab_c = sg.mk(ab_c);
+    SASSERT(sab_c->first() == sa);
+    SASSERT(sab_c->last() == sc);
+
+    // concat(a,concat(b,c)): first=a, last=c
+    expr_ref bc(seq.str.mk_concat(b, c), m);
+    expr_ref a_bc(seq.str.mk_concat(a, bc), m);
+    euf::snode* sa_bc = sg.mk(a_bc);
+    SASSERT(sa_bc->first() == sa);
+    SASSERT(sa_bc->last() == sc);
+
+    // single node: first and last are self
+    SASSERT(sa->first() == sa);
+    SASSERT(sa->last() == sa);
+}
+
+// test concat metadata propagation:
+// ground, regex_free, nullable, level, length
+static void test_sgraph_concat_metadata() {
+    std::cout << "test_sgraph_concat_metadata\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref empty(seq.str.mk_empty(str_sort), m);
+    expr_ref ch(seq.str.mk_char('Z'), m);
+    expr_ref unit_z(seq.str.mk_unit(ch), m);
+
+    euf::snode* sx = sg.mk(x);
+    euf::snode* se = sg.mk(empty);
+    euf::snode* sz = sg.mk(unit_z);
+
+    // concat(x, unit('Z')): not ground (x is variable), regex_free, not nullable
+    expr_ref xz(seq.str.mk_concat(x, unit_z), m);
+    euf::snode* sxz = sg.mk(xz);
+    SASSERT(!sxz->is_ground());
+    SASSERT(sxz->is_regex_free());
+    SASSERT(!sxz->is_nullable());
+    SASSERT(sxz->length() == 2);
+    SASSERT(sxz->level() == 2);
+
+    // concat(empty, empty): nullable (both empty)
+    expr_ref empty2(seq.str.mk_concat(empty, empty), m);
+    euf::snode* see = sg.mk(empty2);
+    SASSERT(see->is_nullable());
+    SASSERT(see->is_ground());
+    SASSERT(see->length() == 0);
+
+    // deep chain: concat(concat(x,x),concat(x,x)) has level 3, length 4
+    expr_ref xx(seq.str.mk_concat(x, x), m);
+    expr_ref xxxx(seq.str.mk_concat(xx, xx), m);
+    euf::snode* sxxxx = sg.mk(xxxx);
+    SASSERT(sxxxx->level() == 3);
+    SASSERT(sxxxx->length() == 4);
+}
+
+// test display does not crash
+static void test_sgraph_display() {
+    std::cout << "test_sgraph_display\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::sgraph sg(m);
+    seq_util seq(m);
+    sort_ref str_sort(seq.str.mk_string_sort(), m);
+
+    expr_ref x(m.mk_const("x", str_sort), m);
+    expr_ref y(m.mk_const("y", str_sort), m);
+    expr_ref xy(seq.str.mk_concat(x, y), m);
+    sg.mk(xy);
+
+    std::ostringstream oss;
+    sg.display(oss);
+    std::string out = oss.str();
+    SASSERT(out.find("var") != std::string::npos);
+    SASSERT(out.find("concat") != std::string::npos);
+    std::cout << out;
+}
+
+void tst_euf_sgraph() {
+    test_sgraph_classify();
+    test_sgraph_regex();
+    test_sgraph_power();
+    test_sgraph_push_pop();
+    test_sgraph_nested_scopes();
+    test_sgraph_find_idempotent();
+    test_sgraph_mk_concat();
+    test_sgraph_mk_power();
+    test_sgraph_first_last();
+    test_sgraph_concat_metadata();
+    test_sgraph_display();
+}

src/test/main.cpp

@@ -281,6 +281,8 @@ int main(int argc, char ** argv) {
     TST(distribution);
     TST(euf_bv_plugin);
     TST(euf_arith_plugin);
+    TST(euf_sgraph);
+    TST(euf_seq_plugin);
     TST(sls_test);
     TST(scoped_vector);
     TST(sls_seq_plugin);