From 568218e1ed59ecdc5cc709939249d3258d6800c7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Jul 2026 13:59:27 -0700 Subject: [PATCH] add notes Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_monadic.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 1ecd0c5180..18418e7d50 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -23,6 +23,8 @@ TODOs: - if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead) - create a validation harness: expose certificates for correctness that can be checked. - extend with lower and upper bound constraints +- cache calls to cofactors so they are only computed once per regex. +- consider using expr_ref as alternative to pinned expressions - encapsulate within general interface: create: undo_trail x dependency_manager x ast_manager -> regex_membership add_constraint : expr* x expr* x dependency* -> void