From 79cdc91a75958369d5a3724deff962f107fed3d6 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Sun, 28 Jun 2026 14:14:52 +0200 Subject: [PATCH] Explicit formula for length computation of regexes --- src/params/smt_params.cpp | 2 + src/params/smt_params.h | 1 + src/params/smt_params_helper.pyg | 1 + src/smt/seq/seq_nielsen.cpp | 97 ++++++++++++------- src/smt/seq/seq_nielsen.h | 12 ++- src/smt/seq/seq_parikh.cpp | 161 ++++++++++++++++++++++++++++++- src/smt/seq/seq_parikh.h | 55 +++++++++++ src/smt/theory_nseq.cpp | 8 +- 8 files changed, 288 insertions(+), 49 deletions(-) diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index 597a253f26..ce07ade25a 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -60,6 +60,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_nseq_regex_precheck = p.nseq_regex_precheck(); m_nseq_regex_factorization_threshold = p.nseq_regex_factorization_threshold(); m_nseq_regex_factorization_eager = p.nseq_regex_factorization_eager(); + m_nseq_regex_dynamic_decomposition = p.nseq_regex_dynamic_decomposition(); m_nseq_signature = p.nseq_signature(); m_nseq_axiomatize_diseq = p.nseq_axiomatize_diseq(); m_nseq_eager = p.nseq_eager(); @@ -178,6 +179,7 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nseq_regex_precheck); DISPLAY_PARAM(m_nseq_regex_factorization_threshold); DISPLAY_PARAM(m_nseq_regex_factorization_eager); + DISPLAY_PARAM(m_nseq_regex_dynamic_decomposition); DISPLAY_PARAM(m_nseq_axiomatize_diseq); DISPLAY_PARAM(m_profile_res_sub); diff --git a/src/params/smt_params.h b/src/params/smt_params.h index 729d502962..326a9a80a5 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -255,6 +255,7 @@ struct smt_params : public preprocessor_params, bool m_nseq_regex_precheck = true; unsigned m_nseq_regex_factorization_threshold = 1; bool m_nseq_regex_factorization_eager = false; + bool m_nseq_regex_dynamic_decomposition = true; bool m_nseq_signature = false; bool m_nseq_axiomatize_diseq = false; bool m_nseq_eager = true; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index d64c946ffb..d0a67b0ea6 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -139,6 +139,7 @@ def_module_params(module_name='smt', ('nseq.regex_precheck', BOOL, True, 'enable regex membership pre-check before DFS in theory_nseq: checks intersection emptiness per-variable and short-circuits SAT/UNSAT for regex-only problems'), ('nseq.regex_factorization_threshold', UINT, 1, 'maximum number of cases to factor a classical regex into in a single step (gives completeness on classical regexes)'), ('nseq.regex_factorization_eager', BOOL, False, 'apply regex factorization (sigma splitting) eagerly in the theory interface (propagate_pos_mem) instead of lazily inside the Nielsen graph'), + ('nseq.regex_dynamic_decomposition', BOOL, True, 'decompose cyles detected by unwinding regexes'), ('nseq.signature', BOOL, False, 'enable heuristic signature-based string equation splitting in Nielsen solver'), ('nseq.axiomatize_diseq', BOOL, False, 'eagerly axiomatize sequence disequalities'), ('nseq.eager', BOOL, True, 'enable the incremental eager structural Nielsen closure during propagation, detecting conflicts before final_check'), diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 6faf0f1aed..106f1a8f64 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -271,11 +271,12 @@ namespace seq { } bool str_mem::is_trivial(nielsen_node const* n) const { - if (!(m_str && m_regex)) - return false; + SASSERT(m_str && m_regex); if (m_kind == mem_kind::no_loop) // guard: discharged ⇒ Σ* (accepts all); ε has no non-empty lap-prefix. return m_discharged || m_str->is_empty(); + if (m_regex->is_full_seq()) + return true; if (!m_str->is_empty()) return false; if (m_kind == mem_kind::stab_view) @@ -362,17 +363,29 @@ namespace seq { SASSERT(m_constraints.size() == parent.m_constraints.size()); } - void nielsen_node::add_str_eq(str_eq const& eq) { + void nielsen_node::add_str_eq(str_eq& eq) { SASSERT(eq.m_lhs != nullptr); SASSERT(eq.m_rhs != nullptr); if (eq.is_trivial()) return; + eq.sort(); + // check if root node contains this equation already + if (std::ranges::any_of(str_eqs(), + [&](const str_eq &e) { return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs; })) + // already present, no need to add again + return; m_str_eq.push_back(eq); } - void nielsen_node::add_str_deq(str_deq const& deq) { + void nielsen_node::add_str_deq(str_deq& deq) { SASSERT(deq.m_lhs != nullptr); SASSERT(deq.m_rhs != nullptr); + deq.sort(); + // check if root node contains this equation already + if (std::ranges::any_of(str_deqs(), + [&](const str_deq &e) { return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs; })) + // already present, no need to add again + return; m_str_deq.push_back(deq); } @@ -381,6 +394,11 @@ namespace seq { SASSERT(mem.m_regex != nullptr); if (mem.is_trivial(this)) return; + // check if root node contains this membership constraint already + if (std::ranges::any_of(str_mems(), + [&](const str_mem &e) { return e.m_regex == mem.m_regex && e.m_str == mem.m_str; })) + // already present, no need to add again + return; m_str_mem.push_back(mem); } @@ -391,10 +409,12 @@ namespace seq { return true; if (!m_graph.m_context_solver.lower_bound(e, lo, lits, eqs)) return false; - for (auto lit : lits) + for (auto lit : lits) { dep = m_graph.dep_mgr().mk_join(dep, m_graph.dep_mgr().mk_leaf(lit)); - for (auto eq : eqs) + } + for (auto eq : eqs) { dep = m_graph.dep_mgr().mk_join(dep, m_graph.dep_mgr().mk_leaf(eq)); + } const expr_ref lo_expr(m_graph.a.mk_int(lo), m_graph.m); m_graph.add_le_dependency(dep, this, lo_expr, e); @@ -549,7 +569,7 @@ namespace seq { reset(); } - bool nielsen_graph::projection_state_in_Q(expr *state, unsigned nu) { + bool nielsen_graph::projection_state_in_Q(expr* state, unsigned nu) { if (!state || nu == 0) return false; const unsigned sid = state->get_id(); @@ -572,26 +592,26 @@ namespace seq { return incident(m_partial_dfa_out) || incident(m_partial_dfa_in); } - nielsen_node *nielsen_graph::mk_node() { + nielsen_node* nielsen_graph::mk_node() { const unsigned id = m_nodes.size(); - nielsen_node *n = alloc(nielsen_node, *this, id); + nielsen_node* n = alloc(nielsen_node, *this, id); m_nodes.push_back(n); SASSERT(n->id() == m_nodes.size() - 1); return n; } - nielsen_node *nielsen_graph::mk_child(nielsen_node *parent) { + nielsen_node* nielsen_graph::mk_child(nielsen_node* parent) { nielsen_node *child = mk_node(); child->clone_from(*parent); child->m_parent_ic_count = parent->constraints().size(); return child; } - nielsen_edge *nielsen_graph::mk_edge(nielsen_node *src, nielsen_node *tgt, const char *rule, + nielsen_edge *nielsen_graph::mk_edge(nielsen_node* src, nielsen_node* tgt, const char* rule, const bool is_progress) { SASSERT(src != nullptr); SASSERT(tgt != nullptr); - nielsen_edge *e = alloc(nielsen_edge, src, tgt, rule, is_progress); + nielsen_edge* e = alloc(nielsen_edge, src, tgt, rule, is_progress); m_edges.push_back(e); src->add_outgoing(e); return e; @@ -600,53 +620,38 @@ namespace seq { void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs, smt::enode *l, smt::enode *r) const { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r)); str_eq eq(lhs, rhs, dep); - eq.sort(); - // check if root node contains this equation already - if (std::ranges::any_of(m_root->str_eqs(), - [&](const str_eq &e) { return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs; })) - // already present, no need to add again - return; m_root->add_str_eq(eq); } void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs, sat::literal l) const { const dep_tracker dep = m_dep_mgr.mk_leaf(l); str_deq deq(lhs, rhs, dep); - // check if root node contains this equation already - if (std::ranges::any_of(m_root->str_deqs(), - [&](const str_deq &e) { return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs; })) - // already present, no need to add again - return; m_root->add_str_deq(deq); } void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex, sat::literal l) const { - // check if root node contains this membership constraint already - if (std::ranges::any_of(m_root->str_mems(), - [&](const str_mem &e) { return e.m_regex == regex && e.m_str == str; })) - // already present, no need to add again - return; const dep_tracker dep = m_dep_mgr.mk_leaf(l); m_root->add_str_mem(str_mem(str, regex, dep)); } // test-friendly overloads (no external dependency tracking) - void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs) { + void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs) const { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); str_eq eq(lhs, rhs, dep); eq.sort(); m_root->add_str_eq(eq); } - void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs) { + void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs) const { const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); str_deq deq(lhs, rhs, dep); m_root->add_str_deq(deq); } - void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex) { + void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex) const { const dep_tracker dep = nullptr; - m_root->add_str_mem(str_mem(str, regex, dep)); + str_mem mem(str, regex, dep); + m_root->add_str_mem(mem); } void nielsen_graph::reset() { @@ -2019,14 +2024,15 @@ namespace seq { dep_tracker dep = m_dep_mgr.mk_leaf(lit); lhs = eager_rewrite(lhs, dep); rhs = eager_rewrite(rhs, dep); - m_eager_leaf->add_str_deq(str_deq(lhs, rhs, dep)); + str_deq deq(lhs, rhs, dep); + m_eager_leaf->add_str_deq(deq); } void nielsen_graph::eager_add_str_mem(euf::snode const* str, euf::snode const* regex, sat::literal lit) { SASSERT(m_eager_active && m_eager_leaf); dep_tracker dep = m_dep_mgr.mk_leaf(lit); str = eager_rewrite(str, dep); - regex = eager_rewrite(regex, dep); // no-op for ground regexes, mirrors apply_subst + regex = eager_rewrite(regex, dep); m_eager_leaf->add_str_mem(str_mem(str, regex, dep)); } @@ -2199,7 +2205,7 @@ namespace seq { return search_result::unknown; #ifdef Z3DEBUG - if (m_stats.m_num_dfs_nodes % 50 == 0) { + if (m_stats.m_num_dfs_nodes % 20 == 0) { std::string dot = to_dot(); std::cout << ""; } @@ -3637,6 +3643,8 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_cycle_subsumption(nielsen_node* node) { + if (!m_regex_dynamic_decomposition) + return false; for (unsigned mi = 0; mi < node->str_mems().size(); ++mi) { str_mem const& mem = node->str_mems()[mi]; SASSERT(mem.well_formed()); @@ -3707,6 +3715,8 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_cycle_decomposition(nielsen_node* node) { + if (!m_regex_dynamic_decomposition) + return false; // Look for a str_mem with a variable-headed string for (unsigned mi = 0; mi < node->str_mems().size(); ++mi) { str_mem const& mem = node->str_mems()[mi]; @@ -4663,8 +4673,8 @@ namespace seq { const expr_ref vp_len(compute_length_expr(vp), m); euf::snode const* wau = dir_concat(m_sg, dir_concat(m_sg, w, a, true), up, true); euf::snode const* wbv = dir_concat(m_sg, dir_concat(m_sg, w, b, true), vp, true); - const str_eq u_eq(u, wau, first.m_dep); - const str_eq v_eq(v, wbv, first.m_dep); + str_eq u_eq(u, wau, first.m_dep); + str_eq v_eq(v, wbv, first.m_dep); // Branch 1: |u| < |v| { @@ -4835,6 +4845,19 @@ namespace seq { TRACE(seq, tout << "Parikh " << mk_pp(mem.m_regex->get_expr(), m) << " bound: " << bound << "\n"); constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, false, m)); } + + // Exact semi-linear length set (visit-count Parikh) for classical + // regexes; captures unions/strides precisely, unlike the coarse + // interval above (which we keep alongside - we might want to delete it eventually) + if (mem.is_plain() && mem.m_regex->is_classical()) { + vector exact; + if (m_parikh->encode_length_set(mem.m_str->get_expr(), mem.m_regex->get_expr(), len_str, mem.m_dep, exact)) { + for (auto const& c : exact) { + TRACE(seq, tout << "semilinear " << mk_pp(mem.m_regex->get_expr(), m) << ": " << c.fml << "\n"); + constraints.push_back(length_constraint(c.fml, c.dep, length_kind::bound, false, m)); + } + } + } } } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index ebc05d682e..95d3276da5 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -543,8 +543,8 @@ namespace seq { vector const& str_mems() const { return m_str_mem; } vector& str_mems() { return m_str_mem; } - void add_str_eq(str_eq const& eq); - void add_str_deq(str_deq const& deq); + void add_str_eq(str_eq& eq); + void add_str_deq(str_deq& deq); void add_str_mem(str_mem const& mem); void add_constraint(constraint const &ic); @@ -775,6 +775,7 @@ namespace seq { bool m_signature_split = false; unsigned m_regex_factorization_threshold = 1; bool m_regex_factorization_eager = false; + bool m_regex_dynamic_decomposition = true; unsigned m_fresh_cnt = 0; nielsen_stats m_stats; @@ -922,9 +923,9 @@ namespace seq { void add_str_mem(euf::snode const* str, euf::snode const* regex, sat::literal l) const; // test-friendly overloads (no external dependency tracking) - void add_str_eq(euf::snode const* lhs, euf::snode const* rhs); - void add_str_deq(euf::snode const* lhs, euf::snode const* rhs); - void add_str_mem(euf::snode const* str, euf::snode const* regex); + void add_str_eq(euf::snode const* lhs, euf::snode const* rhs) const; + void add_str_deq(euf::snode const* lhs, euf::snode const* rhs) const; + void add_str_mem(euf::snode const* str, euf::snode const* regex) const; // access all nodes ptr_vector const& nodes() const { return m_nodes; } @@ -943,6 +944,7 @@ namespace seq { void set_regex_factorization_threshold(unsigned max) { m_regex_factorization_threshold = max; } void set_regex_factorization_eager(bool e) { m_regex_factorization_eager = e; } + void set_regex_dynamic_decomposition(bool e) { m_regex_dynamic_decomposition = e; } // display for debugging std::ostream& display(std::ostream& out) const; diff --git a/src/smt/seq/seq_parikh.cpp b/src/smt/seq/seq_parikh.cpp index 383d82180e..fc967cf2f8 100644 --- a/src/smt/seq/seq_parikh.cpp +++ b/src/smt/seq/seq_parikh.cpp @@ -25,12 +25,13 @@ Author: #include "smt/seq/seq_parikh.h" #include "util/mpz.h" +#include "util/zstring.h" #include namespace seq { seq_parikh::seq_parikh(euf::sgraph& sg) - : m(sg.get_manager()), seq(m), a(m), m_fresh_cnt(0) {} + : m(sg.get_manager()), seq(m), a(m), m_rw(m), m_sk(m, m_rw), m_fresh_cnt(0) {} expr_ref seq_parikh::mk_fresh_int_var() { std::string name = "pk!" + std::to_string(m_fresh_cnt++); @@ -168,6 +169,150 @@ namespace seq { return 1; } + // ----------------------------------------------------------------------- + // Exact semi-linear length encoding (visit-count Parikh) + // ----------------------------------------------------------------------- + + expr_ref seq_parikh::mk_count_var(vector& out, dep_tracker dep, + expr* str_key, expr* root_re, unsigned& idx) { + // Deterministic Skolem term keyed on the membership + a per-encoding DFS + // index: re-encoding the same membership reuses the same counters. + expr_ref c = m_sk.mk("seq.rc", str_key, root_re, a.mk_int(idx++), a.mk_int()); + out.push_back(constraint(a.mk_ge(c, a.mk_int(0)), dep, m)); + return c; + } + + void seq_parikh::push_zero_guard(vector& out, dep_tracker dep, expr* count, expr* c1) { + // count = 0 -> c1 = 0 (an unentered subterm produces nothing) + expr_ref guard(m.mk_implies(m.mk_eq(count, a.mk_int(0)), + m.mk_eq(c1, a.mk_int(0))), m); + m_rw(guard); + if (m.is_false(guard)) + return; + out.push_back(constraint(guard, dep, m)); + } + + bool seq_parikh::rec(expr* re, expr* count, expr* str_key, expr* root_re, unsigned& idx, + dep_tracker dep, vector& out, expr_ref& contrib) { + SASSERT(re); + contrib = expr_ref(a.mk_int(0), m); + + expr* r1 = nullptr, *r2 = nullptr, *s = nullptr; + unsigned lo = 0, hi = 0; + + // ∅: this subterm can never be visited. + if (seq.re.is_empty(re)) { + out.push_back(constraint(m.mk_eq(count, a.mk_int(0)), dep, m)); + return true; + } + + // ε: contributes no length. + if (seq.re.is_epsilon(re)) + return true; + + // single character (range / allchar): one char per visit. + if (seq.re.is_range(re) || seq.re.is_full_char(re)) { + contrib = expr_ref(count, m); + return true; + } + + // to_re("w"): fixed-length literal → n chars per visit. + if (seq.re.is_to_re(re, s)) { + zstring zs; + if (!seq.str.is_string(s, zs)) + return false; // symbolic to_re: not a classical length leaf + unsigned n = zs.length(); + if (n != 0) + contrib = expr_ref(a.mk_mul(a.mk_int(n), count), m); + return true; + } + + // Σ* (full_seq, incl. allchar*): any number of chars; gated by reachability. + // NB: checked before is_star so star(allchar) is treated as Σ*. + if (seq.re.is_full_seq(re)) { + expr_ref c1 = mk_count_var(out, dep, str_key, root_re, idx); + push_zero_guard(out, dep, count, c1); + contrib = c1; + return true; + } + + // concat(r1, r2): both children visited exactly `count` times; lengths add. + if (seq.re.is_concat(re, r1, r2)) { + expr_ref l1(m), l2(m); + if (!rec(r1, count, str_key, root_re, idx, dep, out, l1)) return false; + if (!rec(r2, count, str_key, root_re, idx, dep, out, l2)) return false; + contrib = expr_ref(a.mk_add(l1, l2), m); + return true; + } + + // union(r1, r2): each visit goes to exactly one branch: count = c1 + c2. + if (seq.re.is_union(re, r1, r2)) { + expr_ref c1 = mk_count_var(out, dep, str_key, root_re, idx); + expr_ref c2 = mk_count_var(out, dep, str_key, root_re, idx); + out.push_back(constraint(m.mk_eq(count, a.mk_add(c1, c2)), dep, m)); + expr_ref l1(m), l2(m); + if (!rec(r1, c1, str_key, root_re, idx, dep, out, l1)) return false; + if (!rec(r2, c2, str_key, root_re, idx, dep, out, l2)) return false; + contrib = expr_ref(a.mk_add(l1, l2), m); + return true; + } + + // star(r1): body visited c1 >= 0 times total; reachability guard. + if (seq.re.is_star(re, r1)) { + expr_ref c1 = mk_count_var(out, dep, str_key, root_re, idx); + push_zero_guard(out, dep, count, c1); + return rec(r1, c1, str_key, root_re, idx, dep, out, contrib); + } + + // plus(r1): >= 1 iteration per visit → c1 >= count; plus reachability guard. + if (seq.re.is_plus(re, r1)) { + expr_ref c1 = mk_count_var(out, dep, str_key, root_re, idx); + out.push_back(constraint(a.mk_ge(c1, count), dep, m)); + push_zero_guard(out, dep, count, c1); + return rec(r1, c1, str_key, root_re, idx, dep, out, contrib); + } + + // opt(r1): 0 or 1 iteration per visit → c1 <= count (and c1 >= 0). + if (seq.re.is_opt(re, r1)) { + expr_ref c1 = mk_count_var(out, dep, str_key, root_re, idx); + out.push_back(constraint(a.mk_le(c1, count), dep, m)); + return rec(r1, c1, str_key, root_re, idx, dep, out, contrib); + } + + // loop(r1, lo, hi): between lo and hi iterations per visit. + if (seq.re.is_loop(re, r1, lo, hi)) { + expr_ref c1 = mk_count_var(out, dep, str_key, root_re, idx); + out.push_back(constraint(a.mk_ge(c1, a.mk_mul(a.mk_int(lo), count)), dep, m)); + out.push_back(constraint(a.mk_le(c1, a.mk_mul(a.mk_int(hi), count)), dep, m)); + return rec(r1, c1, str_key, root_re, idx, dep, out, contrib); + } + // loop(r1, lo): at least lo iterations per visit, unbounded above. + if (seq.re.is_loop(re, r1, lo)) { + expr_ref c1 = mk_count_var(out, dep, str_key, root_re, idx); + out.push_back(constraint(a.mk_ge(c1, a.mk_mul(a.mk_int(lo), count)), dep, m)); + push_zero_guard(out, dep, count, c1); + return rec(r1, c1, str_key, root_re, idx, dep, out, contrib); + } + + // intersection / complement / diff / xor / of_pred / reverse / derivative / + // antimirov-union / anything else: the visit-count flow does not capture + // these exactly — bail so the caller keeps the coarse fallback. + return false; + } + + bool seq_parikh::encode_length_set(expr* str_key, expr* re, expr* len_target, dep_tracker dep, vector& out) { + SASSERT(str_key && re && len_target && seq.is_re(re)); + unsigned before = out.size(); + unsigned idx = 0; + expr_ref contrib(m); + if (!rec(re, a.mk_int(1), str_key, re, idx, dep, out, contrib)) { + out.shrink(before); // discard any partial constraints on bail + return false; + } + out.push_back(constraint(m.mk_eq(len_target, contrib), dep, m)); + return true; + } + // ----------------------------------------------------------------------- // Constraint generation // ----------------------------------------------------------------------- @@ -232,8 +377,20 @@ namespace seq { void seq_parikh::apply_to_node(nielsen_node& node) { vector constraints; - for (str_mem const& mem : node.str_mems()) + for (str_mem const& mem : node.str_mems()) { generate_parikh_constraints(mem, constraints); + + // Exact semi-linear length encoding for classical regex states. + // Only plain memberships: view/guard kinds carry projection run + // states, not plain regexes. is_classical() pre-filters extended + // ops (∩, complement, …); encode_length_set self-bails on anything + // else (e.g. symbolic to_re) it cannot encode exactly. + if (mem.is_plain() && mem.m_str && mem.m_regex && mem.m_regex->is_classical() + && seq.is_re(mem.m_regex->get_expr())) { + expr_ref len_str(seq.str.mk_length(mem.m_str->get_expr()), m); + encode_length_set(mem.m_str->get_expr(), mem.m_regex->get_expr(), len_str, mem.m_dep, constraints); + } + } for (auto& ic : constraints) node.add_constraint(ic); } diff --git a/src/smt/seq/seq_parikh.h b/src/smt/seq/seq_parikh.h index 7b78bc90a8..4704996fd0 100644 --- a/src/smt/seq/seq_parikh.h +++ b/src/smt/seq/seq_parikh.h @@ -43,6 +43,8 @@ Author: #include "ast/arith_decl_plugin.h" #include "ast/seq_decl_plugin.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/rewriter/seq_skolem.h" #include "smt/seq/seq_nielsen.h" namespace seq { @@ -63,6 +65,8 @@ namespace seq { ast_manager& m; seq_util seq; arith_util a; + th_rewriter m_rw; + skolem m_sk; // for deterministic, reusable visit-count vars unsigned m_fresh_cnt; // counter for fresh variable names // Compute the stride (period) of the length language of a regex. @@ -86,6 +90,34 @@ namespace seq { // Parikh multiplier variable k in len(str) = min_len + stride·k. expr_ref mk_fresh_int_var(); + // --- exact semi-linear length encoding (visit-count Parikh) --------- + // Recursively encode the length set of a NON-EXTENDED (classical) regex + // by introducing, per subterm, an integer "visit-count" variable and + // Presburger flow constraints (paper "On the Complexity of Equational + // Horn Clauses", Verma/Seidl/Schwentick). `count` is the count expr of + // the current subterm; on success pushes the subterm's structural + // constraints into `out` and returns its linear length contribution in + // `contrib`. Returns false (caller discards) for any operator the flow + // cannot capture exactly (intersection, complement, diff, xor, of_pred, + // reverse, derivative, …). + // + // Count variables are NOT fresh constants — they are Skolem terms + // seq.rc(str_key, root_re, idx) + // keyed on the membership (str + root regex) and a per-encoding DFS index + // `idx`. Re-encoding the same membership therefore reuses the exact same + // counters instead of leaking new constants on every final_check / node. + bool rec(expr* re, expr* count, expr* str_key, expr* root_re, unsigned& idx, + dep_tracker dep, vector& out, expr_ref& contrib); + + // Deterministic non-negative integer count variable + // seq.rc(str_key, root_re, idx++) + // emits c >= 0 into out and bumps idx. + expr_ref mk_count_var(vector& out, dep_tracker dep, + expr* str_key, expr* root_re, unsigned& idx); + + // Emit the reachability guard count = 0 -> c1 = 0. + void push_zero_guard(vector& out, dep_tracker dep, expr* count, expr* c1); + public: explicit seq_parikh(euf::sgraph& sg); @@ -127,6 +159,29 @@ namespace seq { // Exposed for testing and external callers. unsigned get_length_stride(expr* re) { return compute_length_stride(re); } + // Exact semi-linear length encoding for a regex membership. + // + // For a NON-EXTENDED (classical) regex R, encodes the *exact* set + // { |w| : w ∈ L(R) } + // as an existential Presburger formula over fresh visit-count variables, + // asserting len_target = Σ (char-leaf counts) together with the + // per-subterm flow constraints (concat: equal child counts; union: + // count = c1 + c2; star/plus/loop: bounded body count with the + // reachability guard count=0 → body=0). This is linear in |R| and, + // unlike the single gcd `stride`, does not collapse on unions — e.g. + // (aa)*|(aaa)* yields len = 2·c1 + 3·c2 with c1+c2 the active branch, + // i.e. exactly {2k} ∪ {3k}. + // + // Returns true and appends the encoding (all carrying `dep`) to `out` + // when R is classical; returns false (leaving `out` unchanged) for + // extended regexes (intersection / complement / diff / of_pred / …), + // in which case the caller keeps the coarse interval/stride fallback. + // + // `str_key` identifies the membership's string term (mem.m_str): together + // with `re` it keys the reusable Skolem count variables, so re-encoding + // the same membership does not allocate new counters. + bool encode_length_set(expr* str_key, expr* re, expr* len_target, dep_tracker dep, vector& out); + // Convert a regex minterm expression to a char_set. // // A minterm is a Boolean combination of character-class predicates diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 96263acf77..117e7cf48d 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -496,8 +496,7 @@ namespace smt { // Eager structural pruning: once the queue is drained, run a cheap // branch-free Nielsen closure over the currently-asserted constraints to - // surface structural conflicts long before final_check. Sound because - // the current set is a subset of any completion (see eager_structural_check). + // surface structural conflicts long before final_check if (!ctx.inconsistent()) eager_structural_check(); } @@ -552,13 +551,13 @@ namespace smt { auto const& mem = std::get(item); int triv = m_regex.check_trivial(mem); if (triv > 0) - continue; // trivially satisfied + continue; if (triv < 0) { m_nielsen.eager_add_str_mem(mem.m_str, mem.m_regex, mem.lit); continue; } if (m_ignored_mem.contains(mem.lit)) - continue; // already handled via Boolean closure + continue; vector processed; if (!m_regex.process_str_mem(mem, processed)) { m_nielsen.eager_add_str_mem(mem.m_str, mem.m_regex, mem.lit); @@ -567,7 +566,6 @@ namespace smt { for (auto const& pm : processed) m_nielsen.eager_add_str_mem(pm.m_str, pm.m_regex, mem.lit); } - // axiom_item: not Nielsen-relevant, skip } const auto r = m_nielsen.eager_close();