From b616f714add439e7b881216c32bfea8aabbda267 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Jul 2026 12:08:35 -0700 Subject: [PATCH] Add continuation-regex split service (seq_monadic) Port seq_monadic to the split_set branch, reimplemented against the cont_regex / split / split_manager API. Element-sort agnostic: relies on the derivative engine and th_rewriter, no character-specific reasoning. - Global derivative-transition graph reused across regexes (intern_state / expand_state / build_graph) so states, nullability and cofactor successors are computed once. - embed(r) = ; the epsilon accept-state marks the membership (nullable) case uniformly. - intersect handles general cont_regex, including non-epsilon reach targets N (membership BFS + product-reachability paths). - No budget / reset_pin. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 34aa9af0-4977-411d-aaa7-7cb81cc4e9f8 --- src/ast/rewriter/CMakeLists.txt | 1 + src/ast/rewriter/seq_monadic.cpp | 425 +++++++++++++++++++++++++++++++ src/ast/rewriter/seq_monadic.h | 199 +++++++++++++++ src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/seq_monadic.cpp | 174 +++++++++++++ 6 files changed, 801 insertions(+) create mode 100644 src/ast/rewriter/seq_monadic.cpp create mode 100644 src/ast/rewriter/seq_monadic.h create mode 100644 src/test/seq_monadic.cpp diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index df06cedfe3..9f4d7fe436 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -40,6 +40,7 @@ z3_add_component(rewriter seq_axioms.cpp seq_eq_solver.cpp seq_derive.cpp + seq_monadic.cpp seq_subset.cpp seq_split.cpp seq_derive.cpp diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp new file mode 100644 index 0000000000..4af73793eb --- /dev/null +++ b/src/ast/rewriter/seq_monadic.cpp @@ -0,0 +1,425 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.cpp + +Abstract: + + Continuation-regex split service and intersection non-emptiness. See + seq_monadic.h. + + Automaton-based (product/derivative reachability) and element-sort agnostic: + guard feasibility and successor states are computed entirely by the symbolic + derivative engine (seq_rewriter::brz_derivative_cofactors, which prunes + infeasible guards internally), so there is no character-specific reasoning in + this module. A single global derivative-transition graph is grown lazily and + recycled across every regex, so no derivative is computed twice. th_rewriter is + used to normalize the intersection regex. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ + +#include "ast/rewriter/seq_monadic.h" +#include +#include +#include + +namespace seq { + + // ------------------------------------------------------------------ + // global derivative-transition graph (shared / recycled across regexes) + // ------------------------------------------------------------------ + + unsigned split_manager::intern_state(expr* s) { + unsigned id; + if (m_state_id.find(s, id)) + return id; // recycle the global state + id = m_gstate.size(); + m_state_id.insert(s, id); + m_gstate.push_back(s); + m_pin.push_back(s); + expr_ref nb = m_rw.is_nullable(s); + m_gmaybe_null.push_back(!m.is_false(nb)); // unknown nullability => keep (conservative) + m_gexpanded.push_back(false); + m_gsucc.push_back(svector()); + return id; + } + + void split_manager::expand_state(unsigned i, bool& ok) { + ok = true; + if (m_gexpanded[i]) + return; // successors already computed once + if (!m.inc()) { ok = false; return; } + expr* s = m_gstate[i]; // captured before any interning realloc + expr_ref_pair_vector cof(m); + m_rw.brz_derivative_cofactors(s, cof); + svector edges; + for (auto const& [g, t] : cof) { + if (re().is_empty(t)) continue; // engine already pruned infeasible guards + unsigned k = intern_state(t); // may realloc m_gsucc: collect edges first + m_pin.push_back(g); + edges.push_back(gedge{ g, k }); + } + for (gedge const& e : edges) // m_gsucc stable now (no more interning) + m_gsucc[i].push_back(e); + m_gexpanded[i] = true; + } + + // ------------------------------------------------------------------ + // live-state / reachability machinery (projected out of the global graph) + // ------------------------------------------------------------------ + + void split_manager::build_graph(expr* R, ptr_vector& states, + vector>& succ, + bool_vector& maybe_null, bool& ok) { + ok = true; + states.reset(); + succ.reset(); + maybe_null.reset(); + obj_map local; // state expr -> local index + svector l2g; // local index -> global id + auto local_of = [&](expr* s) -> unsigned { + unsigned li; + if (local.find(s, li)) return li; + unsigned gid = intern_state(s); + li = states.size(); + local.insert(s, li); + l2g.push_back(gid); + states.push_back(s); + maybe_null.push_back(m_gmaybe_null[gid]); + succ.push_back(svector()); + return li; + }; + local_of(R); + const unsigned STATE_CAP = 1u << 12; + for (unsigned i = 0; i < states.size(); ++i) { + if (states.size() > STATE_CAP || !m.inc()) { ok = false; return; } + unsigned gid = l2g[i]; + expand_state(gid, ok); + if (!ok) return; + svector tgts; // snapshot: local_of may realloc m_gsucc + for (edge const& e : m_gsucc[gid]) + tgts.push_back(e.target); + for (unsigned t : tgts) + succ[i].push_back(local_of(m_gstate[t])); + } + } + + void split_manager::live_states(expr* R, ptr_vector& out, bool& ok) { + ptr_vector states; + vector> succ; + bool_vector maybe_null; + build_graph(R, states, succ, maybe_null, ok); + if (!ok) return; + 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)); + } + + void split_manager::reaching_states(expr* R, expr* N, ptr_vector& out, bool& ok) { + ptr_vector states; + vector> succ; + bool_vector maybe_null; + build_graph(R, states, succ, maybe_null, ok); + if (!ok) return; + unsigned n = states.size(); + unsigned tgt = UINT_MAX; + for (unsigned i = 0; i < n; ++i) + if (states.get(i) == N) { tgt = i; break; } + if (tgt == UINT_MAX) return; // N unreachable => no midpoints + bool_vector reach; + reach.resize(n, false); + reach[tgt] = true; + for (bool ch = true; ch; ) { + ch = false; + for (unsigned i = 0; i < n; ++i) + if (!reach[i]) + for (unsigned j : succ[i]) + if (reach[j]) { reach[i] = true; ch = true; break; } + } + for (unsigned i = 0; i < n; ++i) + if (reach[i]) out.push_back(states.get(i)); + } + + // ------------------------------------------------------------------ + // intersection non-emptiness + // ------------------------------------------------------------------ + + // A component is a membership (nullable) component when N_i is null or + // the epsilon regex; otherwise it is a reach component with structural target N_i. + static bool is_membership(seq_util::rex& re, cont_regex const& cr) { + expr* N = cr.second.get(); + return N == nullptr || re.is_epsilon(N); + } + + // Flatten the operands of a (possibly nested) re.inter into `out`. + static void flatten_inter(seq_util::rex& re, expr* e, ptr_vector& out) { + expr* a = nullptr, * b = nullptr; + if (re.is_intersection(e, a, b)) { + flatten_inter(re, a, out); + flatten_inter(re, b, out); + } + else + out.push_back(e); + } + + lbool split_manager::intersect(vector const& crs, unsigned lo, unsigned hi, + expr_ref_vector& seq) { + seq.reset(); + unsigned n = crs.size(); + if (n == 0) { + // universal language: contains a word of every length; non-empty iff lo <= hi + if (lo > hi) return l_false; + for (unsigned k = 0; k < lo; ++k) + seq.push_back(m.mk_true()); // trivial guard: any element admissible + return l_true; + } + // Fast, robust path when every component is a membership (nullable) component: + // the intersection is non-empty iff some reachable product state is nullable. + bool all_memb = true; + for (auto const& cr : crs) + if (!is_membership(re(), cr)) { all_memb = false; break; } + if (all_memb) + return intersect_membership(crs, lo, hi, seq); + + // General case: a tuple product search that also handles reach targets + // N != epsilon via structural target matching. + return intersect_product(crs, lo, hi, seq); + } + + lbool split_manager::intersect_membership(vector const& crs, unsigned lo, + unsigned hi, expr_ref_vector& seq) { + unsigned n = crs.size(); + // The normalized intersection regex; the derivative engine handles guard + // feasibility and successor computation internally. + expr_ref P(crs[0].first.get(), m); + for (unsigned i = 1; i < n; ++i) + P = re().mk_inter(P, crs[i].first.get()); + m_th(P); + unsigned r0 = intern_state(P.get()); + + // Search node with witness reconstruction: `guard` is the derivative path + // condition on the incoming edge (a predicate over the element (:var 0)). + struct node { unsigned st; unsigned depth; int parent; expr* guard; }; + std::vector nodes; + + // Beyond `cap` elements the length no longer changes acceptance, so we cap + // the depth in the visited key to keep the state space finite. + unsigned cap = (hi == UINT_MAX) ? lo : hi; + auto key = [&](unsigned st, unsigned depth) { + return std::make_pair(st, depth < cap ? depth : cap); + }; + + std::set> visited; + nodes.push_back(node{ r0, 0, -1, nullptr }); + visited.insert(key(r0, 0)); + + bool undecided = false; + for (size_t head = 0; head < nodes.size(); ++head) { + if (!m.inc()) return l_undef; + int cur = (int) head; + unsigned st = nodes[cur].st; // note: `nodes` may grow below + unsigned depth = nodes[cur].depth; + + if (depth >= lo && depth <= hi && m_gmaybe_null[st]) { + expr_ref nb = m_rw.is_nullable(m_gstate[st]); + if (m.is_true(nb)) { + ptr_vector gs; + for (int j = cur; j >= 0 && nodes[j].parent >= 0; j = nodes[j].parent) + gs.push_back(nodes[j].guard); + for (unsigned k = gs.size(); k-- > 0; ) + seq.push_back(gs[k]); + return l_true; + } + if (!m.is_false(nb)) + undecided = true; // undecidable nullability => cannot claim l_false + } + if (depth >= hi) + continue; // cannot extend further + bool ok = true; + expand_state(st, ok); + if (!ok) return l_undef; + for (edge const& e : m_gsucc[st]) // no interning here => m_gsucc stable + if (visited.insert(key(e.target, depth + 1)).second) + nodes.push_back(node{ e.target, depth + 1, cur, e.guard }); + } + return undecided ? l_undef : l_false; + } + + lbool split_manager::intersect_product(vector const& crs, unsigned lo, + unsigned hi, expr_ref_vector& seq) { + unsigned n = crs.size(); + + bool_vector memb; // per component: membership (nullable) vs reach + ptr_vector tgt; // per component: reach target (or null) + svector start; // start tuple + for (auto const& cr : crs) { + bool mb = is_membership(re(), cr); + memb.push_back(mb); + tgt.push_back(mb ? nullptr : cr.second.get()); + start.push_back(cr.first.get()); + m_pin.push_back(cr.first.get()); + if (!mb) m_pin.push_back(cr.second.get()); + } + + // Search node: a product tuple, its depth, its parent, and the joint guard on + // the incoming edge (a predicate over the element variable (:var 0)). + struct node { svector st; unsigned depth; int parent; expr* guard; }; + std::vector nodes; + + // Beyond `cap` elements the length no longer changes acceptance, so we cap the + // depth in the visited key to keep the state space finite. + unsigned cap = (hi == UINT_MAX) ? lo : hi; + auto key = [&](svector const& st, unsigned depth) { + std::vector k; + k.reserve(st.size() + 1); + for (expr* e : st) k.push_back(e->get_id()); + k.push_back(depth < cap ? depth : cap); + return k; + }; + + auto is_accept = [&](svector const& st, bool& undecided) -> bool { + for (unsigned i = 0; i < n; ++i) { + if (memb[i]) { + expr_ref nb = m_rw.is_nullable(st[i]); + if (m.is_true(nb)) continue; + if (m.is_false(nb)) return false; + undecided = true; return false; + } + else if (st[i] != tgt[i]) + return false; // reach component: structural target match + } + return true; + }; + + std::set> visited; + nodes.push_back(node{ start, 0, -1, nullptr }); + visited.insert(key(start, 0)); + + bool undecided = false; + for (size_t head = 0; head < nodes.size(); ++head) { + if (!m.inc()) return l_undef; + int cur = (int) head; + svector st = nodes[cur].st; // copy: `nodes` may grow below + unsigned depth = nodes[cur].depth; + + if (depth >= lo && depth <= hi) { + bool u2 = false; + if (is_accept(st, u2)) { + ptr_vector gs; // reconstruct the per-position guards + for (int j = cur; j >= 0 && nodes[j].parent >= 0; j = nodes[j].parent) + gs.push_back(nodes[j].guard); + for (unsigned k = gs.size(); k-- > 0; ) + seq.push_back(gs[k]); + return l_true; + } + if (u2) undecided = true; + } + if (depth >= hi) + continue; // cannot extend further + + // Joint transitions: cofactors of inter(st_0,...,st_{n-1}). The engine + // prunes infeasible joint guards and yields the product successor as an + // re.inter in source order, which we decompose positionally. + expr_ref P(st[0], m); + for (unsigned i = 1; i < n; ++i) + P = re().mk_inter(P, st[i]); + expr_ref_pair_vector cof(m); + m_rw.brz_derivative_cofactors(P, cof); + for (auto const& [g, t] : cof) { + if (re().is_empty(t)) continue; + svector nst; + if (n == 1) + nst.push_back(t); + else { + ptr_vector ops; + flatten_inter(re(), t, ops); + if (ops.size() != n) { // engine collapsed the product: give up soundly + undecided = true; + continue; + } + for (unsigned i = 0; i < n; ++i) nst.push_back(ops[i]); + } + for (expr* s : nst) m_pin.push_back(s); + m_pin.push_back(g); + if (visited.insert(key(nst, depth + 1)).second) + nodes.push_back(node{ nst, depth + 1, cur, g }); + } + } + return undecided ? l_undef : l_false; + } + + bool split_manager::test_intersect(vector const& crs) { + // one-sided cheap check: an obviously-empty start (or reach target) state + // certainly makes the intersection empty. Normalize via th_rewriter first so + // that e.g. concat(empty, epsilon) collapses to the empty regex. + expr_ref tmp(m); + for (auto const& cr : crs) { + m_th(cr.first, tmp); + if (re().is_empty(tmp)) + return false; + if (cr.second.get()) { + m_th(cr.second, tmp); + if (re().is_empty(tmp)) + return false; + } + } + return true; + } + + // ------------------------------------------------------------------ + // seq::split / seq::split_iterator + // ------------------------------------------------------------------ + + split_iterator::split_iterator(split_manager& sm, cont_regex const& cr) { + m_sm = &sm; + m_R = cr.first.get(); + m_N = cr.second.get(); + bool ok = true; + bool membership = (m_N == nullptr) || sm.re().is_epsilon(m_N); + if (membership) + sm.live_states(m_R, m_mids, ok); + else + sm.reaching_states(m_R, m_N, m_mids, ok); + if (!ok) { m_failed = true; m_mids.reset(); } + } + + split_pair split_iterator::operator*() const { + ast_manager& m = m_sm->mgr(); + expr* mid = m_mids[m_pos]; + cont_regex left(expr_ref(m_R, m), expr_ref(mid, m)); + cont_regex right(expr_ref(mid, m), m_N ? expr_ref(m_N, m) : expr_ref(m)); + return split_pair(left, right); + } + + split_iterator& split_iterator::operator++() { + if (m_pos < m_mids.size()) ++m_pos; + return *this; + } + + split::split(split_manager& sm, expr* r) + : m_sm(sm), m_R(r, sm.mgr()), m_N(sm.mgr()) {} + + split::split(split_manager& sm, cont_regex const& cr) + : m_sm(sm), m_R(cr.first), m_N(cr.second) {} + + split_iterator split::begin() { + return split_iterator(m_sm, cont_regex(m_R, m_N)); + } +} diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h new file mode 100644 index 0000000000..9875e2a077 --- /dev/null +++ b/src/ast/rewriter/seq_monadic.h @@ -0,0 +1,199 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.h + +Abstract: + + Continuation-regex split service and intersection non-emptiness for regular + expressions, following the design sketched in + paper/bench/eval/monadic-vs-nielsen-eval.md. + + * A continuation regex (seq::cont_regex) is a pair of regexes. R is + the start state and N is the accept state. A word w is accepted iff + delta_w(R) == N, with one distinguished case: when N is the epsilon regex + (the regex accepting the empty sequence) acceptance is ordinary membership + w in L(R), i.e. delta_w(R) is nullable. This is because the Brzozowski + derivative folds the epsilon tail into nullability (the epsilon state is not + structurally reachable for looping nullable regexes). Every regex R is + embedded as the continuation regex . + + * seq::split exposes, for a continuation regex, an (opaque) iterator of + seq::split_pair splits: uv in ==> u in /\ v in , + where R' ranges over the live cofactors of R that can still reach N. + + * seq::split_manager owns the live-state / reachability machinery shared across + regexes, and decides emptiness of an intersection of continuation regexes. + It maintains one global derivative-transition graph and recycles the states + (and their computed nullability / cofactor successors) across every regex it + processes, so the same derivative is never recomputed. + + The module is element-sort agnostic: it does NOT hard-code any character + reasoning. Guard feasibility and successor computation are delegated entirely + to the symbolic derivative engine (seq_rewriter::brz_derivative_cofactors, which + prunes infeasible guards internally and, on an re.inter, yields the product + successor in source order) and to th_rewriter for normalization. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ +#pragma once + +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/th_rewriter.h" +#include "util/lbool.h" +#include "util/obj_hashtable.h" +#include "util/vector.h" +#include + +namespace seq { + + // A continuation regex : start state R, accept state N. A word w is + // accepted iff delta_w(R) == N. When N is the epsilon regex (or null), the + // accept condition is ordinary membership (delta_w(R) is nullable). + typedef std::pair cont_regex; + + // A split of uv in into u in and v in . + typedef std::pair split_pair; + + class split_manager; + + // Opaque, lazy iterator over the splits of a continuation regex. The internal + // state (the enumerated midpoints R') is computed on construction. `failed()` + // reports a non-ground regex or a resource limit reached while computing + // derivatives. + class split_iterator { + friend class split; + split_manager* m_sm = nullptr; + expr* m_R = nullptr; // start state of the continuation regex + expr* m_N = nullptr; // accept state (epsilon/null => membership) + ptr_vector m_mids; // enumerated live midpoints R' + unsigned m_pos = 0; // current midpoint index + bool m_failed = false; // non-ground regex / resource limit + + split_iterator(split_manager& sm, cont_regex const& cr); // begin + + bool at_end() const { return m_failed || m_pos >= m_mids.size(); } + + public: + split_iterator() = default; // end sentinel + + split_pair operator*() const; + split_iterator& operator++(); + bool operator==(split_iterator const& other) const { return at_end() && other.at_end(); } + bool operator!=(split_iterator const& other) const { return !(*this == other); } + bool failed() const { return m_failed; } + }; + + // A continuation regex together with the manager that can split it. + class split { + split_manager& m_sm; + expr_ref m_R; + expr_ref m_N; + public: + split(split_manager& sm, expr* r); + split(split_manager& sm, cont_regex const& cr); + split_iterator begin(); + split_iterator end() { return split_iterator(); } + }; + + // Manages live states / abstract reachability across the regexes it processes, + // and decides emptiness of intersections of continuation regexes. One global + // derivative-transition graph is grown lazily and shared across every regex, so + // states, their nullability and their cofactor successors are computed once. + class split_manager { + friend class split; + friend class split_iterator; + + // A cofactor transition of the global graph: on a guard (a predicate over the + // element variable (:var 0)) the derivative moves to the target state. + struct gedge { expr* guard; unsigned target; }; + + ast_manager& m; + seq_rewriter& m_rw; + th_rewriter m_th; // regex normalization (element-sort agnostic) + expr_ref_vector m_pin; // keeps interned states / guards alive + + // Global reachability graph, reused across every processed regex. + obj_map m_state_id; // regex state -> global id + ptr_vector m_gstate; // global id -> state + bool_vector m_gmaybe_null; // per state: !is_false(is_nullable) + bool_vector m_gexpanded; // per state: cofactor successors computed + vector> m_gsucc; // per state: (guard, target) edges + + seq_util& u() const { return m_rw.u(); } + seq_util::rex& re() const { return m_rw.u().re; } + + // Intern a state into the global graph (recycles an existing global state), + // computing its nullability lazily. Returns its global id. + unsigned intern_state(expr* s); + + // Compute (once) the cofactor successors of the global state `i`, recycling + // any target states already present in the graph. Sets `ok` false on a + // resource limit. + void expand_state(unsigned i, bool& ok); + + // Reachable derivative states of R with their transition graph and per-state + // (possible) nullability, projected out of the global graph. Sets `ok` false + // on cap overrun / resource limit. + void build_graph(expr* R, ptr_vector& states, + vector>& succ, bool_vector& maybe_null, bool& ok); + + // Live reachable derivative states of R (can reach a nullable state). + void live_states(expr* R, ptr_vector& out, bool& ok); + + // Reachable derivative states of R from which the state N is reachable. + void reaching_states(expr* R, expr* N, ptr_vector& out, bool& ok); + + // Non-emptiness of an all-membership intersection: BFS over the normalized + // product state inter(R_0,...,R_{n-1}) with an is_nullable acceptance test. + lbool intersect_membership(vector const& crs, unsigned lo, unsigned hi, + expr_ref_vector& seq); + + // Product-reachability of a tuple of continuation regexes (handles general N, + // i.e. reach targets N != epsilon), decomposing the engine's product successor. + lbool intersect_product(vector const& crs, unsigned lo, unsigned hi, + expr_ref_vector& seq); + + public: + split_manager(seq_rewriter& rw) + : m(rw.m()), m_rw(rw), m_th(rw.m()), m_pin(rw.m()) {} + + ast_manager& mgr() const { return m; } + seq_rewriter& rw() const { return m_rw; } + + void pin(expr* e) { m_pin.push_back(e); } + + // Embed a regex R as the continuation regex . The + // epsilon accept-state marks the membership (nullable) case uniformly. + cont_regex embed(expr* r) { + sort* ss = nullptr; + VERIFY(u().is_re(r, ss)); + expr_ref eps(re().mk_epsilon(ss), m); + expr_ref start(re().mk_concat(r, eps), m); + return cont_regex(start, eps); + } + + split mk_split(expr* r) { return split(*this, r); } + split mk_split(cont_regex const& cr) { return split(*this, cr); } + + // Emptiness of the intersection of the continuation regexes `crs`, restricted + // to words of at least `lo` and at most `hi` elements (hi == UINT_MAX for no + // upper bound). A component accepts a word w iff delta_w(R_i) == N_i, + // where an epsilon (or null) N_i means the nullable/membership case. Feasibility + // is decided by the derivative engine (element-sort agnostic). On l_true a + // witness is returned in `seq`: one guard predicate over (:var 0) per position. + // l_false = empty, l_true = non-empty, l_undef = gave up + // (cap overrun, undecidable nullability, or a product target that could not + // be decomposed). + lbool intersect(vector const& crs, unsigned lo, unsigned hi, expr_ref_vector& seq); + + // Cheap, sound one-sided partial check: false only when the intersection is + // certainly empty; true otherwise (may be a false positive). + bool test_intersect(vector const& crs); + }; +} diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 4563752812..ce93b91339 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -25,6 +25,7 @@ add_executable(test-z3 parametric_datatype.cpp arith_rewriter.cpp seq_rewriter.cpp + seq_monadic.cpp arith_simplifier_plugin.cpp ast.cpp bdd.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 3a3cab41db..8f55cdbb1a 100644 --- a/src/test/main.cpp +++ b/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) \ diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp new file mode 100644 index 0000000000..2161ed79b5 --- /dev/null +++ b/src/test/seq_monadic.cpp @@ -0,0 +1,174 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.cpp + +Abstract: + + Unit tests for the continuation-regex split service in + ast/rewriter/seq_monadic.{h,cpp}: seq::split_manager::intersect (element-sort + agnostic intersection non-emptiness, decided by the derivative engine) and the + seq::split midpoint iterator. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ + +#include "ast/ast.h" +#include "ast/reg_decl_plugins.h" +#include "ast/seq_decl_plugin.h" +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_monadic.h" +#include +#include + +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::split_manager m_sm; + 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 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 none() { return expr_ref(re().mk_empty(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); } + + static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; } + + // intersection non-emptiness of the given membership regexes, words of length in [lo,hi] + lbool inter(std::initializer_list rs, unsigned lo, unsigned hi) { + vector crs; + for (expr* r : rs) crs.push_back(m_sm.embed(r)); + expr_ref_vector wit(m); + return m_sm.intersect(crs, lo, hi, wit); + } + + // intersection non-emptiness of a single reach continuation regex + lbool reach(expr* R, expr* N, unsigned lo, unsigned hi) { + vector crs; + crs.push_back(seq::cont_regex(expr_ref(R, m), expr_ref(N, m))); + expr_ref_vector wit(m); + return m_sm.intersect(crs, lo, hi, wit); + } + + void check(char const* name, lbool got, lbool expected) { + 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_sm(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 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* + expr_ref digitp = cat(rng('0', '9'), star(rng('0', '9'))); // [0-9]+ + + std::cout << "=== split_manager::intersect (membership) ===\n"; + + check("Sigma* ", inter({ sig }, 0, UINT_MAX), l_true); + check("empty regex ", inter({ none() }, 0, UINT_MAX), l_false); + check("~Sigma* ", inter({ comp(sig) }, 0, UINT_MAX), l_false); + // a* & b* = { epsilon } + check("a* & b* (any length) ", inter({ star(a), star(b) }, 0, UINT_MAX), l_true); + check("a* & b* (>= 1 char) ", inter({ star(a), star(b) }, 1, UINT_MAX), l_false); + // Sigma*aaSigma* & Sigma*bbSigma* has a common word (e.g. aabb) + check("SaaS & SbbS ", inter({ saas, sbbs }, 0, UINT_MAX), l_true); + // (a|b)* intersect ~(SaaS) intersect ~(SbbS) is non-empty (alternating words) + check("(a|b)* & ~SaaS & ~SbbS ", + inter({ star(alt(a, b)), comp(saas), comp(sbbs) }, 0, UINT_MAX), l_true); + // nested complement (L3-03) non-empty + check("L3-03 nested complement ", + inter({ comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))) }, 0, UINT_MAX), l_true); + + std::cout << "=== split_manager::intersect (length bounds) ===\n"; + check("[0-9]+ length 0..0 ", inter({ digitp }, 0, 0), l_false); + check("[0-9]+ length 1..1 ", inter({ digitp }, 1, 1), l_true); + check("a* length 2..2 ", inter({ star(a) }, 2, 2), l_true); + check("a* & b* length 3..3 ", inter({ star(a), star(b) }, 3, 3), l_false); + check("[0-9]{2} & [0-9]+ len 2 ", inter({ loop(rng('0','9'), 2, 2), digitp }, 2, 2), l_true); + check("[0-9]{2} len 3 ", inter({ loop(rng('0','9'), 2, 2) }, 3, 3), l_false); + + std::cout << "=== split_manager::intersect (reach, general N) ===\n"; + { + expr_ref aSig = cat(a, sig); // a . Sigma* + // : delta_epsilon(Sigma*) == Sigma* already at depth 0 + check(" len0 ", reach(sig, sig, 0, UINT_MAX), l_true); + // : Sigma* never derives to the empty regex + check(" ", reach(sig, none(), 0, UINT_MAX), l_false); + // : reached exactly after consuming one element + check(" len1 ", reach(aSig, sig, 1, 1), l_true); + check(" len0 ", reach(aSig, sig, 0, 0), l_false); + } + + std::cout << "=== split_manager::test_intersect ===\n"; + { + vector good, bad; + good.push_back(m_sm.embed(sig)); + bad.push_back(m_sm.embed(none())); + check("test_intersect Sigma* ", m_sm.test_intersect(good) ? l_true : l_false, l_true); + check("test_intersect empty ", m_sm.test_intersect(bad) ? l_true : l_false, l_false); + } + + std::cout << "=== split midpoint iterator ===\n"; + { + seq::split sp = m_sm.mk_split(star(alt(a, b))); + seq::split_iterator it = sp.begin(); + bool failed = it.failed(); + unsigned count = 0; + for (; it != sp.end(); ++it) { + seq::split_pair pr = *it; + // left = , right = : the shared midpoint agrees + if (pr.first.second.get() != pr.second.first.get()) ++m_fail; + ++count; + } + check("(a|b)* split not failed ", failed ? l_true : l_false, l_false); + check("(a|b)* has >=1 midpoint ", count > 0 ? l_true : l_false, 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(); +}