From 5e259943c00311381ee1843caeb88a70da04a58e Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 20 Jul 2026 20:09:46 +0200 Subject: [PATCH] Updates to seq_monadic --- src/ast/rewriter/seq_monadic.cpp | 315 +++++++++++++++++-------------- src/ast/rewriter/seq_monadic.h | 14 +- src/test/seq_monadic.cpp | 127 +++++++++++++ 3 files changed, 308 insertions(+), 148 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index be05dce203..7987407047 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -63,6 +63,11 @@ namespace seq { // global derivative-transition graph (shared / recycled across regexes) // ------------------------------------------------------------------ + lbool split_manager::nullable(expr* s) { + expr_ref nb = m_rw.is_nullable(s); + return m.is_true(nb) ? l_true : m.is_false(nb) ? l_false : l_undef; + } + unsigned split_manager::intern_state(expr* s) { unsigned id; if (m_state_id.find(s, id)) @@ -71,8 +76,7 @@ namespace seq { 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_gmaybe_null.push_back(nullable(s) != l_false); // unknown nullability => keep (conservative) m_gexpanded.push_back(false); m_gsucc.push_back(svector()); return id; @@ -131,58 +135,52 @@ namespace seq { expand_state(gid, ok); if (!ok) return; svector tgts; // snapshot: local_of may realloc m_gsucc - for (edge const& e : m_gsucc[gid]) + for (gedge const& e : m_gsucc[gid]) tgts.push_back(e.target); - for (unsigned t : tgts) - succ[i].push_back(local_of(m_gstate[t])); + for (unsigned t : tgts) { + // hoist local_of out of the subscript: it may push_back onto succ + // (reallocating it), which would dangle a succ[i] taken first. + unsigned li = local_of(m_gstate[t]); + succ[i].push_back(li); + } } } - 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]; + // Backward closure of `seed` over the transition graph `succ`: mark every + // state that can reach an already-marked one, then collect the marked states + // into `out`. `seed` is used in place as the working set. + static void collect_backward_closure(vector> const& succ, bool_vector& seed, + ptr_vector const& states, ptr_vector& out) { + const unsigned n = states.size(); for (bool ch = true; ch; ) { ch = false; for (unsigned i = 0; i < n; ++i) - if (!live[i]) + if (!seed[i]) for (unsigned j : succ[i]) - if (live[j]) { live[i] = true; ch = true; break; } + if (seed[j]) { seed[i] = true; ch = true; break; } } for (unsigned i = 0; i < n; ++i) - if (live[i]) out.push_back(states.get(i)); + if (seed[i]) out.push_back(states.get(i)); } - void split_manager::reaching_states(expr* R, expr* N, ptr_vector& out, bool& ok) { + void split_manager::reachable_states(expr* R, expr* accept_target, + ptr_vector& out, bool& ok) { ptr_vector states; vector> succ; - bool_vector maybe_null; + bool_vector maybe_null; // membership acceptance seed 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; } + if (!accept_target) { // membership: seed = nullable states + collect_backward_closure(succ, maybe_null, states, out); + return; } - for (unsigned i = 0; i < n; ++i) - if (reach[i]) out.push_back(states.get(i)); + bool_vector reach; // reach: seed = the target state N + reach.resize(states.size(), false); + bool found = false; + for (unsigned i = 0; i < states.size(); ++i) + if (states.get(i) == accept_target) { reach[i] = true; found = true; break; } + if (found) // N unreachable => no midpoints + collect_backward_closure(succ, reach, states, out); } // ------------------------------------------------------------------ @@ -207,6 +205,68 @@ namespace seq { out.push_back(e); } + // Beyond `depth_cap` elements the length no longer changes acceptance, so the + // BFS caps the depth component of its visited key there to stay finite. + static unsigned depth_cap(unsigned lo, unsigned hi) { return hi == UINT_MAX ? lo : hi; } + + // Reconstruct the per-position guard sequence of the accepting node `cur` by + // walking its parent chain and reversing. `Node` has `.parent` (int) and + // `.guard` (expr*); the root (parent < 0) contributes no guard. + template + static void emit_witness(std::vector const& nodes, int cur, expr_ref_vector& seq) { + 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]); + } + + // Shared bounded BFS with witness reconstruction, used by both the membership + // and the product intersection search. It explores states of type `State` up + // to depth `hi`, deduping on (key_of(state), min(depth, depth_cap)) so the walk + // stays finite even for hi == UINT_MAX. The callbacks abstract the two engines: + // key_of(state) -- comparable dedup key for the state + // accept(state) -> lbool -- l_true accepting / l_false not / l_undef unknown + // expand(state, out) -- append (successor, incoming-guard) pairs; return + // false on a resource limit + // Returns l_true with the per-position guard witness in `seq`, l_false, or + // l_undef (resource limit or an undecidable acceptance encountered en route). + template + static lbool bounded_search(ast_manager& m, State const& start, unsigned lo, unsigned hi, + KeyOf key_of, Accept accept, Expand expand, expr_ref_vector& seq) { + struct node { State st; unsigned depth; int parent; expr* guard; }; + std::vector nodes; + const unsigned cap = depth_cap(lo, hi); + auto vkey = [&](State const& s, unsigned d) { + return std::make_pair(key_of(s), d < cap ? d : cap); + }; + std::set visited; + nodes.push_back(node{ start, 0, -1, nullptr }); + visited.insert(vkey(start, 0)); + bool undecided = false; + for (size_t head = 0; head < nodes.size(); ++head) { + if (!m.inc()) return l_undef; + int cur = (int) head; + State st = nodes[cur].st; // copy: `nodes` may grow below + unsigned depth = nodes[cur].depth; + if (depth >= lo && depth <= hi) { + switch (accept(st)) { + case l_true: emit_witness(nodes, cur, seq); return l_true; + case l_undef: undecided = true; break; // cannot claim l_false + case l_false: break; + } + } + if (depth >= hi) + continue; // cannot extend further + std::vector> next; + if (!expand(st, next)) return l_undef; + for (auto const& [ns, g] : next) + if (visited.insert(vkey(ns, depth + 1)).second) + nodes.push_back(node{ ns, depth + 1, cur, g }); + } + return undecided ? l_undef : l_false; + } + lbool split_manager::intersect(vector const& crs, unsigned lo, unsigned hi, expr_ref_vector& seq) { seq.reset(); @@ -235,59 +295,28 @@ namespace seq { unsigned hi, expr_ref_vector& seq) { unsigned n = crs.size(); // The normalized intersection regex; the derivative engine handles guard - // feasibility and successor computation internally. + // feasibility and successor computation internally. A single (interned, + // globally cached) state is searched: acceptance is nullability, successors + // are the cached cofactor edges. 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); + auto key_of = [](unsigned st) { return st; }; + auto accept = [&](unsigned st) { + return m_gmaybe_null[st] ? nullable(m_gstate[st]) : l_false; }; - - 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 + auto expand = [&](unsigned st, std::vector>& out) { 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; + if (!ok) return false; + for (gedge const& e : m_gsucc[st]) // no interning here => m_gsucc stable + out.push_back({ e.target, e.guard }); + return true; + }; + return bounded_search(m, r0, lo, hi, key_of, accept, expand, seq); } lbool split_manager::intersect_product(vector const& crs, unsigned lo, @@ -306,65 +335,63 @@ namespace seq { 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) { + // Search state is the product tuple; acceptance is per-component (nullable + // for membership, structural target match for reach); successors are the + // cofactors of inter(st_0,...,st_{n-1}) decomposed positionally. + auto key_of = [](svector const& st) { std::vector k; - k.reserve(st.size() + 1); + k.reserve(st.size()); 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 { + auto accept = [&](svector const& st) -> lbool { 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; + if (!memb[i]) { + if (st[i] != tgt[i]) return l_false; // reach: structural target + continue; + } + switch (nullable(st[i])) { + case l_true: continue; + case l_false: return l_false; + case l_undef: return l_undef; } - else if (st[i] != tgt[i]) - return false; // reach component: structural target match } - return true; + return l_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; + // The engine prunes infeasible joint guards and yields the product successor + // as the re.inter of the per-component derivatives -- but we must NOT assume + // it keeps them in source order (mk_inter subset-collapses, De-Morgan-merges, + // and may reorder operands). So we recover the correspondence by IDENTITY: + // each operand of the joint target is matched to the component whose own + // derivative-target set contains it. A cofactor whose operands cannot be + // assigned bijectively (a merge dropped one, or the match is ambiguous) sets + // `collapsed`, softening a final l_false to l_undef -- we cannot certify + // emptiness through an edge we could not decompose. + bool collapsed = false; + auto expand = [&](svector const& st, std::vector, expr*>>& out) { + // Per-component derivative targets (order-independent recovery dictionary). + std::vector> comp_succ(n); + for (unsigned i = 0; i < n; ++i) { + expr_ref_pair_vector ci(m); + m_rw.brz_derivative_cofactors(st[i], ci); + for (auto const& [gi, ti] : ci) + if (!re().is_empty(ti)) + comp_succ[i].push_back(ti); } - if (depth >= hi) - continue; // cannot extend further + // The unique operand of `ops` that is a derivative target of component i, + // or null if none / more than one (ambiguous). + auto derivative_of = [&](unsigned i, ptr_vector const& ops) -> expr* { + expr* hit = nullptr; + for (expr* op : ops) + for (expr* ti : comp_succ[i]) + if (op == ti) { + if (hit && hit != op) return nullptr; // ambiguous + hit = op; + break; + } + return hit; + }; - // 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]); @@ -378,19 +405,24 @@ namespace seq { 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]); + nst.resize(n, nullptr); + bool ok_assign = (ops.size() == n); + for (unsigned i = 0; ok_assign && i < n; ++i) + if (!(nst[i] = derivative_of(i, ops))) + ok_assign = false; + for (unsigned i = 0; ok_assign && i < n; ++i) // require a bijection + for (unsigned j = i + 1; j < n; ++j) + if (nst[i] == nst[j]) ok_assign = false; + if (!ok_assign) { collapsed = true; continue; } } 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 }); + out.push_back({ nst, g }); } - } - return undecided ? l_undef : l_false; + return true; + }; + lbool r = bounded_search>(m, start, lo, hi, key_of, accept, expand, seq); + return (r == l_false && collapsed) ? l_undef : r; } bool split_manager::test_intersect(vector const& crs) { @@ -421,10 +453,7 @@ namespace seq { 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); + sm.reachable_states(m_R, membership ? nullptr : m_N, m_mids, ok); if (!ok) { m_failed = true; m_mids.reset(); } } diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 9875e2a077..45dfc5ff0b 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -128,6 +128,10 @@ namespace seq { seq_util& u() const { return m_rw.u(); } seq_util::rex& re() const { return m_rw.u().re; } + // Tri-state nullability of a state: l_true / l_false when the derivative + // engine decides it, l_undef when it cannot. + lbool nullable(expr* s); + // 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); @@ -143,11 +147,11 @@ namespace seq { 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); + // Derivative states reachable from R that can still reach an accepting + // state. `accept_target` == null selects membership acceptance (the seed + // is the nullable states); otherwise it is reach acceptance (the seed is + // the state structurally equal to `accept_target`, i.e. N). + void reachable_states(expr* R, expr* accept_target, 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. diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 2161ed79b5..d2b7b6b320 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -57,6 +57,9 @@ class seq_monadic_test { 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); } + expr_ref plus(expr* a) { return cat(a, star(a)); } + expr_ref inter2(expr* a, expr* b) { return expr_ref(re().mk_inter(a, b), m); } + expr_ref eps() { return expr_ref(re().mk_epsilon(m_str), m); } static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; } @@ -76,6 +79,16 @@ class seq_monadic_test { return m_sm.intersect(crs, lo, hi, wit); } + // intersection non-emptiness of two reach continuation regexes (drives the + // n>=2 product search / positional-independent operand recovery) + lbool reach2(expr* R1, expr* N1, expr* R2, expr* N2, unsigned lo, unsigned hi) { + vector crs; + crs.push_back(seq::cont_regex(expr_ref(R1, m), expr_ref(N1, m))); + crs.push_back(seq::cont_regex(expr_ref(R2, m), expr_ref(N2, 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; @@ -83,6 +96,23 @@ class seq_monadic_test { << " got=" << s(got) << " expected=" << s(expected) << "\n"; } + // Enumerate the midpoints of sigma(r); report count and whether the shared + // midpoint of each split pair agrees (left.second == right.first). + unsigned split_count(expr* r, bool& failed, bool& consistent) { + seq::split sp = m_sm.mk_split(r); + seq::split_iterator it = sp.begin(); + failed = it.failed(); + consistent = true; + unsigned count = 0; + for (; it != sp.end(); ++it) { + seq::split_pair pr = *it; + if (pr.first.second.get() != pr.second.first.get()) + consistent = false; + ++count; + } + return count; + } + 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(); @@ -115,6 +145,28 @@ public: check("L3-03 nested complement ", inter({ comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))) }, 0, UINT_MAX), l_true); + // concrete words + check("abc & abc ", inter({ word("abc"), word("abc") }, 0, UINT_MAX), l_true); + check("abc & abd ", inter({ word("abc"), word("abd") }, 0, UINT_MAX), l_false); + check("abc & S*cS* ", inter({ word("abc"), cat(sig, cat(word("c"), sig)) }, 0, UINT_MAX), l_true); + check("abc & S*zS* ", inter({ word("abc"), cat(sig, cat(word("z"), sig)) }, 0, UINT_MAX), l_false); + // epsilon vs star / plus + check("eps & a* ", inter({ eps(), star(a) }, 0, UINT_MAX), l_true); + check("eps & a+ ", inter({ eps(), plus(a) }, 0, UINT_MAX), l_false); + check("a+ & a* ", inter({ plus(a), star(a) }, 0, UINT_MAX), l_true); + // unions + check("(a|b) & (b|c) ", inter({ alt(a, b), alt(b, word("c")) }, 0, UINT_MAX), l_true); + check("(a|b) & (c|d) ", inter({ alt(a, b), alt(word("c"), word("d")) }, 0, UINT_MAX), l_false); + // complement fundamentals + check("~empty (= S*) ", inter({ comp(none()) }, 0, UINT_MAX), l_true); + check("~(a*) ", inter({ comp(star(a)) }, 0, UINT_MAX), l_true); + check("(a|b)* & ~((a|b)*) ", inter({ star(alt(a, b)), comp(star(alt(a, b))) }, 0, UINT_MAX), l_false); + check("a* & ~(a*) ", inter({ star(a), comp(star(a)) }, 0, UINT_MAX), l_false); + check("~(a*) | a* (= S*) ", inter({ alt(comp(star(a)), star(a)) }, 0, UINT_MAX), l_true); + // three-way intersections + check("a* & (a|b)* & S*aS* ", inter({ star(a), star(alt(a, b)), cat(sig, cat(a, sig)) }, 0, UINT_MAX), l_true); + check("a* & b* & S*aS* ", inter({ star(a), star(b), cat(sig, cat(a, sig)) }, 0, UINT_MAX), l_false); + 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); @@ -122,6 +174,22 @@ public: 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); + check("(a|b) len 1 ", inter({ alt(a, b) }, 1, 1), l_true); + check("(a|b) len 2 ", inter({ alt(a, b) }, 2, 2), l_false); + check("abc len 3 ", inter({ word("abc") }, 3, 3), l_true); + check("abc len 2 ", inter({ word("abc") }, 2, 2), l_false); + check("a* len 0 ", inter({ star(a) }, 0, 0), l_true); + // parity / counting via periodic stars + check("(aa)* len 2 ", inter({ star(cat(a, a)) }, 2, 2), l_true); + check("(aa)* len 3 ", inter({ star(cat(a, a)) }, 3, 3), l_false); + check("(aa)* len 4 ", inter({ star(cat(a, a)) }, 4, 4), l_true); + check("(aa)* & (aaa)* len 6 ", inter({ star(cat(a, a)), star(cat(a, cat(a, a))) }, 6, 6), l_true); + check("(aa)* & (aaa)* len 3 ", inter({ star(cat(a, a)), star(cat(a, cat(a, a))) }, 3, 3), l_false); + // length must both admit an 'a' and stay empty-word: contradiction at len 0 + check("a* & S*aS* len 0 ", inter({ star(a), cat(sig, cat(a, sig)) }, 0, 0), l_false); + check("[0-9]{2,4} len 3 ", inter({ loop(rng('0','9'), 2, 4) }, 3, 3), l_true); + check("[0-9]{2,4} len 5 ", inter({ loop(rng('0','9'), 2, 4) }, 5, 5), l_false); + check("[0-9]{2,4} len 1 ", inter({ loop(rng('0','9'), 2, 4) }, 1, 1), l_false); std::cout << "=== split_manager::intersect (reach, general N) ===\n"; { @@ -133,6 +201,31 @@ public: // : reached exactly after consuming one element check(" len1 ", reach(aSig, sig, 1, 1), l_true); check(" len0 ", reach(aSig, sig, 0, 0), l_false); + // via a self-loop: still on target after one step + check(" len1 ", reach(sig, sig, 1, 1), l_true); + // : a* is its own 'a'-derivative (fixpoint state) + check(" len0 ", reach(star(a), star(a), 0, 0), l_true); + check(" len1 ", reach(star(a), star(a), 1, 1), l_true); + // : the empty word already sits on the target + check(" len0 ", reach(none(), none(), 0, 0), l_true); + // : after the first 'a' the state is the S* fixpoint, so it + // stays on target for every further element (reachable at len2 too) + check(" len2 ", reach(aSig, sig, 2, 2), l_true); + + // --- n>=2 product search --- + expr_ref c = word("c"); + // both : on target already at depth 0 (accept before expansion) + check("& len0 ", reach2(sig, sig, sig, sig, 0, 0), l_true); + // & : no single word reaches both targets (first + // element cannot be both a and b) -> empty + check("& ", reach2(cat(a, sig), sig, cat(b, sig), sig, 0, UINT_MAX), l_false); + // Distinct, incomparable component derivatives (b.S* vs c.S*) force the + // joint target inter(b.S*, c.S*) to keep BOTH operands -> exercises the + // identity-based operand-to-component recovery (order independence). + expr_ref R1 = cat(a, cat(b, sig)); // a.b.S* -> d_a = b.S* + expr_ref R2 = cat(a, cat(c, sig)); // a.c.S* -> d_a = c.S* + check("& l1", reach2(R1, cat(b, sig), R2, cat(c, sig), 1, 1), l_true); + check("& l0", reach2(R1, cat(b, sig), R2, cat(c, sig), 0, 0), l_false); } std::cout << "=== split_manager::test_intersect ===\n"; @@ -142,6 +235,18 @@ public: 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); + + // one-sided: a+ and b+ are disjoint but neither is *syntactically* + // empty, so the cheap check does NOT detect it (allowed false positive) + vector disjoint; + disjoint.push_back(m_sm.embed(plus(a))); + disjoint.push_back(m_sm.embed(plus(b))); + check("test_intersect a+,b+ ", m_sm.test_intersect(disjoint) ? l_true : l_false, l_true); + + // concat(empty, a) normalizes to the empty regex → detected + vector normempty; + normempty.push_back(m_sm.embed(cat(none(), a))); + check("test_intersect empty-concat", m_sm.test_intersect(normempty) ? l_true : l_false, l_false); } std::cout << "=== split midpoint iterator ===\n"; @@ -159,6 +264,28 @@ public: 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); } + { + bool failed, consistent; + unsigned c; + // empty regex: no live states, so no midpoints (and not a failure) + c = split_count(none(), failed, consistent); + check("split(empty) not failed ", failed ? l_true : l_false, l_false); + check("split(empty) 0 midpoints ", c == 0 ? l_true : l_false, l_true); + // finite word: at least one live midpoint, all pairs consistent + c = split_count(word("a"), failed, consistent); + check("split(a) not failed ", failed ? l_true : l_false, l_false); + check("split(a) >=1 midpoint ", c >= 1 ? l_true : l_false, l_true); + check("split(a) consistent ", consistent ? l_true : l_false, l_true); + // epsilon: the (single, nullable) start state is a live midpoint + c = split_count(eps(), failed, consistent); + check("split(eps) not failed ", failed ? l_true : l_false, l_false); + check("split(eps) >=1 midpoint ", c >= 1 ? l_true : l_false, l_true); + // ground finite word a.b.c (concat form): several live midpoints + c = split_count(cat(a, cat(b, word("c"))), failed, consistent); + check("split(a.b.c) not failed ", failed ? l_true : l_false, l_false); + check("split(a.b.c) >=1 midpoint ", c >= 1 ? l_true : l_false, l_true); + check("split(a.b.c) consistent ", consistent ? l_true : l_false, l_true); + } std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " (" << m_fail << " fail) ===\n";