diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index afe18ad3f3..5dd3e2e578 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -48,6 +48,7 @@ z3_add_component(rewriter seq_range_predicate.cpp seq_rewriter.cpp seq_regex_bisim.cpp + seq_regex_live.cpp seq_skolem.cpp term_enumeration.cpp th_rewriter.cpp diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 1876f4ddfb..b04516de63 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -39,7 +39,8 @@ namespace seq { m_br(m), m_re(re), m_trail(m), - m_cofactor_cache(m), + m_brz_cofactor_cache(m), + m_ant_cofactor_cache(m), m_ele(m), m_path_expr(m) { m_br.set_flat_and_or(false); @@ -1572,15 +1573,18 @@ namespace seq { } expr_ref_pair_vector const &derive::get_cached_cofactors(transition_mode mode, expr *r) { + cofactor_cache& cache = + mode == transition_mode::light_antimirov_tm ? + m_ant_cofactor_cache : m_brz_cofactor_cache; expr_ref_pair_vector *v = nullptr; - if (m_cofactor_cache.find(r, v)) + if (cache.find(r, v)) return *v; v = alloc(expr_ref_pair_vector, m); if (mode == transition_mode::light_antimirov_tm) light_ant_derivative_cofactors(r, *v); else derivative_cofactors(r, *v); - m_cofactor_cache.insert(r, v); // takes ownership of v and pins the key r + cache.insert(r, v); // takes ownership of v and pins the key r return *v; } @@ -1659,4 +1663,3 @@ namespace seq { } } - diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index 46ec0157fe..1a91b9e2e7 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/src/ast/rewriter/seq_derive.h @@ -95,7 +95,8 @@ namespace seq { obj_pair_map m_atop_cache, m_btop_cache; // post-simplify cache expr_ref_vector m_trail; // pin cached results - cofactor_cache m_cofactor_cache; + cofactor_cache m_brz_cofactor_cache; + cofactor_cache m_ant_cofactor_cache; // Op cache for ITE-hoisting operations (union, inter, concat, complement) // Path-aware caches: key is (a, b, path_expr) for binary ops, (a, path_expr) for complement @@ -276,7 +277,8 @@ namespace seq { expr_ref_pair_vector const &get_cached_cofactors(transition_mode mode, expr *r); void maybe_reset_cached_cofactors(unsigned cap) { - m_cofactor_cache.maybe_reset(cap); + m_brz_cofactor_cache.maybe_reset(cap); + m_ant_cofactor_cache.maybe_reset(cap); } /** diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index a0265f0803..4d96ccba5a 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -51,6 +51,7 @@ Author: #include "ast/rewriter/seq_monadic.h" #include "ast/rewriter/guard_set.h" +#include "ast/rewriter/seq_range_collapse.h" #include #include #include @@ -131,74 +132,91 @@ expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) { return m_rw.get_derive().get_cached_cofactors(m_config.m_mode, r); } -bool seq_monadic::live_states(expr* R, expr_ref_vector& out) { - obj_map id; - expr_ref_vector states(m); - vector> succ; - bool_vector maybe_null; - auto intern = [&](expr* s) -> unsigned { - unsigned k; - if (id.find(s, k)) return k; - k = states.size(); - id.insert(s, k); - states.push_back(s); - succ.push_back(svector()); - maybe_null.push_back(nullable(s) != l_false); // unknown nullability => keep (conservative) - return k; - }; - intern(R); - const unsigned STATE_CAP = 1u << 12; - for (unsigned i = 0; i < states.size(); ++i) { - if (states.size() > STATE_CAP) { - m_stats.inc_bail(bail_reason::state_cap); - return false; - } - if (!m.inc()) { - m_stats.inc_bail(bail_reason::resource); - return false; - } - expr_ref_pair_vector const& cof = derivative_cofactors(states.get(i)); - for (auto const& [g, t] : cof) { - if (re().is_empty(t)) continue; - unsigned k = intern(t); // MUST precede succ[i] indexing: intern may - succ[i].push_back(k); // grow (realloc) succ, invalidating succ[i]& - } - } - 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)); m_pin.push_back(states.get(i)); } - return true; +void seq_monadic::reset_ivl_cache() { + for (auto& kv : m_ivl_cache) + dealloc(kv.m_value); + m_ivl_cache.reset(); + m_ivl_pin.reset(); } -expr_ref_vector const* seq_monadic::live_states_cached(expr* R) { - expr_ref_vector* v = nullptr; - if (m_live_cache.find(R, v)) - return v; // may be null: previously gave up on R - v = alloc(expr_ref_vector, m); - if (!live_states(R, *v)) { - dealloc(v); - v = nullptr; - } - m_pin.push_back(R); // keep the key alive for the cache's lifetime - m_live_cache.insert(R, v); - return v; -} +// Canonical interval form of r's derivative: the cofactor guards, translated into the +// range algebra, refined into a sorted list of disjoint ranges, each labelled with the +// targets reachable on it. Adjacent ranges with identical target sets are merged, so the +// result is the minimal ordered-ITE ("t-regex") representation of the transition relation. +// Returns null when some guard falls outside the range algebra. +seq_monadic::ivl_list const* seq_monadic::interval_cofactors(expr* r, expr* v0) { + ivl_list* res = nullptr; + if (m_ivl_cache.find(r, res)) + return res && res->ok ? res : nullptr; -void seq_monadic::reset_live_cache() { - for (auto const& [k, v] : m_live_cache) - dealloc(v); - m_live_cache.reset(); + unsigned max_char = u().max_char(); + res = alloc(ivl_list); + m_ivl_cache.insert(r, res); + m_ivl_pin.push_back(r); + + // (lo, hi, target) triples, plus the boundary set of this state's own partition. + struct tr_t { unsigned lo, hi; expr* t; }; + svector tr; + svector bounds; + bounds.push_back(0); + for (auto const& [g, t] : derivative_cofactors(r)) { + if (re().is_empty(t)) + continue; + seq::range_predicate* p = nullptr; + if (!m_rp_cache.find(g, p)) { + p = m_rp_cache.fresh(max_char); + if (!seq::guard_to_range_predicate(u(), v0, g, *p)) { + m_rp_cache.insert(g, nullptr); + res->ok = false; + return nullptr; + } + m_rp_cache.insert(g, p); + } + else if (!p) { + res->ok = false; + return nullptr; + } + m_ivl_pin.push_back(t); + for (auto const& rg : p->ranges()) { + tr.push_back({ rg.first, rg.second, t }); + bounds.push_back(rg.first); + if (rg.second < max_char) + bounds.push_back(rg.second + 1); + } + } + if (tr.empty()) + return res; // dead state: no outgoing transition + + std::sort(bounds.begin(), bounds.end()); + bounds.shrink((unsigned)(std::unique(bounds.begin(), bounds.end()) - bounds.begin())); + + ptr_vector hits; + for (unsigned bi = 0; bi < bounds.size(); ++bi) { + unsigned lo = bounds[bi]; + unsigned hi = bi + 1 < bounds.size() ? bounds[bi + 1] - 1 : max_char; + hits.reset(); + for (auto const& e : tr) + if (e.lo <= lo && lo <= e.hi) + hits.push_back(e.t); + if (hits.empty()) + continue; // gap: no transition on this range + // extend the previous range when it carries exactly the same target set + if (!res->ranges.empty()) { + ivl_range& prev = res->ranges.back(); + if (prev.hi + 1 == lo && prev.count == hits.size()) { + bool same = true; + for (unsigned k = 0; k < hits.size() && same; ++k) + same = res->targets[prev.first + k] == hits[k]; + if (same) { + prev.hi = hi; + continue; + } + } + } + res->ranges.push_back({ lo, hi, res->targets.size(), hits.size() }); + res->targets.append(hits.size(), hits.data()); + } + return res; } lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* witness_word) { @@ -290,6 +308,92 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w branches.resize(n); key st_key; bool bail = false; + + // ---- interval-refinement ("t-regex merge") product -------------------------- + // Over the character sort every cofactor guard denotes a union of ranges, so each + // component's derivative has a canonical ordered-interval ("t-regex") form, cached + // per state by interval_cofactors. The joint transitions are then exactly the cells + // of the common refinement of those n interval lists, obtained by a cursor merge in + // O(sum_i intervals_i) -- whereas the cartesian enumeration below tries + // prod_i(k_i) combinations, almost all of which are pruned as empty. + bool const sweep_ok = u().is_char(m_elem_sort); + unsigned const max_char = sweep_ok ? u().max_char() : 0; + svector sw_lists; + svector sw_cur, sw_odo; + sw_lists.resize(n); + sw_cur.resize(n); + sw_odo.resize(n); + + // Returns false when some guard falls outside the range algebra, in which case the + // caller falls back to the cartesian enumeration for this product state. + auto sweep = [&]() -> bool { + for (unsigned i = 0; i < n; ++i) { + sw_lists[i] = interval_cofactors(st[i], var0); + if (!sw_lists[i]) + return false; + if (sw_lists[i]->ranges.empty()) + return true; // component is stuck: no joint transition + sw_cur[i] = 0; + } + uint64_t b = 0; + while (b <= max_char) { + uint64_t next = (uint64_t)max_char + 1; + bool covered = true, done = false; + for (unsigned i = 0; i < n; ++i) { + auto const& rs = sw_lists[i]->ranges; + unsigned& c = sw_cur[i]; + while (c < rs.size() && rs[c].hi < b) + ++c; + if (c == rs.size()) { // this component has no transition left + done = true; + break; + } + if (rs[c].lo > b) { // gap in this component: skip ahead + covered = false; + next = std::min(next, (uint64_t)rs[c].lo); + } + else + next = std::min(next, (uint64_t)rs[c].hi + 1); + } + if (done) + break; + if (covered) { + // Emit every combination of the targets active on this cell. The modes + // whose cofactors partition the domain give exactly one target per + // component; the antimirov-style modes may give several. + for (unsigned i = 0; i < n; ++i) + sw_odo[i] = 0; + while (true) { + for (unsigned i = 0; i < n; ++i) { + auto const& r = sw_lists[i]->ranges[sw_cur[i]]; + cur[i] = sw_lists[i]->targets[r.first + sw_odo[i]]; + } + key const& ck = fill_key(cur); + if (visited.find(ck) == visited.end()) { + visited.insert(ck); + if (witness_word) { + expr* e = u().mk_char((unsigned)b); + m_pin.push_back(e); + parent[ck] = { st_key, e }; + } + for (unsigned j = 0; j < n; ++j) + work.push_back(cur[j]); + } + unsigned i = n; + while (i-- > 0) { + if (++sw_odo[i] < sw_lists[i]->ranges[sw_cur[i]].count) + break; + sw_odo[i] = 0; + } + if (i == UINT_MAX) + break; // odometer wrapped: cell exhausted + } + } + b = next; + } + return true; + }; + std::function rec = [&](unsigned i, guard_set const& acc) { if (bail) return; @@ -352,13 +456,17 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w return l_undef; } + if (witness_word) + st_key = fill_key(st); + + if (sweep_ok && sweep()) + continue; + for (unsigned i = 0; i < n; ++i) branches[i] = &derivative_cofactors(st[i]); // joint transitions = cartesian product of the branches with the guards // conjoined; prune as soon as the accumulated guard is empty, bail on unknown. - if (witness_word) - st_key = fill_key(st); guard_set top(m, u(), m_elem_sort, var0, &m_rp_cache); rec(0, top); if (bail) @@ -417,7 +525,7 @@ void seq_monadic::reset_search() { m_der_cache.reset(); m_nullable_cache.reset(); m_undef_vars = 0; - reset_live_cache(); + m_live_states.reset(); } bool seq_monadic::prepare(membership_vec const& memberships) { @@ -546,23 +654,13 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { // A variable: the last atom is a plain membership in R, otherwise the variable drives // the derivative automaton from R to some live state q, which splits the search. bool last_atom = (i + 1 == atoms.size()); - ptr_vector targets; - if (last_atom) - targets.push_back(nullptr); - else { - expr_ref_vector const* Q = live_states_cached(R); - if (!Q) - return l_undef; - for (expr* q : *Q) - targets.push_back(q); - } - unsigned vi = var_index(a.var.get()); uint64_t pos = (static_cast(mi) << 32) | i; uint64_t last = 0; bool finalize = m_last_occ.find(a.var.get(), last) && last == pos; - bool any_undef = false; - for (expr* target : targets) { + + // Explores one split target; the caller stops at the first l_true. + auto explore = [&](expr* target) -> lbool { m_groups[vi].push_back(component{ a.var.get(), R, target }); // The group's emptiness test has to be run at some point anyway; running it as // soon as the group is complete (or as soon as it holds several components, where @@ -583,6 +681,19 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { --m_undef_vars; } m_groups[vi].pop_back(); + return r; + }; + + if (last_atom) + return explore(nullptr); + + // The live states are consumed as they are produced, so a satisfying branch under an + // early state means the rest of the reachable set is never expanded. That is what + // makes a root with an exponential live set tractable when a witness is found early. + bool any_undef = false; + auto live = m_live_states.reachable_live(R); + for (expr* q : live) { + lbool r = explore(q); if (r == l_true) return l_true; if (r == l_undef) { @@ -591,6 +702,14 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { any_undef = true; } } + // Short of the full reachable set the unexplored split states could still hold a + // solution, so the l_false the loop would otherwise report is not justified. + if (live.failed()) { + m_stats.inc_bail( + live.failure_reason() == seq::live_states::failure::state_cap ? + bail_reason::state_cap : bail_reason::resource); + return l_undef; + } return any_undef ? l_undef : l_false; } @@ -600,6 +719,7 @@ lbool seq_monadic::decide(membership_vec const& memberships) { reset_search(); // clear the caches before dropping the m_pin.reset(); // pins that keep their keys alive m_rp_cache.maybe_reset(1u << 16); + reset_ivl_cache(); m_rw.get_derive().maybe_reset_cached_cofactors(1u << 16); m_budget = 200000; m_giveup = false; @@ -835,7 +955,7 @@ std::ostream& seq_monadic::display(std::ostream& out) const { << " :group-cache-size " << m_group_cache.size() << "\n" << " :derivative-cache-size " << m_der_cache.size() << "\n" << " :nullable-cache-size " << m_nullable_cache.size() << "\n" - << " :live-cache-size " << m_live_cache.size() << "\n" + << " :live-cache-size " << m_live_states.num_states() << "\n" << " :pinned-expressions " << m_pin.size() << ")\n"; out << " :statistics\n" diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index eaa0bb3638..c878a8b40e 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -63,6 +63,7 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_range_predicate.h" +#include "ast/rewriter/seq_regex_live.h" #include "ast/rewriter/guard_set.h" #include "ast/rewriter/th_rewriter.h" #include "util/lbool.h" @@ -113,6 +114,20 @@ class seq_monadic { statistics m_stats; obj_map m_model; // last extracted model (var -> witness); see get_model() guard_set::cache m_rp_cache; // cofactor guard -> range predicate + // Interval ("t-regex") form of a state's derivative cofactors over the character sort: + // a canonical list of disjoint ranges in increasing order, each carrying the targets + // reachable on that range. Built once per state and merged by the product, so the + // product enumerates only the cells of the common refinement. + struct ivl_range { unsigned lo, hi, first, count; }; + struct ivl_list { + svector ranges; + ptr_vector targets; // ranges[i] owns targets[first .. first+count) + bool ok = true; // false: some guard is outside the range algebra + }; + obj_map m_ivl_cache; + expr_ref_vector m_ivl_pin; // pins the states and targets the cache refers to + ivl_list const* interval_cofactors(expr* r, expr* v0); + void reset_ivl_cache(); obj_pair_map m_der_cache; // memoizes der_elem per (regex, element) obj_map m_nullable_cache; // memoizes nullability (0 false / 1 true / 2 unknown); // seq_rewriter's own cache is capped and flushed whole @@ -166,7 +181,7 @@ class seq_monadic { }; group_sig m_sig_buf; // reused by group_nonempty (avoids allocating per lookup) std::unordered_map m_group_cache; - obj_map m_live_cache; // regex -> live split states (null = gave up) + seq::live_states m_live_states; // Brzozowski derivative of regex `r` by the concrete element `elem`. Memoized on // (r, elem): the search revisits the same constant step on many branches. @@ -175,20 +190,10 @@ class seq_monadic { // Memoized nullability of a derivative state: l_true / l_false / l_undef (unknown). lbool nullable(expr* r); - // Symbolic transition cofactors in the selected mode. Memoized per regex `r` in - // m_cofactors: the returned vector is owned by that cache (see the cofactor_cache - // class above for the persistence/reset policy). + // Symbolic transition cofactors in the selected mode. The returned vector is owned + // by seq_rewriter's mode-specific cofactor cache. expr_ref_pair_vector const& derivative_cofactors(expr* r); - // Live reachable derivative states of R (BFS over cofactor targets + liveness - // least-fixpoint). These are the split states q. Returns false on a cap overrun. - bool live_states(expr* R, expr_ref_vector& out); - - // Memoized live_states. Returns null if the computation gave up for this regex. - expr_ref_vector const* live_states_cached(expr* R); - - void reset_live_cache(); - // Product-reachability emptiness of a conjunction of components (all on one // variable). l_false = empty (unsat), l_true = non-empty (sat), l_undef = gave up // (cap overrun, non-range guard, or undecidable nullability). @@ -248,10 +253,10 @@ public: seq_monadic(seq_rewriter& rw, trail_stack& undo_trail, seq::transition_mode mode = seq::transition_mode::light_antimirov_tm) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail), - m_pin(rw.m()), m_config(mode), m_rp_cache(rw.m()), - m_regexes(rw.m()) {} + m_pin(rw.m()), m_config(mode), m_rp_cache(rw.m()), m_ivl_pin(rw.m()), + m_regexes(rw.m()), m_live_states(rw, mode, 1u << 12) {} - ~seq_monadic() { reset_live_cache(); } + ~seq_monadic() { reset_ivl_cache(); } void collect_statistics(::statistics &st) const; diff --git a/src/ast/rewriter/seq_regex_live.cpp b/src/ast/rewriter/seq_regex_live.cpp new file mode 100644 index 0000000000..bd2196e438 --- /dev/null +++ b/src/ast/rewriter/seq_regex_live.cpp @@ -0,0 +1,312 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_regex_live.cpp + +Abstract: + + Shared lazy live-state traversal for regular-expression derivatives. + +--*/ + +#include "ast/rewriter/seq_regex_live.h" +#include "ast/rewriter/seq_rewriter.h" +#include "util/obj_hashtable.h" +#include "util/uint_set.h" + +namespace seq { + + struct live_states::search { + svector m_to_explore; + unsigned m_explore_head = 0; + uint_set m_seen; + vector> m_predecessors; + bool_vector m_live; + bool_vector m_closed; + svector m_live_frontier; + unsigned m_root_id = 0; + failure m_failure = failure::none; + bool m_complete = false; + }; + + struct live_states::imp { + seq_rewriter& m_rw; + ast_manager& m; + seq_util::rex& m_re; + transition_mode m_mode; + unsigned m_max_states; + obj_map m_ids; + expr_ref_vector m_states; + vector> m_successors; + svector m_nullable; + bool_vector m_expanded; + obj_map m_searches; + + imp(seq_rewriter& rw, transition_mode mode, unsigned max_states) : + m_rw(rw), + m(rw.m()), + m_re(rw.u().re), + m_mode(mode), + m_max_states(max_states), + m_states(m) { + } + + ~imp() { + reset(); + } + + unsigned intern(expr* r) { + unsigned id = 0; + if (m_ids.find(r, id)) + return id; + id = m_states.size(); + m_ids.insert(r, id); + m_states.push_back(r); + m_successors.push_back(svector()); + m_nullable.push_back(2); + m_expanded.push_back(false); + return id; + } + + void resize(search& s) { + unsigned size = m_states.size(); + if (s.m_predecessors.size() < size) + s.m_predecessors.resize(size); + if (s.m_live.size() < size) + s.m_live.resize(size, false); + if (s.m_closed.size() < size) + s.m_closed.resize(size, false); + } + + char nullable(unsigned id) { + if (m_nullable[id] != 2) + return m_nullable[id]; + expr* r = m_states.get(id); + lbool n = m_re.get_info(r).nullable; + if (n == l_undef) { + expr_ref f = m_rw.is_nullable(r); + n = m.is_true(f) ? l_true : m.is_false(f) ? l_false : l_undef; + } + m_nullable[id] = n == l_true ? 1 : n == l_false ? 0 : 3; + return m_nullable[id]; + } + + void mark_live(search& s, unsigned id) { + svector todo; + todo.push_back(id); + while (!todo.empty()) { + id = todo.back(); + todo.pop_back(); + if (!s.m_seen.contains(id) || s.m_live[id]) + continue; + s.m_live[id] = true; + s.m_live_frontier.push_back(id); + for (unsigned predecessor : s.m_predecessors[id]) + todo.push_back(predecessor); + } + } + + bool add_state(search& s, unsigned id) { + if (s.m_seen.contains(id)) + return true; + if (s.m_to_explore.size() >= m_max_states) { + s.m_failure = failure::state_cap; + return false; + } + resize(s); + s.m_seen.insert(id); + s.m_to_explore.push_back(id); + if (nullable(id) != 0) + mark_live(s, id); + return true; + } + + bool expand_state(unsigned id, failure& f) { + if (m_expanded[id]) + return true; + if (!m.inc()) { + f = failure::resource; + return false; + } + m_expanded[id] = true; + nullable(id); + auto const& cofactors = m_rw.get_derive().get_cached_cofactors(m_mode, m_states.get(id)); + for (auto const& [guard, target] : cofactors) { + if (m_re.is_empty(target)) + continue; + unsigned target_id = intern(target); + if (!m_successors[id].contains(target_id)) + m_successors[id].push_back(target_id); + } + return true; + } + + void close(search& s) { + for (unsigned id : s.m_to_explore) + if (!s.m_live[id]) + s.m_closed[id] = true; + s.m_complete = true; + } + + void expand(search& s) { + if (s.m_complete || s.m_failure != failure::none) + return; + if (s.m_explore_head == s.m_to_explore.size()) { + close(s); + return; + } + + unsigned id = s.m_to_explore[s.m_explore_head++]; + if (!expand_state(id, s.m_failure)) + return; + resize(s); + for (unsigned target : m_successors[id]) { + if (!add_state(s, target)) + return; + if (!s.m_predecessors[target].contains(id)) + s.m_predecessors[target].push_back(id); + if (s.m_live[target]) + mark_live(s, id); + } + } + + bool ensure(search& s, unsigned index) { + while (index >= s.m_live_frontier.size() && + !s.m_complete && + s.m_failure == failure::none) + expand(s); + return index < s.m_live_frontier.size(); + } + + search* get_search(expr* root) { + search* s = nullptr; + if (m_searches.find(root, s)) + return s; + s = alloc(search); + unsigned root_id = intern(root); + s->m_root_id = root_id; + add_state(*s, root_id); + m_searches.insert(root, s); + return s; + } + + void reset() { + for (auto const& [root, s] : m_searches) + dealloc(s); + m_searches.reset(); + m_ids.reset(); + m_states.reset(); + m_successors.reset(); + m_nullable.reset(); + m_expanded.reset(); + } + }; + + live_states::live_states(seq_rewriter& rw, transition_mode mode, unsigned max_states) : + m_imp(alloc(imp, rw, mode, max_states)) { + } + + live_states::~live_states() { + dealloc(m_imp); + } + + expr* live_states::iterator::operator*() const { + return m_owner->get_live(m_search, m_index); + } + + live_states::iterator& live_states::iterator::operator++() { + ++m_index; + return *this; + } + + bool live_states::iterator::operator!=(iterator const& other) const { + if (other.m_end) + return m_owner->ensure(m_search, m_index); + return m_owner != other.m_owner || + m_search != other.m_search || + m_index != other.m_index || + m_end != other.m_end; + } + + live_states::iterator live_states::reachable::begin() const { + return iterator(m_owner, m_search, 0, false); + } + + live_states::iterator live_states::reachable::end() const { + return iterator(m_owner, m_search, 0, true); + } + + bool live_states::reachable::failed() const { + return m_owner->get_failure(m_search) != failure::none; + } + + live_states::failure live_states::reachable::failure_reason() const { + return m_owner->get_failure(m_search); + } + + bool live_states::reachable::is_dead() { + return !m_owner->ensure(m_search, 0) && !failed(); + } + + live_states::reachable live_states::reachable_live(expr* r) { + return reachable(this, m_imp->get_search(r)); + } + + bool live_states::contains(expr* r) const { + return m_imp->m_ids.contains(r); + } + + unsigned live_states::state_id(expr* r) { + return m_imp->intern(r) + 1; + } + + unsigned live_states::num_states() const { + return m_imp->m_states.size(); + } + + void live_states::reset() { + m_imp->reset(); + } + + bool live_states::ensure(search* s, unsigned index) { + return m_imp->ensure(*s, index); + } + + /* + Yield the root before the rest of the frontier. + + States enter m_live_frontier in the order their liveness is *discovered*, which is + bottom-up: a nullable state is marked first and liveness then propagates backwards to + its predecessors, so the root -- reachable to every state, and rarely nullable itself + -- is typically marked last. Callers use this order as a search order, and the + eager traversal this replaced emitted states in interning order with the root at + index 0. Dropping the root to the back therefore reordered the consumer's search and + cost several benchmarks their witness-first branch. + + The remap is well defined because every state in the search is reachable from the + root, so liveness of any state propagates to the root within the same expand() step: + whenever the frontier is non-empty at an ensure() boundary the root is already live + and present in it, and the element count is unchanged. + */ + expr* live_states::get_live(search* s, unsigned index) const { + unsigned root = s->m_root_id; + if (!s->m_live.get(root, false)) + return m_imp->m_states.get(s->m_live_frontier[index]); + if (index == 0) + return m_imp->m_states.get(root); + for (unsigned i = 0, seen = 0; i < s->m_live_frontier.size(); ++i) { + if (s->m_live_frontier[i] == root) + continue; + if (++seen == index) + return m_imp->m_states.get(s->m_live_frontier[i]); + } + return m_imp->m_states.get(s->m_live_frontier[index]); + } + + live_states::failure live_states::get_failure(search* s) const { + return s->m_failure; + } + +} diff --git a/src/ast/rewriter/seq_regex_live.h b/src/ast/rewriter/seq_regex_live.h new file mode 100644 index 0000000000..28fa0a9f51 --- /dev/null +++ b/src/ast/rewriter/seq_regex_live.h @@ -0,0 +1,83 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_regex_live.h + +Abstract: + + Shared lazy live-state traversal for regular-expression derivatives. + +--*/ +#pragma once + +#include "ast/rewriter/seq_derive.h" +#include "ast/ast.h" + +class seq_rewriter; + +namespace seq { + + class live_states { + struct search; + struct imp; + + public: + enum class failure { + none, + state_cap, + resource + }; + + class iterator { + live_states* m_owner = nullptr; + search* m_search = nullptr; + unsigned m_index = 0; + bool m_end = false; + + public: + iterator(live_states* owner, search* s, unsigned index, bool end) : + m_owner(owner), m_search(s), m_index(index), m_end(end) {} + expr* operator*() const; + iterator& operator++(); + bool operator!=(iterator const& other) const; + }; + + class reachable { + live_states* m_owner = nullptr; + search* m_search = nullptr; + + public: + reachable(live_states* owner, search* s) : + m_owner(owner), m_search(s) {} + iterator begin() const; + iterator end() const; + bool failed() const; + failure failure_reason() const; + bool is_dead(); + }; + + private: + imp* m_imp; + + bool ensure(search* s, unsigned index); + expr* get_live(search* s, unsigned index) const; + failure get_failure(search* s) const; + + public: + live_states(seq_rewriter& rw, + transition_mode mode = transition_mode::brzozowski_tm, + unsigned max_states = UINT_MAX); + ~live_states(); + live_states(live_states const&) = delete; + live_states& operator=(live_states const&) = delete; + + reachable reachable_live(expr* r); + bool contains(expr* r) const; + unsigned state_id(expr* r); + // Number of interned derivative states, i.e. the size of the shared state table. + unsigned num_states() const; + void reset(); + }; +} diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 1951266165..59336556c1 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -31,8 +31,7 @@ namespace smt { ctx(th.get_context()), m(th.get_manager()), m_monadic(seq_rw(), ctx.get_trail_stack()), - m_state_to_expr(m), - m_state_graph(state_graph::state_pp(this, pp_state)) { + m_live_states(seq_rw(), seq::transition_mode::brzozowski_tm, 10000) { m_monadic.set_is_var([&th](expr *e) { return th.is_var(e); }); } @@ -640,8 +639,8 @@ namespace smt { } if (info.interpreted) { - update_state_graph(r); - if (m_state_graph.is_dead(get_state_id(r))) { + auto live = m_live_states.reachable_live(r); + if (live.is_dead()) { STRACE(seq_regex_brief, tout << "(dead) ";); th.add_axiom(~lit); return true; @@ -665,8 +664,7 @@ namespace smt { /** * Propagate the atom (accept s i r) * - * Propagation triggers updating the state graph for dead state detection: - * (accept s i r) => update_state_graph(r) + * Propagation triggers derivative reachability for dead state detection: * (accept s i r) & dead(r) => false * * Propagation is also blocked under certain conditions to throttle @@ -1292,101 +1290,10 @@ namespace smt { return sk().mk("re.first", n, a().mk_int(r->get_id()), elem_sort); } - /** - * Dead state elimination using the state_graph class - */ - - unsigned seq_regex::get_state_id(expr* e) { - // Assign increasing IDs starting from 1 - if (!m_expr_to_state.contains(e)) { - m_state_to_expr.push_back(e); - unsigned new_id = m_state_to_expr.size(); - m_expr_to_state.insert(e, new_id); - STRACE(seq_regex_brief, tout << "new(" << expr_id_str(e) - << ")=" << state_str(e) << " ";); - STRACE(seq_regex, tout - << "New state ID: " << new_id - << " = " << mk_pp(e, m) << std::endl;); - SASSERT(get_expr_from_id(new_id) == e); - } - return m_expr_to_state.find(e); - } - expr* seq_regex::get_expr_from_id(unsigned id) { - SASSERT(id >= 1); - SASSERT(id <= m_state_to_expr.size()); - return m_state_to_expr.get(id - 1); - } - - bool seq_regex::can_be_in_cycle(expr *r1, expr *r2) { - // TBD: This can be used to optimize the state graph: - // return false here if it is known that r1 -> r2 can never be - // in a cycle. There are various easy syntactic checks on r1 and r2 - // that can be used to infer this (e.g. star height, or length if - // both are star-free). - // This check need not be sound, but if it is not, some dead states - // will be missed. - return true; - } - - /* - Update the state graph with expression r and all its derivatives. - */ - bool seq_regex::update_state_graph(expr* r) { - unsigned r_id = get_state_id(r); - if (m_state_graph.is_done(r_id)) return false; - if (m_state_graph.get_size() >= m_max_state_graph_size) { - STRACE(seq_regex, tout << "Warning: ignored state graph update -- max size of seen states reached!" << std::endl;); - STRACE(seq_regex_brief, tout << "(MAX SIZE REACHED) ";); - return false; - } - STRACE(seq_regex, tout << "Updating state graph for regex " - << mk_pp(r, m) << ") ";); - - STRACE(state_graph, - if (!m_state_graph.is_seen(r_id)) - tout << std::endl << "state(" << r_id << ") = " << re().to_str(r) << std::endl << "info(" << r_id << ") = " << re().get_info(r) << std::endl;); - // Add state - m_state_graph.add_state(r_id); - STRACE(seq_regex, tout << "Updating state graph for regex " - << mk_pp(r, m) << ") " << std::endl;); - STRACE(seq_regex_brief, tout << std::endl << "USG(" - << state_str(r) << ") ";); - expr_ref r_nullable = is_nullable_wrapper(r); - if (m.is_true(r_nullable)) { - m_state_graph.mark_live(r_id); - } - else { - // Add edges to all derivatives - expr_ref_vector derivatives(m); - STRACE(seq_regex_verbose, tout - << "getting all derivs: " << r_id << " " << std::endl;); - get_derivative_targets(r, derivatives); - for (auto const& dr: derivatives) { - unsigned dr_id = get_state_id(dr); - STRACE(seq_regex_verbose, tout - << std::endl << " traversing deriv: " << dr_id << " ";); - STRACE(state_graph, - if (!m_state_graph.is_seen(dr_id)) - tout << "state(" << dr_id << ") = " << re().to_str(dr) << std::endl << "info(" << dr_id << ") = " << re().get_info(dr) << std::endl;); - // Add state - m_state_graph.add_state(dr_id); - bool maybecycle = can_be_in_cycle(r, dr); - m_state_graph.add_edge(r_id, dr_id, maybecycle); - } - m_state_graph.mark_done(r_id); - } - - STRACE(seq_regex, m_state_graph.display(tout);); - STRACE(seq_regex_brief, tout << std::endl;); - STRACE(seq_regex_brief, m_state_graph.display(tout);); - return true; - } - std::string seq_regex::state_str(expr* e) { - if (m_expr_to_state.contains(e)) - return std::to_string(get_state_id(e)); - else - return expr_id_str(e); + if (m_live_states.contains(e)) + return std::to_string(m_live_states.state_id(e)); + return expr_id_str(e); } std::string seq_regex::expr_id_str(expr* e) { return std::string("id") + std::to_string(e->get_id()); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index eaa68dc781..b1832cfffb 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -17,9 +17,9 @@ Author: #pragma once #include "util/scoped_vector.h" -#include "util/state_graph.h" #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_monadic.h" +#include "ast/rewriter/seq_regex_live.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_skolem.h" #include "smt/smt_context.h" @@ -56,13 +56,6 @@ Author: (next states) d(r1)=r2: r2 is the derivative of r1 n(r1)=b: b = whether r1 is nullable or not - USG(r): updating state graph for regex r (add all derivatives) - - -tr:state_graph - This is the tracing done by util/state_graph, the data structure - that seq_regex uses to track live and dead regexes, which can - altneratively be used to get a high-level picture of what states - are being explored and updated as the solver progresses. -tr:seq_regex_verbose Used for some more frequent tracing (in the style of seq_regex, @@ -72,21 +65,12 @@ Author: These are the underlying sequence theory tracing, often used by the rewriter. - DEBUGGING AND VIEWING STATE GRAPH GRAPHICAL OUTPUT + DEBUGGING -dbg:seq_regex Debugging that checks invariants. Currently, checks that derivative normal form is correctly preserved in the rewriter. - -dbg:state_graph - Debugging for the state graph, which - 1. Checks state graph invariants, and - 2. Generates the files .z3-state-graph.dgml and .z3-state-graph.dot - which can be used to visually view the state graph being explored, - during or after executing Z3. - The output can be viewed: - - Using Visual Studio for .dgml - - Using a tool such as xdot (`xdot .z3-state-graph.dot`) for .dot */ namespace smt { @@ -163,23 +147,9 @@ namespace smt { unsigned m_monadic_assumption_generation = UINT_MAX; unsigned m_monadic_fallback_generation = UINT_MAX; - /* - state_graph for dead state detection, and associated methods - */ - ptr_addr_map m_expr_to_state; - expr_ref_vector m_state_to_expr; - state_graph m_state_graph; + seq::live_states m_live_states; /* map from uninterpreted regex constants to assigned regex expressions by EQ */ // expr_map m_const_to_expr; - unsigned m_max_state_graph_size { 10000 }; - // Convert between expressions and states (IDs) - unsigned get_state_id(expr* e); - expr* get_expr_from_id(unsigned id); - // Cycle-detection heuristic - // Note: Doesn't need to be sound or complete (doesn't affect soundness) - bool can_be_in_cycle(expr* r1, expr* r2); - // Update the graph - bool update_state_graph(expr* r); // Printing expressions for seq_regex_brief std::string state_str(expr* e); @@ -239,17 +209,6 @@ namespace smt { seq_regex_ptr must be a pointer to seq_regex and the id must be a valid state id or else nothing is printed. */ - static void pp_state(void* seq_regex_ptr, std::ostream& out, unsigned id, bool html_encode) { - seq_regex* sr = (seq_regex*)seq_regex_ptr; - if (sr) { - seq_util::rex re_util(sr->re()); - if (1 <= id && id <= sr->m_state_to_expr.size()) { - expr* r = sr->get_expr_from_id(id); - seq_util::rex::pp(re_util, r, html_encode).display(out); - } - } - } - bool block_if_empty(expr* r, literal lit); void add_monadic_membership(literal lit, expr* s, expr* r); // Expand a term through theory_seq's solution map, but substitute a sub-term only