From 2441ae2f3097e386c70bc636287b5f3d27f5d5ad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Aug 2026 10:11:15 -0700 Subject: [PATCH] Update seq_monadic.cpp --- src/ast/rewriter/seq_monadic.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index ecd1903997..2dc65ebaaf 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -40,6 +40,11 @@ TODOs: explored and we can check the variable intersection membership constraints if the new expansion is feasible. Constant characters are consumed at the same time to also prune the choice. +- separate out "live-state" and enumerator over reachable live states: + - make it share live states between callers. + - make it expose an iterator instead of using vectors of live states to allow on-demand expansion of live states. + - make use of DFS exploration of derivatives to extract live states without visiting all states up front. + - use it in seq_regex legacy mode that also has this notion.