From 596cc14e8394b8e555130afe3e794e9fd30e4b30 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Thu, 9 Jul 2026 23:24:11 +0200 Subject: [PATCH] Replaced stabilizers by landing decomposition (faster!) Rank membership constraints by estimated size of their automaton Some refactoring Some bug fixes --- src/ast/euf/euf_seq_plugin.cpp | 2 +- src/ast/euf/euf_seq_plugin.h | 2 +- src/ast/euf/euf_sgraph.cpp | 109 +++- src/ast/euf/euf_sgraph.h | 20 +- src/ast/euf/euf_snode.h | 18 +- src/smt/seq/seq_nielsen.cpp | 919 ++++++++++++++++++++++++++------- src/smt/seq/seq_nielsen.h | 156 ++++-- src/smt/seq/seq_nielsen_pp.cpp | 3 +- src/smt/seq/seq_parikh.cpp | 2 +- src/smt/seq/seq_parikh.h | 6 +- src/smt/seq/seq_regex.cpp | 520 +------------------ src/smt/seq/seq_regex.h | 164 +----- src/smt/seq_model.cpp | 13 +- src/smt/theory_nseq.cpp | 3 +- src/smt/theory_nseq.h | 1 - src/test/seq_parikh.cpp | 2 +- src/test/seq_regex.cpp | 370 ------------- src/util/zstring.h | 2 - 18 files changed, 996 insertions(+), 1316 deletions(-) diff --git a/src/ast/euf/euf_seq_plugin.cpp b/src/ast/euf/euf_seq_plugin.cpp index bac403e49c..899e30fa04 100644 --- a/src/ast/euf/euf_seq_plugin.cpp +++ b/src/ast/euf/euf_seq_plugin.cpp @@ -242,7 +242,7 @@ namespace euf { } // - // Concat simplification rules from ZIPT: + // Concat simplification rules: // // 1. Kleene star merging: concat(u, v*, v*, w) = concat(u, v*, w) // when adjacent children in a concat chain have congruent star bodies. diff --git a/src/ast/euf/euf_seq_plugin.h b/src/ast/euf/euf_seq_plugin.h index d03d34286a..201c1d1c9b 100644 --- a/src/ast/euf/euf_seq_plugin.h +++ b/src/ast/euf/euf_seq_plugin.h @@ -11,7 +11,7 @@ Abstract: Merges equivalence classes taking into account associativity of concatenation and algebraic properties of strings and - regular expressions. Implements features from ZIPT: + regular expressions. -- Concat associativity: str.++ is associative, so concat(a, concat(b, c)) = concat(concat(a, b), c). diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index a4bea74346..af6b308557 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -172,11 +172,9 @@ namespace euf { } case snode_kind::s_power: { - // s^n: nullable follows base, consistent with ZIPT's PowerToken + // s^n: nullable follows base: // the exponent n is assumed to be a symbolic integer, may or may not be zero - // NSB review: SASSERT(n->num_args() == 2); and simplify code - // NSB review: is this the correct definition of ground what about the exponent? - SASSERT(n->num_args() >= 1); + SASSERT(n->num_args() == 2); snode const* base = n->arg(0); n->m_ground = base->is_ground(); n->m_regex_free = base->is_regex_free(); @@ -307,6 +305,108 @@ namespace euf { } } + // --------------------------------------------------------------------- + // Regex weight estimate + // + // A crude estimate of the size of the automaton for a regex, used to order + // membership constraints in regex factorization (smaller = factorized + // first, see str_mem::operator<). All arithmetic saturates at WEIGHT_MAX + // rather than wrapping, so a complement/intersection blow-up produces a + // huge-but-finite weight instead of aliasing a small one. + // --------------------------------------------------------------------- + static const unsigned WEIGHT_MAX = UINT_MAX; + + static unsigned sat_add(unsigned a, unsigned b) { + return a > WEIGHT_MAX - b ? WEIGHT_MAX : a + b; + } + + static unsigned sat_mul(unsigned a, unsigned b) { + if (a == 0 || b == 0) + return 0; + return a > WEIGHT_MAX / b ? WEIGHT_MAX : a * b; + } + + static unsigned sat_pow2(unsigned e) { + // 2^e; 1u<<31 still fits, e>=32 overflows unsigned -> saturate + return e >= 32 ? WEIGHT_MAX : (1u << e); + } + + // Weight recurrence (children are already weighted -> O(1)): + // w(ε)=0 w(a)=1 w(r1·r2)=w(r1)+w(r2) + // w(r*)=w(r)+1 w(r1|r2)=w(r1)+w(r2) w(r1&r2)=w(r1)·w(r2) + // w(~r)=2^{w(r)} w(ite(c,r1,r2))=max(w(r1),w(r2)) + void sgraph::compute_regex_weight(snode* n) { + unsigned w = 0; + switch (n->m_kind) { + case snode_kind::s_empty: + w = 0; + break; + case snode_kind::s_char: + case snode_kind::s_unit: + case snode_kind::s_range: + case snode_kind::s_full_char: + // a single (possibly symbolic) character / character class + w = 1; + break; + case snode_kind::s_var: + case snode_kind::s_power: + // not a regex proper; treated as an atom + w = 1; + break; + case snode_kind::s_fail: + case snode_kind::s_full_seq: + // trivial one-state automata (∅ and .*) + w = 1; + break; + case snode_kind::s_concat: + w = sat_add(n->arg(0)->regex_weight(), n->arg(1)->regex_weight()); + break; + case snode_kind::s_union: + w = sat_add(n->arg(0)->regex_weight(), n->arg(1)->regex_weight()); + break; + case snode_kind::s_intersect: + // product automaton + w = sat_mul(n->arg(0)->regex_weight(), n->arg(1)->regex_weight()); + break; + case snode_kind::s_star: + w = sat_add(n->arg(0)->regex_weight(), 1u); + break; + case snode_kind::s_plus: + w = sat_add(sat_mul(n->arg(0)->regex_weight(), 2u), 2u); + break; + case snode_kind::s_complement: + // determinization blow-up + w = sat_pow2(n->arg(0)->regex_weight()); + break; + case snode_kind::s_loop: { + // r{lo,hi}: ~hi unrolled copies (bounded) or r^lo·r* (unbounded) + const unsigned base = n->num_args() > 0 ? n->arg(0)->regex_weight() : 0; + unsigned lo = 1, hi = 1; + expr* body = nullptr; + if (n->get_expr() && m_seq.re.is_loop(n->get_expr(), body, lo, hi)) + w = sat_mul(base, std::max(hi, 1u)); + else if (n->get_expr() && m_seq.re.is_loop(n->get_expr(), body, lo)) + w = sat_add(sat_mul(base, sat_add(lo, 1u)), 1u); + else + w = sat_add(base, 1u); + break; + } + case snode_kind::s_ite: + // ite(c, r1, r2): args 1 and 2 are the branches + w = std::max(n->arg(1)->regex_weight(), n->arg(2)->regex_weight()); + break; + case snode_kind::s_to_re: + // to_re(s): one state per character of the (possibly symbolic) word + w = n->arg(0)->length(); + break; + case snode_kind::s_in_re: + default: + w = 1; + break; + } + n->m_regex_weight = w; + } + static constexpr unsigned HASH_BASE = 31; // Compute a 2x2 polynomial hash matrix for associativity-respecting hashing. @@ -361,6 +461,7 @@ namespace euf { const unsigned id = m_nodes.size(); snode *n = snode::mk(m_region, e, k, id, num_args, args); compute_metadata(n); + compute_regex_weight(n); compute_hash_matrix(n); m_nodes.push_back(n); SASSERT(!n->is_char_or_unit() || m_seq.str.is_unit(n->get_expr())); diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h index c2798a7023..26a81d3537 100644 --- a/src/ast/euf/euf_sgraph.h +++ b/src/ast/euf/euf_sgraph.h @@ -10,7 +10,6 @@ Abstract: Sequence/string graph layer Encapsulates string and regex expressions for the string solver. - Implements the string graph layer from ZIPT (https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT). The sgraph maps Z3 sequence/regex AST expressions to snode structures organized as binary concatenation trees with metadata, and owns an egraph with a seq_plugin for congruence closure. @@ -29,24 +28,6 @@ Abstract: * re.++ identity/absorption (concat(a, epsilon) = a, concat(a, ∅) = ∅). -- enode registration via mk_enode(expr*). - ZIPT features not yet ported: - - -- Str operations: normalisation with union-find representatives and - cache migration, balanced tree maintenance, drop left/right with - caching, substitution, indexed access, iteration, ToList caching, - simplification, derivative computation, structural equality with - associative hashing, rotation equality, expression reconstruction, - Graphviz export. - - -- StrToken subclasses: SymCharToken, StrAtToken, SubStrToken, - SetToken, PostToken/PreToken. - - -- StrToken features: Nielsen-style GetDecomposition with side - constraints, NamedStrToken extension tracking for variable - splitting with PowerExtension, CollectSymbols for Parikh analysis, - MinTerms for character class analysis, token ordering, Derivable - and BasicRegex flags. - Author: Clemens Eisenhofer 2026-03-01 @@ -112,6 +93,7 @@ namespace euf { snode* mk_snode(expr* e, snode_kind k, unsigned num_args, snode const** args); snode_kind classify(expr* e) const; void compute_metadata(snode* n); + void compute_regex_weight(snode* n); void compute_hash_matrix(snode* n); void collect_re_predicates(snode const* re, expr_ref_vector& preds); diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index b19d285f2c..459e1f9337 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -10,7 +10,7 @@ Abstract: snode layer for sequence/string graph Encapsulates strings in the style of euf_enode.h. - Maps Z3 sequence expressions to a ZIPT-style representation where + Maps Z3 sequence expressions to a representation where strings are composed of tokens (characters, variables, powers, regex, etc.) organized as a binary tree of concatenations. @@ -66,13 +66,15 @@ namespace euf { unsigned m_id = UINT_MAX; unsigned m_num_args = 0; - // metadata flags, analogous to ZIPT's Str/StrToken properties + // metadata flags bool m_ground = true; // no uninterpreted string variables bool m_regex_free = true; // no regex constructs bool m_is_classical = true; // classical regular expression bool m_rigid = false; // defined seq op (replace/replace_all/replace_re*) — opaque to Nielsen, never substitute/split unsigned m_level = 0; // tree depth/level (0 for empty, 1 for singletons) unsigned m_length = 0; // token count, number of leaf tokens in the tree + unsigned m_regex_weight = 0; // estimated automaton size of this regex (saturating); + // cached at creation by sgraph::compute_regex_weight // hash matrix for associativity-respecting hashing (2x2 polynomial hash matrix) // all zeros means not cached, non-zero means cached @@ -222,6 +224,15 @@ namespace euf { unsigned length() const { return m_length; } + // Estimated size ("weight") of the automaton for this regex, computed + // with saturating arithmetic (see sgraph::compute_regex_weight) and + // cached at node creation. Used to order membership constraints in + // regex factorization (smaller weight = factorized first). Meaningful + // for regex snodes; for pure string/word nodes it just tracks a token + // count and is ignored by the membership heuristic. + unsigned regex_weight() const { + return m_regex_weight; + } // associativity-respecting hash: cached if the 2x2 matrix is non-zero. // M[0][0] = HASH_BASE^(num_leaves) which is always nonzero since HASH_BASE @@ -328,7 +339,7 @@ namespace euf { } return true; } - // is this a leaf token (analogous to ZIPT's StrToken as opposed to Str) + // is this a leaf token bool is_token() const { switch (m_kind) { case snode_kind::s_empty: @@ -341,7 +352,6 @@ namespace euf { return m_expr ? m_expr->get_sort() : nullptr; } - // analogous to ZIPT's Str.First / Str.Last snode const *first() const { snode const* s = this; while (s->is_concat()) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 2f35c8f873..a1f33600b8 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -9,9 +9,6 @@ Abstract: Nielsen graph implementation for string constraint solving. - Ports the constraint types and Nielsen graph structures from - ZIPT (https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT/Constraints) - Author: Clemens Eisenhofer 2026-03-02 @@ -181,7 +178,7 @@ namespace seq { return !cur->is_fail(); } - // Directional helpers mirroring ZIPT's fwd flag: + // Directional helpers: // fwd=true -> left-to-right (prefix/head) // fwd=false -> right-to-left (suffix/tail) static euf::snode const* dir_token(euf::snode const* s, const bool fwd) { @@ -288,21 +285,35 @@ namespace seq { bool str_mem::is_trivial(nielsen_node const* n) const { SASSERT(m_str && m_regex); + if (m_kind == mem_kind::stab_view) + // The plain full-seq shortcut below does NOT apply to a view: its + // language L_{Q,{s}}(state) is about *landing* at s, not membership + // in L(state) — a view whose run state is Σ* with s ≠ Σ* denotes ∅ + // (see is_contradiction), so treating it as trivial would silently + // drop the constraint. + // ε ∈ L_{Q,{s}}(state) iff current state ≡ acceptance state s (=m_root). + return m_str->is_empty() && m_regex == m_root; if (m_regex->is_full_seq()) return true; if (!m_str->is_empty()) return false; - if (m_kind == mem_kind::stab_view) - // ε ∈ L_{Q,{s}}(state) iff current state ≡ acceptance state s (=m_root). - return m_regex == m_root; return n->graph().sg().re_nullable(m_regex) == l_true; } bool str_mem::is_contradiction(nielsen_node const* n) const { - if (!(m_str && m_regex && m_str->is_empty())) + if (!(m_str && m_regex)) + return false; + if (m_kind == mem_kind::stab_view) { + // δ_a(Σ*) = Σ* for every a: once the run state is Σ*, it stays + // there, so no continuation can land at a different acceptance + // state — the view denotes ∅ regardless of the remaining string. + if (m_regex->is_full_seq() && m_regex != m_root) + return true; + // ε ∉ view when current state ≢ acceptance s + return m_str->is_empty() && m_regex != m_root; + } + if (!m_str->is_empty()) return false; - if (m_kind == mem_kind::stab_view) - return m_regex != m_root; // ε ∉ view when current state ≢ acceptance s return n->graph().sg().re_nullable(m_regex) == l_false; } @@ -663,9 +674,16 @@ namespace seq { if (!state || nu == 0) return false; const unsigned sid = state->get_id(); - // r ∈ Q_nu iff r is incident to a partial-DFA edge whose extraction - // index lies in [1, nu] (the "edges marked ≤ ν" subautomaton of the - // implementation-aspects section of the paper). + // Exact semantics: ν names the state set recorded when the view was + // created (paper: a view is identified by ν AND its recorded state + // set Q; see mark_reachable_projection_edges). + const auto sit = m_projection_snapshots.find(nu); + if (sit != m_projection_snapshots.end()) + return sit->second.m_ids.contains(sid); + // Fallback for a ν minted without snapshot (none are anymore; kept for + // robustness): r ∈ Q_ν iff r is incident to a partial-DFA edge whose + // extraction index lies in [1, ν] — the historical watermark, which + // over-approximates the intended Q by the union of all extractions. auto incident = [&](std::unordered_map const &adj) { auto it = adj.find(sid); if (it == adj.end()) @@ -771,6 +789,8 @@ namespace seq { m_partial_dfa_edge_index.clear(); m_partial_dfa_pin.reset(); m_projection_extract_idx = 0; + m_projection_snapshots.clear(); + m_projection_head_cache.clear(); m_explored_automaton.reset(); m_unsat_node_cache.clear(); m_siblings.clear(); @@ -819,8 +839,7 @@ namespace seq { } // ----------------------------------------------------------------------- - // Power simplification helpers (mirrors ZIPT's MergePowers, - // SimplifyPowerElim/CommPower, SimplifyPowerSingle) + // Power simplification helpers // ----------------------------------------------------------------------- // Check if exponent b equals exponent a + diff for some rational constant diff. @@ -1032,7 +1051,7 @@ namespace seq { // CommPower: count how many times a power's base pattern appears in // the directional prefix of the other side (fwd=true: left prefix, - // fwd=false: right suffix). Mirrors ZIPT's CommPower helper. + // fwd=false: right suffix). // Returns (count_expr, num_tokens_consumed). count_expr is nullptr // when no complete base-pattern match is found. static std::pair comm_power( @@ -1290,33 +1309,49 @@ namespace seq { } unsigned nielsen_graph::mark_reachable_projection_edges(euf::snode const* head_re) { - // Generalizes mark_scc_projection_edges to the forward-reachable set: - // mark every edge whose source is reachable from head_re with the current - // extraction index ν, bumping ν iff something new was marked. Views/co- - // views gate on projection_state_in_Q (edges marked ≤ ν), so the ν - // returned here identifies exactly this Q. + // Snapshot semantics (paper "Implementation Aspects": a view is + // identified by ν AND its recorded state set Q). The returned ν names + // the EXACT forward-reachable set Q of head_re at this moment, stored + // in m_projection_snapshots; views gate on membership in that snapshot + // (projection_state_in_Q). The per-edge watermark is still written — + // as the fallback for a ν without snapshot — but no longer defines + // view semantics: on its own, "edges marked ≤ ν" is the union of ALL + // extractions up to ν, blurring this view's Q with unrelated heads' + // regions once exploration is partial (lazy mode). + if (!head_re || !head_re->get_expr()) + return 0; + const unsigned head_id = head_re->get_expr()->get_id(); + + // Fast path: the partial DFA is monotone, so an unchanged edge count + // means the head's reachable set is unchanged — reuse the previous ν. + auto cit = m_projection_head_cache.find(head_id); + if (cit != m_projection_head_cache.end() + && cit->second.first == m_partial_dfa_edges.size()) + return cit->second.second; + uint_set Q; collect_reachable_from_head(head_re, Q); - unsigned newly_marked = 0; - for (const unsigned src_id : Q) { - auto it = m_partial_dfa_out.find(src_id); - if (it == m_partial_dfa_out.end()) - continue; - for (const unsigned edge_idx : it->second) { - if (edge_idx >= m_partial_dfa_edges.size()) - continue; - partial_dfa_edge const& e = m_partial_dfa_edges[edge_idx]; - if (!e.m_dst || !Q.contains(e.m_dst->get_id())) - continue; - if (e.m_projection_idx == 0) - ++newly_marked; + + // Slow path: the graph grew, but possibly only outside the head's + // region — reuse the previous snapshot if the set is unchanged. + if (cit != m_projection_head_cache.end()) { + const auto sit = m_projection_snapshots.find(cit->second.second); + if (sit != m_projection_snapshots.end() + && sit->second.m_ids.num_elems() == Q.num_elems()) { + bool same = true; + for (const unsigned id : Q) + if (!sit->second.m_ids.contains(id)) { same = false; break; } + if (same) { + cit->second.first = m_partial_dfa_edges.size(); + return cit->second.second; + } } } - if (newly_marked == 0) - return m_projection_extract_idx; // Q already covered by the current ν - ++m_projection_extract_idx; - const unsigned extract_idx = m_projection_extract_idx; + const unsigned nu = ++m_projection_extract_idx; + + // Watermark the in-Q edges (only previously unmarked ones) — fallback + // data only, see above. for (const unsigned src_id : Q) { auto it = m_partial_dfa_out.find(src_id); if (it == m_partial_dfa_out.end()) @@ -1328,10 +1363,194 @@ namespace seq { if (!e.m_dst || !Q.contains(e.m_dst->get_id())) continue; if (e.m_projection_idx == 0) - e.m_projection_idx = extract_idx; + e.m_projection_idx = nu; } } - return extract_idx; + + // Record the snapshot: the id set plus the state exprs (head first, + // then in-Q edge endpoints). Pin the head so every stored expr + // outlives sgraph pops (edge endpoints are already pinned by + // record_partial_derivative_edge). + projection_snapshot snap; + snap.m_ids = Q; + uint_set added; + m_partial_dfa_pin.push_back(head_re->get_expr()); + snap.m_states.push_back(head_re->get_expr()); + added.insert(head_id); + for (partial_dfa_edge const& e : m_partial_dfa_edges) { + for (expr* ep : { e.m_src, e.m_dst }) { + if (!ep) + continue; + const unsigned id = ep->get_id(); + if (!Q.contains(id) || added.contains(id)) + continue; + added.insert(id); + snap.m_states.push_back(ep); + } + } + m_projection_snapshots.emplace(nu, std::move(snap)); + m_projection_head_cache[head_id] = { m_partial_dfa_edges.size(), nu }; + return nu; + } + + void nielsen_graph::collect_projection_states(unsigned nu, svector& out) { + // Enumeration counterpart of projection_state_in_Q — keep in sync with + // it (it is the membership test the view gates use in consume_view and + // comp_step). Exact semantics: the states of the ν-snapshot. + if (nu == 0) + return; + const auto sit = m_projection_snapshots.find(nu); + if (sit != m_projection_snapshots.end()) { + for (expr* ep : sit->second.m_states) { + // mk, not find: the exprs are pinned but their snodes may have + // been released by an sgraph pop. + euf::snode const* sn = m_sg.mk(ep); + if (sn) + out.push_back(sn); + } + return; + } + // Fallback for a ν without snapshot: the states incident to an edge + // with extraction index in [1, ν] (historical watermark). + uint_set added; + for (partial_dfa_edge const& e : m_partial_dfa_edges) { + if (e.m_projection_idx == 0 || e.m_projection_idx > nu) + continue; + for (expr* ep : { e.m_src, e.m_dst }) { + if (!ep) + continue; + const unsigned id = ep->get_id(); + if (added.contains(id)) + continue; + // mk, not find: the expr is pinned (m_partial_dfa_pin) but its + // snode may have been released by an sgraph pop since the edge + // was recorded (see the analogous collection of Qstates in + // apply_landing_decomposition). + euf::snode const* sn = m_sg.mk(ep); + if (sn) { added.insert(id); out.push_back(sn); } + } + } + } + + void nielsen_graph::compute_view_length_info(unsigned nu, expr* from, view_len_info& info) { + info.m_dist.reset(); + info.m_stride = 0; + info.m_ok = false; + if (!from || nu == 0) + return; + const auto sit = m_projection_snapshots.find(nu); + if (sit == m_projection_snapshots.end()) + return; // watermark-fallback ν without an exact snapshot: no abstraction + uint_set const& Q = sit->second.m_ids; + if (!Q.contains(from->get_id())) + return; // gate closed at the head: L ⊆ {ε}, handled by the degenerate cases + + // BFS over the recorded in-Q edges (each edge consumes one character). + // At ν-minting time compute_frontier saturated these edges, so they are + // exactly the one-character transitions among Q_ν states; edges are only + // ever added, so saturation persists and the abstraction stays sound. + unsigned_vector queue; + unsigned qhead = 0; + info.m_dist.insert(from->get_id(), 0); + queue.push_back(from->get_id()); + while (qhead < queue.size()) { + const unsigned u = queue[qhead++]; + const unsigned du = info.m_dist.find(u); + auto it = m_partial_dfa_out.find(u); + if (it == m_partial_dfa_out.end()) + continue; + for (const unsigned edge_idx : it->second) { + if (edge_idx >= m_partial_dfa_edges.size()) + continue; + partial_dfa_edge const& e = m_partial_dfa_edges[edge_idx]; + if (!e.m_dst) + continue; + const unsigned v = e.m_dst->get_id(); + if (!Q.contains(v) || info.m_dist.contains(v)) + continue; + info.m_dist.insert(v, du + 1); + queue.push_back(v); + } + } + + // Stride g = gcd over reachable in-Q edges (u,v) of (d(u) + 1 − d(v)): + // by telescoping, every gated walk from the head to v has length + // ≡ d(v) (mod g); g = 0 means every such walk has length exactly d(v). + unsigned g = 0; + for (const unsigned u : queue) { + const unsigned du = info.m_dist.find(u); + auto it = m_partial_dfa_out.find(u); + if (it == m_partial_dfa_out.end()) + continue; + for (const unsigned edge_idx : it->second) { + if (edge_idx >= m_partial_dfa_edges.size()) + continue; + partial_dfa_edge const& e = m_partial_dfa_edges[edge_idx]; + if (!e.m_dst) + continue; + const unsigned v = e.m_dst->get_id(); + if (!Q.contains(v)) + continue; + SASSERT(info.m_dist.contains(v)); // v is reachable since u is + const unsigned t = du + 1 - info.m_dist.find(v); + if (t != 0) + g = g == 0 ? t : u_gcd(g, t); + } + } + info.m_stride = g; + info.m_ok = true; + } + + void nielsen_graph::add_view_length_constraints(nielsen_edge* e, view_len_info const& info, unsigned nu, + euf::snode const* pinned, expr* to, dep_tracker const& dep) { + if (!e || !info.m_ok || !pinned || !to) + return; + + unsigned min_len = 0, stride = 0; + bool exact = false; + if (projection_state_in_Q(to, nu)) { + // Walk and landing state stay inside Q_ν, where the recorded edges + // are saturated: min = d(to), stride = g. + if (!info.m_dist.contains(to->get_id())) + return; // unreachable ⇒ empty view; the branch dies at its leaf + min_len = info.m_dist.find(to->get_id()); + stride = info.m_stride; + exact = stride == 0; + } + else { + // Landing target outside Q_ν (view landing at root ∉ Q_ν): the + // final hop may be an UNRECORDED transition from any reachable + // q ∈ Q_ν, of length d(q) + 1 ≡ 1 (mod gcd(g, all reachable d(q))), + // so only this weakened progression is sound. + min_len = 1; + stride = info.m_stride; + for (auto const& [id, d] : info.m_dist) { + (void)id; + if (d != 0) + stride = stride == 0 ? d : u_gcd(stride, d); + } + exact = stride == 0; // only the head is reachable: len = 1 exactly + } + + if (!exact && min_len == 0 && stride <= 1) + return; // trivial + + const expr_ref len = compute_length_expr(pinned); + if (exact) { + e->add_side_constraint(mk_constraint(a.mk_eq(len, a.mk_int(min_len)), dep)); + return; + } + if (min_len > 0) + e->add_side_constraint(mk_constraint(a.mk_ge(len, a.mk_int(min_len)), dep)); + if (stride > 1) { + // stride | (len − min). Rewrite eagerly — the raw divisibility + // predicate is not internalized automatically (see the analogous + // gradient propagation in theory_nseq). + expr_ref div(a.mk_divides(a.mk_int(stride), a.mk_sub(len, a.mk_int(min_len))), m); + th_rewriter rw(m); + rw(div); + e->add_side_constraint(mk_constraint(div, dep)); + } } void nielsen_graph::compute_frontier(uint_set const& Q, svector const& Qstates, @@ -1615,8 +1834,7 @@ namespace seq { } } - // pass 3: power simplification (mirrors ZIPT's LcpCompression + - // SimplifyPowerElim + SimplifyPowerSingle) + // pass 3: power simplification for (str_eq& eq : m_str_eq) { SASSERT(eq.well_formed()); if (eq.is_trivial()) @@ -1645,8 +1863,7 @@ namespace seq { // 3c: CommPower-based power elimination — when one side starts // with a power w^p, count base-pattern occurrences c on the // other side's prefix. If we can determine the ordering between - // p and c, cancel the matched portion. Mirrors ZIPT's - // SimplifyPowerElim calling CommPower. + // p and c, cancel the matched portion. // Spec: CommPower cancellation. // Given: pow_side = w^p · rest_pow and other_side = w^c · rest_other // where c is the number of times the base pattern w occurs in the @@ -1798,7 +2015,7 @@ namespace seq { } // consume concrete characters from str_mem via Brzozowski derivatives - // in both directions (left-to-right, then right-to-left), mirroring ZIPT. + // in both directions (left-to-right, then right-to-left). for (str_mem& mem : m_str_mem) { SASSERT(mem.well_formed()); if (mem.is_primitive() || !mem.is_plain()) @@ -1940,12 +2157,15 @@ namespace seq { // the string by replacing variables with their regex intersection // and check if the result intersected with the target regex is empty. // Detects infeasible constraints that would otherwise require - // expensive exploration. Mirrors ZIPT NielsenNode.CheckRegexWidening. + // expensive exploration. SASSERT(m_graph.m_seq_regex); for (str_mem const& mem : m_str_mem) { SASSERT(mem.well_formed()); if (mem.is_primitive()) continue; + // Views are widened as well: check_regex_widening substitutes a + // sound over-approximation of the view language (see there) and + // returns false when none applies. dep_tracker dep = mem.m_dep; if (m_graph.check_regex_widening(*this, mem, dep)) { set_general_conflict(); @@ -2467,9 +2687,9 @@ namespace seq { // Before declaring SAT, check leaf-node regex feasibility: // for each variable with multiple regex constraints, verify // that the intersection of all its regexes is non-empty. - // Mirrors ZIPT NielsenNode.CheckRegex. dep_tracker dep = nullptr; - if (!check_leaf_regex(*node, dep)) { + const lbool leaf_feasible = check_leaf_regex(*node, dep); + if (leaf_feasible == l_false) { node->set_general_conflict(); node->set_conflict(backtrack_reason::regex, dep); // string-only conflict (empty intersection) → memoize. @@ -2478,6 +2698,12 @@ namespace seq { m_unsat_node_cache.insert(node); return search_result::unsat; } + if (leaf_feasible == l_undef) + // The product search exhausted its budget: the leaf can be + // neither confirmed nor refuted. Declaring SAT here would let + // the model builder emit a witness that may violate the very + // constraints the check could not decide. + return search_result::unknown; assert_node_side_constraints(node); // We need to have everything asserted before reporting SAT // (otw. the outer solver might assume false-assigned literals to be true) @@ -3202,7 +3428,6 @@ namespace seq { // ----------------------------------------------------------------------- // EqSplit: find_eq_split_point - // Port of ZIPT's StrEq.SplitEq algorithm. // // Walks tokens from each side tracking two accumulators: // - lhs_has_symbolic / rhs_has_symbolic : whether a variable-length token @@ -3334,7 +3559,7 @@ namespace seq { } // ----------------------------------------------------------------------- - // apply_eq_split — Port of ZIPT's EqSplitModifier.Apply + // apply_eq_split // // For a regex-free equation LHS = RHS, finds a split point and decomposes // into two shorter equations with optional padding variable: @@ -3483,6 +3708,15 @@ namespace seq { if (!harvest_mode() && apply_landing_decomposition(node)) return ++m_stats.m_mod_star_intr, true; + // Priority 6b: ViewLandingDecomp - land-only decomposition of a view + // constraint made non-primitive by a substitution on a pinned variable + // (paper §5.3, "Landing decomposition on view constraints"). Must + // preempt RegexVarSplit: character-unwinding a pinned variable would + // re-introduce the cycle-unrolling divergence the views prevent. + // (regex-related: skipped in benchmark-harvest mode) + if (!harvest_mode() && apply_view_landing_decomposition(node)) + return ++m_stats.m_mod_view_land, true; + // Priority 7: GPowerIntr - ground power introduction if (apply_gpower_intr(node)) return ++m_stats.m_mod_gpower_intr, true; @@ -3669,16 +3903,11 @@ namespace seq { // starts with a power token u^n. In that case, branch: // (1) base u → ε (base is empty, so u^n = ε) // (2) u^n → ε (the power is zero, replace power with empty) - // mirrors ZIPT's PowerEpsilonModifier (which requires LHS.IsEmpty()) // ----------------------------------------------------------------------- bool nielsen_graph::apply_power_epsilon(nielsen_node* node) { // Match only when one equation side is empty and the other starts - // with a power. This mirrors ZIPT where PowerEpsilonModifier is - // constructed only inside the "if (LHS.IsEmpty())" branch of - // ExtendDir. When both sides are non-empty and a power faces a - // constant, ConstNumUnwinding (priority 4) handles it with both - // n=0 and n≥1 branches. + // with a power. euf::snode const* power = nullptr; dep_tracker dep = m_dep_mgr.mk_empty(); for (str_eq const& eq : node->str_eqs()) { @@ -3730,7 +3959,6 @@ namespace seq { // For equations involving two power tokens u^m and u^n with the same base, // branch on the numeric relationship: m <= n vs n < m. // Generates proper integer side constraints for each branch. - // mirrors ZIPT's NumCmpModifier // ----------------------------------------------------------------------- bool nielsen_graph::apply_num_cmp(nielsen_node* node) { @@ -3789,7 +4017,6 @@ namespace seq { // Branch 2: c ≤ p (add constraint p ≥ c) // After branching, simplify_and_init's CommPower pass (3c) can resolve // the ordering deterministically and cancel the matched portion. - // mirrors ZIPT's SplitPowerElim + NumCmpModifier // ----------------------------------------------------------------------- bool nielsen_graph::apply_split_power_elim(nielsen_node* node) { @@ -3852,7 +4079,6 @@ namespace seq { // For a power token u^n facing a constant (char) head, // branch: (1) n = 0 → u^n = ε, (2) n >= 1 → peel one u from power. // Generates integer side constraints for each branch. - // mirrors ZIPT's ConstNumUnwindingModifier // ----------------------------------------------------------------------- bool nielsen_graph::apply_const_num_unwinding(nielsen_node* node) { @@ -3884,7 +4110,7 @@ namespace seq { // Side constraint: n >= 1 // Create a proper nested power base^(n-1) instead of a fresh string variable. // This preserves power structure so that simplify_and_init can merge and - // cancel adjacent same-base powers (mirroring ZIPT's SimplifyPowerUnwind). + // cancel adjacent same-base powers. // Explored first because the n≥1 branch is typically more productive // for SAT instances (preserves power structure). const seq_util &seq = m_sg.get_seq_util(); @@ -3908,22 +4134,31 @@ namespace seq { } // ----------------------------------------------------------------------- - // Helper: ensure_automaton_explored (lazy, on-demand, cached) - // Records the *complete* reachable Brzozowski automaton of root_re into the - // partial DFA — but only once per regex component. This is the lazy - // Q-completion: instead of re-running a fixed-depth BFS on every cycle - // decomposition (the old precompute_partial_dfa(R, depth), which re-explored - // R's automaton on each of the ~hundreds of decompositions and, with a - // shallow depth, left Q incomplete so guards discharged prematurely and laps - // never closed), we explore each component once to saturation and remember - // every state we visited. A later decomposition whose head was reached by an - // earlier exploration finds it already covered and does no work. + // Helper: ensure_automaton_explored (budgeted, on-demand, cached) + // Records the reachable Brzozowski automaton of root_re into the partial + // DFA, once per regex component, up to a per-call STATE BUDGET. This is + // the eager/lazy hybrid of the paper's two modes: + // - a component smaller than the budget (the common case) is saturated + // in one go: every land-at-s block of the landing decomposition is + // available immediately, the frontier is empty, and no escape ever + // re-walks explored structure; + // - a larger component is left PARTIAL — a sound under-approximation, + // exactly as at the resource limit: the frontier is then non-empty + // and the ESCAPE branches grow Q on demand, one recorded edge at a + // time — the paper's lazy mode. This avoids materializing large + // derivative automata (complement/intersection blowups, e.g. the + // paper's Σ*bΣ^k example) up front. + // States dequeued before the cutoff are in m_explored_automaton; the + // truncated remainder is NOT, so consumption-time minterm-edge recording + // stays active for those sources — escapes keep making progress and the + // termination bound (escapes ≤ edges of the finite monotone G) holds. // - // Completeness matters: the cycle guard / stabilizer view gate on whether the - // current state lies in Q (projection_state_in_Q), and that is only sound as - // a *bound* when Q contains the whole SCC of the head. The BFS is bounded by - // the finite reachable automaton (Brzozowski states modulo ACI), so it - // terminates; m.inc() keeps it responsive to the resource limit. + // Soundness never depends on completeness of Q: a land-at-s view forces + // δ_x(head) = s for ANY Q, and the stabilizer invariant holds for any Q + // (paper, Invariant 1); a partial Q only shifts work to the escapes. + // The BFS is bounded by the budget and the finite reachable automaton + // (Brzozowski states modulo ACI); m.inc() keeps it responsive to the + // resource limit. // ----------------------------------------------------------------------- void nielsen_graph::ensure_automaton_explored(euf::snode const* root_re) { @@ -3933,6 +4168,12 @@ namespace seq { if (m_explored_automaton.contains(root_re->get_expr()->get_id())) return; + // Per-call cap on eagerly explored states. Components that overflow + // it fall back to the paper's lazy escape-driven exploration. + // TODO: expose as smt.nseq parameter if tuning proves worthwhile. + static constexpr unsigned exploration_budget = 512; + unsigned processed = 0; + svector queue; queue.push_back(root_re); @@ -3944,6 +4185,8 @@ namespace seq { const unsigned re_eid = re->get_expr()->get_id(); if (m_explored_automaton.contains(re_eid)) continue; // already explored (here or in a previous component) + if (processed++ >= exploration_budget) + return; // budget: leave the remainder to the escape branches m_explored_automaton.insert(re_eid); euf::snode_vector mts; @@ -4074,13 +4317,14 @@ namespace seq { if (!R->is_ground() || R->kind() == euf::snode_kind::s_ite) continue; - // Eagerly explore R's reachable automaton (once, cached) so the SCC - // gate below and the landing enumeration see the full explored region - // Q — this is the automaton-based landing. Without it the cycle would - // not be recorded before factorization/var_split fire, so landing - // would never trigger. If exploration hits the resource limit Q is - // left partial (a sound under-approximation) and the escape branches - // recover completeness. + // Explore R's reachable automaton (once, cached, BUDGETED) so the + // SCC gate below and the landing enumeration see the explored + // region Q. Without it the cycle would not be recorded before + // factorization/var_split fire, so landing would never trigger. + // If exploration is cut off (state budget or resource limit) Q is + // left partial — a sound under-approximation, the paper's lazy + // mode — and the escape branches recover completeness, growing Q + // one recorded edge at a time. ensure_automaton_explored(R); // Trigger: R must sit on a detected cycle in the explored G. This is @@ -4108,7 +4352,12 @@ namespace seq { if (!ep) continue; const unsigned id = ep->get_id(); if (!Q.contains(id) || added.contains(id)) continue; - euf::snode const* sn = m_sg.find(ep); + // mk, not find: the expr is pinned (m_partial_dfa_pin) but its + // snode may have been released by an sgraph pop since the edge + // was recorded. Silently skipping the state would delete its + // land-at-s block from the frontier partition — the split would + // no longer cover all values of x (unsound UNSAT). + euf::snode const* sn = m_sg.mk(ep); if (sn) { added.insert(id); Qstates.push_back(sn); } } } @@ -4118,23 +4367,36 @@ namespace seq { vector frontier; compute_frontier(Q, Qstates, frontier); - // Mark the reachable subautomaton, fixing the ν that identifies Q_ν - // for every view created below. ν may be 0 in the Q = {R} bootstrap - // (no in-Q edges yet); a view with ν = 0 denotes exactly {ε} at R, - // which is precisely what unwinding needs. + // Fix the ν identifying Q for every view created below: it names + // the exact snapshot of R's reachable set (the internal edges just + // recorded by compute_frontier connect existing Q states only, so + // the snapshot coincides with Qstates). The views therefore gate + // on precisely the enumerated region, and together with the + // escape blocks the branches partition Σ* exactly (Lemma 4.7). const unsigned nu = mark_reachable_projection_edges(R); + SASSERT(nu > 0); + + // Length abstraction of the region (one BFS serves every land and + // escape pin below): every pinned view gets len ≥ d(s) and + // stride | (len − d(s)) side constraints, so the outer arith + // model can only assign the pinned variable a length the view can + // realize (otherwise seq_model's witness search fails at the + // assigned length and the emitted model is length-inconsistent). + view_len_info vli; + compute_view_length_info(nu, R->get_expr(), vli); sort* seq_sort = x->get_expr()->get_sort(); // (a) LAND-AT-s branches (progress: x removed). for (euf::snode const* s : Qstates) { nielsen_node* child = mk_child(node); - mk_edge(node, child, "land", /*progress*/ true); + nielsen_edge* le = mk_edge(node, child, "land", /*progress*/ true); str_mem& cm = child->m_str_mem[mi]; cm.m_str = m_sg.drop_first(cm.m_str); // u cm.m_regex = s; // active becomes u ∈ s // x ∈_{Q_ν,{s}} R : state = R (start), root = s (acceptance). child->add_str_mem(str_mem::mk_view(m, x, R, s, nu, mem.m_dep)); + add_view_length_constraints(le, vli, nu, x, s->get_expr(), mem.m_dep); TRACE(seq, tout << "landing: land x=" << mk_pp(x->get_expr(), m) << " at " << mk_pp(s->get_expr(), m) << " R=" << mk_pp(R->get_expr(), m) << " nu=" << nu << "\n"); @@ -4146,9 +4408,25 @@ namespace seq { char_set cs = m_seq_regex->minterm_to_char_set(fe.m_mt->get_expr()); if (cs.is_empty()) continue; - euf::snode const* aunit = - m_sg.mk(m_seq.str.mk_unit(m_seq.mk_char(cs.first_char()))); euf::snode const* x1 = mk_fresh_var(seq_sort); + // Escape char: a singleton class contributes its concrete char. + // A multi-char class must NOT be collapsed to a representative: + // the substitution x → x1·a·x2 reaches EVERY constraint on x, + // where the characters of p's minterm are distinguishable (other + // memberships, equations, later derivative steps from different + // states), so committing to one char would drop every model whose + // escape char is another member of the class. Use the symbolic + // char x[|x1|] instead, range-restricted to the class; the + // ordinary symbolic consumption + apply_regex_if_split machinery + // then enumerates exactly the feasible sub-cases. + const bool concrete = cs.is_unit(); + euf::snode const* aunit; + if (concrete) + aunit = m_sg.mk(m_seq.str.mk_unit(m_seq.mk_char(cs.first_char()))); + else { + const expr_ref nth(m_seq.str.mk_nth_u(x->get_expr(), compute_length_expr(x1).get()), m); + aunit = m_sg.mk(m_seq.str.mk_unit(nth.get())); + } // x2 = x[|x1|+1:] (slice tail after the landed prefix and the char) const expr_ref after = normalize_arith(m, a.mk_add(compute_length_expr(x1).get(), a.mk_int(1))); @@ -4160,19 +4438,24 @@ namespace seq { const nielsen_subst sub(x, repl, mem.m_dep); e->add_subst(sub); child->apply_subst(m_sg, sub); + if (!concrete) + child->add_char_range(aunit, cs, mem.m_dep); // x1 lands at p: drop it from the active constraint, whose state - // becomes p; the leading a is then consumed by simplify_and_init - // (stepping p →a δ_a(p) and recording the edge). + // becomes p; the leading char is then consumed by simplify_and_init + // (stepping p →a δ_a(p) — via apply_regex_if_split for a symbolic + // char — and recording the edge). str_mem& cm = child->m_str_mem[mi]; SASSERT(cm.m_str->first() == x1); cm.m_str = dir_drop(m_sg, cm.m_str, 1, true); // a·x2·u cm.m_regex = p; // x1 ∈_{Q_ν,{p}} R child->add_str_mem(str_mem::mk_view(m, x1, R, p, nu, mem.m_dep)); + add_view_length_constraints(e, vli, nu, x1, p->get_expr(), mem.m_dep); TRACE(seq, tout << "landing: escape x=" << mk_pp(x->get_expr(), m) << " via (" << mk_pp(p->get_expr(), m) << ", " - << cs.first_char() << ") R=" << mk_pp(R->get_expr(), m) + << (concrete ? "char " : "class first ") << cs.first_char() + << ") R=" << mk_pp(R->get_expr(), m) << " nu=" << nu << "\n"); } @@ -4181,6 +4464,145 @@ namespace seq { return false; } + // ----------------------------------------------------------------------- + // Modifier: apply_view_landing_decomposition (paper §5.3, "Landing + // decomposition on view constraints") + // + // A substitution applied throughout the node (an escape x → x1·a·x2, a + // Nielsen split x → y·x', a power introduction, …) can hit a variable that + // an earlier landing has pinned, turning its primitive view into the + // NON-PRIMITIVE view constraint y·u ∈_{Q_ν,F} p with a leading variable + // y. consume_view only consumes leading characters, and letting + // apply_regex_var_split unwind y character-by-character would re-introduce + // exactly the cycle-unrolling divergence the views were built to prevent: + // each lap around a cycle of p's region would spawn a fresh variable that + // is never pinned, so the search could unroll forever. This rule removes + // the leading variable in one step instead: + // + // p ∉ Q_ν (degenerate case): L_{Q_ν,F}(p) ⊆ {ε}, since consuming any + // first character requires the gate p ∈ Q_ν. The whole remaining + // LHS must denote ε: conflict if p ∉ F (ε itself inadmissible) or a + // character/unit token remains; otherwise deterministically + // substitute the LHS variables to ε. Remaining power tokens (if + // any) are left to the power modifiers, whose n = 0 / peel-one split + // disposes of them — a peeled character dies at the gate at once. + // + // p ∈ Q_ν (land-only case): branch on WHERE the value of y lands. Any + // admissible value w of the whole LHS keeps δ_{w'}(p) ∈ Q_ν for + // every proper prefix w' ≺ w and lands in F = {root}. The value of + // y is a prefix of w: a proper prefix lands in Q_ν, and y = w (the + // remainder u taking ε) lands at root. So branching s over + // Q_ν ∪ {root}, pinning y ∈_{Q_ν,{s}} p and advancing the residual + // to u ∈_{Q_ν,F} s is exhaustive, and the blocks are pairwise + // disjoint because the landing state is unique (determinism). There + // are NO escape branches: a value of y leaving Q_ν at a proper + // prefix of the LHS violates the view outright. (Unlike the paper + // we cannot assume a character follows y — Nielsen splits on + // equations create adjacent variables — which is why root joins the + // landing set: only proper prefixes are Q-gated, the final state is + // constrained to F instead.) + // + // Soundness is the view derivative law (Theorem "Soundness of views"), + // applied once per character of y's value: w1 ∈ L_{Q,{s}}(p) gives + // w1⁻¹ L_{Q,F}(p) = L_{Q,F}(s). Termination: the leading variable is + // removed outright, no fresh variables are introduced, and the branching + // is over the finitely many states of Q_ν — so the "active work strictly + // decreases between escapes" bound of the paper's termination proof + // extends unchanged. + // ----------------------------------------------------------------------- + + bool nielsen_graph::apply_view_landing_decomposition(nielsen_node* node) { + for (unsigned mi = 0; mi < node->str_mems().size(); ++mi) { + str_mem const& mem = node->str_mems()[mi]; + SASSERT(mem.well_formed()); + if (!mem.is_view() || mem.is_primitive()) + continue; + euf::snode const* y = mem.m_str->first(); + SASSERT(y); + if (!y->is_var()) + continue; // leading char/unit: consume_view; leading power: power modifiers + euf::snode const* p = mem.m_regex; + // The current state must be settled; an unresolved symbolic ite + // residual is left to apply_regex_if_split. + if (!p->is_ground() || p->kind() == euf::snode_kind::s_ite) + continue; + + // ---- degenerate case: p ∉ Q_ν → L_{Q_ν,F}(p) ⊆ {ε} ---------- + if (!projection_state_in_Q(p->get_expr(), mem.m_nu)) { + if (p != mem.m_root) { + // ε ∉ L_{Q_ν,{root}}(p): the view denotes ∅. + node->set_general_conflict(); + node->set_conflict(backtrack_reason::regex, mem.m_dep); + return true; + } + euf::snode_vector tokens; + mem.m_str->collect_tokens(tokens); + if (any_of(tokens, [](euf::snode const* t) { return t->is_char_or_unit(); })) { + // a character remains — σ(lhs) = ε is impossible. + node->set_general_conflict(); + node->set_conflict(backtrack_reason::regex, mem.m_dep); + return true; + } + // Force every variable of the LHS to ε (single deterministic + // child; the substitution reaches all constraints, including + // this view, whose LHS thereby shrinks). + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, "view eps", /*progress*/ true); + uint_set done; + for (euf::snode const* tok : tokens) { + if (!tok->is_var() || done.contains(tok->id())) + continue; + done.insert(tok->id()); + const nielsen_subst s(tok, m_sg.mk_empty_seq(tok->get_sort()), mem.m_dep); + e->add_subst(s); + child->apply_subst(m_sg, s); + } + TRACE(seq, tout << "view landing: eps-forcing " << mem_pp(mem) + << " (state outside Q, nu=" << mem.m_nu << ")\n"); + return true; + } + + // ---- land-only branching over Q_ν ∪ {root} -------------------- + svector Sstates; + collect_projection_states(mem.m_nu, Sstates); + if (all_of(Sstates, [&](euf::snode const* s) { return s != mem.m_root; })) + Sstates.push_back(mem.m_root); + + // Length abstraction from the current state p over the view's own + // region (see apply_landing_decomposition): keeps the arith length + // of the pinned y realizable in L_{Q_ν,{s}}(p). + view_len_info vli; + compute_view_length_info(mem.m_nu, p->get_expr(), vli); + + for (euf::snode const* s : Sstates) { + // Skip provably-empty landing blocks (L_{Q_ν,{s}}(p) = ∅): the + // paper's rule only branches on non-empty blocks, and this + // keeps the fan-out at the size of p's gated region rather + // than all of Q_ν. Keep the branch on l_undef. The block for + // s = p contains ε, so at least one branch always survives. + vector block; + block.push_back(prod_comp::mk_view(p, s, mem.m_nu, /*complemented*/ false)); + if (check_product_emptiness(block, 1000) == l_true) + continue; + + nielsen_node* child = mk_child(node); + nielsen_edge* le = mk_edge(node, child, "view land", /*progress*/ true); + str_mem& cm = child->m_str_mem[mi]; + cm.m_str = m_sg.drop_first(cm.m_str); // u (kind/root/ν stay) + cm.m_regex = s; // residual u ∈_{Q_ν,F} s + // pin y ∈_{Q_ν,{s}} p + child->add_str_mem(str_mem::mk_view(m, y, p, s, mem.m_nu, mem.m_dep)); + add_view_length_constraints(le, vli, mem.m_nu, y, s->get_expr(), mem.m_dep); + TRACE(seq, tout << "view landing: land y=" << mk_pp(y->get_expr(), m) + << " at " << mk_pp(s->get_expr(), m) + << " from " << mk_pp(p->get_expr(), m) + << " nu=" << mem.m_nu << "\n"); + } + return true; + } + return false; + } + // ----------------------------------------------------------------------- // Modifier: apply_gpower_intr // Generalized power introduction: for an equation where one side's head @@ -4188,7 +4610,6 @@ namespace seq { // variable x that forms a dependency cycle back to v, introduce // v = base^n · suffix where base is the ground prefix. // Generates side constraints n >= 0 and 0 <= len(suffix) < len(base). - // mirrors ZIPT's GPowerIntrModifier (SplitGroundPower + TryGetPowerSplitBase) // ----------------------------------------------------------------------- bool nielsen_graph::apply_gpower_intr(nielsen_node* node) { @@ -4197,7 +4618,7 @@ namespace seq { if (eq.is_trivial()) continue; - // Try both directions (ZIPT's ExtendDir(fwd=true/false)). + // Try both directions for (unsigned od = 0; od < 2; ++od) { const bool fwd = (od == 0); euf::snode const* lhead = dir_token(eq.m_lhs, fwd); @@ -4245,7 +4666,7 @@ namespace seq { } } // TODO: Extend to transitive cycles across multiple equations - // (ZIPT's varDep + HasDepCycle). Currently only self-cycles are detected. + // Currently only self-cycles are detected. } return false; } @@ -4469,11 +4890,10 @@ namespace seq { nielsen_node* node, str_eq const& eq, euf::snode const* var, euf::snode_vector const& ground_prefix_orig, const bool fwd) { - // Compress repeated patterns in the ground prefix (mirrors ZIPT's LcpCompressionFull). - // E.g., [a,b,a,b] has minimal period 2 → use [a,b] as the power base. + // Compress repeated patterns in the ground prefix. + // e.g., [a,b,a,b] has minimal period 2 → use [a,b] as the power base. // This ensures we use the minimal repeating unit: x = (ab)^n · suffix // instead of x = (abab)^n · suffix. - // (mirrors ZIPT: if b.Length == 1 && b is PowerToken pt => b = pt.Base) euf::snode_vector ground_prefix; const unsigned n = ground_prefix_orig.size(); unsigned period = n; @@ -4495,7 +4915,6 @@ namespace seq { // If the compressed prefix is a single power snode, unwrap it to use // its base tokens, avoiding nested powers. // E.g., [(ab)^3] → [a, b] so we get (ab)^n instead of ((ab)^3)^n. - // (mirrors ZIPT: if b.Length == 1 && b is PowerToken pt => b = pt.Base) if (ground_prefix.size() == 1 && ground_prefix[0]->is_power()) { expr* base_e = get_power_base_expr(ground_prefix[0], m_seq); if (base_e) { @@ -4536,7 +4955,7 @@ namespace seq { const expr_ref zero(a.mk_int(0), m); - // Generate children mirroring ZIPT's GetDecompose: + // Generate children: // P(t0 · t1 · ... · t_{k-1}) = P(t0) | t0·P(t1) | ... | t0·...·t_{k-2}·P(t_{k-1}) // For char tokens P(c) = {ε}, for power tokens P(u^m) = {u^m', 0 ≤ m' ≤ m}. // Child at position i substitutes var → base^n · t0·...·t_{i-1} · P(t_i). @@ -4842,7 +5261,6 @@ namespace seq { // (2) x → c · x' for each minterm character class c // More general than regex_char_split; uses minterm partitioning rather // than just extracting concrete characters. - // mirrors ZIPT's RegexVarSplitModifier // ----------------------------------------------------------------------- bool nielsen_graph::apply_regex_var_split(nielsen_node* node) { @@ -4880,13 +5298,16 @@ namespace seq { // into its own ite — which apply_regex_if_split then resolves // independently, materializing a cross-product of their states — we // branch directly on the joint minterm partition of all of x's - // constraint regexes, using one CONCRETE representative character per - // minterm. The derivative is constant over a minterm, so a - // representative is sound and (for the singleton/∅-complement minterms - // of these small concrete alphabets) complete; the Z3DEBUG conflict - // cross-check catches any missed model. Every constraint on x then - // consumes the same concrete char synchronously — no ites, no - // cross-product. + // constraint regexes. A SINGLETON minterm contributes its concrete + // character, which every constraint on x then consumes synchronously — + // no ites, no cross-product. A multi-char minterm must NOT be + // collapsed to a concrete representative: the minterms are joint only + // over the memberships x LEADS, while equations, disequations and + // non-leading occurrences of x can still distinguish characters within + // the class (committing to one char would drop every model whose first + // char is another member — unsound UNSAT). Such classes get the + // symbolic char ?c range-restricted to the class instead, paying the + // ite resolution only where it is needed for completeness. euf::snode_vector states; for (auto const& m2 : node->str_mems()) if (m2.m_str->first() == first) @@ -4905,13 +5326,18 @@ namespace seq { char_set cs = m_seq_regex->minterm_to_char_set(mt->get_expr()); if (cs.is_empty()) continue; - euf::snode const* cunit = m_sg.mk(m_seq.str.mk_unit(m_seq.mk_char(cs.first_char()))); + const bool concrete = cs.is_unit(); + euf::snode const* cunit = concrete + ? m_sg.mk(m_seq.str.mk_unit(m_seq.mk_char(cs.first_char()))) + : m_sg.mk(get_or_create_char_var(first)); euf::snode const* replacement = m_sg.mk_concat(cunit, tail); nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, "regex var split", false); const nielsen_subst s(first, replacement, mem.m_dep); e->add_subst(s); child->apply_subst(m_sg, s); + if (!concrete) + child->add_char_range(cunit, cs, mem.m_dep); } return true; } @@ -4936,7 +5362,6 @@ namespace seq { // (1) x = u^m · prefix(u) with m < n (bounded power prefix) // (2) x = u^n · x' (the variable extends past the full power) // Generates integer side constraints for the fresh exponent variables. - // mirrors ZIPT's PowerSplitModifier // ----------------------------------------------------------------------- bool nielsen_graph::apply_power_split(nielsen_node* node) { @@ -5045,7 +5470,6 @@ namespace seq { // (1) n = 0 → u^n = ε (replace power with empty) // (2) n >= 1 → peel one u from the power // Generates integer side constraints for each branch. - // mirrors ZIPT's VarNumUnwindingModifier // ----------------------------------------------------------------------- bool nielsen_graph::apply_var_num_unwinding_eq(nielsen_node* node) { @@ -5388,8 +5812,6 @@ namespace seq { // ----------------------------------------------------------------------- // Modification counter: substitution length tracking - // mirrors ZIPT's LocalInfo.CurrentModificationCnt + NielsenEdge.IncModCount/DecModCount - // + NielsenNode constructor length assertion logic // ----------------------------------------------------------------------- expr_ref nielsen_graph::get_or_create_char_var(euf::snode const* var) { @@ -5586,23 +6008,32 @@ namespace seq { } // ----------------------------------------------------------------------- - // Regex widening: overapproximate string and check intersection emptiness - // Mirrors ZIPT NielsenNode.CheckRegexWidening (NielsenNode.cs:1350-1380) + // Regex widening: over-approximate the string and check emptiness against + // the membership's language — at the CONSTRAINT level (paper, "Pruning + // incrementally during construction"): one product factor per token of + // Ω(str) and one component for the right-hand side, decided by the + // concatenation-aware synchronous derivative search below. No closed-form + // regex for Ω(str) ⊓ rhs is ever built, and land-state views participate + // EXACTLY via their gated one-character law — both as the widened + // membership itself and as pinned constraints inside Ω. // ----------------------------------------------------------------------- bool nielsen_graph::check_regex_widening(nielsen_node const& node, str_mem const& mem, dep_tracker& dep) { const auto str = mem.m_str; const auto regex = mem.m_regex; SASSERT(m_seq_regex); - // Only apply to ground regexes with non-trivial strings - if (!regex->is_ground()) + // The right-hand side must be a settled plain state; an unresolved + // symbolic ite residual is left to apply_regex_if_split. + if (!regex->is_ground() || regex->kind() == euf::snode_kind::s_ite) return false; - - // Build the overapproximation regex for the string. - // Variables → intersection of their primitive regex constraints (or Σ*) - // Symbolic chars → re.range from char_ranges (or full_char) - // Concrete chars → to_re(unit(c)) + // Build Ω(str) as one component factor per token: + // concrete char c → plain component to_re(unit(c)) + // variable x → the variable's primitive components — plain + // regexes AND land-state views, handled exactly; + // the empty factor denotes Σ* when unconstrained + // symbolic char → plain component from char_ranges (or Σ¹) + // anything else → empty factor (Σ*) euf::snode_vector tokens; str->collect_tokens(tokens); if (tokens.empty()) @@ -5610,37 +6041,30 @@ namespace seq { SASSERT(dep); - euf::snode const* approx = nullptr; + vector> factors; for (euf::snode const* tok : tokens) { - euf::snode const* tok_re = nullptr; + vector factor; if (tok->is_char()) { // Concrete character → to_re(unit(c)) expr* te = tok->get_expr(); SASSERT(te); - tok_re = m_sg.mk(m_seq.re.mk_to_re(te)); + factor.push_back(prod_comp::mk_plain(m_sg.mk(m_seq.re.mk_to_re(te)))); } else if (tok->is_var()) { - // Variable → intersection of primitive regex constraints, or Σ* - euf::snode const* x_range = m_seq_regex->collect_primitive_regex_intersection(tok, node, m_dep_mgr, dep); - if (x_range) - tok_re = x_range; - else { - // Unconstrained variable: approximate as Σ* - sort* str_sort = m_seq.str.mk_string_sort(); - expr_ref all_re(m_seq.re.mk_full_seq(m_seq.re.mk_re(str_sort)), m); - tok_re = m_sg.mk(all_re); - } - TRACE(seq, tout << "intersection-collection\n" << spp(tok, m) - << "\n" << spp(tok_re, m) << "\n"); + // Variable → ⊓Reg_x as components (views join exactly, with + // their own gate/acceptance); empty factor = Σ* if unconstrained. + collect_var_components(tok, node, factor, dep); + TRACE(seq, tout << "widening factor " << spp(tok, m) + << ": " << factor.size() << " components\n"); } else if (tok->is_unit()) { - // Symbolic char — try to get char_range + // Symbolic char — char_range if known, otherwise Σ¹. + euf::snode const* range_re = nullptr; if (node.char_ranges().contains(tok->id())) { auto& cs = node.char_ranges()[tok->id()]; if (!cs.first.is_empty()) { // Build union of re.range for each interval - euf::snode const* range_re = nullptr; for (auto const& r : cs.first.ranges()) { expr_ref rng(m_seq.re.mk_range( m_seq.str.mk_string(zstring(r.m_lo)), @@ -5654,59 +6078,35 @@ namespace seq { } } dep = dep_mgr().mk_join(dep, cs.second); - tok_re = range_re; } } - if (!tok_re) { - // Unconstrained symbolic char: approximate as full_char (single char, any value) + if (!range_re) { + // Unconstrained symbolic char: full_char (single char, any value) sort* str_sort = m_seq.str.mk_string_sort(); expr_ref fc(m_seq.re.mk_full_char(m_seq.re.mk_re(str_sort)), m); - tok_re = m_sg.mk(fc); + range_re = m_sg.mk(fc); } + factor.push_back(prod_comp::mk_plain(range_re)); } - else { - // Unknown token type — approximate as Σ* - sort* str_sort = m_seq.str.mk_string_sort(); - expr_ref all_re(m_seq.re.mk_full_seq(m_seq.re.mk_re(str_sort)), m); - tok_re = m_sg.mk(all_re); - } + // else: unknown token type (e.g. power) — empty factor = Σ*. - SASSERT(tok_re); - - if (!approx) - approx = tok_re; - else { - expr* ae = approx->get_expr(); - expr* te = tok_re->get_expr(); - SASSERT(ae && te); - approx = m_sg.mk(m_seq.re.mk_concat(ae, te)); - } + factors.push_back(factor); } - if (!approx) - return false; + // Right-hand side component: exact for plain memberships and views alike + // (the view's Q-gate and land-state acceptance are the component's own + // one-character law, Theorem "Soundness of views"). + const prod_comp rhs = mem.is_view() + ? prod_comp::mk_view(mem.m_regex, mem.m_root, mem.m_nu, /*complemented*/ false) + : prod_comp::mk_plain(mem.m_regex); - // Check intersection(approx, regex) for emptiness - // Build intersection regex - expr* ae = approx->get_expr(); - expr* re = regex->get_expr(); - SASSERT(ae && re); - const expr_ref inter(m_seq.re.mk_inter(ae, re), m); - euf::snode const* inter_sn = m_sg.mk(inter); - SASSERT(inter_sn); // TODO: Minimize the conflict here - const lbool result = m_seq_regex->is_empty_bfs(inter_sn, 5000); - TRACE(seq, tout << "widen empty-intersect: " << result << " " << mk_pp(re, m) - << " <= " << mk_pp(ae, m) << "\n" << mem_pp(mem) << "\n"; + const lbool result = check_concat_product_emptiness(factors, rhs, 5000); + TRACE(seq, tout << "widen empty-product: " << result << " " << mem_pp(mem) << "\n"; display(tout, &node) << "\n"); return result == l_true; } - // ----------------------------------------------------------------------- - // Leaf-node regex intersection emptiness check - // Mirrors ZIPT NielsenNode.CheckRegex (NielsenNode.cs:1311-1329) - // ----------------------------------------------------------------------- - // ----------------------------------------------------------------------- // Synchronous product over plain / view / guard / co-view components. // ----------------------------------------------------------------------- @@ -5774,6 +6174,7 @@ namespace seq { work.push_back(comps0); visited.insert(encode(comps0)); unsigned explored = 0; + bool undef_acceptance = false; // some tuple's acceptance was undecidable while (!work.empty()) { if (!m.inc()) @@ -5798,6 +6199,10 @@ namespace seq { } if (all_acc && !any_undef) return l_false; // found a common word + if (all_acc && any_undef) + // possibly accepting, but undecidable: exhaustion may no longer + // claim emptiness (pruning/subsuming on it would be unsound) + undef_acceptance = true; // joint first-character partition = minterms of the intersection of // all still-discriminating component states. @@ -5826,7 +6231,149 @@ namespace seq { work.push_back(nxt); } } - return l_true; // exhausted with no accepting tuple → empty + // exhausted with no accepting tuple → empty, unless some tuple's + // acceptance could not be decided + return undef_acceptance ? l_undef : l_true; + } + + // ----------------------------------------------------------------------- + // Concatenation-aware synchronous product (paper, "Pruning incrementally + // during construction"): emptiness of + // ( L(F_0) · L(F_1) · … · L(F_{k-1}) ) ⊓ L(rhs) + // where each factor F_i is the intersection of its components (an EMPTY + // component list denotes Σ*) and rhs is one further component consumed + // synchronously with the whole concatenation. A search state is + // (factor index i, component tuple of F_i, rhs component); a character + // step derives every live component on a joint minterm, and when all of + // F_i's components accept the search may ε-advance to F_{i+1} + // (nondeterministically — both continuations are explored). A word is + // found when every factor has been consumed (i = k) and rhs accepts. + // + // l_true: empty — pruning on this verdict is sound; + // l_false: a common word exists; + // l_undef: budget exhausted or acceptance undecidable — the caller must + // NOT prune (dropping the ε-advance or the final acceptance on + // an undecided component could wrongly report emptiness). + // ----------------------------------------------------------------------- + + lbool nielsen_graph::check_concat_product_emptiness(vector> const& factors, + prod_comp const& rhs, unsigned max_states) { + const unsigned k = factors.size(); + + struct cstate { + unsigned m_idx; // current factor (k = all factors consumed) + vector m_comps; // components of factor m_idx + prod_comp m_rhs; // right-hand-side component + }; + + auto encode = [](unsigned idx, vector const& cs, prod_comp const& r) { + std::vector key; + key.reserve(4 + cs.size() * 3); + key.push_back(idx); + auto push_comp = [&key](prod_comp const& c) { + key.push_back(static_cast(c.m_kind)); + key.push_back((c.m_complemented ? 1u : 0u) | (c.m_sink ? 2u : 0u) | (c.m_dead ? 4u : 0u)); + key.push_back(c.m_state ? c.m_state->id() : UINT_MAX); + }; + push_comp(r); + for (auto const& c : cs) + push_comp(c); + return key; + }; + + std::set> visited; + vector work; + + auto push_state = [&](unsigned idx, vector const& comps, prod_comp const& r) { + if (visited.insert(encode(idx, comps, r)).second) + work.push_back(cstate{ idx, comps, r }); + }; + + push_state(0, k == 0 ? vector() : factors[0], rhs); + unsigned explored = 0; + + while (!work.empty()) { + if (!m.inc()) + return l_undef; + if (explored >= max_states) + return l_undef; + const cstate cur = work.back(); + work.pop_back(); + ++explored; + + if (cur.m_rhs.m_dead) + continue; // the membership side is ∅ from here + bool any_dead = false; + for (auto const& c : cur.m_comps) if (c.m_dead) { any_dead = true; break; } + if (any_dead) + continue; + + // ε-advance / final acceptance: do all components of the current + // factor accept? (Trivially true for the Σ* empty factor and for + // the terminal index k.) + lbool allacc = l_true; + for (auto const& c : cur.m_comps) { + const lbool a = comp_accepting(c); + if (a == l_false) { allacc = l_false; break; } + if (a == l_undef) allacc = l_undef; + } + if (allacc == l_undef) + return l_undef; // cannot decide the factor split — do not prune + + if (allacc == l_true) { + if (cur.m_idx >= k) { + // all factors consumed: the word ends here + const lbool racc = comp_accepting(cur.m_rhs); + if (racc == l_true) + return l_false; // found a common word + if (racc == l_undef) + return l_undef; + } + else + // ε-advance to the next factor (kept alongside the + // character continuations below) + push_state(cur.m_idx + 1, + cur.m_idx + 1 < k ? factors[cur.m_idx + 1] : vector(), + cur.m_rhs); + } + + if (cur.m_idx >= k) + continue; // terminal: no further characters may be consumed + + // character step: joint first-character partition of the live + // component states (factor + rhs) + expr* combined = nullptr; + auto add_state = [&](prod_comp const& c) { + if (c.m_sink || c.m_dead) + return; + combined = combined ? m_seq.re.mk_inter(combined, c.m_state->get_expr()) + : c.m_state->get_expr(); + }; + add_state(cur.m_rhs); + for (auto const& c : cur.m_comps) + add_state(c); + if (!combined) + continue; + euf::snode_vector mts; + m_sg.compute_minterms(m_sg.mk(combined), mts); + + for (euf::snode const* mt : mts) { + prod_comp r2 = comp_step(cur.m_rhs, mt); + if (r2.m_dead) + continue; + vector nxt; + bool dead = false; + for (auto const& c : cur.m_comps) { + prod_comp d = comp_step(c, mt); + if (d.m_dead) { dead = true; break; } + nxt.push_back(d); + } + if (dead) + continue; + push_state(cur.m_idx, nxt, r2); + } + } + return l_true; // exhausted with no accepting configuration → empty } bool nielsen_graph::collect_var_components(euf::snode const* var, nielsen_node const& node, @@ -5956,7 +6503,12 @@ namespace seq { return false; } - bool nielsen_graph::check_leaf_regex(nielsen_node const& node, dep_tracker& dep) { + // l_true: every variable's primitive intersection is non-empty (leaf feasible) + // l_false: some variable's intersection is empty (dep set to its justification) + // l_undef: the product search ran out of budget/resources — the leaf can be + // neither confirmed nor refuted and must NOT be declared SAT (the + // model builder could otherwise emit an unsatisfiable witness). + lbool nielsen_graph::check_leaf_regex(nielsen_node const& node, dep_tracker& dep) { SASSERT(m_seq_regex); // distinct variables carrying a primitive constraint @@ -5976,10 +6528,12 @@ namespace seq { if (result == l_true) { TRACE(seq, tout << "empty intersection\n"); dep = d; - return false; + return l_false; } + if (result == l_undef) + return l_undef; } - return true; + return l_true; } // ----------------------------------------------------------------------- @@ -6006,6 +6560,7 @@ namespace seq { st.update("nseq mod eq split", m_stats.m_mod_eq_split); st.update("nseq mod star intr", m_stats.m_mod_star_intr); st.update("nseq mod cycle subsump", m_stats.m_mod_cycle_subsumption); + st.update("nseq mod view land", m_stats.m_mod_view_land); st.update("nseq mod gpower intr", m_stats.m_mod_gpower_intr); st.update("nseq mod regex fact", m_stats.m_mod_regex_factorization); st.update("nseq mod const nielsen", m_stats.m_mod_const_nielsen); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 1b1cb47000..95d7c562c4 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -9,10 +9,6 @@ Abstract: Nielsen graph for string constraint solving. - Ports the constraint types and Nielsen graph structures from - ZIPT (https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT/Constraints) - into Z3's smt/seq framework. - The Nielsen graph is used for solving word equations and regex membership constraints via Nielsen transformations. Each node contains a set of constraints (string equalities, regex memberships, @@ -71,7 +67,6 @@ namespace seq { std::string snode_label_html(euf::snode const* n, ast_manager& m, bool html_escape); // simplification result for constraint processing - // mirrors ZIPT's SimplifyResult enum enum class simplify_result { proceed, // no change, continue conflict, // constraint is unsatisfiable @@ -81,7 +76,6 @@ namespace seq { }; // reason for backtracking in the Nielsen graph - // mirrors ZIPT's BacktrackReasons enum enum class backtrack_reason { unevaluated, extended, @@ -181,7 +175,6 @@ namespace seq { bool split_lookahead_viable(expr* n_regex, euf::sgraph& sg, zstring const& c); // string equality constraint: lhs = rhs - // mirrors ZIPT's StrEq (both sides are regex-free snode trees) struct str_eq { ast_manager& m; euf::snode const* m_lhs; // assumed to be non-null @@ -315,7 +308,6 @@ namespace seq { enum class mem_kind : unsigned char { plain, stab_view }; // regex membership constraint: str in regex - // mirrors ZIPT's StrMem struct str_mem { ast_manager& m; euf::snode const* m_str; // assumed to be non-null @@ -359,6 +351,15 @@ namespace seq { } bool operator<(const str_mem& other) const { + // Regex-factorization heuristic: order primarily by the estimated + // automaton size of the regex so that the cheapest membership is + // factorized first (see snode::regex_weight / sgraph::compute_regex_weight). + // The remaining pointer comparisons are just deterministic tie-breakers + // to keep this a total order for canonicalization/sorting. + const unsigned w1 = m_regex->regex_weight(); + const unsigned w2 = other.m_regex->regex_weight(); + if (w1 != w2) + return w1 < w2; if (m_str != other.m_str) return m_str < other.m_str; return m_regex < other.m_regex; @@ -398,7 +399,6 @@ namespace seq { // string variable substitution: var -> replacement // (can be used as well to substitute arbitrary nodes - like powers) - // mirrors ZIPT's Subst struct nielsen_subst { euf::snode const* m_var; euf::snode const* m_replacement; @@ -427,12 +427,10 @@ namespace seq { // ----------------------------------------------- // integer constraint: equality or inequality over length expressions - // mirrors ZIPT's IntEq and IntLe // ----------------------------------------------- // integer constraint stored per nielsen_node, tracking arithmetic // relationships between length variables and power exponents. - // mirrors ZIPT's IntEq / IntLe over Presburger arithmetic polynomials. struct constraint { expr_ref fml; // the formula (eq, le, or ge, unit-diseq expression) dep_tracker dep; // tracks which input constraints contributed @@ -477,7 +475,6 @@ namespace seq { }; // edge in the Nielsen graph connecting two nodes - // mirrors ZIPT's NielsenEdge class nielsen_edge { nielsen_node* m_src; nielsen_node* m_tgt; @@ -525,7 +522,6 @@ namespace seq { }; // node in the Nielsen graph - // mirrors ZIPT's NielsenNode class nielsen_node { friend class nielsen_graph; @@ -536,11 +532,11 @@ namespace seq { vector m_str_eq; // string equalities vector m_str_deq; // string disequalities vector m_str_mem; // regex memberships - vector m_constraints; // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe) + vector m_constraints; // integer equalities/inequalities sat::literal m_conflict_external_literal = sat::null_literal; dep_tracker m_conflict_internal = nullptr; - // character constraints (mirrors ZIPT's DisEqualities and CharRanges) + // character constraints // key: snode id of the s_unit symbolic character u_map> m_char_ranges; // ?c in [lo, hi) @@ -639,7 +635,7 @@ namespace seq { bool lower_bound(expr* e, rational& lo, dep_tracker& dep); bool upper_bound(expr* e, rational& up, dep_tracker& dep); - // character constraint access (mirrors ZIPT's CharRanges) + // character constraint access u_map>& char_ranges() { return m_char_ranges; } u_map> const &char_ranges() const { return m_char_ranges; @@ -758,7 +754,6 @@ namespace seq { bool references_rigid() const; // render constraint set as an HTML fragment for DOT node labels. - // mirrors ZIPT's NielsenNode.ToHtmlString() std::ostream& to_html(std::ostream& out, obj_map& names, uint64_t& next_id, ast_manager& m) const; std::ostream& to_html(std::ostream& out, ast_manager& m) const; @@ -813,6 +808,7 @@ namespace seq { unsigned m_mod_eq_split = 0; unsigned m_mod_star_intr = 0; unsigned m_mod_cycle_subsumption = 0; + unsigned m_mod_view_land = 0; unsigned m_mod_gpower_intr = 0; unsigned m_mod_regex_factorization = 0; unsigned m_mod_const_nielsen = 0; @@ -834,7 +830,6 @@ namespace seq { }; // the overall Nielsen transformation graph - // mirrors ZIPT's NielsenGraph class nielsen_graph { friend class nielsen_node; friend class nielsen_edge; @@ -954,10 +949,28 @@ namespace seq { // egraph cannot release them on pop. We never shrink this — the // cache is meant to be monotone. expr_ref_vector m_partial_dfa_pin; - // Monotone snapshot index ν. Bumped by mark_scc_projection_edges only - // when the explored SCC's edge set actually grows; identifies which - // partial-DFA edges (m_projection_idx ≤ ν) belong to a projection's Q. + // Monotone snapshot index ν, bumped whenever a new view state set is + // recorded (mark_reachable_projection_edges). A view's Q is the EXACT + // snapshot stored under its ν in m_projection_snapshots (the paper's + // "recorded state set Q" of a view, Implementation Aspects); the + // per-edge watermark m_projection_idx ≤ ν is kept only as a fallback — + // on its own it would denote the union of ALL extractions up to ν, + // blurring a view's Q with unrelated heads' regions once exploration + // is partial (lazy mode). unsigned m_projection_extract_idx = 0; + // ν → the snapshot of Q taken when the view index was minted. The + // state exprs are pinned via m_partial_dfa_pin, so the stored expr* + // (and their ids) stay valid across sgraph pops. + struct projection_snapshot { + uint_set m_ids; // expr ids of the states of Q + ptr_vector m_states; // the states themselves + }; + std::unordered_map m_projection_snapshots; + // head expr id → (partial-DFA edge count at snapshot time, ν). The + // partial DFA only grows, so an unchanged edge count means the head's + // reachable set — hence its snapshot — is unchanged and ν is reused + // instead of minting a fresh snapshot per decomposition. + std::unordered_map> m_projection_head_cache; // Expr ids of regex states whose full reachable automaton has already // been recorded into the partial DFA (lazy, once-per-component Q growth; // see ensure_automaton_explored). @@ -1115,7 +1128,6 @@ namespace seq { // output the graph in graphviz DOT format. // nodes on the sat_path are highlighted green; conflict nodes red/darkred. - // mirrors ZIPT's NielsenGraph.ToDot() std::ostream& to_dot(std::ostream& out) const; std::string to_dot() const; @@ -1234,15 +1246,18 @@ namespace seq { // unconstrained), replacing symbolic chars with their char ranges, // then checking if the approximation intersected with `regex` is empty. // Returns true if widening detects infeasibility (UNSAT). - // Mirrors ZIPT NielsenNode.CheckRegexWidening (NielsenNode.cs:1350-1380) + // Decided at the constraint level by check_concat_product_emptiness + // (one factor per token of Ω(str), one component for the right-hand + // side); land-state views participate exactly, both as the widened + // membership and as pinned constraints inside Ω. bool check_regex_widening(nielsen_node const& node, str_mem const& mem, dep_tracker& dep); // Check regex feasibility at a leaf node: for each variable with // multiple primitive regex constraints, check that the intersection // of all its regexes is non-empty. - // Returns true if all constraints are feasible. - // Mirrors ZIPT NielsenNode.CheckRegex) - bool check_leaf_regex(nielsen_node const& node, dep_tracker& dep); + // l_true: feasible; l_false: some intersection empty (dep set); + // l_undef: product-search budget exhausted — must not be treated as SAT. + lbool check_leaf_regex(nielsen_node const& node, dep_tracker& dep); // ------------------------------------------------------------------- // Synchronous product over plain / view / guard / co-view components @@ -1277,6 +1292,18 @@ namespace seq { // was reached), l_undef = budget exhausted / inconclusive. lbool check_product_emptiness(vector const& comps, unsigned max_states); + // Concatenation-aware variant (paper, "Pruning incrementally during + // construction"): emptiness of (L(F_0)·…·L(F_{k-1})) ⊓ L(rhs), where + // each factor F_i is the intersection of its components (an empty + // component list denotes Σ*) and rhs is one further component consumed + // synchronously with the whole concatenation. Used by regex widening; + // no closed-form regex for the concatenation is ever built, and view + // components participate exactly via their gated one-character law. + // l_true = empty, l_false = a common word exists, l_undef = budget + // exhausted / undecided acceptance (callers must NOT prune on it). + lbool check_concat_product_emptiness(vector> const& factors, + prod_comp const& rhs, unsigned max_states); + // acceptance / single-character step of one product component. lbool comp_accepting(prod_comp const& c) const; prod_comp comp_step(prod_comp const& c, euf::snode const* mt); @@ -1316,6 +1343,45 @@ namespace seq { // (0 if there is nothing marked, i.e. no reachable edge). unsigned mark_reachable_projection_edges(euf::snode const* head_re); + // Collect the snode handles of every state of Q_ν — the states incident + // to a partial-DFA edge with extraction index in [1, ν]. This is the + // enumeration counterpart of the membership test projection_state_in_Q + // (keep the two in sync); used to enumerate the landing states of the + // land-only view decomposition. + void collect_projection_states(unsigned nu, svector& out); + + // Length abstraction of the land-state views over one gated region: + // BFS distances d(·) from a head state over the recorded in-Q_ν edges + // (each edge consumes exactly one character/minterm), plus the stride + // g = gcd over reachable in-Q edges (u,v) of (d(u) + 1 − d(v)). + // By the telescoping/potential argument, EVERY gated walk head→v has + // length ≡ d(v) (mod g); g = 0 means every such walk has length exactly + // d(v). Sound because at ν-minting time compute_frontier has saturated + // the in-Q edges (every one-character transition among Q states is + // recorded), and edges are only ever added. + struct view_len_info { + u_map m_dist; // expr id → shortest gated distance from the head + unsigned m_stride = 0; // 0 ⇒ walk lengths are exact + bool m_ok = false; // snapshot found and head ∈ Q_ν + }; + void compute_view_length_info(unsigned nu, expr* from, view_len_info& info); + + // Emit the length side constraints for a variable pinned to the view + // L_{Q_ν,{to}}(head) onto the branch edge e: len ≥ min and + // stride | (len − min) (collapsed to len = min when exact). For a + // landing target outside Q_ν (view landing at root ∉ Q_ν) the final + // hop may be an UNRECORDED transition from any reachable in-Q state, + // so only the conservative variant (min = 1, stride weakened by the + // gcd of all reachable distances) is sound. These ride the normal + // side-constraint channel: branch-locally enforced by the subsolver + // (check_int_feasibility) and surfaced to the outer solver at a SAT + // leaf via add_nielsen_assumptions — keeping the outer arith model's + // len(x) realizable in the view, which seq_model::mk_fresh_value + // relies on (a non-realizable length forces a witness of a different + // length: an inconsistent model). + void add_view_length_constraints(nielsen_edge* e, view_len_info const& info, unsigned nu, + euf::snode const* pinned, expr* to, dep_tracker const& dep); + // A frontier edge (p, mt, q): p ∈ Q, mt a minterm of p, q = δ_mt(p) ∉ Q // and q ≠ ⊥. The escape candidates of the landing decomposition. struct frontier_edge { @@ -1365,7 +1431,6 @@ namespace seq { // eq split modifier: splits a regex-free equation at a chosen index into // two shorter equalities with optional padding (single progress child). - // Mirrors ZIPT's EqSplitModifier + StrEq.SplitEq. bool apply_eq_split(nielsen_node* node); // helper: classify whether a token has variable (symbolic) length @@ -1376,7 +1441,6 @@ namespace seq { unsigned token_const_length(euf::snode const* tok) const; // helper: find a split point in a regex-free equation. - // ports ZIPT's StrEq.SplitEq algorithm. // returns true if a valid split point is found, with results in out params. bool find_eq_split_point( euf::snode_vector const& lhs_toks, @@ -1387,12 +1451,10 @@ namespace seq { // power epsilon modifier: for a power token u^n in an equation, // branch: (1) base u = ε, (2) power is empty (n = 0 semantics). - // mirrors ZIPT's PowerEpsilonModifier bool apply_power_epsilon(nielsen_node* node); // numeric comparison modifier: for equations involving power tokens // u^m and u^n with the same base, branch on m < n vs n <= m. - // mirrors ZIPT's NumCmpModifier bool apply_num_cmp(nielsen_node* node); // CommPower-based power elimination split: when one side starts with @@ -1401,12 +1463,10 @@ namespace seq { // (1) p < c (2) c ≤ p // After branching, simplify_and_init's CommPower pass resolves the // cancellation deterministically. - // mirrors ZIPT's SplitPowerElim + NumCmpModifier bool apply_split_power_elim(nielsen_node* node); // constant numeric unwinding: for a power token u^n vs a constant // (non-variable), branch: (1) n = 0 (u^n = ε), (2) n >= 1 (peel one u). - // mirrors ZIPT's ConstNumUnwindingModifier bool apply_const_num_unwinding(nielsen_node* node); // regex if split: for str_mem s ∈ R where R decomposes as ite(c, th, el), @@ -1426,6 +1486,25 @@ namespace seq { // the old split-and-guard apply_cycle_decomposition. bool apply_landing_decomposition(nielsen_node* node); + // Land-only decomposition of a NON-PRIMITIVE view constraint (paper + // §5.3, "Landing decomposition on view constraints"): a substitution + // applied throughout the node (an escape, a Nielsen split, a power + // introduction) can hit a pinned variable and turn its primitive view + // into y·u ∈_{Q_ν,F} p with a leading variable y. Character- + // unwinding y (regex_var_split) would re-introduce exactly the + // cycle-unrolling divergence views exist to prevent, so instead: + // - p ∉ Q_ν (degenerate): L_{Q_ν,F}(p) ⊆ {ε} — conflict if p ∉ F or + // a character remains, else force the LHS variables to ε; + // - p ∈ Q_ν: branch on the landing state s of y over Q_ν ∪ F only + // (no escapes: every admissible LHS value keeps its proper-prefix + // states inside Q_ν and lands in F, so y's own landing state lies + // in Q_ν ∪ F), pinning y ∈_{Q_ν,{s}} p and advancing the residual + // to u ∈_{Q_ν,F} s. + // Removes the leading variable, introduces no fresh variables and + // branches over finitely many states, so the paper's termination + // argument extends unchanged. + bool apply_view_landing_decomposition(nielsen_node* node); + // cycle subsumption: for a str_mem x·rest ∈ R where x is constrained // to L(Reg_x) ⊆ L(stabilizer of R), simplify to rest ∈ R. // Fires without the novelty guard, using the current partial DFA state. @@ -1442,7 +1521,6 @@ namespace seq { // generalized power introduction: for an equation where one head is // a variable v and the other side has ground prefix + a variable x // forming a cycle back to v, introduce v = base^n · suffix. - // mirrors ZIPT's GPowerIntrModifier bool apply_gpower_intr(nielsen_node* node); // generalized regex factorization (Boolean closure derivation rule). @@ -1467,8 +1545,7 @@ namespace seq { 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. + // `fwd=true` uses left-to-right decomposition; `fwd=false` bool fire_gpower_intro(nielsen_node* node, str_eq const& eq, euf::snode const* var, euf::snode_vector const& ground_prefix_orig, bool fwd); @@ -1478,17 +1555,14 @@ namespace seq { // regex variable split: for str_mem x·s ∈ R where x is a variable, // split using minterms: x → ε, or x → c·x' for each minterm c. // More general than regex_char_split, uses minterm partitioning. - // mirrors ZIPT's RegexVarSplitModifier bool apply_regex_var_split(nielsen_node* node); // power split: for a variable x facing a power token u^n, // branch: x = u^m · prefix(u) with m < n, or x = u^n · x. - // mirrors ZIPT's PowerSplitModifier bool apply_power_split(nielsen_node* node); // variable numeric unwinding: for a power token u^n vs a variable, // branch: (1) n = 0 (u^n = ε), (2) n >= 1 (peel one u). - // mirrors ZIPT's VarNumUnwindingModifier bool apply_var_num_unwinding_eq(nielsen_node* node); bool apply_var_num_unwinding_mem(nielsen_node* node); @@ -1516,7 +1590,6 @@ namespace seq { // m_solver at the base level (outside push/pop). Called once at the start // of solve(). Makes derived constraints immediately visible to m_solver // for arithmetic pruning at every DFS node, not just the root. - // Mirrors ZIPT's Constraint.Shared forwarding mechanism. void assert_root_constraints_to_solver(); // Generate |LHS| = |RHS| length constraints for a non-root node's own @@ -1524,7 +1597,6 @@ namespace seq { // Called once per node (guarded by m_node_len_constraints_generated). // Uses compute_length_expr (mod-count-aware) so that variables with // non-zero modification counts get fresh length variables. - // Mirrors ZIPT's Constraint.Shared forwarding for per-node equations. void generate_node_length_constraints(nielsen_node* node); // check integer feasibility of the constraints along the current path. @@ -1538,7 +1610,7 @@ namespace seq { dep_tracker get_subsolver_dependency(nielsen_node* n) const; // check whether lhs <= rhs is implied by the path constraints. - // mirrors ZIPT's NielsenNode.IsLe(): temporarily asserts NOT(lhs <= rhs) + // temporarily asserts NOT(lhs <= rhs) // and returns true iff the result is unsatisfiable (i.e., lhs <= rhs is // entailed). Path constraints are already in the solver incrementally. bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep); @@ -1551,8 +1623,6 @@ namespace seq { // ----------------------------------------------- // Modification counter methods for substitution length tracking. - // mirrors ZIPT's NielsenEdge.IncModCount / DecModCount and - // NielsenNode constructor length assertion logic. // ----------------------------------------------- // Get or create a fresh symbolic character variable for the given variable diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 7092244035..57a7190594 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -257,7 +257,6 @@ namespace seq { // ----------------------------------------------------------------------- // nielsen_node: display_html // Render constraint set as an HTML fragment for DOT labels. - // Mirrors ZIPT's NielsenNode.ToHtmlString(). // ----------------------------------------------------------------------- // Helper: HTML-escape a string and replace literal \n with
. @@ -743,7 +742,7 @@ namespace seq { // ----------------------------------------------------------------------- // nielsen_graph: to_dot // Output the graph in graphviz DOT format, optionally colour-highlighting - // the satisfying path. Mirrors ZIPT's NielsenGraph.ToDot(). + // the satisfying path. // ----------------------------------------------------------------------- // Convert a backtrack_reason to a short display string. diff --git a/src/smt/seq/seq_parikh.cpp b/src/smt/seq/seq_parikh.cpp index fc967cf2f8..2e7e9476e6 100644 --- a/src/smt/seq/seq_parikh.cpp +++ b/src/smt/seq/seq_parikh.cpp @@ -7,7 +7,7 @@ Module Name: Abstract: - Parikh image filter implementation for the ZIPT-based Nielsen string + Parikh image filter implementation for the Nielsen string solver. See seq_parikh.h for the full design description. The key operation is compute_length_stride(re), which performs a diff --git a/src/smt/seq/seq_parikh.h b/src/smt/seq/seq_parikh.h index 4704996fd0..ba6a8f64ef 100644 --- a/src/smt/seq/seq_parikh.h +++ b/src/smt/seq/seq_parikh.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Parikh image filter for the ZIPT-based Nielsen string solver. + Parikh image filter for the Nielsen string solver. Implements Parikh-based arithmetic constraint generation for nielsen_node instances. For a regex membership constraint str ∈ r, @@ -29,10 +29,6 @@ Abstract: set and discharged by the integer subsolver (see seq_nielsen.h, simple_solver). - Implements the Parikh filter described in ZIPT - (https://github.com/CEisenhofer/ZIPT/tree/parikh/ZIPT/Constraints) - replacing ZIPT's PDD-based Parikh subsolver with Z3's linear arithmetic. - Author: Clemens Eisenhofer 2026-03-10 diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp index 61d5e88a35..ef3e8af2aa 100644 --- a/src/smt/seq/seq_regex.cpp +++ b/src/smt/seq/seq_regex.cpp @@ -19,15 +19,6 @@ Author: namespace seq { - // NSB code review: change the stabilizers set to - // add the regexes in the domain of m_stabilizers to a trail (expr_ref_vector - // change the range to be a vector of expressions, not snodes - // add regexes in the range of m_stabilizers to the trail - // this is to ensure that the expressions are valid also after scope changes. - // maybe all regexes entered are created at base level for quantifier free formulas - // but we should not assume this. The sgraph also can change based on scope. - // the Stabilizer data-structure persists across search. - // Collect possible first characters of a syntactically known *string* // expression (the body of to_re). Regex operators (union, complement, // intersection, ...) are not expected here. @@ -78,203 +69,6 @@ namespace seq { } - // ----------------------------------------------------------------------- - // Stabilizer store - // ----------------------------------------------------------------------- - - void seq_regex::reset_stabilizers() { - m_stabilizers.reset(); - m_self_stabilizing.reset(); - } - - void seq_regex::add_stabilizer(euf::snode const* regex, euf::snode const* stabilizer) { - if (!regex || !stabilizer) - return; - - const unsigned id = regex->id(); - auto& stabs = m_stabilizers.insert_if_not_there(id, euf::snode_vector()); - - // De-duplicate by pointer equality (mirrors ZIPT Environment.AddStabilizer - // which checks reference equality before adding). - for (euf::snode const* s : stabs) - if (s == stabilizer) - return; - stabs.push_back(stabilizer); - } - - euf::snode const* seq_regex::get_stabilizer_union(euf::snode const* regex) { - if (!regex) - return nullptr; - - if (!m_stabilizers.contains(regex->id())) - return nullptr; - - auto& stabs = m_stabilizers[regex->id()]; - if (stabs.empty()) - return nullptr; - - // Single stabilizer: return it directly. - if (stabs.size() == 1) - return stabs[0]; - - // Multiple stabilizers: build re.union chain. - // union(s1, union(s2, ... union(sN-1, sN)...)) - euf::snode const* result = stabs[stabs.size() - 1]; - for (unsigned i = stabs.size() - 1; i-- > 0; ) { - expr* lhs = stabs[i]->get_expr(); - expr* rhs = result->get_expr(); - result = m_sg.mk(seq.re.mk_union(lhs, rhs)); - } - return result; - } - - bool seq_regex::has_stabilizers(euf::snode const* regex) const { - if (!regex) - return false; - if (!m_stabilizers.contains(regex->id())) - return false; - return !m_stabilizers[regex->id()].empty(); - } - - euf::snode_vector const* seq_regex::get_stabilizers(euf::snode const* regex) const { - if (!regex) - return nullptr; - if (!m_stabilizers.contains(regex->id())) - return nullptr; - return &m_stabilizers[regex->id()]; - } - - void seq_regex::set_self_stabilizing(euf::snode const* regex) { - if (regex) - m_self_stabilizing.insert(regex->id()); - } - - bool seq_regex::is_self_stabilizing(euf::snode const* regex) const { - return regex && m_self_stabilizing.contains(regex->id()); - } - - // ----------------------------------------------------------------------- - // Self-stabilizing auto-detection - // ----------------------------------------------------------------------- - - bool seq_regex::compute_self_stabilizing(euf::snode const* regex) const { - return false; - } - - // ----------------------------------------------------------------------- - // Self-stabilizing propagation through derivatives - // ----------------------------------------------------------------------- - - void seq_regex::propagate_self_stabilizing(euf::snode const* parent, euf::snode const* deriv) { - if (!parent || !deriv) - return; - - // If the derivative is already known to be self-stabilizing (either - // inherently or from a prior propagation), nothing to do. - if (is_self_stabilizing(deriv)) - return; - - // If the derivative is itself inherently self-stabilizing - // (e.g., it is a star or full_seq), mark it now. - if (compute_self_stabilizing(deriv)) { - set_self_stabilizing(deriv); - return; - } - - // Rule 1: Star parent. - // D(c, R*) = D(c, R) · R*. The derivative always contains the - // R* tail, so it is self-stabilizing regardless of D(c,R). - if (parent->is_star()) { - set_self_stabilizing(deriv); - return; - } - - // Rule 2: Full_seq parent. - // D(c, Σ*) = Σ*, and Σ* is self-stabilizing. - // (The derivative should be Σ* itself; mark it for safety.) - if (parent->is_full_seq()) { - set_self_stabilizing(deriv); - return; - } - - // Check if parent is self-stabilizing (either inherently or marked). - bool parent_ss = is_self_stabilizing(parent) || compute_self_stabilizing(parent); - - // Rule 3: Concat parent R · S. - // D(c, R·S) = D(c,R)·S | (nullable(R) ? D(c,S) : ∅). - // If S is self-stabilizing, the D(c,R)·S branch inherits it. - // If the whole parent R·S is self-stabilizing, the derivative is too. - if (parent->is_concat() && parent->num_args() == 2) { - euf::snode const* tail = parent->arg(1); - bool tail_ss = is_self_stabilizing(tail) || compute_self_stabilizing(tail); - if (tail_ss || parent_ss) { - set_self_stabilizing(deriv); - return; - } - } - - // Rule 4: Union parent R | S. - // D(c, R|S) = D(c,R) | D(c,S). - // Self-stabilizing if both children are self-stabilizing. - if (parent->is_union() && parent->num_args() == 2) { - euf::snode const* lhs = parent->arg(0); - euf::snode const* rhs = parent->arg(1); - bool lhs_ss = is_self_stabilizing(lhs) || compute_self_stabilizing(lhs); - bool rhs_ss = is_self_stabilizing(rhs) || compute_self_stabilizing(rhs); - if (lhs_ss && rhs_ss) { - set_self_stabilizing(deriv); - return; - } - } - - // Rule 5: Intersection parent R ∩ S. - // D(c, R∩S) = D(c,R) ∩ D(c,S). - // Self-stabilizing if both children are self-stabilizing. - if (parent->is_intersect() && parent->num_args() == 2) { - euf::snode const* lhs = parent->arg(0); - euf::snode const* rhs = parent->arg(1); - bool lhs_ss = is_self_stabilizing(lhs) || compute_self_stabilizing(lhs); - bool rhs_ss = is_self_stabilizing(rhs) || compute_self_stabilizing(rhs); - if (lhs_ss && rhs_ss) { - set_self_stabilizing(deriv); - return; - } - } - - // Rule 6: Complement parent ~R. - // D(c, ~R) = ~D(c, R). - // Preserves self-stabilizing from R. - if (parent->is_complement() && parent->num_args() == 1) { - euf::snode const* inner = parent->arg(0); - bool inner_ss = is_self_stabilizing(inner) || compute_self_stabilizing(inner); - if (inner_ss) { - set_self_stabilizing(deriv); - return; - } - } - - // Rule 7: Generic self-stabilizing parent. - // If the parent was explicitly marked self-stabilizing (e.g., via - // a previous propagation), propagate to the derivative. - if (parent_ss) { - set_self_stabilizing(deriv); - return; - } - } - - // ----------------------------------------------------------------------- - // Derivative with propagation - // ----------------------------------------------------------------------- - - euf::snode const* seq_regex::derivative_with_propagation(euf::snode const* re, euf::snode const* elem) { - if (!re || !elem) - return nullptr; - euf::snode const* deriv = derivative(re, elem); - if (deriv) - propagate_self_stabilizing(re, deriv); - return deriv; - } - // ----------------------------------------------------------------------- // Uniform derivative (symbolic character consumption) // ----------------------------------------------------------------------- @@ -320,7 +114,7 @@ namespace seq { } // ----------------------------------------------------------------------- - // Ground prefix consumption + // Basic regex predicates // ----------------------------------------------------------------------- bool seq_regex::is_empty_regex(euf::snode const* re) const { @@ -549,7 +343,6 @@ namespace seq { // ----------------------------------------------------------------------- // Multi-regex intersection emptiness check // BFS over the product of Brzozowski derivative automata. - // Mirrors ZIPT NielsenNode.CheckEmptiness (NielsenNode.cs:1429-1469) // ----------------------------------------------------------------------- lbool seq_regex::check_intersection_emptiness(euf::snode_vector const& regexes, unsigned max_states) { @@ -573,77 +366,6 @@ namespace seq { return is_empty_bfs(result, max_states); } - // ----------------------------------------------------------------------- - // Language subset check: L(A) ⊆ L(B) - // via intersection(A, complement(B)) = ∅ - // Mirrors ZIPT NielsenNode.IsLanguageSubset (NielsenNode.cs:1382-1385) - // ----------------------------------------------------------------------- - - lbool seq_regex::is_language_subset(euf::snode const* subset_re, euf::snode const* superset_re) { - if (!subset_re || !superset_re) - return l_undef; - - // Quick checks - if (subset_re->is_fail() || is_empty_regex(subset_re)) - return l_true; // ∅ ⊆ anything - if (superset_re->is_full_seq()) - return l_true; // anything ⊆ Σ* - if (subset_re == superset_re) - return l_true; // L ⊆ L - - // Build complement(superset) - expr* sup_expr = superset_re->get_expr(); - euf::snode const* comp_sn = m_sg.mk(seq.re.mk_complement(sup_expr)); - - // Build intersection and check emptiness - // subset ∩ complement(superset) should be empty for subset relation - expr* sub_expr = subset_re->get_expr(); - auto inter = seq.re.mk_inter(sub_expr, comp_sn->get_expr()); - euf::snode const* inter_sn = m_sg.mk(inter); - return is_empty_bfs(inter_sn); - } - - // ----------------------------------------------------------------------- - // Collect primitive regex intersection for a variable - // ----------------------------------------------------------------------- - - euf::snode const* seq_regex::collect_primitive_regex_intersection( - euf::snode const* var, nielsen_node const& node, dep_manager& dep_mgr, dep_tracker& dep) const { - SASSERT(var); - - euf::snode const* result = nullptr; - - for (auto const& mem : node.str_mems()) { - // Primitive constraint: str is a single variable. View/guard - // memberships do not denote a plain regex on `var` (their m_regex - // is a derivative *state*), so skip them — yielding a coarser but - // sound over-approximation for the caller (regex widening). - if (!mem.is_primitive() || !mem.is_plain()) - continue; - euf::snode const* first = mem.m_str->first(); - // NSB review: why is this "first" and not mem.m_str? - SASSERT(first); - if (first != var) - continue; - TRACE(seq, tout << spp(first, m) << " " << mem_pp(mem) << "\n"); - - if (!result) { - result = mem.m_regex; - dep = dep_mgr.mk_join(dep, mem.m_dep); - } - else { - expr* r1 = result->get_expr(); - expr* r2 = mem.m_regex->get_expr(); - if (r1 && r2) { - auto inter = seq.re.mk_inter(r1, r2); - result = m_sg.mk(inter); - dep = dep_mgr.mk_join(dep, mem.m_dep); - } - } - } - return result; - } - // ----------------------------------------------------------------------- // Ground prefix consumption // ----------------------------------------------------------------------- @@ -662,8 +384,6 @@ namespace seq { break; if (deriv->is_fail()) return simplify_status::conflict; - // propagate self-stabilizing flag from parent to derivative - propagate_self_stabilizing(parent_re, deriv); mem.m_str = m_sg.drop_first(mem.m_str); mem.m_regex = deriv; } @@ -776,244 +496,6 @@ namespace seq { return true; } - // ----------------------------------------------------------------------- - // Stabilizer from cycle - // ----------------------------------------------------------------------- - - euf::snode const* seq_regex::stabilizer_from_cycle(euf::snode const* cycle_regex, - euf::snode const* current_regex) { - if (!cycle_regex || !current_regex) - return nullptr; - - expr* re_expr = cycle_regex->get_expr(); - auto star_expr = seq.re.mk_star(re_expr); - return m_sg.mk(star_expr); - } - - // ----------------------------------------------------------------------- - // Extract cycle history tokens - // ----------------------------------------------------------------------- - - euf::snode const* seq_regex::extract_cycle_history(seq::str_mem const& current, - seq::str_mem const& ancestor) { - // The history is built by simplify_and_init as a left-associative - // string concat chain: concat(concat(concat(nil, c1), c2), c3). - // Extract the tokens consumed since the ancestor. - return nullptr; - } - - // ----------------------------------------------------------------------- - // Get filtered stabilizer star - // Mirrors ZIPT StrMem.GetFilteredStabilizerStar (StrMem.cs:228-243) - // ----------------------------------------------------------------------- - - euf::snode const* seq_regex::get_filtered_stabilizer_star(euf::snode const* re, - euf::snode const* excluded_char) const { - if (!re) - return nullptr; - - euf::snode_vector const* stabs = get_stabilizers(re); - if (!stabs || stabs->empty()) - return nullptr; - euf::snode const* filtered_union = nullptr; - - for (euf::snode const* s : *stabs) { - if (!s) - continue; - // Keep only stabilizers whose language cannot start with excluded_char - euf::snode const* d = m_sg.brzozowski_deriv(s, excluded_char); - if (d && d->is_fail()) { - if (!filtered_union) { - filtered_union = s; - } - else { - expr* e1 = filtered_union->get_expr(); - expr* e2 = s->get_expr(); - if (e1 && e2) { - auto u = seq.re.mk_union(e1, e2); - filtered_union = m_sg.mk(u); - } - } - } - } - - if (!filtered_union) - return nullptr; - - expr* fe = filtered_union->get_expr(); - if (!fe) - return nullptr; - return m_sg.mk(seq.re.mk_star(fe)); - } - - // ----------------------------------------------------------------------- - // Strengthened stabilizer construction with sub-cycle detection - // Mirrors ZIPT StrMem.StabilizerFromCycle (StrMem.cs:163-225) - // ----------------------------------------------------------------------- - - euf::snode const* seq_regex::strengthened_stabilizer(euf::snode const* cycle_regex, - euf::snode const* cycle_history) { - if (!cycle_regex || !cycle_history) - return nullptr; - - // Flatten the history concat chain into a vector of character tokens. - euf::snode_vector tokens; - cycle_history->collect_tokens(tokens); - - if (tokens.empty()) - return nullptr; - - // Replay tokens on the cycle regex, detecting sub-cycles. - // A sub-cycle is detected when the derivative returns to cycle_regex. - svector> sub_cycles; - unsigned cycle_start = 0; - euf::snode const* current_re = cycle_regex; - - for (unsigned i = 0; i < tokens.size(); ++i) { - euf::snode const* tok = tokens[i]; - if (!tok) - return nullptr; - - euf::snode const* deriv = m_sg.brzozowski_deriv(current_re, tok); - if (!deriv) - return nullptr; - - // Sub-cycle: derivative returned to the cycle entry regex - if (deriv == cycle_regex || - (deriv->get_expr() && cycle_regex->get_expr() && - deriv->get_expr() == cycle_regex->get_expr())) { - sub_cycles.push_back(std::make_pair(cycle_start, i + 1)); - cycle_start = i + 1; - current_re = cycle_regex; - } else { - current_re = deriv; - } - } - - // Remaining tokens that don't complete a sub-cycle - if (cycle_start < tokens.size()) - sub_cycles.push_back(std::make_pair(cycle_start, tokens.size())); - - if (sub_cycles.empty()) - return nullptr; - - // Build a stabilizer body for each sub-cycle. - // body = to_re(t0) · [filteredStar(R1, t1)] · to_re(t1) · ... · to_re(t_{n-1}) - euf::snode const* overall_union = nullptr; - - for (auto const& sc : sub_cycles) { - unsigned start = sc.first; - unsigned end = sc.second; - if (start >= end) - continue; - - euf::snode const* re_state = cycle_regex; - euf::snode const* body = nullptr; - - for (unsigned i = start; i < end; ++i) { - euf::snode const* tok = tokens[i]; - if (!tok) - break; - - // Insert filtered stabilizer star before each token after the first - if (i > start) { - euf::snode const* filtered = get_filtered_stabilizer_star(re_state, tok); - if (filtered) { - expr* fe = filtered->get_expr(); - if (fe) { - if (!body) - body = filtered; - else { - expr* be = body->get_expr(); - body = m_sg.mk(seq.re.mk_concat(be, fe)); - } - } - } - } - - // Convert char token to regex: to_re(unit(tok)) - expr* tok_expr = tok->get_expr(); - - expr_ref unit_str(seq.str.mk_unit(tok_expr), m); - expr_ref tok_re(seq.re.mk_to_re(unit_str), m); - euf::snode const* tok_re_sn = m_sg.mk(tok_re); - - if (!body) { - body = tok_re_sn; - } else { - expr* be = body->get_expr(); - expr* te = tok_re_sn->get_expr(); - if (be && te) { - expr_ref cat(seq.re.mk_concat(be, te), m); - body = m_sg.mk(cat); - } - } - - // Advance the regex state - euf::snode const* deriv = m_sg.brzozowski_deriv(re_state, tok); - if (!deriv) - break; - re_state = deriv; - } - - if (!body) - continue; - - if (!overall_union) { - overall_union = body; - } else { - expr* oe = overall_union->get_expr(); - expr* be = body->get_expr(); - if (oe && be) { - expr_ref u(seq.re.mk_union(oe, be), m); - overall_union = m_sg.mk(u); - } - } - } - - return overall_union; - } - - // ----------------------------------------------------------------------- - // Stabilizer-based subsumption (enhanced) - // Mirrors ZIPT StrMem.TrySubsume (StrMem.cs:354-386) - // ----------------------------------------------------------------------- - - bool seq_regex::try_subsume(str_mem const& mem, nielsen_node const& node) { -#if 0 - SASSERT(mem.m_str && mem.m_regex); - - // 1. Leading token must be a variable - euf::snode const* first = mem.m_str->first(); - if (!first || !first->is_var()) - return false; - - // 2. Must have stabilizers for the regex - if (!has_stabilizers(mem.m_regex)) - return false; - - // 3. Build stabStar = star(union(all stabilizers for this regex)) - euf::snode const* stab_union = get_stabilizer_union(mem.m_regex); - if (!stab_union) - return false; - - expr* su_expr = stab_union->get_expr(); - expr_ref stab_star(seq.re.mk_star(su_expr), m); - euf::snode const* stab_star_sn = m_sg.mk(stab_star); - - // 4. Collect all primitive regex constraints on variable `first` - euf::snode const* x_range = collect_primitive_regex_intersection(first, node, dep); - if (!x_range) - return false; - - // 5. Check L(x_range) ⊆ L(stab_star) - lbool result = is_language_subset(x_range, stab_star_sn); - return result == l_true; -#else - return false; -#endif - } - char_set seq_regex::minterm_to_char_set(expr* re_expr) { unsigned max_c = seq.max_char(); diff --git a/src/smt/seq/seq_regex.h b/src/smt/seq/seq_regex.h index 45b911d8b7..ef9e1c2c95 100644 --- a/src/smt/seq/seq_regex.h +++ b/src/smt/seq/seq_regex.h @@ -10,13 +10,12 @@ Abstract: Lazy regex membership processing for the Nielsen-based string solver. Provides Brzozowski derivative computation, ground prefix/suffix - consumption, cycle detection in derivation histories, and - stabilizer-based subsumption for regex membership constraints. + consumption, BFS emptiness/intersection checks, and minterm/char-set + utilities for regex membership constraints. - Ports the following ZIPT StrMem operations: - - SimplifyCharRegex / SimplifyDir (ground prefix/suffix consumption) - - ExtractCycle / StabilizerFromCycle (cycle detection and widening) - - TrySubsume (stabilizer-based subsumption) + Cycle detection and stabilizer-based subsumption live in the landing + decomposition and land-state views of nielsen_graph (seq_nielsen.cpp); + the legacy stabilizer store that used to reside here has been removed. The class wraps sgraph operations (brzozowski_deriv, compute_minterms, drop_first, etc.) and provides a higher-level interface for @@ -45,22 +44,6 @@ namespace seq { // cache for emptiness check (snode id -> lbool) u_map m_empty_cache; - // ----------------------------------------------------------------- - // Stabilizer store (non-backtrackable, persists across solve() calls) - // Mirrors ZIPT Environment.stabilizers / selfStabilizing - // (Environment.cs:36-37) - // ----------------------------------------------------------------- - - // Maps regex snode id → list of stabilizer snodes. - // Each regex may accumulate multiple stabilizers from different - // cycle detections. The list is deduplicated by pointer equality. - u_map m_stabilizers; - - // Set of regex snode ids that are self-stabilizing, i.e., the - // stabilizer for the regex is the regex itself (e.g., r*). - // Mirrors ZIPT Environment.selfStabilizing (Environment.cs:37) - uint_set m_self_stabilizing; - // ----------------------------------------------------------------- // BFS emptiness check helpers (private) // ----------------------------------------------------------------- @@ -100,75 +83,6 @@ namespace seq { euf::sgraph& sg() { return m_sg; } - // ----------------------------------------------------------------- - // Stabilizer store API - // Mirrors ZIPT Environment stabilizer management - // (Environment.cs:114-146) - // ----------------------------------------------------------------- - - // Reset all stabilizer data. Called at the start of each solve() - // invocation if fresh stabilizer state is desired. - // Note: stabilizers persist across depth-bound iterations by default; - // only call this to clear accumulated state. - void reset_stabilizers(); - - // Add a stabilizer for a regex. De-duplicates by pointer equality. - // Mirrors ZIPT Environment.AddStabilizer (Environment.cs:114-123). - void add_stabilizer(euf::snode const* regex, euf::snode const* stabilizer); - - // Get the union of all stabilizers registered for a regex. - // Returns a single re.union snode combining all stabilizers, - // or nullptr if no stabilizers exist for the regex. - // Mirrors ZIPT Environment.GetStabilizerUnion (Environment.cs:125-128). - euf::snode const* get_stabilizer_union(euf::snode const* regex); - - // Check if any stabilizers have been registered for a regex. - bool has_stabilizers(euf::snode const* regex) const; - - // Get raw stabilizer list for a regex (read-only). - // Returns nullptr if no stabilizers exist. - euf::snode_vector const* get_stabilizers(euf::snode const* regex) const; - - // Mark a regex as self-stabilizing (stabilizer == regex itself). - // Mirrors ZIPT Environment.SetSelfStabilizing (Environment.cs:143-146). - void set_self_stabilizing(euf::snode const* regex); - - // Check if a regex is marked as self-stabilizing. - // Mirrors ZIPT Environment.IsSelfStabilizing (Environment.cs:134-141). - bool is_self_stabilizing(euf::snode const* regex) const; - - // ----------------------------------------------------------------- - // Self-stabilizing auto-detection and propagation through derivatives - // ----------------------------------------------------------------- - - // Determine if a regex is inherently self-stabilizing based on its - // structure. Returns true for: - // - R* (Kleene star): D(c, R*) = D(c,R)·R*, so R* is its own - // stabilizer regardless of the character. - // - Σ* (full_seq): D(c, Σ*) = Σ*, trivially self-stabilizing. - // - ∅ (fail/empty language): no live derivatives, trivially stable. - // - Complement of full_seq (~Σ* = ∅): also trivially stable. - // Does NOT mark the snode; call set_self_stabilizing to persist. - bool compute_self_stabilizing(euf::snode const* regex) const; - - // After computing a derivative of parent, propagate the self- - // stabilizing flag to the derivative result if warranted. - // Applies structural rules: - // - If parent is R* → derivative is always self-stabilizing - // (derivative has the form D(c,R)·R* which contains the R* tail). - // - If parent is R·S and S is self-stabilizing → derivative may - // inherit from the self-stabilizing tail. - // - If parent is R|S and both are self-stabilizing → derivative is. - // - If parent is R∩S and both are self-stabilizing → derivative is. - // - If parent is ~R and R is self-stabilizing → derivative is. - // Updates the internal self-stabilizing set for the derivative. - void propagate_self_stabilizing(euf::snode const* parent, euf::snode const* deriv); - - // Convenience: compute derivative and propagate self-stabilizing flags. - // Equivalent to calling derivative() followed by - // propagate_self_stabilizing(). - euf::snode const* derivative_with_propagation(euf::snode const* re, euf::snode const* elem); - // ----------------------------------------------------------------- // Basic regex predicates // ----------------------------------------------------------------- @@ -192,21 +106,8 @@ namespace seq { // l_true — intersection is definitely empty // l_false — intersection is definitely non-empty // l_undef — inconclusive (hit exploration bound) - // Mirrors ZIPT NielsenNode.CheckEmptiness (NielsenNode.cs:1429-1469) lbool check_intersection_emptiness(euf::snode_vector const& regexes, unsigned max_states = UINT_MAX); - // Check if L(subset_re) ⊆ L(superset_re). - // Computed as: subset_re ∩ complement(superset_re) = ∅. - // Mirrors ZIPT NielsenNode.IsLanguageSubset (NielsenNode.cs:1382-1385) - lbool is_language_subset(euf::snode const* subset_re, euf::snode const* superset_re); - - // Collect all primitive regex constraints on variable `var` from - // the node's str_mem list and return their intersection as a - // single regex snode (using re.inter). - // Returns nullptr if no primitive constraints found. - euf::snode const* collect_primitive_regex_intersection( - euf::snode const* var, nielsen_node const& node, dep_manager& dep_mgr, dep_tracker& dep) const; - // check if regex is the full language (Σ* / re.all) static bool is_full_regex(euf::snode const* re) { return re && re->is_full_seq(); @@ -239,17 +140,12 @@ namespace seq { // deriv(regex, c) = result. This enables deterministic consumption // of symbolic (variable) characters without branching. // Returns the uniform derivative if found, nullptr otherwise. - // Mirrors ZIPT's SimplifyCharRegex uniform-derivative fast path. euf::snode const* try_uniform_derivative(euf::snode const* regex) const; // compute derivative of a str_mem constraint: advance past one character. // the string side is shortened by drop_first and the regex is derived. - // Propagates self-stabilizing flags from the parent regex to the derivative. str_mem derive(str_mem const& mem, euf::snode const* elem) { - euf::snode const* parent_re = mem.m_regex; - euf::snode const* deriv = m_sg.brzozowski_deriv(parent_re, elem); - if (deriv) - propagate_self_stabilizing(parent_re, deriv); + euf::snode const* deriv = m_sg.brzozowski_deriv(mem.m_regex, elem); euf::snode const* new_str = m_sg.drop_first(mem.m_str); return str_mem(mem.m, new_str, deriv, mem.m_dep); } @@ -316,54 +212,6 @@ namespace seq { // (empty string in non-nullable regex, or derivative yields ∅). bool process_str_mem(str_mem const& mem, vector& out_mems); - - // ----------------------------------------------------------------- - // Cycle detection and stabilizers - // ----------------------------------------------------------------- - - // compute a Kleene star stabilizer from a cycle. - // given the regex at the cycle point and the current regex, - // builds r* that over-approximates any number of cycle iterations. - // returns nullptr if no stabilizer can be computed. - euf::snode const* stabilizer_from_cycle(euf::snode const* cycle_regex, - euf::snode const* current_regex); - - // Strengthened stabilizer construction with sub-cycle detection. - // Replays the consumed character tokens from cycle_history on the - // cycle regex, detecting sub-cycles (where the derivative loops - // back to the original regex). For each sub-cycle, builds a - // stabilizer from the interleaved character tokens and filtered - // sub-stabilizers. - // Returns a union of all sub-cycle stabilizer bodies, or nullptr - // if no non-trivial stabilizer can be built. - // Mirrors ZIPT StrMem.StabilizerFromCycle (StrMem.cs:163-225). - euf::snode const* strengthened_stabilizer(euf::snode const* cycle_regex, - euf::snode const* cycle_history); - - // Get filtered stabilizer star: for regex state re, retrieve - // existing stabilizers, filter out those whose language can - // start with any character in excluded_char, and wrap the - // remaining in star(union(...)). - // Returns nullptr (or empty-equivalent) if no valid stabilizers. - // Mirrors ZIPT StrMem.GetFilteredStabilizerStar (StrMem.cs:228-243). - euf::snode const* get_filtered_stabilizer_star(euf::snode const* re, - euf::snode const* excluded_char) const; - - // Extract the cycle portion of a str_mem's history by comparing - // the current history with an ancestor's history length. - // Returns the sub-sequence of tokens consumed since the ancestor, - // or nullptr if the history did not advance. - euf::snode const* extract_cycle_history(str_mem const& current, - str_mem const& ancestor); - - // try to subsume a str_mem constraint using stabilizer-based - // reasoning. Enhanced version: checks if the leading variable's - // language (intersection of all its primitive regex constraints) - // is a subset of star(union(stabilizers)) for the current regex. - // Falls back to cycle-based pointer equality check. - // returns true if the constraint can be dropped. - // Mirrors ZIPT StrMem.TrySubsume (StrMem.cs:354-386). - bool try_subsume(str_mem const& mem, nielsen_node const& node); }; } diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 4ffc89c10e..946b0dfc59 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -474,8 +474,19 @@ namespace smt { // length and the regex are only loosely coupled), retry unconstrained so // the emitted word still satisfies every regex/view constraint. bool ok = m_nielsen->product_witness(var, *m_sat_node, len, w); - if (!ok && len != UINT_MAX) + if (!ok && len != UINT_MAX) { ok = m_nielsen->product_witness(var, *m_sat_node, UINT_MAX, w); + // The view-length side constraints (add_view_length_constraints) + // keep the arith-assigned length realizable up to a semilinear + // over-approximation of the view language, so this retry should + // be rare. When it fires, the emitted word's length differs + // from the arith model's len(var): surface it instead of + // degrading the model silently. + IF_VERBOSE(1, if (ok && w.length() != len) + verbose_stream() << "nseq: view witness for " << mk_pp(var->get_expr(), m) + << " has length " << w.length() << " but arith assigned " << len + << " (model may be length-inconsistent)\n";); + } if (ok) { expr* witness = m_seq.str.mk_string(w); m_trail.push_back(witness); diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index a3c365e04f..d54ca06c5c 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -7,7 +7,6 @@ Module Name: Abstract: - ZIPT string solver theory for Z3. Implementation of theory_nseq. Author: @@ -1745,7 +1744,7 @@ namespace smt { // ----------------------------------------------------------------------- // Regex membership pre-check // For each variable with regex membership constraints, check intersection - // emptiness before DFS. Mirrors ZIPT's per-variable regex evaluation. + // emptiness before DFS. // // Returns: // l_true — conflict asserted (empty intersection for some variable) diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 628e78d1c0..85aec28224 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -7,7 +7,6 @@ Module Name: Abstract: - ZIPT string solver theory for Z3. Implements theory_nseq, a theory plugin for string/sequence constraints using the Nielsen transformation graph (Nielsen graph). diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp index 7a9e48a2be..7650949372 100644 --- a/src/test/seq_parikh.cpp +++ b/src/test/seq_parikh.cpp @@ -7,7 +7,7 @@ Module Name: Abstract: - Unit tests for seq_parikh (Parikh image filter for the ZIPT Nielsen solver). + Unit tests for seq_parikh. Tests cover: - compute_length_stride / get_length_stride for all regex forms diff --git a/src/test/seq_regex.cpp b/src/test/seq_regex.cpp index 6c5969718e..c0891d33de 100644 --- a/src/test/seq_regex.cpp +++ b/src/test/seq_regex.cpp @@ -71,227 +71,6 @@ static void test_seq_regex_is_full() { std::cout << " ok: re.all not recognized as empty\n"; } -// Test 4: strengthened_stabilizer — null safety -static void test_strengthened_stabilizer_null() { - std::cout << "test_strengthened_stabilizer_null\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - - SASSERT(nr.strengthened_stabilizer(nullptr, nullptr) == nullptr); - - seq_util su(m); - sort* str_sort = su.str.mk_string_sort(); - sort* re_sort = su.re.mk_re(str_sort); - const expr_ref full_e(su.re.mk_full_seq(re_sort), m); - euf::snode const* full_re = sg.mk(full_e); - - SASSERT(nr.strengthened_stabilizer(full_re, nullptr) == nullptr); - SASSERT(nr.strengthened_stabilizer(nullptr, full_re) == nullptr); - std::cout << " ok\n"; -} - -// Test 5: strengthened_stabilizer — single char cycle on a* -// Regex a*, history = 'a'. D('a', a*) = a* (sub-cycle back to start). -// Stabilizer body should be to_re("a"). -static void test_strengthened_stabilizer_single_char() { - std::cout << "test_strengthened_stabilizer_single_char\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - // Build a* - const expr_ref star_a(su.re.mk_star(su.re.mk_to_re(su.str.mk_string("a"))), m); - euf::snode const* re_star_a = sg.mk(star_a); - - // Build history = char 'a' (single token, no concat needed) - euf::snode const* tok_a = sg.mk_char('a'); - euf::snode const* history = tok_a; - - euf::snode const* result = nr.strengthened_stabilizer(re_star_a, history); - // Should produce a non-null stabilizer body (to_re("a")) - SASSERT(result != nullptr); - std::cout << " ok: a* with history 'a' -> non-null stabilizer\n"; -} - -// Test 6: strengthened_stabilizer — two-char cycle with sub-cycle -// Regex (ab)*, history = 'a', 'b'. D('a', (ab)*) = b(ab)*, D('b', b(ab)*) = (ab)* -// This should detect a sub-cycle and build a stabilizer body. -static void test_strengthened_stabilizer_two_char() { - std::cout << "test_strengthened_stabilizer_two_char\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - // Build (ab)* - const expr_ref ab(su.re.mk_to_re(su.str.mk_string("ab")), m); - const expr_ref star_ab(su.re.mk_star(ab), m); - euf::snode const* re_star_ab = sg.mk(star_ab); - - // Build history: concat(char_a, char_b) using string concat - euf::snode const* tok_a = sg.mk_char('a'); - euf::snode const* tok_b = sg.mk_char('b'); - euf::snode const* history = sg.mk_concat(tok_a, tok_b); - - euf::snode const* result = nr.strengthened_stabilizer(re_star_ab, history); - // Should produce a non-null stabilizer body - SASSERT(result != nullptr); - std::cout << " ok: (ab)* with history 'ab' -> non-null stabilizer\n"; -} - -// Test 7: get_filtered_stabilizer_star — no stabilizers registered -static void test_filtered_stabilizer_star_empty() { - std::cout << "test_filtered_stabilizer_star_empty\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - const seq::seq_regex nr(sg); - seq_util su(m); - - sort* str_sort = su.str.mk_string_sort(); - sort* re_sort = su.re.mk_re(str_sort); - const expr_ref full_e(su.re.mk_full_seq(re_sort), m); - euf::snode const* full_re = sg.mk(full_e); - euf::snode const* tok_a = sg.mk_char('a'); - - euf::snode const* result = nr.get_filtered_stabilizer_star(full_re, tok_a); - SASSERT(result == nullptr); - std::cout << " ok: no stabilizers -> nullptr\n"; -} - -// Test 8: get_filtered_stabilizer_star — with registered stabilizer that passes filter -static void test_filtered_stabilizer_star_with_stab() { - std::cout << "test_filtered_stabilizer_star_with_stab\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - // Build a* as the regex state - const expr_ref star_a(su.re.mk_star(su.re.mk_to_re(su.str.mk_string("a"))), m); - euf::snode const* re_star_a = sg.mk(star_a); - - // Register a stabilizer: to_re("b") — only accepts "b" - const expr_ref stab_b(su.re.mk_to_re(su.str.mk_string("b")), m); - euf::snode const* stab_b_sn = sg.mk(stab_b); - nr.add_stabilizer(re_star_a, stab_b_sn); - - // Exclude char 'a': D('a', to_re("b")) should be fail - euf::snode const* tok_a = sg.mk_char('a'); - euf::snode const* result = nr.get_filtered_stabilizer_star(re_star_a, tok_a); - // to_re("b") should pass the filter → result is star(to_re("b")) - SASSERT(result != nullptr); - SASSERT(result->is_star()); - std::cout << " ok: filter keeps to_re('b') when excluding 'a'\n"; -} - -// Test 9: get_filtered_stabilizer_star — stabilizer filtered out -static void test_filtered_stabilizer_star_filtered() { - std::cout << "test_filtered_stabilizer_star_filtered\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - // Build a* as the regex state - const expr_ref star_a(su.re.mk_star(su.re.mk_to_re(su.str.mk_string("a"))), m); - euf::snode const* re_star_a = sg.mk(star_a); - - // Register a stabilizer: to_re("a") — accepts "a" - const expr_ref stab_a(su.re.mk_to_re(su.str.mk_string("a")), m); - euf::snode const* stab_a_sn = sg.mk(stab_a); - nr.add_stabilizer(re_star_a, stab_a_sn); - - // Exclude char 'a': D('a', to_re("a")) is NOT fail → filtered out - euf::snode const* tok_a = sg.mk_char('a'); - euf::snode const* result = nr.get_filtered_stabilizer_star(re_star_a, tok_a); - SASSERT(result == nullptr); - std::cout << " ok: filter removes to_re('a') when excluding 'a'\n"; -} - -// Test 10: extract_cycle_history — basic extraction -static void test_extract_cycle_history_basic() { - std::cout << "test_extract_cycle_history_basic\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - sort* str_sort = su.str.mk_string_sort(); - sort* re_sort = su.re.mk_re(str_sort); - const expr_ref full_e(su.re.mk_full_seq(re_sort), m); - euf::snode const* full_re = sg.mk(full_e); - - euf::snode const* tok_a = sg.mk_char('a'); - euf::snode const* tok_b = sg.mk_char('b'); - euf::snode const* tok_c = sg.mk_char('c'); - - // Ancestor history: just 'a' (length 1) - euf::snode const* anc_hist = tok_a; - - // Current history: concat(concat(a, b), c) = a,b,c (length 3) - euf::snode const* cur_hist = sg.mk_concat(sg.mk_concat(tok_a, tok_b), tok_c); - - euf::snode const* empty_str = sg.mk_empty_seq(str_sort); - const seq::dep_tracker empty_dep = nullptr; - - const seq::str_mem ancestor(m, empty_str, full_re, empty_dep); - const seq::str_mem current(m, empty_str, full_re, empty_dep); - - euf::snode const* cycle = nr.extract_cycle_history(current, ancestor); - // Should return the last 2 tokens (b, c) - SASSERT(cycle != nullptr); - SASSERT(cycle->length() == 2); - std::cout << " ok: extracted cycle of length 2\n"; -} - -// Test 11: extract_cycle_history — null ancestor history -static void test_extract_cycle_history_null_ancestor() { - std::cout << "test_extract_cycle_history_null_ancestor\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - sort* str_sort = su.str.mk_string_sort(); - sort* re_sort = su.re.mk_re(str_sort); - const expr_ref full_e(su.re.mk_full_seq(re_sort), m); - euf::snode const* full_re = sg.mk(full_e); - - euf::snode const* tok_a = sg.mk_char('a'); - euf::snode const* tok_b = sg.mk_char('b'); - euf::snode const* cur_hist = sg.mk_concat(tok_a, tok_b); - euf::snode const* empty_str = sg.mk_empty_seq(str_sort); - const seq::dep_tracker empty_dep = nullptr; - - // Ancestor has no history (nullptr) - const seq::str_mem ancestor(m, empty_str, full_re, empty_dep); - const seq::str_mem current(m, empty_str, full_re, empty_dep); - - euf::snode const* cycle = nr.extract_cycle_history(current, ancestor); - // With null ancestor history, entire current history is the cycle - SASSERT(cycle != nullptr); - SASSERT(cycle->length() == 2); - std::cout << " ok: null ancestor -> full history as cycle\n"; -} - // Test 12: BFS emptiness — re.none (empty language) is empty static void test_bfs_empty_none() { std::cout << "test_bfs_empty_none\n"; @@ -490,63 +269,6 @@ static void test_char_set_is_subset() { std::cout << " ok\n"; } -// Test: stabilizer store basic operations -static void test_stabilizer_store_basic() { - std::cout << "test_stabilizer_store_basic\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - const expr_ref a_re(su.re.mk_to_re(su.str.mk_string("a")), m); - const expr_ref b_re(su.re.mk_to_re(su.str.mk_string("b")), m); - euf::snode const* a_sn = sg.mk(a_re); - euf::snode const* b_sn = sg.mk(b_re); - - SASSERT(!nr.has_stabilizers(a_sn)); - nr.add_stabilizer(a_sn, b_sn); - SASSERT(nr.has_stabilizers(a_sn)); - SASSERT(nr.get_stabilizer_union(a_sn) == b_sn); - - // dedup: adding same stabilizer again - nr.add_stabilizer(a_sn, b_sn); - auto* stabs = nr.get_stabilizers(a_sn); - SASSERT(stabs && stabs->size() == 1); - - // reset - nr.reset_stabilizers(); - SASSERT(!nr.has_stabilizers(a_sn)); - - std::cout << " ok\n"; -} - -// Test: self-stabilizing flag -static void test_self_stabilizing() { - std::cout << "test_self_stabilizing\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - const expr_ref a_re(su.re.mk_to_re(su.str.mk_string("a")), m); - euf::snode const* a_sn = sg.mk(a_re); - - SASSERT(!nr.is_self_stabilizing(a_sn)); - nr.set_self_stabilizing(a_sn); - SASSERT(nr.is_self_stabilizing(a_sn)); - - // star should be detected as self-stabilizing - const expr_ref star_a(su.re.mk_star(a_re), m); - euf::snode const* star_sn = sg.mk(star_a); - SASSERT(nr.compute_self_stabilizing(star_sn)); - - std::cout << " ok\n"; -} - // Test: check_intersection_emptiness — SAT case static void test_check_intersection_sat() { std::cout << "test_check_intersection_sat\n"; @@ -600,85 +322,6 @@ static void test_check_intersection_unsat() { std::cout << " ok: to_re(a) ∩ to_re(b) is empty\n"; } -// Test: is_language_subset — true case -static void test_is_language_subset_true() { - std::cout << "test_is_language_subset_true\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - // a* ⊆ (a|b)* should be true - const expr_ref a_re(su.re.mk_to_re(su.str.mk_string("a")), m); - const expr_ref star_a(su.re.mk_star(a_re), m); - const expr_ref b_re(su.re.mk_to_re(su.str.mk_string("b")), m); - const expr_ref ab_union(su.re.mk_union(a_re, b_re), m); - const expr_ref star_ab(su.re.mk_star(ab_union), m); - - euf::snode const* subset = sg.mk(star_a); - euf::snode const* superset = sg.mk(star_ab); - - const lbool result = nr.is_language_subset(subset, superset); - SASSERT(result == l_true); - std::cout << " ok: a* ⊆ (a|b)*\n"; -} - -// Test: is_language_subset — false case -static void test_is_language_subset_false() { - std::cout << "test_is_language_subset_false\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - - // (a|b)* ⊄ a* should be false (b ∈ (a|b)* but b ∉ a*) - const expr_ref a_re(su.re.mk_to_re(su.str.mk_string("a")), m); - const expr_ref star_a(su.re.mk_star(a_re), m); - const expr_ref b_re(su.re.mk_to_re(su.str.mk_string("b")), m); - const expr_ref ab_union(su.re.mk_union(a_re, b_re), m); - const expr_ref star_ab(su.re.mk_star(ab_union), m); - - euf::snode const* subset = sg.mk(star_ab); - euf::snode const* superset = sg.mk(star_a); - - const lbool result = nr.is_language_subset(subset, superset); - SASSERT(result == l_false); - std::cout << " ok: (a|b)* ⊄ a*\n"; -} - -// Test: is_language_subset — trivial cases -static void test_is_language_subset_trivial() { - std::cout << "test_is_language_subset_trivial\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq::seq_regex nr(sg); - seq_util su(m); - sort* str_sort = su.str.mk_string_sort(); - - // ∅ ⊆ anything = true - const expr_ref none(su.re.mk_empty(su.re.mk_re(str_sort)), m); - const expr_ref a_re(su.re.mk_to_re(su.str.mk_string("a")), m); - euf::snode const* empty_sn = sg.mk(none); - euf::snode const* a_sn = sg.mk(a_re); - SASSERT(nr.is_language_subset(empty_sn, a_sn) == l_true); - - // anything ⊆ Σ* = true - const expr_ref full(su.re.mk_full_seq(su.re.mk_re(str_sort)), m); - euf::snode const* full_sn = sg.mk(full); - SASSERT(nr.is_language_subset(a_sn, full_sn) == l_true); - - // L ⊆ L = true (same pointer) - SASSERT(nr.is_language_subset(a_sn, a_sn) == l_true); - - std::cout << " ok\n"; -} - // Regression test: representative chosen from bounds must respect accumulated excludes. // Example language is [A-Z] \ {"A"}, so a valid witness exists (e.g., "B") but not "A". static void test_some_seq_in_re_excluded_low_regression() { @@ -815,14 +458,6 @@ void tst_seq_regex() { test_seq_regex_instantiation(); test_seq_regex_is_empty(); test_seq_regex_is_full(); - test_strengthened_stabilizer_null(); - test_strengthened_stabilizer_single_char(); - test_strengthened_stabilizer_two_char(); - test_filtered_stabilizer_star_empty(); - test_filtered_stabilizer_star_with_stab(); - test_filtered_stabilizer_star_filtered(); - test_extract_cycle_history_basic(); - test_extract_cycle_history_null_ancestor(); test_bfs_empty_none(); test_bfs_nonempty_full(); test_bfs_nonempty_to_re(); @@ -832,13 +467,8 @@ void tst_seq_regex() { test_bfs_empty_complement_full(); // New tests for regex membership completion test_char_set_is_subset(); - test_stabilizer_store_basic(); - test_self_stabilizing(); test_check_intersection_sat(); test_check_intersection_unsat(); - test_is_language_subset_true(); - test_is_language_subset_false(); - test_is_language_subset_trivial(); test_some_seq_in_re_excluded_low_regression(); test_some_seq_in_re_inter_loop_regression(); // test_bfs_null_safety has a pre-existing failure, run it last diff --git a/src/util/zstring.h b/src/util/zstring.h index 0cf982874b..18dd66b3f2 100644 --- a/src/util/zstring.h +++ b/src/util/zstring.h @@ -96,7 +96,6 @@ public: }; // half-open character interval [lo, hi) -// mirrors ZIPT's CharacterRange struct char_range { unsigned m_lo; unsigned m_hi; // exclusive @@ -117,7 +116,6 @@ struct char_range { }; // sorted list of non-overlapping character intervals -// mirrors ZIPT's CharacterSet class char_set { svector m_ranges; public: