seq_monadic: self-contained monadic-decomposition regex membership solver (generic elements, witnesses, Boolean combinations) (#10296)

## Summary

Adds `seq_monadic` (`src/ast/rewriter/seq_monadic.{h,cpp}`), a
self-contained,
rewriter-level decision procedure for regex membership of a term that is
a
concatenation of sequence variables and constant elements — e.g. `x·a·x
∈ R`,
including repeated and multiple variables. It uses a whole-language
*monadic
decomposition* plus automaton product-reachability; it is minterm-free
and does
**not** use Nielsen word-equation splitting or `seq_split`.

The component is **purely additive**: it is not wired into any solver
path, so
default behavior is unchanged. It ships with a unit test and an opt-in
benchmark
harness that is inert unless `Z3_SEQ_BENCH_DIR` is set.

## What it does

- `x·u ∈ R  ⇔  ⋁_q ( x reaches q in A_R  ∧  u ∈ q )` over the derivative
  automaton; `reach(q)` is never materialized as a regex (avoids the
state-elimination blowup). A variable's constraint is decided by a lazy
product-reachability search over tuples of derivative states, with
transitions
= the product of `brz_derivative_cofactors` branches and
pairwise-conjoined
  `seq::range_predicate` guards.
- **Generic in the element sort**: characters use the exact
`range_predicate`
algebra; any other element sort uses a candidate-basis over the element
values
the guards mention (sound and complete for the
`{true,false,=,<=,and,or,not}`
  guard grammar the derivatives emit).
- **Concrete witnesses**: on sat it reconstructs a witness value (a
sequence of
concrete elements, not predicates) per variable from the accepting
product path.
- **Boolean combinations**: `solve_and` decides a conjunction of
memberships
jointly, so a variable shared across memberships is constrained
consistently.
This is the natural extension since `¬(t∈R) ≡ t∈~R`, `∨` = union of
DNFs, and
  `∧` = product of DNFs.

Also de-duplicates the char-guard → `range_predicate` translator into a
single
public `seq::guard_to_range_predicate` in `seq_range_collapse` (it was
previously
duplicated there and in `seq_monadic`).

## Testing

- `tst_seq_monadic`: single / multiple / repeated variables, nested
complement,
bounded loops, per-variable constraints, a generic `(Seq Int)` section,
witness
  verification (substitute the model back and re-decide membership), and
  `solve_and` cases that are individually sat but jointly unsat.
- Full unit suite `test-z3 /a` passes (93/93).

## Evaluation (offline harness, not part of CI)

On a regex-membership benchmark corpus, restricted to files carrying a
genuine
`(set-info :status)`, the solver decides 318 and 316 are correct
(99.4%); the
only 2 disagreements are a length limitation (`|x|=2k`) that is outside
the
membership fragment.

## Known limitations / follow-ups

- Pathological deeply-nested, high-multiplicity regexes can overflow the
recursive derivative stack; a recursion-depth guard to degrade to
`unknown` is
  a natural follow-up.
- Out-of-fragment constraints (word equations, length / Parikh) are not
handled,
  by design — this decides regex membership only.

---------

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: 916db256-43c6-4067-b6f4-fa8d2cf2f37f

src/test/CMakeLists.txt

@@ -24,7 +24,6 @@ add_executable(test-z3
   api_datalog.cpp
   parametric_datatype.cpp
   arith_rewriter.cpp
-  seq_rewriter.cpp
   arith_simplifier_plugin.cpp
   ast.cpp
   bdd.cpp
@@ -132,6 +131,8 @@ add_executable(test-z3
   sat_user_scope.cpp
   scoped_timer.cpp
   scoped_vector.cpp
+  seq_rewriter.cpp
+  seq_monadic.cpp
   simple_parser.cpp
   scanner_io.cpp
   simplex.cpp

src/test/main.cpp

@@ -116,6 +116,7 @@
     X(range_predicate) \
     X(regex_range_collapse) \
     X(seq_rewriter) \
+    X(seq_monadic) \
     X(check_assumptions) \
     X(smt_context) \
     X(theory_dl) \

src/test/seq_monadic.cpp

@@ -0,0 +1,314 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    seq_monadic.cpp
+
+Abstract:
+
+    Unit tests for the whole-language monadic-decomposition membership solver in
+    ast/rewriter/seq_monadic.cpp.  Mirrors the validated Python prototype
+    (files/solve_proto.py): single-variable repeated-membership shapes  x.a.x in R.
+
+Author:
+
+    Nikolaj Bjorner / Margus Veanes 2026
+
+--*/
+
+#include "ast/ast.h"
+#include "ast/reg_decl_plugins.h"
+#include "ast/seq_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/rewriter/seq_rewriter.h"
+#include "ast/rewriter/seq_monadic.h"
+#include "ast/rewriter/expr_safe_replace.h"
+#include <iostream>
+
+namespace {
+
+struct plugin_registrar {
+    plugin_registrar(ast_manager& m) { reg_decl_plugins(m); }
+};
+
+class seq_monadic_test {
+    ast_manager      m;
+    plugin_registrar m_reg;
+    seq_rewriter     m_rw;
+    seq_monadic      m_mon;
+    seq_util         u;
+    sort_ref         m_str;   // String sort
+    sort_ref         m_re;    // RegEx sort over m_str
+    unsigned         m_fail = 0;
+
+    seq_util::rex& re() { return u.re; }
+
+    // regex builders
+    expr_ref word(char const* s) { return expr_ref(re().mk_to_re(u.str.mk_string(zstring(s))), m); }
+    expr_ref cat(expr* a, expr* b) { return expr_ref(re().mk_concat(a, b), m); }
+    expr_ref alt(expr* a, expr* b) { return expr_ref(re().mk_union(a, b), m); }
+    expr_ref star(expr* a) { return expr_ref(re().mk_star(a), m); }
+    expr_ref inter(expr* a, expr* b) { return expr_ref(re().mk_inter(a, b), m); }
+    expr_ref comp(expr* a) { return expr_ref(re().mk_complement(a), m); }
+    expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); }
+    expr_ref rng(char lo, char hi) {
+        char sl[2] = { lo, 0 }, sh[2] = { hi, 0 };
+        return expr_ref(re().mk_range(u.str.mk_string(zstring(sl)), u.str.mk_string(zstring(sh))), m);
+    }
+    expr_ref loop(expr* r, unsigned lo, unsigned hi) { return expr_ref(re().mk_loop(r, lo, hi), m); }
+
+    // string-term builders
+    expr_ref var(char const* nm) { return expr_ref(m.mk_const(nm, m_str), m); }
+    expr_ref sword(char const* s) { return expr_ref(u.str.mk_string(zstring(s)), m); }
+    expr_ref sconcat(expr* a, expr* b) { return expr_ref(u.str.mk_concat(a, b), m); }
+    // term  x . w . x  (w a constant word)
+    expr_ref xwx(expr* x, char const* w) { return sconcat(x, sconcat(sword(w), x)); }
+    // term  x . a . y  (two distinct variables)
+    expr_ref xay(expr* x, expr* y) { return sconcat(x, sconcat(sword("a"), y)); }
+    // term  x . y . x
+    expr_ref xyx(expr* x, expr* y) { return sconcat(x, sconcat(y, x)); }
+
+    static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; }
+
+    void check(char const* name, expr* term, expr* R, lbool expected) {
+        lbool got = m_mon.solve(term, R);
+        bool ok = (got == expected);
+        if (!ok) ++m_fail;
+        std::cout << (ok ? "  OK   " : "  FAIL ") << name
+                  << "  got=" << s(got) << " expected=" << s(expected) << "\n";
+    }
+
+    void check_extra(char const* name, expr* term, expr* R,
+                     obj_map<expr, expr*> const& ve, lbool expected) {
+        lbool got = m_mon.solve(term, R, ve);
+        bool ok = (got == expected);
+        if (!ok) ++m_fail;
+        std::cout << (ok ? "  OK   " : "  FAIL ") << name
+                  << "  got=" << s(got) << " expected=" << s(expected) << "\n";
+    }
+
+    // flatten a ground sequence term into its element values.
+    void flatten_seq(expr* seqv, ptr_vector<expr>& elems) {
+        zstring zs;
+        if (u.str.is_concat(seqv)) {
+            for (expr* arg : *to_app(seqv)) flatten_seq(arg, elems);
+            return;
+        }
+        if (u.str.is_empty(seqv))
+            return;
+        if (u.str.is_string(seqv, zs)) {
+            for (unsigned i = 0; i < zs.length(); ++i) elems.push_back(u.str.mk_char(zs, i));
+            return;
+        }
+        if (u.str.is_unit(seqv))
+            elems.push_back(to_app(seqv)->get_arg(0));
+    }
+
+    // decide membership of a concrete word (list of element values) in R by folding
+    // derivatives and testing nullability of the residual.
+    bool word_in_re(ptr_vector<expr> const& elems, expr* R) {
+        expr_ref cur(R, m);
+        for (expr* e : elems) cur = m_rw.mk_derivative(e, cur);
+        return m.is_true(m_rw.is_nullable(cur));
+    }
+
+    // solve for a model, then check the returned witness assignment actually makes
+    // term a member of R (substitute var -> witness and re-decide by derivatives).
+    void check_witness(char const* name, expr* term, expr* R,
+                       obj_map<expr, expr*> const& ve) {
+        obj_map<expr, expr*> model;
+        lbool got = m_mon.solve(term, R, ve, &model);
+        bool ok = (got == l_true) && !model.empty();
+        if (ok) {
+            expr_safe_replace rep(m);
+            for (auto const& kv : model) rep.insert(kv.m_key, kv.m_value);
+            expr_ref g(m);
+            rep(term, g);
+            ptr_vector<expr> elems;
+            flatten_seq(g, elems);
+            ok = word_in_re(elems, R);
+        }
+        if (!ok) ++m_fail;
+        std::cout << (ok ? "  OK   " : "  FAIL ") << name
+                  << "  solve=" << s(got) << " witness-verified=" << (ok ? "yes" : "no") << "\n";
+    }
+
+    // decide a conjunction of memberships jointly (shared variables constrained together).
+    void check_and(char const* name, vector<std::pair<expr*, expr*>> const& mems, lbool expected) {
+        obj_map<expr, expr*> nove;
+        lbool got = m_mon.solve_and(mems, nove, nullptr);
+        bool ok = (got == expected);
+        if (!ok) ++m_fail;
+        std::cout << (ok ? "  OK   " : "  FAIL ") << name
+                  << "  got=" << s(got) << " expected=" << s(expected) << "\n";
+    }
+
+public:
+    seq_monadic_test() : m_reg(m), m_rw(m), m_mon(m_rw), u(m), m_str(m), m_re(m) {
+        m_str = u.str.mk_string_sort();
+        m_re  = re().mk_re(m_str);
+    }
+
+    void run() {
+        expr_ref x  = var("x");
+        expr_ref a  = word("a");
+        expr_ref b  = word("b");
+        expr_ref ab = cat(a, b);
+        expr_ref sig = dotstar();                                   // Sigma*
+        expr_ref saas = cat(sig, cat(cat(a, a), sig));              // Sigma* a a Sigma*
+        expr_ref sbbs = cat(sig, cat(cat(b, b), sig));              // Sigma* b b Sigma*
+
+        std::cout << "=== seq_monadic: single-variable membership (x.a.x in R) ===\n";
+
+        // sanity
+        check("(a|b)*        x.a.x", xwx(x, "a"), star(alt(a, b)), l_true);
+        check("b*            x.a.x", xwx(x, "a"), star(b), l_false);
+        check("Sig*aaSig*    x.a.x", xwx(x, "a"), saas, l_true);
+        check("x in (a|b)*        ", x, star(alt(a, b)), l_true);
+        check("x in b* (x=aa)     ", xwx(x, "a"), star(b), l_false);
+
+        // ALT = (a|b)* & ~(Sig*aaSig*) & ~(Sig*bbSig*)  (strictly alternating)
+        expr_ref altre = inter(star(alt(a, b)), inter(comp(saas), comp(sbbs)));
+        check("ALT           x.a.x", xwx(x, "a"), altre, l_true);
+
+        // R*.S complement family
+        check("~(a*.b)       x.a.x", xwx(x, "a"), comp(cat(star(a), b)), l_true);
+
+        // L3-02 ~((ab)*.~((ab)*))   -> unsat (odd length)
+        check("L3-02         x.a.x", xwx(x, "a"),
+              comp(cat(star(ab), comp(star(ab)))), l_false);
+
+        // L3-03 ~(a*.~(b*.~((ab)*)))  -> sat
+        check("L3-03         x.a.x", xwx(x, "a"),
+              comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))), l_true);
+
+        std::cout << "=== seq_monadic: multi-variable ===\n";
+        expr_ref y = var("y");
+        check("(a|b)*        x.a.y", xay(x, y), star(alt(a, b)), l_true);
+        check("b*            x.a.y", xay(x, y), star(b), l_false);
+        check("L3-02         x.a.y", xay(x, y), comp(cat(star(ab), comp(star(ab)))), l_true);
+        check("L3-03         x.a.y", xay(x, y),
+              comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))), l_true);
+        check("empty ~Sig*   x.y.x", xyx(x, y), comp(dotstar()), l_false);
+        check("Sig*          x.y.x", xyx(x, y), dotstar(), l_true);
+        check("(a|b)*        x.y.x", xyx(x, y), star(alt(a, b)), l_true);
+
+        std::cout << "=== seq_monadic: per-variable constraints ===\n";
+        expr_ref digitp = cat(rng('0', '9'), star(rng('0', '9')));   // [0-9]+
+        obj_map<expr, expr*> ve;
+        ve.insert(y, digitp);
+        // y must be in the (a|b)* tail AND in [0-9]+  -> empty -> unsat
+        check_extra("(a|b)* & y in[0-9]+ x.a.y", xay(x, y), star(alt(a, b)), ve, l_false);
+        // y any digits, x/'a' anything -> sat
+        check_extra("Sig*   & y in[0-9]+ x.a.y", xay(x, y), dotstar(), ve, l_true);
+
+        // Bounded loop (re.loop) with repeated variable -- exercises live_states on a
+        // counted automaton (t04-exact benchmark family).  Regression for a
+        // reference-invalidation bug in live_states (succ[i].push_back(intern(t))).
+        std::cout << "=== seq_monadic: bounded loop (t04-exact family) ===\n";
+        expr_ref clsr    = rng('0', '9');                            // [0-9]
+        expr_ref digitS  = star(clsr);                               // [0-9]*
+        expr_ref loop22  = loop(clsr, 2, 2);                         // [0-9]{2}
+        check("[0-9]{2}      x    ", x, loop22, l_true);             // x = "00"
+        check("[0-9]{2}      x.a.x", xwx(x, "a"), loop22, l_false);  // 'a' not a digit
+        obj_map<expr, expr*> ve2; ve2.insert(x, digitp); ve2.insert(y, digitS);
+        // x.y.x in [0-9]{2}, x in [0-9]+, y in [0-9]*  -> sat (x="0", y="")
+        check_extra("[0-9]{2} & x[0-9]+ y[0-9]* x.y.x", xyx(x, y), loop22, ve2, l_true);
+        obj_map<expr, expr*> ve3; ve3.insert(x, digitp);
+        check_extra("[0-9]{2} & x[0-9]+       x.y.x", xyx(x, y), loop22, ve3, l_true);
+        obj_map<expr, expr*> ve4; ve4.insert(x, digitp);
+        // x.y.x in [0-9]{3}, x in [0-9]+ -> sat (x=1 digit, y=1 digit)
+        check_extra("[0-9]{3} & x[0-9]+       x.y.x", xyx(x, y), loop(clsr, 3, 3), ve4, l_true);
+
+        // ---- witness extraction: a produced witness must be a concrete SEQUENCE of
+        // ---- elements that actually satisfies the membership (not a predicate).
+        std::cout << "=== seq_monadic: witness extraction (char) ===\n";
+        obj_map<expr, expr*> nove;
+        check_witness("(a|b)*        x.a.x", xwx(x, "a"), star(alt(a, b)), nove);
+        check_witness("Sig*aaSig*    x.a.x", xwx(x, "a"), saas, nove);      // forces nonempty x
+        check_witness("~(a*.b)       x.a.x", xwx(x, "a"), comp(cat(star(a), b)), nove);
+        check_witness("L3-03         x.a.x", xwx(x, "a"),
+                      comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))), nove);
+        check_witness("(a|b)*        x.a.y", xay(x, y), star(alt(a, b)), nove);
+        check_witness("Sig*          x.y.x", xyx(x, y), dotstar(), nove);
+        check_witness("Sig* & y[0-9]+ x.a.y", xay(x, y), dotstar(), ve);    // ve: y in [0-9]+
+        check_witness("[0-9]{2}&x[0-9]+ y[0-9]* x.y.x", xyx(x, y), loop22, ve2);
+
+        // ---- generic element sort: sequences of Int exercise the non-character guard
+        // ---- algebra (candidate-basis emptiness + witness), not seq::range_predicate.
+        std::cout << "=== seq_monadic: generic element sort (Seq Int) ===\n";
+        arith_util ar(m);
+        sort_ref intS(ar.mk_int(), m);
+        sort_ref seqI(u.str.mk_seq(intS), m);
+        sort_ref reI(u.re.mk_re(seqI), m);
+        expr_ref i1(ar.mk_numeral(rational(1), true), m);
+        expr_ref i2(ar.mk_numeral(rational(2), true), m);
+        expr_ref one_seq(u.str.mk_unit(i1), m);                 // [1] : (Seq Int)
+        expr_ref re1(re().mk_to_re(u.str.mk_unit(i1)), m);      // matches [1]
+        expr_ref re2(re().mk_to_re(u.str.mk_unit(i2)), m);      // matches [2]
+        expr_ref re12s(star(alt(re1, re2)), m);                 // ([1]|[2])*
+        expr_ref re2s(star(re2), m);                            // [2]*
+        expr_ref xi(m.mk_const("xi", seqI), m);
+        expr_ref yi(m.mk_const("yi", seqI), m);
+        expr_ref xi1xi(sconcat(xi, sconcat(one_seq, xi)), m);   // xi.[1].xi
+        expr_ref xiyi(sconcat(xi, sconcat(one_seq, yi)), m);    // xi.[1].yi
+        obj_map<expr, expr*> nove2;
+        check("([1]|[2])*   xi.[1].xi", xi1xi, re12s, l_true);
+        check("[2]*         xi.[1].xi", xi1xi, re2s,  l_false); // the middle [1] is not in [2]*
+        check("([1]|[2])*   xi        ", xi, re12s, l_true);
+        check("([1]|[2])*   xi.[1].yi", xiyi, re12s, l_true);
+        check_witness("([1]|[2])* xi.[1].xi", xi1xi, re12s, nove2);
+        check_witness("([1]|[2])* xi       ", xi, re12s, nove2);
+        check_witness("([1]|[2])* xi.[1].yi", xiyi, re12s, nove2);
+        // per-variable extra constraint over (Seq Int): yi must also be in [2]*
+        obj_map<expr, expr*> veI; veI.insert(yi, re2s.get());
+        check_extra("([1]|[2])* & yi[2]* xi.[1].yi", xiyi, re12s, veI, l_true);
+        check_witness("([1]|[2])* & yi[2]* xi.[1].yi", xiyi, re12s, veI);
+
+        // ---- conjunction of memberships (solve_and): a variable shared across memberships
+        // ---- is constrained jointly.  These are cases that are individually SAT but
+        // ---- jointly UNSAT -- exactly what independent per-membership solving gets wrong.
+        std::cout << "=== seq_monadic: conjunction of memberships (solve_and) ===\n";
+        expr_ref aaS(star(cat(a, a)), m);           // (aa)*     : even number of a's
+        expr_ref a_aaS(cat(a, star(cat(a, a))), m); // a(aa)*    : odd number of a's
+        expr_ref abS(star(ab), m);                  // (ab)*
+        expr_ref sig2(dotstar(), m);                // Sigma*
+        // x in (aa)* /\ x in a(aa)*  : even-and-odd length of a's -> unsat (each alone sat)
+        vector<std::pair<expr*, expr*>> mUnsat1;
+        mUnsat1.push_back(std::make_pair((expr*)x.get(), (expr*)aaS.get()));
+        mUnsat1.push_back(std::make_pair((expr*)x.get(), (expr*)a_aaS.get()));
+        check_and("x in (aa)* & x in a(aa)*", mUnsat1, l_false);
+        // compound terms sharing x: x.a in (aa)* (x odd) /\ x.aa in (aa)* (x even) -> unsat
+        expr_ref tXa(sconcat(x, sword("a")), m);
+        expr_ref tXaa(sconcat(x, sword("aa")), m);
+        vector<std::pair<expr*, expr*>> mUnsat2;
+        mUnsat2.push_back(std::make_pair((expr*)tXa.get(),  (expr*)aaS.get()));
+        mUnsat2.push_back(std::make_pair((expr*)tXaa.get(), (expr*)aaS.get()));
+        check_and("x.a in (aa)* & x.aa in (aa)*", mUnsat2, l_false);
+        // consistent conjunction: x in (ab)* /\ x in Sigma*  -> sat (x=eps or ab)
+        vector<std::pair<expr*, expr*>> mSat;
+        mSat.push_back(std::make_pair((expr*)x.get(), (expr*)abS.get()));
+        mSat.push_back(std::make_pair((expr*)x.get(), (expr*)sig2.get()));
+        check_and("x in (ab)* & x in Sigma*", mSat, l_true);
+        // two variables, two memberships: x.a.y in (a|b)* /\ y.b.x in (a|b)* -> sat
+        expr_ref tXaY(xay(x, y), m);
+        expr_ref tYbX(sconcat(y, sconcat(sword("b"), x)), m);
+        expr_ref abStar(star(alt(a, b)), m);
+        vector<std::pair<expr*, expr*>> mSat2;
+        mSat2.push_back(std::make_pair((expr*)tXaY.get(), (expr*)abStar.get()));
+        mSat2.push_back(std::make_pair((expr*)tYbX.get(), (expr*)abStar.get()));
+        check_and("x.a.y & y.b.x in (a|b)*", mSat2, l_true);
+
+        std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " ("
+                  << m_fail << " fail) ===\n";
+        ENSURE(m_fail == 0);
+    }
+};
+
+}
+
+void tst_seq_monadic() {
+    seq_monadic_test t;
+    t.run();
+}