From d1e1d6cb80b4c3ffa149c5c461d537cec3244d0b Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 20 Jul 2026 19:57:51 +0200 Subject: [PATCH] seq_monadic refactoring Bug fix in seq_monadic --- src/ast/rewriter/seq_monadic.cpp | 229 +++++++++++++++++-------------- src/ast/rewriter/seq_monadic.h | 10 +- src/test/seq_monadic.cpp | 25 ++++ 3 files changed, 156 insertions(+), 108 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index c743287e47..7987407047 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -163,28 +163,24 @@ namespace seq { if (seed[i]) out.push_back(states.get(i)); } - void split_manager::live_states(expr* R, 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; // seed: states that can accept + bool_vector maybe_null; // membership acceptance seed build_graph(R, states, succ, maybe_null, ok); if (!ok) return; - collect_backward_closure(succ, maybe_null, states, out); - } - - 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; - bool_vector reach; // seed: the target state N + if (!accept_target) { // membership: seed = nullable states + collect_backward_closure(succ, maybe_null, states, out); + return; + } + 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) == N) { reach[i] = true; found = true; break; } - if (!found) return; // N unreachable => no midpoints - collect_backward_closure(succ, reach, states, out); + 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); } // ------------------------------------------------------------------ @@ -225,6 +221,52 @@ namespace seq { 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(); @@ -253,51 +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; - - const unsigned cap = depth_cap(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]) { - switch (nullable(m_gstate[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 + auto expand = [&](unsigned st, std::vector>& out) { bool ok = true; expand_state(st, ok); - if (!ok) return l_undef; + if (!ok) return false; for (gedge 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; + 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, @@ -316,61 +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; - - const unsigned cap = depth_cap(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]) { - if (st[i] != tgt[i]) - return false; // reach component: structural target match + if (st[i] != tgt[i]) return l_false; // reach: structural target continue; } switch (nullable(st[i])) { case l_true: continue; - case l_false: return false; - case l_undef: undecided = true; return false; + case l_false: return l_false; + case l_undef: return l_undef; } } - 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)) { - emit_witness(nodes, cur, seq); - 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]); @@ -384,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) { @@ -427,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 2b286e8f6b..45dfc5ff0b 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -147,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 2af12ca6d4..d2b7b6b320 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -79,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; @@ -201,6 +211,21 @@ public: // : 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";