Add lazy regex live-state traversal

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: 2bcccba7-ac7d-476e-8dfe-718a21d37554

src/ast/rewriter/CMakeLists.txt

@@ -48,6 +48,7 @@ z3_add_component(rewriter
     seq_range_predicate.cpp
     seq_rewriter.cpp
     seq_regex_bisim.cpp
+    seq_regex_live.cpp
     seq_skolem.cpp
     term_enumeration.cpp
     th_rewriter.cpp

src/ast/rewriter/seq_derive.cpp

@@ -39,7 +39,8 @@ namespace seq {
         m_br(m),
         m_re(re),
         m_trail(m), 
-        m_cofactor_cache(m),
+        m_brz_cofactor_cache(m),
+        m_ant_cofactor_cache(m),
         m_ele(m),
         m_path_expr(m) {
         m_br.set_flat_and_or(false);
@@ -1572,15 +1573,18 @@ namespace seq {
     }
 
     expr_ref_pair_vector const &derive::get_cached_cofactors(transition_mode mode, expr *r) {
+        cofactor_cache& cache =
+            mode == transition_mode::light_antimirov_tm ?
+            m_ant_cofactor_cache : m_brz_cofactor_cache;
         expr_ref_pair_vector *v = nullptr;
-        if (m_cofactor_cache.find(r, v))
+        if (cache.find(r, v))
             return *v;
         v = alloc(expr_ref_pair_vector, m);
         if (mode == transition_mode::light_antimirov_tm)
             light_ant_derivative_cofactors(r, *v);
         else
             derivative_cofactors(r, *v);
-        m_cofactor_cache.insert(r, v);  // takes ownership of v and pins the key r
+        cache.insert(r, v);  // takes ownership of v and pins the key r
         return *v;
     }
 
@@ -1659,4 +1663,3 @@ namespace seq {
     }
 
 }
-

src/ast/rewriter/seq_derive.h

@@ -95,7 +95,8 @@ namespace seq {
         obj_pair_map<expr, expr, expr*> m_atop_cache, m_btop_cache; // post-simplify cache
         expr_ref_vector      m_trail;    // pin cached results
        
-        cofactor_cache       m_cofactor_cache;
+        cofactor_cache       m_brz_cofactor_cache;
+        cofactor_cache       m_ant_cofactor_cache;
 
         // Op cache for ITE-hoisting operations (union, inter, concat, complement)
         // Path-aware caches: key is (a, b, path_expr) for binary ops, (a, path_expr) for complement
@@ -276,7 +277,8 @@ namespace seq {
         expr_ref_pair_vector const &get_cached_cofactors(transition_mode mode, expr *r);
 
         void maybe_reset_cached_cofactors(unsigned cap) {
-            m_cofactor_cache.maybe_reset(cap);
+            m_brz_cofactor_cache.maybe_reset(cap);
+            m_ant_cofactor_cache.maybe_reset(cap);
         }
 
         /**

src/ast/rewriter/seq_monadic.cpp

@@ -131,76 +131,6 @@ expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) {
     return m_rw.get_derive().get_cached_cofactors(m_config.m_mode, r);
 }
 
-bool seq_monadic::live_states(expr* R, expr_ref_vector& out) {
-    obj_map<expr, unsigned> id;
-    expr_ref_vector states(m);
-    vector<svector<unsigned>> succ;
-    bool_vector maybe_null;
-    auto intern = [&](expr* s) -> unsigned {
-        unsigned k;
-        if (id.find(s, k)) return k;
-        k = states.size();
-        id.insert(s, k);
-        states.push_back(s);
-        succ.push_back(svector<unsigned>());
-        maybe_null.push_back(nullable(s) != l_false);   // unknown nullability => keep (conservative)
-        return k;
-    };
-    intern(R);
-    const unsigned STATE_CAP = 1u << 12;
-    for (unsigned i = 0; i < states.size(); ++i) {
-        if (states.size() > STATE_CAP) {
-            m_stats.inc_bail(bail_reason::state_cap);
-            return false;
-        }
-        if (!m.inc()) {
-            m_stats.inc_bail(bail_reason::resource);
-            return false;
-        }
-        expr_ref_pair_vector const& cof = derivative_cofactors(states.get(i));
-        for (auto const& [g, t] : cof) {
-            if (re().is_empty(t)) continue;
-            unsigned k = intern(t);           // MUST precede succ[i] indexing: intern may
-            succ[i].push_back(k);             // grow (realloc) succ, invalidating succ[i]&
-        }
-    }
-    unsigned n = states.size();
-    bool_vector live;
-    live.resize(n, false);
-    for (unsigned i = 0; i < n; ++i)
-        live[i] = maybe_null[i];
-    for (bool ch = true; ch; ) {
-        ch = false;
-        for (unsigned i = 0; i < n; ++i)
-            if (!live[i])
-                for (unsigned j : succ[i])
-                    if (live[j]) { live[i] = true; ch = true; break; }
-    }
-    for (unsigned i = 0; i < n; ++i)
-        if (live[i]) { out.push_back(states.get(i)); m_pin.push_back(states.get(i)); }
-    return true;
-}
-
-expr_ref_vector const* seq_monadic::live_states_cached(expr* R) {
-    expr_ref_vector* v = nullptr;
-    if (m_live_cache.find(R, v))
-        return v;                          // may be null: previously gave up on R
-    v = alloc(expr_ref_vector, m);
-    if (!live_states(R, *v)) {
-        dealloc(v);
-        v = nullptr;
-    }
-    m_pin.push_back(R);                    // keep the key alive for the cache's lifetime
-    m_live_cache.insert(R, v);
-    return v;
-}
-
-void seq_monadic::reset_live_cache() {
-    for (auto const& [k, v] : m_live_cache)
-        dealloc(v);
-    m_live_cache.reset();
-}
-
 lbool seq_monadic::product_nonempty(svector<component> const& comps, expr_ref* witness_word) {
     unsigned n = comps.size();
     if (n == 0) {
@@ -417,7 +347,7 @@ void seq_monadic::reset_search() {
     m_der_cache.reset();
     m_nullable_cache.reset();
     m_undef_vars = 0;
-    reset_live_cache();
+    m_live_states.reset();
 }
 
 bool seq_monadic::prepare(membership_vec const& memberships) {
@@ -550,11 +480,15 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
     if (last_atom)
         targets.push_back(nullptr);
     else {
-        expr_ref_vector const* Q = live_states_cached(R);
-        if (!Q)
-            return l_undef;
-        for (expr* q : *Q)
+        auto live = m_live_states.reachable_live(R);
+        for (expr* q : live)
             targets.push_back(q);
+        if (live.failed()) {
+            m_stats.inc_bail(
+                live.failure_reason() == seq::live_states::failure::state_cap ?
+                bail_reason::state_cap : bail_reason::resource);
+            return l_undef;
+        }
     }
 
     unsigned vi = var_index(a.var.get());

src/ast/rewriter/seq_monadic.h

@@ -63,6 +63,7 @@ Author:
 
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/seq_range_predicate.h"
+#include "ast/rewriter/seq_regex_live.h"
 #include "ast/rewriter/guard_set.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "util/lbool.h"
@@ -166,7 +167,7 @@ class seq_monadic {
     };
     group_sig m_sig_buf;                    // reused by group_nonempty (avoids allocating per lookup)
     std::unordered_map<group_sig, lbool, group_sig_hash> m_group_cache;
-    obj_map<expr, expr_ref_vector*> m_live_cache;  // regex -> live split states (null = gave up)
+    seq::live_states m_live_states;
 
     // Brzozowski derivative of regex `r` by the concrete element `elem`.  Memoized on
     // (r, elem): the search revisits the same constant step on many branches.
@@ -175,20 +176,10 @@ class seq_monadic {
     // Memoized nullability of a derivative state: l_true / l_false / l_undef (unknown).
     lbool nullable(expr* r);
 
-    // Symbolic transition cofactors in the selected mode.  Memoized per regex `r` in
-    // m_cofactors: the returned vector is owned by that cache (see the cofactor_cache
-    // class above for the persistence/reset policy).
+    // Symbolic transition cofactors in the selected mode.  The returned vector is owned
+    // by seq_rewriter's mode-specific cofactor cache.
     expr_ref_pair_vector const& derivative_cofactors(expr* r);
 
-    // Live reachable derivative states of R (BFS over cofactor targets + liveness
-    // least-fixpoint).  These are the split states q.  Returns false on a cap overrun.
-    bool live_states(expr* R, expr_ref_vector& out);
-
-    // Memoized live_states.  Returns null if the computation gave up for this regex.
-    expr_ref_vector const* live_states_cached(expr* R);
-
-    void reset_live_cache();
-
     // Product-reachability emptiness of a conjunction of components (all on one
     // variable).  l_false = empty (unsat), l_true = non-empty (sat), l_undef = gave up
     // (cap overrun, non-range guard, or undecidable nullability).
@@ -249,9 +240,9 @@ public:
                 seq::transition_mode mode = seq::transition_mode::light_antimirov_tm) :
         m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail),
         m_pin(rw.m()), m_config(mode), m_rp_cache(rw.m()),
-        m_regexes(rw.m()) {}
+        m_regexes(rw.m()), m_live_states(rw, mode, 1u << 12) {}
 
-    ~seq_monadic() { reset_live_cache(); }
+    ~seq_monadic() = default;
 
     void collect_statistics(::statistics &st) const;
 

src/ast/rewriter/seq_regex_live.cpp

@@ -0,0 +1,279 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    seq_regex_live.cpp
+
+Abstract:
+
+    Shared lazy live-state traversal for regular-expression derivatives.
+
+--*/
+
+#include "ast/rewriter/seq_regex_live.h"
+#include "ast/rewriter/seq_rewriter.h"
+#include "util/obj_hashtable.h"
+#include "util/uint_set.h"
+
+namespace seq {
+
+    struct live_states::search {
+        svector<unsigned> m_to_explore;
+        unsigned m_explore_head = 0;
+        uint_set m_seen;
+        vector<svector<unsigned>> m_predecessors;
+        bool_vector m_live;
+        bool_vector m_closed;
+        svector<unsigned> m_live_frontier;
+        failure m_failure = failure::none;
+        bool m_complete = false;
+    };
+
+    struct live_states::imp {
+        seq_rewriter& m_rw;
+        ast_manager& m;
+        seq_util::rex& m_re;
+        transition_mode m_mode;
+        unsigned m_max_states;
+        obj_map<expr, unsigned> m_ids;
+        expr_ref_vector m_states;
+        vector<svector<unsigned>> m_successors;
+        svector<char> m_nullable;
+        bool_vector m_expanded;
+        obj_map<expr, search*> m_searches;
+
+        imp(seq_rewriter& rw, transition_mode mode, unsigned max_states) :
+            m_rw(rw),
+            m(rw.m()),
+            m_re(rw.u().re),
+            m_mode(mode),
+            m_max_states(max_states),
+            m_states(m) {
+        }
+
+        ~imp() {
+            reset();
+        }
+
+        unsigned intern(expr* r) {
+            unsigned id = 0;
+            if (m_ids.find(r, id))
+                return id;
+            id = m_states.size();
+            m_ids.insert(r, id);
+            m_states.push_back(r);
+            m_successors.push_back(svector<unsigned>());
+            m_nullable.push_back(2);
+            m_expanded.push_back(false);
+            return id;
+        }
+
+        void resize(search& s) {
+            unsigned size = m_states.size();
+            if (s.m_predecessors.size() < size)
+                s.m_predecessors.resize(size);
+            if (s.m_live.size() < size)
+                s.m_live.resize(size, false);
+            if (s.m_closed.size() < size)
+                s.m_closed.resize(size, false);
+        }
+
+        char nullable(unsigned id) {
+            if (m_nullable[id] != 2)
+                return m_nullable[id];
+            expr* r = m_states.get(id);
+            lbool n = m_re.get_info(r).nullable;
+            if (n == l_undef) {
+                expr_ref f = m_rw.is_nullable(r);
+                n = m.is_true(f) ? l_true : m.is_false(f) ? l_false : l_undef;
+            }
+            m_nullable[id] = n == l_true ? 1 : n == l_false ? 0 : 3;
+            return m_nullable[id];
+        }
+
+        void mark_live(search& s, unsigned id) {
+            svector<unsigned> todo;
+            todo.push_back(id);
+            while (!todo.empty()) {
+                id = todo.back();
+                todo.pop_back();
+                if (!s.m_seen.contains(id) || s.m_live[id])
+                    continue;
+                s.m_live[id] = true;
+                s.m_live_frontier.push_back(id);
+                for (unsigned predecessor : s.m_predecessors[id])
+                    todo.push_back(predecessor);
+            }
+        }
+
+        bool add_state(search& s, unsigned id) {
+            if (s.m_seen.contains(id))
+                return true;
+            if (s.m_to_explore.size() >= m_max_states) {
+                s.m_failure = failure::state_cap;
+                return false;
+            }
+            resize(s);
+            s.m_seen.insert(id);
+            s.m_to_explore.push_back(id);
+            if (nullable(id) != 0)
+                mark_live(s, id);
+            return true;
+        }
+
+        bool expand_state(unsigned id, failure& f) {
+            if (m_expanded[id])
+                return true;
+            if (!m.inc()) {
+                f = failure::resource;
+                return false;
+            }
+            m_expanded[id] = true;
+            nullable(id);
+            auto const& cofactors = m_rw.get_derive().get_cached_cofactors(m_mode, m_states.get(id));
+            for (auto const& [guard, target] : cofactors) {
+                if (m_re.is_empty(target))
+                    continue;
+                unsigned target_id = intern(target);
+                if (!m_successors[id].contains(target_id))
+                    m_successors[id].push_back(target_id);
+            }
+            return true;
+        }
+
+        void close(search& s) {
+            for (unsigned id : s.m_to_explore)
+                if (!s.m_live[id])
+                    s.m_closed[id] = true;
+            s.m_complete = true;
+        }
+
+        void expand(search& s) {
+            if (s.m_complete || s.m_failure != failure::none)
+                return;
+            if (s.m_explore_head == s.m_to_explore.size()) {
+                close(s);
+                return;
+            }
+
+            unsigned id = s.m_to_explore[s.m_explore_head++];
+            if (!expand_state(id, s.m_failure))
+                return;
+            resize(s);
+            for (unsigned target : m_successors[id]) {
+                if (!add_state(s, target))
+                    return;
+                if (!s.m_predecessors[target].contains(id))
+                    s.m_predecessors[target].push_back(id);
+                if (s.m_live[target])
+                    mark_live(s, id);
+            }
+        }
+
+        bool ensure(search& s, unsigned index) {
+            while (index >= s.m_live_frontier.size() &&
+                   !s.m_complete &&
+                   s.m_failure == failure::none)
+                expand(s);
+            return index < s.m_live_frontier.size();
+        }
+
+        search* get_search(expr* root) {
+            search* s = nullptr;
+            if (m_searches.find(root, s))
+                return s;
+            s = alloc(search);
+            unsigned root_id = intern(root);
+            add_state(*s, root_id);
+            m_searches.insert(root, s);
+            return s;
+        }
+
+        void reset() {
+            for (auto const& [root, s] : m_searches)
+                dealloc(s);
+            m_searches.reset();
+            m_ids.reset();
+            m_states.reset();
+            m_successors.reset();
+            m_nullable.reset();
+            m_expanded.reset();
+        }
+    };
+
+    live_states::live_states(seq_rewriter& rw, transition_mode mode, unsigned max_states) :
+        m_imp(alloc(imp, rw, mode, max_states)) {
+    }
+
+    live_states::~live_states() {
+        dealloc(m_imp);
+    }
+
+    expr* live_states::iterator::operator*() const {
+        return m_owner->get_live(m_search, m_index);
+    }
+
+    live_states::iterator& live_states::iterator::operator++() {
+        ++m_index;
+        return *this;
+    }
+
+    bool live_states::iterator::operator!=(iterator const& other) const {
+        if (other.m_end)
+            return m_owner->ensure(m_search, m_index);
+        return m_owner != other.m_owner ||
+               m_search != other.m_search ||
+               m_index != other.m_index ||
+               m_end != other.m_end;
+    }
+
+    live_states::iterator live_states::reachable::begin() const {
+        return iterator(m_owner, m_search, 0, false);
+    }
+
+    live_states::iterator live_states::reachable::end() const {
+        return iterator(m_owner, m_search, 0, true);
+    }
+
+    bool live_states::reachable::failed() const {
+        return m_owner->get_failure(m_search) != failure::none;
+    }
+
+    live_states::failure live_states::reachable::failure_reason() const {
+        return m_owner->get_failure(m_search);
+    }
+
+    bool live_states::reachable::is_dead() {
+        return !m_owner->ensure(m_search, 0) && !failed();
+    }
+
+    live_states::reachable live_states::reachable_live(expr* r) {
+        return reachable(this, m_imp->get_search(r));
+    }
+
+    bool live_states::contains(expr* r) const {
+        return m_imp->m_ids.contains(r);
+    }
+
+    unsigned live_states::state_id(expr* r) {
+        return m_imp->intern(r) + 1;
+    }
+
+    void live_states::reset() {
+        m_imp->reset();
+    }
+
+    bool live_states::ensure(search* s, unsigned index) {
+        return m_imp->ensure(*s, index);
+    }
+
+    expr* live_states::get_live(search* s, unsigned index) const {
+        return m_imp->m_states.get(s->m_live_frontier[index]);
+    }
+
+    live_states::failure live_states::get_failure(search* s) const {
+        return s->m_failure;
+    }
+
+}

src/ast/rewriter/seq_regex_live.h

@@ -0,0 +1,81 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    seq_regex_live.h
+
+Abstract:
+
+    Shared lazy live-state traversal for regular-expression derivatives.
+
+--*/
+#pragma once
+
+#include "ast/rewriter/seq_derive.h"
+#include "ast/ast.h"
+
+class seq_rewriter;
+
+namespace seq {
+
+    class live_states {
+        struct search;
+        struct imp;
+
+    public:
+        enum class failure {
+            none,
+            state_cap,
+            resource
+        };
+
+        class iterator {
+            live_states* m_owner = nullptr;
+            search* m_search = nullptr;
+            unsigned m_index = 0;
+            bool m_end = false;
+
+        public:
+            iterator(live_states* owner, search* s, unsigned index, bool end) :
+                m_owner(owner), m_search(s), m_index(index), m_end(end) {}
+            expr* operator*() const;
+            iterator& operator++();
+            bool operator!=(iterator const& other) const;
+        };
+
+        class reachable {
+            live_states* m_owner = nullptr;
+            search* m_search = nullptr;
+
+        public:
+            reachable(live_states* owner, search* s) :
+                m_owner(owner), m_search(s) {}
+            iterator begin() const;
+            iterator end() const;
+            bool failed() const;
+            failure failure_reason() const;
+            bool is_dead();
+        };
+
+    private:
+        imp* m_imp;
+
+        bool ensure(search* s, unsigned index);
+        expr* get_live(search* s, unsigned index) const;
+        failure get_failure(search* s) const;
+
+    public:
+        live_states(seq_rewriter& rw,
+                    transition_mode mode = transition_mode::brzozowski_tm,
+                    unsigned max_states = UINT_MAX);
+        ~live_states();
+        live_states(live_states const&) = delete;
+        live_states& operator=(live_states const&) = delete;
+
+        reachable reachable_live(expr* r);
+        bool contains(expr* r) const;
+        unsigned state_id(expr* r);
+        void reset();
+    };
+}

src/smt/seq_regex.cpp

@@ -31,8 +31,7 @@ namespace smt {
         ctx(th.get_context()),
         m(th.get_manager()),
         m_monadic(seq_rw(), ctx.get_trail_stack()),
-        m_state_to_expr(m),
-        m_state_graph(state_graph::state_pp(this, pp_state)) { 
+        m_live_states(seq_rw(), seq::transition_mode::brzozowski_tm, 10000) {
         m_monadic.set_is_var([&th](expr *e) { return th.is_var(e); });
     }
 
@@ -640,8 +639,8 @@ namespace smt {
         }
 
         if (info.interpreted) {
-            update_state_graph(r);            
-            if (m_state_graph.is_dead(get_state_id(r))) {
+            auto live = m_live_states.reachable_live(r);
+            if (live.is_dead()) {
                 STRACE(seq_regex_brief, tout << "(dead) ";);
                 th.add_axiom(~lit);
                 return true;
@@ -665,8 +664,7 @@ namespace smt {
     /**
      * Propagate the atom (accept s i r)
      *
-     * Propagation triggers updating the state graph for dead state detection:
-     * (accept s i r) => update_state_graph(r)
+     * Propagation triggers derivative reachability for dead state detection:
      * (accept s i r) & dead(r) => false
      *
      * Propagation is also blocked under certain conditions to throttle
@@ -1292,101 +1290,10 @@ namespace smt {
         return sk().mk("re.first", n, a().mk_int(r->get_id()), elem_sort);
     }
 
-    /**
-     * Dead state elimination using the state_graph class
-     */
-
-    unsigned seq_regex::get_state_id(expr* e) {
-        // Assign increasing IDs starting from 1
-        if (!m_expr_to_state.contains(e)) {
-            m_state_to_expr.push_back(e);
-            unsigned new_id = m_state_to_expr.size();
-            m_expr_to_state.insert(e, new_id);
-            STRACE(seq_regex_brief, tout << "new(" << expr_id_str(e)
-                                           << ")=" << state_str(e) << " ";);
-            STRACE(seq_regex, tout
-                << "New state ID: " << new_id
-                << " = " << mk_pp(e, m) << std::endl;);
-            SASSERT(get_expr_from_id(new_id) == e);
-        }
-        return m_expr_to_state.find(e);
-    }
-    expr* seq_regex::get_expr_from_id(unsigned id) {
-        SASSERT(id >= 1);
-        SASSERT(id <= m_state_to_expr.size());
-        return m_state_to_expr.get(id - 1);
-    }
-
-    bool seq_regex::can_be_in_cycle(expr *r1, expr *r2) {
-        // TBD: This can be used to optimize the state graph:
-        // return false here if it is known that r1 -> r2 can never be
-        // in a cycle. There are various easy syntactic checks on r1 and r2
-        // that can be used to infer this (e.g. star height, or length if
-        // both are star-free).
-        // This check need not be sound, but if it is not, some dead states
-        // will be missed.
-        return true;
-    }
-
-    /*
-        Update the state graph with expression r and all its derivatives.
-    */
-    bool seq_regex::update_state_graph(expr* r) {
-        unsigned r_id = get_state_id(r);
-        if (m_state_graph.is_done(r_id)) return false;
-        if (m_state_graph.get_size() >= m_max_state_graph_size) {
-            STRACE(seq_regex, tout << "Warning: ignored state graph update -- max size of seen states reached!" << std::endl;);
-            STRACE(seq_regex_brief, tout << "(MAX SIZE REACHED) ";);
-            return false;
-        }
-        STRACE(seq_regex, tout << "Updating state graph for regex "
-                                 << mk_pp(r, m) << ") ";);
-        
-        STRACE(state_graph,
-            if (!m_state_graph.is_seen(r_id))
-                tout << std::endl << "state(" << r_id << ") = " << re().to_str(r) << std::endl << "info(" << r_id << ") = " << re().get_info(r) << std::endl;);
-        // Add state
-        m_state_graph.add_state(r_id);
-        STRACE(seq_regex, tout << "Updating state graph for regex "
-                                 << mk_pp(r, m) << ") " << std::endl;);
-        STRACE(seq_regex_brief, tout << std::endl << "USG("
-                                       << state_str(r) << ") ";);
-        expr_ref r_nullable = is_nullable_wrapper(r);
-        if (m.is_true(r_nullable)) {
-            m_state_graph.mark_live(r_id);
-        }
-        else {
-            // Add edges to all derivatives
-            expr_ref_vector derivatives(m);
-            STRACE(seq_regex_verbose, tout
-                << "getting all derivs: " << r_id << " " << std::endl;);
-            get_derivative_targets(r, derivatives);
-            for (auto const& dr: derivatives) {
-                unsigned dr_id = get_state_id(dr);
-                STRACE(seq_regex_verbose, tout
-                    << std::endl << "  traversing deriv: " << dr_id << " ";);              
-                STRACE(state_graph,
-                    if (!m_state_graph.is_seen(dr_id))
-                        tout << "state(" << dr_id << ") = " << re().to_str(dr) << std::endl << "info(" << dr_id << ") = " << re().get_info(dr) << std::endl;);
-                // Add state
-                m_state_graph.add_state(dr_id);
-                bool maybecycle = can_be_in_cycle(r, dr);
-                m_state_graph.add_edge(r_id, dr_id, maybecycle);
-            }
-            m_state_graph.mark_done(r_id);
-        }
-
-        STRACE(seq_regex, m_state_graph.display(tout););
-        STRACE(seq_regex_brief, tout << std::endl;);
-        STRACE(seq_regex_brief, m_state_graph.display(tout););
-        return true;
-    }
-
     std::string seq_regex::state_str(expr* e) {
-        if (m_expr_to_state.contains(e))
-            return std::to_string(get_state_id(e));
-        else
-            return expr_id_str(e);
+        if (m_live_states.contains(e))
+            return std::to_string(m_live_states.state_id(e));
+        return expr_id_str(e);
     }
     std::string seq_regex::expr_id_str(expr* e) {
         return std::string("id") + std::to_string(e->get_id());

src/smt/seq_regex.h

@@ -17,9 +17,9 @@ Author:
 #pragma once
 
 #include "util/scoped_vector.h"
-#include "util/state_graph.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/seq_monadic.h"
+#include "ast/rewriter/seq_regex_live.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/seq_skolem.h"
 #include "smt/smt_context.h"
@@ -56,13 +56,6 @@ Author:
                     (next states)
                 d(r1)=r2: r2 is the derivative of r1
                 n(r1)=b:  b = whether r1 is nullable or not
-                USG(r):   updating state graph for regex r (add all derivatives)
-
-        -tr:state_graph
-        This is the tracing done by util/state_graph, the data structure
-        that seq_regex uses to track live and dead regexes, which can
-        altneratively be used to get a high-level picture of what states
-        are being explored and updated as the solver progresses.
 
         -tr:seq_regex_verbose
         Used for some more frequent tracing (in the style of seq_regex,
@@ -72,21 +65,12 @@ Author:
         These are the underlying sequence theory tracing, often used by
         the rewriter.
 
-        DEBUGGING AND VIEWING STATE GRAPH GRAPHICAL OUTPUT
+        DEBUGGING
 
         -dbg:seq_regex
         Debugging that checks invariants. Currently, checks that derivative
         normal form is correctly preserved in the rewriter.
 
-        -dbg:state_graph
-        Debugging for the state graph, which
-        1. Checks state graph invariants, and
-        2. Generates the files .z3-state-graph.dgml and .z3-state-graph.dot
-           which can be used to visually view the state graph being explored,
-           during or after executing Z3.
-           The output can be viewed:
-              - Using Visual Studio for .dgml
-              - Using a tool such as xdot (`xdot .z3-state-graph.dot`) for .dot
 */
 
 namespace smt {
@@ -163,23 +147,9 @@ namespace smt {
         unsigned                          m_monadic_assumption_generation = UINT_MAX;
         unsigned                          m_monadic_fallback_generation = UINT_MAX;
 
-        /*
-            state_graph for dead state detection, and associated methods
-        */
-        ptr_addr_map<expr, unsigned>   m_expr_to_state;
-        expr_ref_vector                m_state_to_expr;
-        state_graph                    m_state_graph;
+        seq::live_states               m_live_states;
         /* map from uninterpreted regex constants to assigned regex expressions by EQ */
         // expr_map                       m_const_to_expr;
-        unsigned                       m_max_state_graph_size { 10000 };
-        // Convert between expressions and states (IDs)
-        unsigned get_state_id(expr* e);
-        expr* get_expr_from_id(unsigned id);
-        // Cycle-detection heuristic
-        // Note: Doesn't need to be sound or complete (doesn't affect soundness)
-        bool can_be_in_cycle(expr* r1, expr* r2);
-        // Update the graph
-        bool update_state_graph(expr* r);
 
         // Printing expressions for seq_regex_brief
         std::string state_str(expr* e);
@@ -239,17 +209,6 @@ namespace smt {
            seq_regex_ptr must be a pointer to seq_regex and the 
            id must be a valid state id or else nothing is printed. 
         */
-        static void pp_state(void* seq_regex_ptr, std::ostream& out, unsigned id, bool html_encode) {
-            seq_regex* sr = (seq_regex*)seq_regex_ptr;
-            if (sr) {
-                seq_util::rex re_util(sr->re());
-                if (1 <= id && id <= sr->m_state_to_expr.size()) {
-                    expr* r = sr->get_expr_from_id(id);
-                    seq_util::rex::pp(re_util, r, html_encode).display(out);
-                }
-            }
-        }
-
         bool block_if_empty(expr* r, literal lit);
         void add_monadic_membership(literal lit, expr* s, expr* r);
         // Expand a term through theory_seq's solution map, but substitute a sub-term only