diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 5051ca1d78..7972b8086e 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -408,6 +408,17 @@ public: void simplify_split(split_set& s) { m_split.simplify(s); } + // Build the *suspended* sigma(r) split-set term (no expansion); drive it with + // iterate_split. Returns null on a non-regex argument. See seq_split.h. + expr_ref make_split(expr* r) { return m_split.make(r); } + + // Create a lazy enumerator over a suspended split-set `node` (typically the + // result of make_split()). See seq_split::iterator for the arguments. + seq_split::iterator iterate_split(expr* node, unsigned threshold, + const split_mode mode = split_mode::strong, split_oracle const& oracle = {}) { + return m_split.iterate(node, mode, threshold, oracle); + } + // decompose a membership constraint into a set of pairs of regex splits std::pair split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const { return m_split.split_membership(str, regex, threshold, result); diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index c48eda4a70..8d410f8111 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -72,6 +72,21 @@ namespace seq { return result; } + // Suspended state of a lazy regex factorization (apply_regex_factorization). + // One rf_state drives the whole binary "remaining splits" chain for a single + // membership: it owns the lazy split iterator and remembers the chosen + // head/tail boundary plus the leading constant run consumed from the tail. + struct rf_state { + str_mem m_mem; // the membership being factorized (kept on child B) + euf::snode const* m_head; // prefix boundary (head ∈ Δ) + euf::snode const* m_tail; // suffix boundary, const run already consumed (tail ∈ ∇) + zstring m_c; // leading constant run consumed from the tail + seq_split::iterator m_iter; // lazy split enumerator, shared down the child-B chain + rf_state(str_mem const& mem, euf::snode const* head, euf::snode const* tail, + zstring const& c, seq_split::iterator&& it) : + m_mem(mem), m_head(head), m_tail(tail), m_c(c), m_iter(std::move(it)) {} + }; + std::pair split_membership(euf::snode const *str, euf::snode const *regex, euf::sgraph& sg, unsigned threshold, split_set& result) { seq_util& seq = sg.get_seq_util(); ast_manager& m = sg.get_manager(); @@ -636,7 +651,7 @@ namespace seq { nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i &ctx_solver) : m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_a_rw(m), m_sk(m, m_rw), m_length_solver(solver), m_context_solver(ctx_solver), m_parikh(alloc(seq_parikh, sg)), - m_seq_regex(alloc(seq::seq_regex, sg)), m_partial_dfa_pin(sg.get_manager()) { + m_seq_regex(alloc(seq::seq_regex, sg)), m_split_rw(sg.get_manager()), m_partial_dfa_pin(sg.get_manager()) { } nielsen_graph::~nielsen_graph() { @@ -736,6 +751,12 @@ namespace seq { for (nielsen_edge *e : m_edges) { dealloc(e); } + // suspended factorization iterators (release their pinned expressions + // while m_split_rw / the ast_manager are still alive) + for (rf_state* st : m_rf_states) { + dealloc(st); + } + m_rf_states.reset(); m_nodes.reset(); m_edges.reset(); m_root = nullptr; @@ -2282,8 +2303,13 @@ namespace seq { // reasons, this node is unsat too — independently of its (integer) side // constraints — so we prune without re-exploring its subtree. We derive // the conflict from this node's own constraint deps (a sound over-approx). + // + // A lazy-factorization continuation node (rf_cont set) is EXEMPT: it shares + // its parent's string constraints (only the suspended split iterator + // differs), so it would alias the parent's signature, yet it still has + // pending splits to explore — it is not a true recurrence. { - if (m_unsat_node_cache.contains(node)) { + if (!node->rf_cont() && m_unsat_node_cache.contains(node)) { node->set_conflict(backtrack_reason::sibling, nullptr /*we use the one of the sibling*/); node->set_general_conflict(); node->m_unsat_cacheable = true; @@ -2377,7 +2403,12 @@ namespace seq { // with string-only conflicts and self-contained cuts (see the epilogue). // ------------------------------------------------------------------- node->canonize_and_compute_final_node_hash(); - { + // A lazy-factorization continuation node (rf_cont set) is EXEMPT from the + // loop-cut: it aliases its parent's string signature (only the suspended + // split iterator differs) but is not a true recurrence — it still has + // pending splits. The iterator is finite, so the continuation chain + // terminates on its own (exhaustion → regex conflict). + if (!node->rf_cont()) { auto it = m_siblings.find(node); if (it != m_siblings.end() && !it->second.empty()) { nielsen_node* anc = it->second.back(); // deepest sibling still on the path @@ -4012,16 +4043,185 @@ namespace seq { // Modifier: apply_regex_factorization (Boolean Closure) // ----------------------------------------------------------------------- + // Safety cap handed to the lazy split iterator. Large by design: the whole + // point of the lazy factorization is that the binary child-B chain walks the + // splits one at a time, so the count must not bound how many splits we may + // explore. It still guards internal materialisation of intersection / + // complement bodies against runaway space blow-up. + static const unsigned RF_LAZY_CAP = 1u << 20; + + // The cycle machinery (apply_cycle_decomposition) owns variables it has put + // under a noloop guard: factorizing such a variable's membership would split + // it in a way that violates the guard's premise (that the variable is handled + // by the stabilizer/guard decomposition), yielding a spurious conflict. So + // factorization defers whenever the leading token is a guarded variable. + static bool leading_var_guarded(nielsen_node const* node, euf::snode const* lead) { + for (str_mem const& g : node->str_mems()) + if (g.is_guard() && g.m_str && g.m_str->first() == lead) + return true; + return false; + } + + rf_state* nielsen_graph::mk_rf_state(nielsen_node* /*node*/, str_mem const& mem) { + euf::snode const* const first = mem.m_str->first(); + SASSERT(first); + SASSERT(!first->is_char()); // constants are consumed earlier + + // Choose the factorization boundary so the tail starts with the LONGEST + // run of concrete characters c — this gives the split-engine lookahead + // oracle the most pruning information. head = u' (tokens before the run), + // tail = c · u''' (tokens from the run onward). + euf::snode_vector toks; + mem.m_str->collect_tokens(toks); + const unsigned total = toks.size(); + unsigned run_start = 0, run_len = 0; + for (unsigned i = 0; i < total; ) { + if (!toks[i]->is_char()) { ++i; continue; } + unsigned j = i; + while (j < total && toks[j]->is_char()) ++j; + if (j - i > run_len) { run_len = j - i; run_start = i; } + i = j; + } + // No constant run → fall back to splitting off the first token. + const unsigned p = run_len == 0 ? 1 : run_start; + SASSERT(p >= 1); + euf::snode const* head = p == 1 ? first : m_sg.drop_right(mem.m_str, total - p); + SASSERT(head); + + // Build the constant lookahead c and (if non-empty) an oracle that prunes + // splits whose ∇ cannot match c. The constant run is consumed from the + // tail per split (the δ_c derivative in rf_step), so the stored tail is + // u''' (c already removed). + zstring c; + for (unsigned i = 0; i < run_len; ++i) { + expr* ch = nullptr; + unsigned cv = 0; + VERIFY(m_seq.str.is_unit(toks[run_start + i]->get_expr(), ch)); + VERIFY(m_seq.is_const_char(ch, cv)); + c = c + zstring(cv); + } + euf::snode const* tail = c.empty() ? m_sg.drop_left(mem.m_str, p) + : m_sg.drop_left(mem.m_str, run_start + run_len); + SASSERT(tail); + + // Suspended sigma(regex): the iterator expands it one split at a time. + const expr_ref suspended = m_split_rw.make_split(mem.m_regex->get_expr()); + if (!suspended) + return nullptr; // non-regex argument (should not happen for a well-formed mem) + + split_oracle oracle; + if (!c.empty()) { + euf::sgraph& sg = m_sg; + oracle = [&sg, c](expr*, expr* n) { return split_lookahead_viable(n, sg, c); }; + } + + seq_split::iterator it = + m_split_rw.iterate_split(suspended, RF_LAZY_CAP, split_mode::strong, oracle); + rf_state* st = alloc(rf_state, mem, head, tail, c, std::move(it)); + m_rf_states.push_back(st); + return st; + } + + nielsen_graph::rf_step_result + nielsen_graph::rf_step(nielsen_node* node, rf_state* st, dep_tracker& conflict_dep) { + euf::snode const* const first = st->m_mem.m_str->first(); + dep_tracker eliminated_dep = st->m_mem.m_dep; + + expr_ref d(m), n(m); + while (st->m_iter.next(d, n)) { + // Consume the constant run c from the tail: tail = c·u''' ∈ ∇ ⟺ + // u''' ∈ δ_c(∇) (Brzozowski). Drops any split whose ∇ cannot start + // with c (there δ_c(∇) = ∅). Identity when c is empty. + euf::snode const* sn_q = m_sg.mk(n); + for (unsigned k = 0; sn_q && !sn_q->is_fail() && k < st->m_c.length(); ++k) + sn_q = m_sg.brzozowski_deriv(sn_q, m_sg.mk_char(st->m_c[k])); + SASSERT(sn_q); + if (sn_q->is_fail()) + continue; // ∇ can't start with c → infeasible split, skip + + euf::snode const* sn_p = m_sg.mk(d); + + // Feasibility: Δ must be non-empty. When head is the single token + // `first`, also intersect with other primitive constraints on `first`; + // for a multi-token head Δ constrains the whole prefix, so we only + // check Δ ≠ ∅. + euf::snode_vector regexes_p; + regexes_p.push_back(sn_p); + dep_tracker first_filter_dep = nullptr; + if (st->m_head == first) { + for (auto const& prev_mem : node->str_mems()) { + if (prev_mem.m_str == first) { + regexes_p.push_back(prev_mem.m_regex); + first_filter_dep = m_dep_mgr.mk_join(first_filter_dep, prev_mem.m_dep); + } + } + } + if (m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) { + eliminated_dep = m_dep_mgr.mk_join(eliminated_dep, first_filter_dep); + continue; // infeasible split → skip without branching + } + + const dep_tracker split_dep = m_dep_mgr.mk_join(st->m_mem.m_dep, first_filter_dep); + + // child A — the "first case": apply this split and drop the original + // membership. + nielsen_node* child_a = mk_child(node); + mk_edge(node, child_a, "regex fact", true); + auto& child_mems = child_a->str_mems(); + for (unsigned k = 0; k < child_mems.size(); ++k) { + if (child_mems[k] == st->m_mem) { + child_mems[k] = child_mems.back(); + child_mems.pop_back(); + break; + } + } + child_a->add_str_mem(str_mem(m, st->m_head, sn_p, split_dep)); + child_a->add_str_mem(str_mem(m, st->m_tail, sn_q, split_dep)); + + // child B — the "did not use the first case" branch: keep the + // membership and hand down the SAME iterator so factorization resumes + // from the next split. No substitution: child B is an exact clone, so + // st->m_mem stays valid down the whole chain. + nielsen_node* child_b = mk_child(node); + mk_edge(node, child_b, "regex fact rest", true); + child_b->set_rf_cont(st); + + return rf_step_result::branched; + } + + // No feasible split remained. + conflict_dep = eliminated_dep; + return st->m_iter.gave_up() ? rf_step_result::gaveup : rf_step_result::conflict; + } + bool nielsen_graph::apply_regex_factorization(nielsen_node* node) { if (m_regex_factorization_threshold == 0) return false; - struct rf_split { - euf::snode const* m_p; - euf::snode const* m_q; - dep_tracker m_dep; - }; + // Continuation: resume the iterator handed down to this node by its + // parent's "remaining splits" branch. + if (rf_state* st = node->rf_cont()) { + node->set_rf_cont(nullptr); // the iterator migrates to child B (or is dropped) + // If the cycle machinery has, in the meantime, put the leading variable + // under a guard, stop factorizing and defer (the iterator is dropped). + if (leading_var_guarded(node, st->m_mem.m_str->first())) + return false; + dep_tracker conflict_dep = nullptr; + switch (rf_step(node, st, conflict_dep)) { + case rf_step_result::branched: + return true; + case rf_step_result::conflict: + // Every split has been tried: the membership's split disjunction + // is refuted on this branch. + node->set_general_conflict(); + node->set_conflict(backtrack_reason::regex, conflict_dep); + return true; + case rf_step_result::gaveup: + return false; // engine give-up → let other modifiers handle the membership + } + } + // Fresh: find the first factorizable membership and start an iterator. for (str_mem const& mem : node->str_mems()) { SASSERT(mem.well_formed()); @@ -4035,74 +4235,25 @@ namespace seq { if (!mem.is_plain()) continue; - split_set pairs; - auto [head, tail] = split_membership(mem.m_str, mem.m_regex, sg(), m_regex_factorization_threshold, pairs); - if (!head) { - SASSERT(!tail); + // Defer to the cycle machinery when the leading variable is guarded. + if (leading_var_guarded(node, mem.m_str->first())) continue; - } - SASSERT(tail); - euf::snode const* const first = mem.m_str->first(); + rf_state* st = mk_rf_state(node, mem); + if (!st) + continue; // unsupported regex shape → try the next membership - vector feasible; - dep_tracker eliminated_dep = mem.m_dep; - - for (auto const &[tp, tq] : pairs) { - euf::snode const* sn_p = m_sg.mk(tp); - euf::snode const* sn_q = m_sg.mk(tq); - - // Also check intersection with other primitive constraints on `head`. - // Only valid when head is the single token `first`; for a multi-token - // head Δ constrains the whole prefix, so we only check Δ ≠ ∅. - euf::snode_vector regexes_p; - regexes_p.push_back(sn_p); - dep_tracker first_filter_dep = nullptr; - if (head == first) { - for (auto const& prev_mem : node->str_mems()) { - if (prev_mem.m_str == first) { - regexes_p.push_back(prev_mem.m_regex); - first_filter_dep = m_dep_mgr.mk_join(first_filter_dep, prev_mem.m_dep); - } - } - } - if (m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) { - eliminated_dep = m_dep_mgr.mk_join(eliminated_dep, first_filter_dep); - continue; - } - - feasible.push_back({ sn_p, sn_q, m_dep_mgr.mk_join(mem.m_dep, first_filter_dep) }); - if (feasible.size() > m_regex_factorization_threshold) - break; - } - - if (feasible.empty()) { - node->set_general_conflict(); - node->set_conflict(backtrack_reason::regex, eliminated_dep); + dep_tracker conflict_dep = nullptr; + switch (rf_step(node, st, conflict_dep)) { + case rf_step_result::branched: return true; + case rf_step_result::conflict: + node->set_general_conflict(); + node->set_conflict(backtrack_reason::regex, conflict_dep); + return true; + case rf_step_result::gaveup: + continue; // engine gave up on this membership → try the next one } - - if (feasible.size() > m_regex_factorization_threshold) - continue; - - for (auto& [m_p, m_q, m_dep] : feasible) { - nielsen_node* child = mk_child(node); - mk_edge(node, child, "regex fact", true); - - // remove the original mem from child - auto& child_mems = child->str_mems(); - for (unsigned k = 0; k < child_mems.size(); ++k) { - if (child_mems[k] == mem) { - child_mems[k] = child_mems.back(); - child_mems.pop_back(); - break; - } - } - - child->add_str_mem(str_mem(m, head, m_p, m_dep)); - child->add_str_mem(str_mem(m, tail, m_q, m_dep)); - } - return true; } return false; } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 9764d235a2..4d6a73fccb 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -163,7 +163,12 @@ namespace seq { // and arithmetic <= dependencies. void deps_to_lits(dep_manager &dep_mgr, dep_tracker deps, svector &eqs, svector &lits); - // decompose a membership constraint into a set of pairs of regex splits + // suspended state of a lazy regex factorization (see apply_regex_factorization). + struct rf_state; + + // decompose a membership constraint into a set of pairs of regex splits. + // Eagerly materialises the full split-set (used by the eager propagation path + // in theory_nseq::propagate_pos_mem); the lazy Nielsen path uses rf_state. std::pair split_membership(euf::snode const* str, euf::snode const* regex, euf::sgraph& sg, unsigned threshold, split_set& result); // Lookahead oracle for the split engine: is the split's right component @@ -589,6 +594,12 @@ namespace seq { // Parikh filter: set to true once apply_parikh_to_node has been applied // to this node. Prevents duplicate constraint generation across DFS runs. bool m_parikh_applied = false; + + // Lazy regex factorization continuation. Set only on a "remaining splits" + // child created by apply_regex_factorization: it carries the suspended + // split iterator so factorization resumes from the next split when this + // node is extended. Owned by nielsen_graph::m_rf_states (raw pointer here). + rf_state* m_rf_cont = nullptr; // number of constraints inherited from the parent node at clone time. // constraints[0..m_parent_ic_count) are already asserted at the // parent's solver scope; only [m_parent_ic_count..end) need to be @@ -644,6 +655,10 @@ namespace seq { nielsen_edge* parent_edge() const { return m_parent_edge; } void set_parent_edge(nielsen_edge* e) { m_parent_edge = e; } + // lazy regex factorization continuation (see m_rf_cont). + rf_state* rf_cont() const { return m_rf_cont; } + void set_rf_cont(rf_state* s) { m_rf_cont = s; } + // returns 0 if hash is unknown unsigned hash() const { return m_hash; @@ -897,6 +912,15 @@ namespace seq { // inclusion, derivatives. Allocated in the constructor; owned by this graph. seq_regex* m_seq_regex = nullptr; + // Persistent split engine driving the lazy regex factorization + // (apply_regex_factorization). A single instance kept here so the + // suspended split iterators stored in m_rf_states stay valid across + // search_dfs recursion and iterative deepening. + seq_rewriter m_split_rw; + // Owns the suspended factorization continuations (rf_state); nodes hold + // raw pointers into this pool. Freed in reset(). + ptr_vector m_rf_states; + // Maps each variable to its current length term // ptr_vector m_length_trail; @@ -1344,9 +1368,27 @@ namespace seq { // mirrors ZIPT's GPowerIntrModifier bool apply_gpower_intr(nielsen_node* node); - // generalized regex factorization (Boolean closure derivation rule) + // generalized regex factorization (Boolean closure derivation rule). + // Lazy: instead of materialising every split ⟨Δ,∇⟩ at once and branching + // N-way, it pulls the splits one at a time from a suspended iterator and + // branches binary — child A applies the next feasible split (head∈Δ, + // tail∈∇, original membership dropped); child B keeps the membership and + // carries the SAME iterator (rf_state) so factorization resumes from the + // next split. When the iterator is exhausted the membership's split + // disjunction is refuted → the continuation node is a regex conflict. bool apply_regex_factorization(nielsen_node* node); + // Build a suspended factorization (boundary head/tail + split iterator) + // for `mem`. Returns null if the regex shape is unsupported (the engine + // cannot even start a split). Allocated into m_rf_states. + rf_state* mk_rf_state(nielsen_node* node, str_mem const& mem); + + enum class rf_step_result { branched, conflict, gaveup }; + // Pull the next feasible split from `st` and, on success, create the two + // children of `node` (see apply_regex_factorization). On exhaustion sets + // `conflict_dep` and returns conflict; on engine give-up returns gaveup. + rf_step_result rf_step(nielsen_node* node, rf_state* st, dep_tracker& conflict_dep); + // helper for apply_gpower_intr: fires the substitution. // `fwd=true` uses left-to-right decomposition; `fwd=false` mirrors ZIPT's // backward (right-to-left) direction.