z3-src 503.3.0

/*++
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/rewriter_types.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/seq/seq_monadic.h"
#include "ast/seq/seq_view_witness.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "cmd_context/cmd_context.h"
#include "parsers/smt2/smt2parser.h"
#include "params/smt_params.h"
#include "smt/smt_kernel.h"
#include "solver/solver.h"
#include "util/rlimit.h"
#include <iostream>
#include <sstream>
#include <set>
#include <tuple>
#include <algorithm>
#include <string>

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;
    trail_stack      m_trail;
    seq::monadic     m_mon;
    seq_util         u;
    sort_ref         m_str;   // String sort
    sort_ref         m_re;    // RegEx sort over m_str
    seq::transition_mode m_mode;
    u_dependency_manager m_dm;   // owns the leaf dependencies used in unsat-core tests
    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 dot() { return expr_ref(re().mk_full_char(m_re), 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 };
        expr_ref lhs(u.str.mk_string(zstring(sl)), m);
        expr_ref rhs(u.str.mk_string(zstring(sh)), m);
        return expr_ref(re().mk_range(lhs, rhs), 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"; }
    char const* mode_name() const {
        switch (m_mode) {
        case seq::transition_mode::brzozowski_tm: return "brz";
        case seq::transition_mode::light_antimirov_tm: return "light-ant";
        }
        UNREACHABLE();
        return "";
    }

    bool eval_guard(expr* guard, unsigned ch) {
        sort* elem_sort = nullptr;
        VERIFY(u.is_seq(m_str, elem_sort));
        expr_ref v0(m.mk_var(0, elem_sort), m);
        expr_safe_replace rep(m);
        rep.insert(v0, u.str.mk_char(ch));
        expr_ref instantiated(m), simplified(m);
        rep(guard, instantiated);
        th_rewriter rw(m);
        rw(instantiated, simplified);
        return m.is_true(simplified);
    }

    void check_ant_cofactors() {
        expr_ref a = word("a");
        expr_ref any = dotstar();
        expr_ref dot3 = loop(dot(), 3, 3);
        expr_ref R = cat(any, cat(a, dot3));
        expr_ref_pair_vector cof(m);
        m_rw.light_ant_derivative_cofactors(R, cof);

        bool found_R = false, found_dot3 = false, ok = cof.size() == 2;
        for (auto const& [guard, target] : cof) {
            if (target == R) {
                found_R = eval_guard(guard, 'a') && eval_guard(guard, 'b');
            }

            else if (target == dot3) {
                found_dot3 = eval_guard(guard, 'a') && !eval_guard(guard, 'b');
            }
            else {
                ok = false;
            }
        }
        ok = ok && found_R && found_dot3;
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ")
                  << mode_name() << " cofactor construction\n";
    }

    void check_view_witness() {
        std::cout << "=== seq_view_witness: incremental product checking ===\n";
        expr_ref x = var("view-x");
        expr_ref aa = word("aa");
        expr_ref a = word("a");
        expr_ref even = star(aa);
        expr_ref odd = cat(a, even);
        unsigned dep_even = 0, dep_odd = 1;
        seq::live_states live(m_rw, m_mode, 1u << 12);
        seq::view_witness witness(m_trail, m_rw, live, m_mode);

        m_trail.push_scope();
        witness.add(x, seq::view::membership(even, m), &dep_even);
        lbool first = witness.check();
        unsigned calls = witness.cofactor_calls();
        lbool repeated = witness.check();
        bool cached = first == l_true && repeated == l_true &&
                      calls == witness.cofactor_calls();

        m_trail.push_scope();
        witness.add(x, seq::view::membership(odd, m), &dep_odd);
        lbool conflict = witness.check();
        ptr_vector<void> core = witness.core();
        bool core_ok = conflict == l_false && core.contains(&dep_even) &&
                       core.contains(&dep_odd) && core.size() == 2;
        m_trail.pop_scope(1);

        witness.set_enable_witness(true);
        lbool after_pop = witness.check();
        expr_ref value = witness.materialize_witness(x);
        bool materialized = after_pop == l_true && value;
        m_trail.pop_scope(1);

        witness.set_checkpoint([]() { return seq::view_failure_reason::budget; });
        m_trail.push_scope();
        witness.add(x, seq::view::membership(odd, m), nullptr);
        lbool undef = witness.check();
        bool reason_ok = undef == l_undef &&
                         witness.get_failure_reason() == seq::view_failure_reason::budget;
        m_trail.pop_scope(1);

        bool ok = cached && core_ok && materialized && reason_ok;
        if (!ok)
            ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ")
                  << "cache, trail, core, and witness\n";
    }

    void check(char const* name, expr* term, expr* R, lbool expected) {
        m_mon.set_gen_solution(false);               // this check does not use the model
        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_deep_concat() {
        expr_ref empty = sword("");
        expr_ref left = sword("a"), right = sword("b");
        expr_ref x = var("deep-x");
        for (unsigned i = 0; i < 40000; ++i) {
            left = sconcat(left, empty);
            right = sconcat(empty, right);
            x = sconcat(x, empty);
        }
        ENSURE(m_mon.can_decide_term(left));
        ENSURE(m_mon.can_decide_term(right));
        ENSURE(m_mon.can_decide_term(x));
        expr_ref term = sconcat(left, right);
        check("deep concat preserves order", term, word("ab"), l_true);
        check("deep concat rejects reversed word", term, word("ba"), l_false);
        expr_ref shared = sconcat(term, term);
        check("deep concat preserves shared occurrences", shared, word("abab"), l_true);
        check("deep concat does not deduplicate", shared, word("ab"), l_false);

        arith_util ar(m);
        expr_ref zero(ar.mk_int(0), m);
        expr_ref unsupported(u.str.mk_at(x, zero), m);
        term = sconcat(left, unsupported);
        ENSURE(!m_mon.can_decide_term(term));
        check("deep concat rejects unsupported leaf", term, word("ab"), l_undef);
    }

    // assert the membership list: the primary (term in R) plus one (var in R') per extra
    // constraint, decided jointly by check().
    void add_extra(expr* term, expr* R, obj_map<expr, expr*> const& ve) {
        m_mon.add(term, R, nullptr);
        for (auto const& [k, v] : ve)
            m_mon.add(k, v, nullptr);
    }

    void check_extra(char const* name, expr* term, expr* R,
                     obj_map<expr, expr*> const& ve, lbool expected) {
        m_trail.push_scope();
        add_extra(term, R, ve);
        m_mon.set_gen_solution(false);               // this check does not use the model
        lbool got = m_mon.check();
        m_trail.pop_scope(1);
        bool ok = (got == expected);
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name
                  << "  got=" << s(got) << " expected=" << s(expected) << "\n";
    }

    // decide two memberships on the same term jointly.
    void check_split(char const* name, expr* term, expr* r0, expr* r1, lbool expected) {
        m_trail.push_scope();
        m_mon.add(term, r0, nullptr);
        m_mon.add(term, r1, nullptr);
        m_mon.set_gen_solution(true);                // the refinement loop reads the solution
        lbool got = m_mon.check();
        m_trail.pop_scope(1);
        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) {
        m_trail.push_scope();
        add_extra(term, R, ve);
        m_mon.set_gen_solution(true);                // this check verifies the extracted model
        lbool got = m_mon.check();
        // The solver reports CONSTRAINTS; collapse them to values to check a witness.
        expr_substitution model(m);
        if (got == l_true)
            m_mon.materialize_all(model);
        bool ok = (got == l_true) && !model.empty();
        if (ok) {
            expr_safe_replace rep(m);
            for (auto const& kv : model.sub()) 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);
        }
        m_trail.pop_scope(1);
        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) {
        m_trail.push_scope();
        for (auto const& [t, r] : mems)
            m_mon.add(t, r, nullptr);
        m_mon.set_gen_solution(false);               // this check does not use the model
        lbool got = m_mon.check();
        m_trail.pop_scope(1);
        bool ok = (got == expected);
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name
                  << "  got=" << s(got) << " expected=" << s(expected) << "\n";
    }

    // collect the core ids after a check() into `ids`.
    void core_ids(std::set<unsigned>& ids) {
        ids.clear();
        for (void* dep : m_mon.core()) {
            u_dependency* d = static_cast<u_dependency*>(dep);
            ids.insert(d->leaf_value());
        }
    }

    // Assert each membership with a distinct leaf dependency (id = its index) and expect
    // the conjunction to be UNSAT.  With minimization ON, core() must be exactly
    // `expected_core` (irrelevant constraints omitted); with minimization OFF, core()
    // must be all membership dependencies.
    // Identity of a reported branch: the (var, state, target) triples it commits to.
    typedef std::set<std::tuple<unsigned, unsigned, unsigned>> branch_sig;

    static branch_sig sig_of(obj_map<expr, seq::view_vector> const& sol) {
        branch_sig sig;
        for (auto const& [var, views] : sol) {
            for (auto const& v : views)
                sig.insert(std::make_tuple(var->get_id(), v.m_state->get_id(),
                                           v.m_target ? v.m_target->get_id() : UINT_MAX));
        }
        return sig;
    }

    // Enumerate every branch of a conjunction of memberships and check what the lazy
    // enumeration has to guarantee:
    //   - it terminates, and reports `count()` branches;
    //   - no branch is reported twice (a replay that restarted instead of resuming would
    //     hand out the same first branch forever);
    //   - the iterator survives the trail scope its memberships were asserted in;
    //   - it drains cleanly (nothing given up) on problems this small, and a clean drain
    //     agrees with check(): branches were found iff the conjunction is satisfiable.
    // `min_branches` is a lower bound, not the branch count: how many branches survive is
    // a property of the search's pruning (an infeasible continuation is refuted, not
    // reported), whereas the enumeration only owes the invariants above.  A bound above 1
    // does pin down that resuming works at all, since every branch after the first comes
    // out of a replay.
    void check_enumerate(char const* name, vector<std::pair<expr*, expr*>> const& mems,
                         unsigned min_branches, lbool expected) {
        m_trail.push_scope();
        for (auto const& [t, r] : mems)
            m_mon.add(t, r, nullptr);
        lbool const decided = m_mon.check();
        obj_map<expr, seq::view_vector> first;
        for (auto const& [var, views] : m_mon.solution())
            first.insert(var, views);
        branch_sig const check_sig = sig_of(first);
        seq::monadic::iterator it = m_mon.iterate(1000);
        m_trail.pop_scope(1);                        // the iterator owns its own copy

        std::set<branch_sig> seen;
        obj_map<expr, seq::view_vector> sol;
        bool dup = false, first_matches = true;
        unsigned n = 0;
        while (it.next(sol)) {
            branch_sig sig = sig_of(sol);
            if (n == 0)
                first_matches = (sig == check_sig);
            if (!seen.insert(sig).second)
                dup = true;
            ++n;
        }

        bool const ok = decided == expected && !it.gave_up() && !dup && it.count() == n
                        && (n > 0) == (expected == l_true) && n >= min_branches
                        && first_matches;
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name
                  << "  branches=" << n << " expected>=" << min_branches
                  << (dup ? " DUPLICATE" : "")
                  << (it.gave_up() ? " GAVE-UP" : "")
                  << (first_matches ? "" : " FIRST-DIFFERS")
                  << "  check=" << s(decided) << " expected=" << s(expected) << "\n";
    }

    // Stronger check on a single membership: collapse every reported branch to a
    // concrete word per variable, substitute them into the term, and decide the resulting
    // GROUND membership with the same engine -- a path that involves no views at all.  So
    // every branch has to be a real solution, not merely a non-empty set of views.  The
    // nested solve() also drops the engine's whole search state between pulls, which is
    // exactly the interleaving a suspended iterator has to survive.
    void check_enumerate_words(char const* name, expr* term, expr* R, unsigned min_branches) {
        m_trail.push_scope();
        m_mon.add(term, R, nullptr);
        seq::monadic::iterator it = m_mon.iterate(100);
        m_trail.pop_scope(1);

        expr_ref_vector grounds(m);
        obj_map<expr, seq::view_vector> sol;
        unsigned n = 0;
        bool ok = true;
        while (ok && it.next(sol)) {
            ++n;
            expr_safe_replace rep(m);
            for (auto const& [var, views] : sol) {
                expr_ref w(m);
                if (m_mon.materialize(var, w) != l_true) {
                    ok = false;
                    break;
                }
                rep.insert(var, w);
            }
            if (!ok)
                break;
            expr_ref ground(m);
            rep(term, ground);
            grounds.push_back(ground);
        }
        ok = ok && !it.gave_up() && n >= min_branches;
        for (unsigned i = 0; ok && i < grounds.size(); ++i)
            ok = m_mon.solve(grounds.get(i), R) == l_true;   // independent, view-free re-check
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name
                  << "  branches=" << n << " expected>=" << min_branches
                  << (it.gave_up() ? " GAVE-UP" : "") << "\n";
    }

    void check_core(char const* name, vector<std::pair<expr*, expr*>> const& mems,
                    std::set<unsigned> const& expected_core) {
        m_mon.set_gen_solution(false);
        std::set<unsigned> all_ids, got_ids;
        for (unsigned i = 0; i < mems.size(); ++i)
            all_ids.insert(i);

        // minimization disabled: the core is every asserted membership's dependency.
        m_mon.set_min_core(false);
        m_trail.push_scope();
        for (unsigned i = 0; i < mems.size(); ++i)
            m_mon.add(mems[i].first, mems[i].second, m_dm.mk_leaf(i));
        lbool got0 = m_mon.check();
        core_ids(got_ids);
        bool ok0 = (got0 == l_false) && (got_ids == all_ids);
        m_trail.pop_scope(1);

        // minimization enabled: the core drops constraints irrelevant to the conflict.
        m_mon.set_min_core(true);
        m_trail.push_scope();
        for (unsigned i = 0; i < mems.size(); ++i)
            m_mon.add(mems[i].first, mems[i].second, m_dm.mk_leaf(i));
        lbool got1 = m_mon.check();
        std::set<unsigned> min_ids;
        core_ids(min_ids);
        bool ok1 = (got1 == l_false) && (min_ids == expected_core);
        m_trail.pop_scope(1);
        m_mon.set_min_core(false);                // restore the harness default

        bool ok = ok0 && ok1;
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name << "  got=" << s(got1) << " core={";
        bool first = true;
        for (unsigned id : min_ids) { std::cout << (first ? "" : ",") << id; first = false; }
        std::cout << "} full=" << (ok0 ? "yes" : "no") << "\n";
    }

    // One enumerated branch as a comparable string: per variable, the views it commits to.
    std::string branch_str(obj_map<expr, seq::view_vector> const& sol) {
        std::vector<std::string> per_var;
        for (auto const& [v, views] : sol) {
            std::ostringstream os;
            os << v->get_id() << ":";
            for (seq::view const& c : views)
                os << " " << c.m_state->get_id() << "->"
                   << (c.is_reach() ? c.m_target->get_id() : 0);
            per_var.push_back(os.str());
        }
        std::sort(per_var.begin(), per_var.end());
        std::string r;
        for (std::string const& s : per_var)
            r += s + " | ";
        return r;
    }

    void enum_branches(vector<std::pair<expr*, expr*>> const& mems,
                       std::vector<std::string>& out, bool& giveup,
                       std::pair<expr*, expr*> const* itl = nullptr) {
        m_trail.push_scope();
        for (auto const& [t, r] : mems)
            m_mon.add(t, r, nullptr);
        seq::monadic::iterator it = m_mon.iterate(256);
        m_trail.pop_scope(1);                     // the iterator owns its query

        obj_map<expr, seq::view_vector> sol;
        while (it.next(sol)) {
            out.push_back(branch_str(sol));
            if (itl) {
                m_trail.push_scope();
                m_mon.add(itl->first, itl->second, nullptr);
                (void)m_mon.check();
                m_trail.pop_scope(1);
            }
        }
        giveup = it.gave_up();
    }

    void check_iterate(char const* name, vector<std::pair<expr*, expr*>> const& mems,
                       std::pair<expr*, expr*> const& itl) {
        std::vector<std::string> plain, interrupted;
        bool g1 = true, g2 = true;
        enum_branches(mems, plain, g1);
        enum_branches(mems, interrupted, g2, &itl);

        m_trail.push_scope();
        for (auto const& [t, r] : mems)
            m_mon.add(t, r, nullptr);
        lbool direct = m_mon.check();
        m_trail.pop_scope(1);

        std::set<std::string> distinct(plain.begin(), plain.end());
        bool prefix = interrupted.size() <= plain.size() &&
                      std::equal(interrupted.begin(), interrupted.end(), plain.begin());
        bool ok = !g1 && distinct.size() == plain.size() && prefix &&
                  g2 == !plain.empty() &&           // no pull, no interruption
                  direct == (plain.empty() ? l_false : l_true);
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name
                  << "  branches=" << plain.size() << " exhaustive=" << (g1 ? "no" : "yes")
                  << " interrupted=" << interrupted.size() << (g2 ? " (gave up)" : "")
                  << " check=" << s(direct) << "\n";
    }

    void check_budget_sweep(char const* name, vector<std::pair<expr*, expr*>> const& mems,
                            lbool truth) {
        unsigned const saved = m_mon.budget();
        unsigned wrong = 0, gave_up = 0;
        for (unsigned b = 1; b <= 60; ++b) {
            m_mon.set_budget(b);
            m_trail.push_scope();
            for (auto const& [t, r] : mems)
                m_mon.add(t, r, nullptr);
            lbool got = m_mon.check();
            m_trail.pop_scope(1);
            if (got == l_undef)
                ++gave_up;
            else if (got != truth)
                ++wrong;
        }
        m_mon.set_budget(saved);
        bool ok = wrong == 0;
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name << "  wrong=" << wrong
                  << " gave-up=" << gave_up << "/60\n";
    }

    lbool smt_check(expr_ref_vector const& assertions, bool enable_monadic = true) {
        smt_params params;
        params.m_seq_regex_monadic = enable_monadic;
        smt::kernel solver(m, params);
        for (expr* assertion : assertions)
            solver.assert_expr(assertion);
        return solver.check();
    }

    void check_smt(char const* name, expr_ref_vector const& assertions, lbool expected,
                   bool enable_monadic = true) {
        lbool got = smt_check(assertions, enable_monadic);
        bool ok = got == expected;
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name
                  << "  got=" << s(got) << " expected=" << s(expected) << "\n";
    }

    void check_smt2_no_crash(char const* name, char const* input, unsigned rlimit) {
        cmd_context cmd(false, &m);
        std::istringstream is(input);
        bool ok = parse_smt2_commands(cmd, is);
        bool resource_limited = false;
        if (ok) {
            params_ref p;
            ref<solver> slv = mk_smt2_solver(m, p, symbol::null);
            for (expr* a : cmd.assertions())
                slv->assert_expr(a);
            // Direct solver calls do not install the API's rlimit scope.
            scoped_rlimit limit(m.limit(), rlimit);
            try {
                slv->check_sat(0, nullptr);
            }
            catch (rewriter_exception const& ex) {
                // Internal rewriting can report the installed budget by exception.
                if (!m.limit().is_canceled() || std::string(ex.what()) != Z3_MAX_RESOURCE_MSG)
                    throw;
                resource_limited = true;
            }
        }
        if (!ok) ++m_fail;
        std::cout << (ok ? "  OK   " : "  FAIL ") << name;
        if (!ok)
            std::cout << " parse failed";
        if (resource_limited)
            std::cout << " resource limit reached";
        std::cout << "\n";
    }

public:
    seq_monadic_test(seq::transition_mode mode) :
        m_reg(m), m_rw(m), m_mon(m_rw, m_trail, mode), u(m), m_str(m), m_re(m), m_mode(mode) {
        m_str = u.str.mk_string_sort();
        m_re  = re().mk_re(m_str);
        m_mon.set_min_core(false);   // tests use unminimized cores by default
    }

    void run() {
        std::cout << "=== seq_monadic mode: " << mode_name() << " ===\n";
        check_deep_concat();
        if (m_mode == seq::transition_mode::light_antimirov_tm)
            check_ant_cofactors();
        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
        {
            auto rhs1 = xwx(x, "a");
            auto third = star(alt(a, b));
            check("(a|b)*        x.a.x", rhs1, third, l_true);
        }
        {
            auto rhs1 = xwx(x, "a");
            auto third = star(b);
            check("b*            x.a.x", rhs1, third, 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);
        {
            auto rhs1 = xwx(x, "a");
            auto third = star(b);
            check("x in b* (x=aa)     ", rhs1, third, l_false);
        }
        {
            auto rhs1 = sword("z");
            auto third = star(re().mk_to_re(x));
            check("non-ground regex guard", rhs1, third, l_undef);
        }

        // ALT = (a|b)* & ~(Sig*aaSig*) & ~(Sig*bbSig*)  (strictly alternating)
        auto lhs = star(alt(a, b));
        auto lhs1 = comp(saas);
        auto rhs1 = comp(sbbs);
        auto rhs2 = inter(lhs1, rhs1);
        expr_ref altre = inter(lhs, rhs2);
        check("ALT           x.a.x", xwx(x, "a"), altre, l_true);

        // R*.S complement family
        {
            auto rhs1 = xwx(x, "a");
            auto third = comp(cat(star(a), b));
            check("~(a*.b)       x.a.x", rhs1, third, l_true);
        }

        // L3-02 ~((ab)*.~((ab)*))   -> unsat (odd length)
        {
            auto rhs1 = xwx(x, "a");
            auto lhs = star(ab);
            auto rhs2 = comp(star(ab));
            auto third = comp(cat(lhs, rhs2));
            check("L3-02         x.a.x", rhs1, third, l_false);
        }

        // L3-03 ~(a*.~(b*.~((ab)*)))  -> sat
        {
            auto rhs1 = xwx(x, "a");
            auto lhs = star(a);
            auto lhs1 = star(b);
            auto rhs2 = comp(star(ab));
            auto rhs3 = comp(cat(lhs1, rhs2));
            auto third = comp(cat(lhs, rhs3));
            check("L3-03         x.a.x", rhs1, third, l_true);
        }

        std::cout << "=== seq_monadic: multi-variable ===\n";
        expr_ref y = var("y");
        {
            auto rhs1 = xay(x, y);
            auto third = star(alt(a, b));
            check("(a|b)*        x.a.y", rhs1, third, l_true);
        }
        {
            auto rhs1 = xay(x, y);
            auto third = star(b);
            check("b*            x.a.y", rhs1, third, l_false);
        }
        {
            auto rhs1 = xay(x, y);
            auto lhs = star(ab);
            auto rhs2 = comp(star(ab));
            auto third = comp(cat(lhs, rhs2));
            check("L3-02         x.a.y", rhs1, third, l_true);
        }
        {
            auto rhs1 = xay(x, y);
            auto lhs = star(a);
            auto lhs1 = star(b);
            auto rhs2 = comp(star(ab));
            auto rhs3 = comp(cat(lhs1, rhs2));
            auto third = comp(cat(lhs, rhs3));
            check("L3-03         x.a.y", rhs1, third, l_true);
        }
        {
            auto rhs1 = xyx(x, y);
            auto third = comp(dotstar());
            check("empty ~Sig*   x.y.x", rhs1, third, l_false);
        }
        check("Sig*          x.y.x", xyx(x, y), dotstar(), l_true);
        {
            auto rhs1 = xyx(x, y);
            auto third = star(alt(a, b));
            check("(a|b)*        x.y.x", rhs1, third, l_true);
        }

        std::cout << "=== seq_monadic: per-variable constraints ===\n";
        auto lhs2 = rng('0', '9');
        auto rhs3 = star(rng('0', '9'));
        expr_ref digitp = cat(lhs2, rhs3);  // [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
        {
            auto rhs1 = xay(x, y);
            auto third = star(alt(a, b));
            check_extra("(a|b)* & y in[0-9]+ x.a.y", rhs1, third, 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;
        {
            auto rhs1 = xwx(x, "a");
            auto third = star(alt(a, b));
            check_witness("(a|b)*        x.a.x", rhs1, third, nove);
        }
        check_witness("Sig*aaSig*    x.a.x", xwx(x, "a"), saas, nove);      // forces nonempty x
        {
            auto rhs1 = xwx(x, "a");
            auto third = comp(cat(star(a), b));
            check_witness("~(a*.b)       x.a.x", rhs1, third, nove);
        }
        {
            auto rhs1 = xwx(x, "a");
            auto lhs = star(a);
            auto lhs1 = star(b);
            auto rhs2 = comp(star(ab));
            auto rhs3 = comp(cat(lhs1, rhs2));
            auto third = comp(cat(lhs, rhs3));
            check_witness("L3-03         x.a.x", rhs1, third, nove);
        }
        {
            auto rhs1 = xay(x, y);
            auto third = star(alt(a, b));
            check_witness("(a|b)*        x.a.y", rhs1, third, 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 (add + check): 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 (add + check) ===\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: assertion trail ===\n";
        m_mon.set_gen_solution(false);
        m_trail.push_scope();
        m_mon.add(x, aaS, nullptr);
        lbool before = m_mon.check();
        m_trail.push_scope();
        m_mon.add(x, a_aaS, nullptr);
        lbool with_conflict = m_mon.check();
        lbool repeated = m_mon.check();
        m_trail.pop_scope(1);
        lbool after_pop = m_mon.check();
        m_trail.pop_scope(1);
        lbool empty = m_mon.check();
        bool trail_ok = before == l_true && with_conflict == l_false &&
                        repeated == l_false && after_pop == l_true && empty == l_true;
        if (!trail_ok) ++m_fail;
        std::cout << (trail_ok ? "  OK   " : "  FAIL ")
                  << "check preserves assertions and pop removes them\n";

        std::cout << "=== seq_monadic: display ===\n";
        m_trail.push_scope();
        unsigned display_dep = 0;
        m_mon.set_gen_solution(true);
        m_mon.add(x, aaS, &display_dep);
        lbool display_result = m_mon.check();
        std::ostringstream display_out;
        m_mon.display(display_out);
        std::string display_text = display_out.str();
        bool display_ok =
            display_result == l_true &&
            display_text.find("(seq-monadic") != std::string::npos &&
            display_text.find(":memberships") != std::string::npos &&
            display_text.find(":solution") != std::string::npos &&
            display_text.find(":last-result l_true") != std::string::npos &&
            display_text.find(":last-internal-search") != std::string::npos &&
            display_text.find(":parsed-memberships") != std::string::npos &&
            display_text.find(":statistics") != std::string::npos &&
            display_text.find("x") != std::string::npos;
        m_trail.pop_scope(1);
        if (!display_ok) ++m_fail;
        std::cout << (display_ok ? "  OK   " : "  FAIL ")
                  << "display exposes readable solver state\n";

        m_trail.push_scope();
        unsigned display_dep1 = 1, display_dep2 = 2;
        m_mon.set_min_core(true);
        m_mon.add(x, aaS, &display_dep1);
        m_mon.add(x, a_aaS, &display_dep2);
        lbool unsat_display_result = m_mon.check();
        std::ostringstream unsat_display_out;
        m_mon.display(unsat_display_out);
        std::string unsat_display_text = unsat_display_out.str();
        bool unsat_display_ok =
            unsat_display_result == l_false &&
            unsat_display_text.find(":last-result l_false") != std::string::npos &&
            unsat_display_text.find(":solution ()") != std::string::npos &&
            unsat_display_text.find(":last-internal-search") != std::string::npos;
        m_trail.pop_scope(1);
        m_mon.set_min_core(false);
        if (!unsat_display_ok) ++m_fail;
        std::cout << (unsat_display_ok ? "  OK   " : "  FAIL ")
                  << "display distinguishes unsat result from core-search state\n";

        lbool solve_display_result = m_mon.solve(x, aaS);
        std::ostringstream solve_display_out;
        m_mon.display(solve_display_out);
        bool solve_display_ok =
            solve_display_result == l_true &&
            solve_display_out.str().find(":core ( )") != std::string::npos;
        lbool empty_display_result = m_mon.check();
        std::ostringstream empty_display_out;
        m_mon.display(empty_display_out);
        std::string empty_display_text = empty_display_out.str();
        bool empty_display_ok = empty_display_result == l_true;
        if (!solve_display_ok || !empty_display_ok) ++m_fail;
        std::cout << (solve_display_ok && empty_display_ok ? "  OK   " : "  FAIL ")
                  << "display clears artifacts across solve and empty check\n";

        std::cout << "=== seq_monadic: length bounds ===\n";
        auto check_bound = [&](char const* name, expr* regex, unsigned bound, bool is_lo,
                               lbool expected) {
            m_trail.push_scope();
            m_mon.add(x, regex, nullptr);
            if (is_lo)
                m_mon.add_lo(x, bound, nullptr);
            else
                m_mon.add_hi(x, bound, nullptr);
            lbool got = m_mon.check();
            m_trail.pop_scope(1);
            bool ok = got == expected;
            if (!ok) ++m_fail;
            std::cout << (ok ? "  OK   " : "  FAIL ") << name
                      << "  got=" << s(got) << " expected=" << s(expected) << "\n";
        };
        check_bound("x in a, |x| >= 1", word("a"), 1, true, l_true);
        check_bound("x in a, |x| >= 2", word("a"), 2, true, l_false);
        check_bound("x in aa, |x| <= 2", word("aa"), 2, false, l_true);
        check_bound("x in aa, |x| <= 1", word("aa"), 1, false, l_false);
        check_bound("x in epsilon, |x| <= 0", word(""), 0, false, l_true);
        auto check_len = [&](char const* name, expr* regex, unsigned len, lbool expected) {
            m_trail.push_scope();
            m_mon.add(x, regex, nullptr);
            m_mon.add_len(x, len, nullptr);
            lbool got = m_mon.check();
            m_trail.pop_scope(1);
            bool ok = got == expected;
            if (!ok) ++m_fail;
            std::cout << (ok ? "  OK   " : "  FAIL ") << name
                      << "  got=" << s(got) << " expected=" << s(expected) << "\n";
        };
        check_len("x in aa, |x| = 2", word("aa"), 2, l_true);
        check_len("x in aa, |x| = 1", word("aa"), 1, l_false);
        check_len("x in epsilon, |x| = 0", word(""), 0, l_true);
        m_trail.push_scope();
        unsigned trail_size = m_trail.size();
        m_mon.add_lo(x, 0, m_dm.mk_leaf(0));
        bool zero_lo_ok = m_trail.size() == trail_size && m_mon.check() == l_true;
        m_trail.pop_scope(1);
        if (!zero_lo_ok) ++m_fail;
        std::cout << (zero_lo_ok ? "  OK   " : "  FAIL ")
                  << "|x| >= 0 is a no-op\n";

        // Length bounds on COMPOUND terms and on several variables at once: the shape the
        // SMT-LIB regex benchmarks use (e.g. `x.y.x in R /\ |x|>0 /\ |y|>0`).  A bound on
        // a concatenation constrains the term as a whole; bounds on the individual
        // variables have to be intersected with the split induced by the membership.
        std::cout << "=== seq_monadic: length bounds on compound terms ===\n";
        auto check_bounded = [&](char const* name,
                                 auto&& assert_all, lbool expected) {
            m_trail.push_scope();
            assert_all();
            lbool got = m_mon.check();
            m_trail.pop_scope(1);
            bool ok = got == expected;
            if (!ok) ++m_fail;
            std::cout << (ok ? "  OK   " : "  FAIL ") << name
                      << "  got=" << s(got) << " expected=" << s(expected) << "\n";
        };
        expr_ref t_xyx(xyx(x, y), m);
        expr_ref t_xax(xwx(x, "a"), m);
        // |x.y.x| is odd-free: x.y.x in (ab)* with |x.y.x| = 2 forces x.y.x = "ab"
        check_bounded("x.y.x in (ab)*, |x.y.x| = 2", [&] {
            m_mon.add(t_xyx, abS, nullptr);
            m_mon.add_len(t_xyx, 2, nullptr);
        }, l_true);
        check_bounded("x.y.x in (ab)*, |x.y.x| = 3", [&] {
            m_mon.add(t_xyx, abS, nullptr);
            m_mon.add_len(t_xyx, 3, nullptr);      // (ab)* has only even lengths
        }, l_false);
        // bounds on the individual variables of a compound membership
        check_bounded("x.a.x in Sigma*, |x| >= 2, |x.a.x| <= 5", [&] {
            m_mon.add(t_xax, sig2, nullptr);
            m_mon.add_lo(x, 2, nullptr);
            m_mon.add_hi(t_xax, 5, nullptr);
        }, l_true);
        check_bounded("x.a.x in Sigma*, |x| >= 3, |x.a.x| <= 5", [&] {
            m_mon.add(t_xax, sig2, nullptr);
            m_mon.add_lo(x, 3, nullptr);           // |x.a.x| = 2|x|+1 >= 7 > 5
            m_mon.add_hi(t_xax, 5, nullptr);
        }, l_false);
        // two variables bounded independently under one membership
        check_bounded("x.y.x in (a|b)*, |x| = 1, |y| = 2", [&] {
            m_mon.add(t_xyx, abStar, nullptr);
            m_mon.add_len(x, 1, nullptr);
            m_mon.add_len(y, 2, nullptr);
        }, l_true);
        check_bounded("x.y.x in a*, |x| >= 1, y in b*", [&] {
            m_mon.add(t_xyx, star(a), nullptr);
            m_mon.add(y, star(b), nullptr);        // y must be both a* and b* -> y = eps
            m_mon.add_lo(x, 1, nullptr);
            m_mon.add_lo(y, 1, nullptr);           // ... but |y| >= 1
        }, l_false);
        // the bound is the ONLY reason for unsat: without it the membership is satisfiable
        check_bounded("x in a(aa)* (no bound)", [&] {
            m_mon.add(x, a_aaS, nullptr);
        }, l_true);
        check_bounded("x in a(aa)*, |x| = 2", [&] {
            m_mon.add(x, a_aaS, nullptr);          // only odd lengths
            m_mon.add_len(x, 2, nullptr);
        }, l_false);
        // upper and lower bounds that cross
        check_bounded("x in Sigma*, |x| >= 3, |x| <= 2", [&] {
            m_mon.add(x, sig2, nullptr);
            m_mon.add_lo(x, 3, nullptr);
            m_mon.add_hi(x, 2, nullptr);
        }, l_false);

        // The IPv6 abbreviation benchmark shape: an intersection of a positive "contains"
        // and a complement, restricted to a character range, over  x.y.x  with both
        // variables non-empty.  Without the length bounds the answer is trivially sat via
        // x = y = epsilon, so the bounds are what make the test meaningful.
        {
            expr_ref cc(word("::"), m);
            expr_ref sig_plus(cat(dot(), dotstar()), m);
            expr_ref has_cc(cat(dotstar(), cat(cc, dotstar())), m);
            expr_ref two_cc(cat(dotstar(), cat(cc, cat(sig_plus, cat(cc, dotstar())))), m);
            auto lhs3 = rng('0', '9');
            auto lhs4 = rng('A', 'F');
            auto lhs5 = rng('a', 'f');
            auto rhs4 = word(":");
            auto rhs5 = alt(lhs5, rhs4);
            auto rhs6 = alt(lhs4, rhs5);
            expr_ref hexcol(star(alt(lhs3, rhs6)), m);
            expr_ref R6(inter(has_cc, inter(comp(two_cc), hexcol)), m);
            check_bounded("ipv6: x.y.x in R, |x|>=1, |y|>=1", [&] {
                m_mon.add(t_xyx, R6, nullptr);
                m_mon.add_lo(x, 1, nullptr);
                m_mon.add_lo(y, 1, nullptr);
            }, l_true);
            // "::" cannot be split across a repeated x without creating a second group,
            // and hexcol forbids everything outside [0-9A-Fa-f:], so a long x is hopeless
            check_bounded("ipv6: x.y.x in R, |x|>=1, |y|>=1, |x.y.x|<=2", [&] {
                m_mon.add(t_xyx, R6, nullptr);
                m_mon.add_lo(x, 1, nullptr);
                m_mon.add_lo(y, 1, nullptr);
                m_mon.add_hi(t_xyx, 2, nullptr);   // needs >= 3 chars to hold "::" plus x twice
            }, l_false);
        }

        std::cout << "=== seq_monadic: SMT regex end-game ===\n";
        {
            expr_ref_vector assertions(m);
            assertions.push_back(re().mk_in_re(x, star(alt(a, b))));
            check_smt("enabled SAT membership", assertions, l_true);
            check_smt("disabled legacy membership", assertions, l_true, false);
        }
        {
            arith_util ar2(m);
            expr_ref i(m.mk_fresh_const("issue_10492_i", ar2.mk_int()), m);
            expr_ref y = var("issue_10492_y");
            expr_ref at(u.str.mk_at(y, i), m);
            expr_ref_vector assertions(m);
            assertions.push_back(m.mk_eq(at, u.str.mk_empty(m_str)));
            {
                auto lhs = sword("z");
                auto rhs1 = star(re().mk_to_re(at));
                assertions.push_back(re().mk_in_re(lhs, rhs1));
            }
            check_smt("non-ground regex issue 10492", assertions, l_false);
        }
        if (m_mode == seq::transition_mode::brzozowski_tm)
            check_smt2_no_crash("quantified str.from_code regex issue 10651",
                "(declare-fun v () String)\n"
                "(declare-fun r () Bool)\n"
                "(declare-fun w () String)\n"
                "(declare-fun q () String)\n"
                "(assert (forall ((v String))\n"
                "  (or r\n"
                "      (exists ((V String))\n"
                "        (str.in_re\n"
                "          (str.++ (str.++ (str.++ v V V) q (str.++ w w w)) v)\n"
                "          (re.* (str.to_re (str.from_code (str.len V)))))))))\n",
                100000);
        {
            arith_util ar2(m);
            expr_ref zero(ar2.mk_int(0), m);
            expr_ref one(ar2.mk_int(1), m);
            expr_ref k = var("issue_10379_k");
            expr_ref k0(u.str.mk_at(k, zero), m);
            expr_ref mod00(ar2.mk_mod(zero, zero), m);
            auto lhs6 = sword("1");
            expr_ref rhs7(re().mk_to_re(k), m);
            expr_ref inner_cond(re().mk_in_re(lhs6, rhs7), m);
            auto then_value = sconcat(sword("n"), k0);
            expr_ref else_value(u.str.mk_substr(k, zero, mod00), m);
            expr_ref inner(m.mk_ite(inner_cond, then_value, else_value), m);
            expr_ref lhs7(re().mk_to_re(k0), m);
            auto rhs8 = rng('a', 'z');
            expr_ref outer_regex(cat(lhs7, rhs8), m);
            expr_ref outer_cond(re().mk_in_re(inner, outer_regex), m);
            expr_ref rhs(m.mk_ite(outer_cond, k0, u.str.mk_substr(k, zero, zero)), m);
            expr_ref_vector assertions(m);
            assertions.push_back(m.mk_eq(k, rhs));
            assertions.push_back(ar2.mk_ge(u.str.mk_length(k), one));
            check_smt("legacy nested regex ITE issue 10379", assertions, l_false, false);
        }
        {
            expr_ref_vector assertions(m);
            expr_ref a_star(star(a), m);
            assertions.push_back(re().mk_in_re(x, a_star));
            assertions.push_back(re().mk_in_re(x, comp(a_star)));
            check_smt("enabled joint UNSAT memberships", assertions, l_false);
        }
        {
            expr_ref_vector assertions(m);
            assertions.push_back(m.mk_not(re().mk_in_re(x, star(a))));
            assertions.push_back(re().mk_in_re(x, star(a)));
            check_smt("enabled negative membership", assertions, l_false);
        }
        {
            expr_ref_vector assertions(m);
            assertions.push_back(m.mk_eq(x, sword("aa")));
            assertions.push_back(re().mk_in_re(x, expr_ref(re().mk_plus(a), m)));
            check_smt("rejected witness uses legacy fallback", assertions, l_true);
        }
        {
            expr_ref_vector assertions(m);
            assertions.push_back(m.mk_eq(x, y));
            assertions.push_back(re().mk_in_re(x, star(a)));
            assertions.push_back(re().mk_in_re(y, expr_ref(re().mk_plus(b), m)));
            check_smt("aliased variables use legacy fallback", assertions, l_false);
        }
        {
            arith_util ar2(m);
            sort_ref int_sort(ar2.mk_int(), m);
            sort_ref seq_sort(u.str.mk_seq(int_sort), m);
            sort_ref regex_sort(re().mk_re(seq_sort), m);
            expr_ref seq_var(m.mk_const("seq_var", seq_sort), m);
            expr_ref elem_var(m.mk_const("elem_var", int_sort), m);
            expr_ref symbolic_unit(u.str.mk_unit(elem_var), m);
            expr_ref term(u.str.mk_concat(seq_var, symbolic_unit), m);
            expr_ref_vector assertions(m);
            assertions.push_back(re().mk_in_re(term, re().mk_full_seq(regex_sort)));
            check_smt("unsupported symbolic unit uses fallback", assertions, l_true);
        }
        {
            smt_params params;
            params.m_seq_regex_monadic = true;
            smt::kernel solver(m, params);
            expr_ref a_star(star(a), m);
            solver.assert_expr(re().mk_in_re(x, a_star));
            lbool before_push = solver.check();
            solver.push();
            solver.assert_expr(re().mk_in_re(x, comp(a_star)));
            lbool in_push = solver.check();
            solver.pop(1);
            lbool after_pop = solver.check();
            bool ok = before_push == l_true && in_push == l_false && after_pop == l_true;
            if (!ok) ++m_fail;
            std::cout << (ok ? "  OK   " : "  FAIL ")
                      << "SMT membership trail push/pop\n";
        }

        // ---- unsat cores: the extracted core must contain only constraints that
        // ---- participate in the contradiction, not independent ones.
        // ---- lazy branch enumeration ---------------------------------------------------
        // seq::monadic::iterator hands out the branches of the decomposition one at a time,
        // suspending between them by replaying the choice path of the last one reported.
        std::cout << "=== seq_monadic: branch enumeration ===\n";
        {
            expr_ref y = var("y");
            auto ms1 = [&](expr* t, expr* r) {
                vector<std::pair<expr*, expr*>> v;
                v.push_back(std::make_pair(t, r));
                return v;
            };
            // A single variable is one membership view and no choice at all: the recorded
            // path is empty, which the replay has to handle as well as any other.
            check_enumerate("x in (a|b)*", ms1(x, star(alt(a, b))), 1, l_true);
            // Two occurrences: one branch per live state x can drive the automaton to.
            {
                auto lhs = xwx(x, "a");
                auto rhs1 = star(alt(a, b));
                check_enumerate("x.a.x in (a|b)*", ms1(lhs, rhs1), 1, l_true);
            }
            // Only one of x's two continuations survives here: after the other one the
            // constant `a` has no derivative, so the branch is refuted rather than reported.
            {
                auto lhs = xay(x, y);
                auto rhs1 = star(ab);
                check_enumerate("x.a.y in (ab)*", ms1(lhs, rhs1), 1, l_true);
            }
            // The union keeps several states live at both variables, so the enumeration
            // has to resume repeatedly -- and every branch it reports must be a new one.
            {
                auto lhs = xyx(x, y);
                auto lhs1 = alt(a, b);
                auto rhs1 = word("bba");
                auto rhs2 = star(alt(lhs1, rhs1));
                check_enumerate("x.y.x in (a|b|bba)*", ms1(lhs, rhs2), 4, l_true);
            }
            // Unsat: no branch at all, and the drain is clean, which is what makes "the
            // enumerator ran out" usable as a refutation.
            {
                auto lhs = xwx(x, "a");
                auto rhs1 = star(b);
                check_enumerate("x.a.x in b*", ms1(lhs, rhs1), 0, l_false);
            }
            // Two memberships sharing a variable: branches over the joint decomposition.
            {
                vector<std::pair<expr*, expr*>> ms;
                expr_ref term = xay(x, y);
                expr_ref language = star(ab);
                ms.push_back(std::make_pair(term.get(), language.get()));
                ms.push_back(std::make_pair(x.get(), language.get()));
                check_enumerate("x.a.y in (ab)* & x in (ab)*", ms, 1, l_true);
            }
            // Every branch, collapsed to concrete words, really does satisfy the
            // membership -- decided by the engine on the ground term, without views.
            {
                auto rhs1 = xwx(x, "a");
                auto third = star(alt(a, b));
                check_enumerate_words("words: x.a.x in (a|b)*", rhs1, third, 1);
            }
            {
                auto rhs1 = xyx(x, y);
                auto lhs = alt(a, b);
                auto rhs2 = word("bba");
                auto third = star(alt(lhs, rhs2));
                check_enumerate_words("words: x.y.x in (a|b|bba)*", rhs1, third, 4);
            }
            check_enumerate_words("words: x.a.y in Sig*aaSig*", xay(x, y), saas, 1);
        }

        std::cout << "=== seq_monadic: unsat cores ===\n";
        // x in a* /\ x in ~(a*) /\ y in b*  -> unsat over x; core = {0,1}, not the y-constraint.
        {
            expr_ref aStar(star(a), m), naStar(comp(star(a)), m), bStar(star(b), m);
            vector<std::pair<expr*, expr*>> ms;
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)aStar.get()));
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)naStar.get()));
            ms.push_back(std::make_pair((expr*)y.get(), (expr*)bStar.get()));
            check_core("x in a* & x in ~a* (& y in b*)", ms, std::set<unsigned>{0, 1});
        }
        // x in (aa)* /\ x in a(aa)* /\ y in Sigma*  -> unsat over x; core = {0,1}.
        {
            expr_ref aaS(star(cat(a, a)), m), a_aaS(cat(a, star(cat(a, a))), m), sigStar(dotstar(), m);
            vector<std::pair<expr*, expr*>> ms;
            ms.push_back(std::make_pair((expr*)x.get(),  (expr*)aaS.get()));
            ms.push_back(std::make_pair((expr*)x.get(),  (expr*)a_aaS.get()));
            ms.push_back(std::make_pair((expr*)y.get(),  (expr*)sigStar.get()));
            check_core("x in (aa)* & x in a(aa)* (& y in Sig*)", ms, std::set<unsigned>{0, 1});
        }
        // Three independent constraints, contradiction only between the middle two:
        // z in a* (indep) /\ x in b* /\ x in a+ (x=empty allowed by b*, a+ forbids empty)
        {
            expr_ref z = var("z");
            expr_ref aStarZ(star(a), m), bStarX(star(b), m), aP(cat(a, star(a)), m);   // a+ = at least one a
            vector<std::pair<expr*, expr*>> ms;
            ms.push_back(std::make_pair((expr*)z.get(), (expr*)aStarZ.get()));    // 0: irrelevant
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)bStarX.get()));    // 1: x in b*
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)aP.get()));        // 2: x in a+
            check_core("z in a* (& x in b* & x in a+)", ms, std::set<unsigned>{1, 2});
        }

        std::cout << "=== seq_monadic: resumable enumeration ===\n";
        {
            expr_ref z = var("z");
            expr_ref aStar(star(a), m), abStar(star(cat(a, b)), m);
            expr_ref aaS(star(cat(a, a)), m), a_aaS(cat(a, star(cat(a, a))), m);
            expr_ref t_xax = xwx(x, "a"), t_xyx = xyx(x, y), t_xay = xay(x, y);
            std::pair<expr*, expr*> itl((expr*)z.get(), (expr*)aStar.get());  // z in a*

            vector<std::pair<expr*, expr*>> ms;
            ms.push_back(std::make_pair((expr*)t_xax.get(), (expr*)saas.get()));
            check_iterate("x.a.x in Sig* aa Sig*", ms, itl);

            ms.reset();
            ms.push_back(std::make_pair((expr*)t_xyx.get(), (expr*)abStar.get()));
            check_iterate("x.y.x in (ab)*", ms, itl);

            ms.reset();
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)aStar.get()));
            ms.push_back(std::make_pair((expr*)t_xay.get(), (expr*)saas.get()));
            check_iterate("x in a* & x.a.y in Sig* aa Sig*", ms, itl);

            ms.reset();                                // two views per variable per branch
            ms.push_back(std::make_pair((expr*)t_xax.get(), (expr*)saas.get()));
            ms.push_back(std::make_pair((expr*)t_xax.get(), (expr*)sbbs.get()));
            check_iterate("x.a.x in Sig* aa Sig* & in Sig* bb Sig*", ms, itl);

            ms.reset();
            ms.push_back(std::make_pair((expr*)t_xyx.get(), (expr*)saas.get()));
            check_iterate("x.y.x in Sig* aa Sig*", ms, itl);

            ms.reset();                                // refuted: no branch at all
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)aaS.get()));
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)a_aaS.get()));
            check_iterate("x in (aa)* & x in a(aa)*", ms, itl);
            check_budget_sweep("x in (aa)* & x in a(aa)* (unsat)", ms, l_false);

            ms.reset();
            ms.push_back(std::make_pair((expr*)t_xyx.get(), (expr*)saas.get()));
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)abStar.get()));
            check_budget_sweep("x.y.x in Sig* aa Sig* & x in (ab)* (sat)", ms, l_true);

            auto lhs8 = sword("a");
            auto rhs9 = sconcat(x, sconcat(sword("a"), x));
            expr_ref t5 = sconcat(x, sconcat(lhs8, rhs9));
            expr_ref abS(star(alt(a, b)), m);
            ms.reset();
            ms.push_back(std::make_pair((expr*)t5.get(), (expr*)saas.get()));
            ms.push_back(std::make_pair((expr*)x.get(), (expr*)abS.get()));
            check_budget_sweep("x.a.x.a.x in Sig* aa Sig* & x in (a|b)* (sat)", ms, l_true);

            ms.reset();
            ms.push_back(std::make_pair((expr*)t5.get(), (expr*)saas.get()));
            ms.push_back(std::make_pair((expr*)t5.get(), (expr*)sbbs.get()));
            check_budget_sweep("x.a.x.a.x in Sig* aa Sig* & in Sig* bb Sig* (sat)", ms, l_true);
        }

        // ---- decomposing intersections -------------------------------------------------
        // A membership whose regex intersects a counting constraint with camouflage that
        // the counting constraint alone already refutes.  Under a budget too small for the
        // whole product the undivided search gives up, and only the decomposition -- which
        // decides a relaxation keeping just the counting conjuncts -- reaches the
        // contradiction.  A relaxation is a weaker problem, so its unsat verdict is the
        // original's; the test therefore also pins down that the decomposition is sound.
        std::cout << "=== seq_monadic: intersection decomposition ===\n";
        {
            // camouflage: forbid a handful of infixes.  Satisfied by every word the
            // counting conjuncts allow, so it contributes nothing but product states.
            expr_ref camo(dotstar(), m);
            char const* infixes[] = { "bab", "bba", "abb", "bbb", "aab", "aba", "bab", "abab" };
            for (char const* w : infixes)
                camo = inter(camo, comp(cat(dotstar(), cat(word(w), dotstar()))));
            expr_ref sig3(loop(dot(), 3, 3), m);
            expr_ref mod3(star(sig3), m);                   // lengths divisible by 3
            expr_ref mod3_1(cat(dot(), mod3), m);           // lengths 1 modulo 3
            vector<std::pair<expr*, expr*>> ms;
            expr_ref r0(inter(mod3, camo), m), r1(inter(mod3_1, camo), m);

            unsigned const saved_budget = m_mon.budget();
            m_mon.set_budget(8000);                         // too little for the product
            check_split("x.y.x in Sigma^3*&camo & in Sigma.Sigma^3*&camo, split off",
                        t_xyx, r0, r1, l_undef);
            m_mon.set_split_rounds(8);
            check_split("x.y.x in Sigma^3*&camo & in Sigma.Sigma^3*&camo, split on",
                        t_xyx, r0, r1, l_false);
            m_mon.set_split_rounds(0);
            m_mon.set_budget(saved_budget);
        }

        check_view_witness();
        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 brz(seq::transition_mode::brzozowski_tm);
    brz.run();
    seq_monadic_test light_ant(seq::transition_mode::light_antimirov_tm);
    light_ant.run();
}