From 3baad0f171143f536e884ebd9216d353de2789be Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 17 Jul 2026 15:59:28 +0200 Subject: [PATCH] Fine & Wilf-based elimination of power-vs-power case (disabled by default for now) --- 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 | 383 +++++++++++++++++++- src/smt/seq/seq_nielsen.h | 47 ++- src/smt/theory_nseq.cpp | 1 + src/test/CMakeLists.txt | 3 + src/test/main.cpp | 3 + src/test/nseq_basic.cpp | 99 +++++- src/test/seq_nielsen.cpp | 585 +++++++++++++++++++++++-------- 10 files changed, 961 insertions(+), 164 deletions(-) diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index 40b2c9ef14..4f8fceb1b1 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -64,6 +64,7 @@ void smt_params::updt_local_params(params_ref const & _p) { 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_fine_wilf = p.nseq_fine_wilf(); m_nseq_axiomatize_diseq = p.nseq_axiomatize_diseq(); m_nseq_eager = p.nseq_eager(); m_nseq_harvest = p.nseq_harvest(); @@ -184,6 +185,7 @@ void smt_params::display(std::ostream & out) const { 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_fine_wilf); DISPLAY_PARAM(m_nseq_axiomatize_diseq); DISPLAY_PARAM(m_nseq_harvest); diff --git a/src/params/smt_params.h b/src/params/smt_params.h index 8489d5ab8b..f95c04a5de 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -259,6 +259,7 @@ struct smt_params : public preprocessor_params, bool m_nseq_regex_factorization_eager = false; bool m_nseq_regex_dynamic_decomposition = true; bool m_nseq_signature = false; + bool m_nseq_fine_wilf = false; bool m_nseq_axiomatize_diseq = false; bool m_nseq_eager = true; unsigned m_nseq_harvest = 0; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 35df465026..27269d4e25 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -143,6 +143,7 @@ def_module_params(module_name='smt', ('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.fine_wilf', BOOL, False, 'enable Fine & Wilf overlap splitting for equations with different-base power heads in the Nielsen solver (breaks the divergent one-copy peel loop)'), ('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'), ('nseq.harvest', UINT, 0, 'benchmark-harvest mode: bound on non-progress Nielsen extension steps before dumping the current node as an .smt2 benchmark; 0 = disabled (normal sound reasoning). WARNING: intentionally unsound, for benchmark generation only'), diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 5e3e17c022..c3f9ad81ae 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -475,7 +475,9 @@ namespace seq { m_str_mem.reset(); m_constraints.reset(); m_char_ranges.reset(); + m_fw_applied.reset(); m_str_eq.append(parent.m_str_eq); + m_fw_applied.append(parent.m_fw_applied); m_str_deq.append(parent.m_str_deq); m_str_mem.append(parent.m_str_mem); m_constraints.append(parent.m_constraints); @@ -841,21 +843,31 @@ namespace seq { m_root->add_str_mem(str_mem(m, str, regex, dep)); } - // test-friendly overloads (no external dependency tracking) - void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs) const { + // test-friendly overloads (no external dependency tracking); create the + // root lazily — production callers use the enode/literal overloads after + // an explicit create_root() + void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs) { + if (!m_root) + create_root(); const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); const str_eq eq(m, lhs, rhs, dep); m_root->add_str_eq(eq); } - void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs) const { + void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs) { + if (!m_root) + create_root(); const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); const str_deq deq(m, lhs, rhs, dep); m_root->add_str_deq(deq); } - void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex) const { - const dep_tracker dep = nullptr; + void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex) { + if (!m_root) + create_root(); + // dummy leaf (like the eq/deq overloads): production invariants + // (e.g. check_regex_widening) assume memberships carry a dep + const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr)); const str_mem mem(m, str, regex, dep); m_root->add_str_mem(mem); } @@ -3628,6 +3640,13 @@ namespace seq { if (apply_split_power_elim(node)) return ++m_stats.m_mod_split_power_elim, true; + // Priority 3c: FineWilf - overlap split for a head power vs a + // different-base power behind a concrete-char prefix. Preempts + // ConstNumUnwinding's divergent one-copy peel loop on that shape. + // (opt-in via smt.nseq.fine_wilf, default off) + if (m_fine_wilf && apply_fine_wilf(node)) + return ++m_stats.m_mod_fine_wilf, true; + // Priority 4: ConstNumUnwinding - power vs constant: n=0 or peel if (apply_const_num_unwinding(node)) return ++m_stats.m_mod_const_num_unwinding, true; @@ -4050,6 +4069,359 @@ namespace seq { return false; } + // ----------------------------------------------------------------------- + // Helper: concrete string value of a ground token run (ε, char, or a + // concat of chars). Returns false on any non-concrete token. + // ----------------------------------------------------------------------- + + static bool ground_zstring(euf::snode const* s, seq_util& seq, zstring& out) { + out.reset(); + if (!s) + return false; + if (s->is_empty()) + return true; + euf::snode_vector toks; + s->collect_tokens(toks); + for (euf::snode const* t : toks) { + unsigned val; + if (!t->is_char()) + return false; + VERIFY(seq.is_const_char(to_app(t->get_expr())->get_arg(0), val)); + out += zstring(val); + } + return true; + } + + // ----------------------------------------------------------------------- + // Modifier: apply_fine_wilf + // For an equation U^n · V = Y · W^m · Z (up to direction / side swap) + // where U^n is the directional head of one side, Y a possibly-empty run + // of concrete chars and W^m the first power on the other side with a + // DIFFERENT base, split on the overlap length + // O = min(n·|U| − |Y|, m·|W|) + // against the Fine & Wilf threshold T = |U| + |W| (exact bound is + // T − gcd(|U|,|W|); dropping the gcd term is a sound weakening). + // The overlap word has periods |U| and |W|; O ≥ T forces (F&W) the + // |Y|-rotated conjugate of U and W to share a primitive root, so one of + // the powers can be eliminated. The three cases partition all models: + // Case 1 (O < T): one exponent is bounded. + // Case 2 (O ≥ T, LHS power ends first): U^n eliminated. + // Case 3 (O ≥ T, RHS power ends first): W^m eliminated. + // Ground bases (fast path): the conjugate/prefix conditions are decided + // concretely (failure prunes cases 2/3 — they are F&W-unsat), the cut + // position in the other base is enumerated, and case 1 unrolls the + // concretely-bounded exponent — every child is a progress edge. + // Symbolic bases: fresh cut variables axiomatize the alignment + // (U^n = Y·R1, W^m = R1·R2, V = R2·Z; both directions of the + // equivalence hold, no commutativity lemma needed) and case 1 is an + // arith-split child guarded against refire via m_fw_applied. + // Preempts apply_const_num_unwinding's divergent one-copy peel loop on + // different-base power vs power heads. + // ----------------------------------------------------------------------- + + bool nielsen_graph::apply_fine_wilf(nielsen_node* node) { + + // Per-modifier cap on ground enumeration fan-out; larger instances + // fall back to the symbolic encoding (still linear for ground bases). + static constexpr unsigned FW_ENUM_CAP = 64; + + for (unsigned eq_idx = 0; eq_idx < node->str_eqs().size(); ++eq_idx) { + str_eq const& eq = node->str_eqs()[eq_idx]; + if (eq.is_trivial()) + continue; + + for (unsigned od = 0; od < 2; ++od) { + const bool fwd = od == 0; + for (unsigned sd = 0; sd < 2; ++sd) { + euf::snode const* sideA = sd == 0 ? eq.m_lhs : eq.m_rhs; + euf::snode const* sideB = sd == 0 ? eq.m_rhs : eq.m_lhs; + + euf::snode const* upow = dir_token(sideA, fwd); + if (!upow || !upow->is_power() || upow->num_args() < 1) + continue; + + // other side: concrete-char run Y, then a power W^m + euf::snode_vector btoks; + collect_tokens_dir(sideB, fwd, btoks); + unsigned yi = 0; + while (yi < btoks.size() && btoks[yi]->is_char()) + ++yi; + if (yi >= btoks.size() || !btoks[yi]->is_power() || btoks[yi]->num_args() < 1) + continue; + euf::snode const* wpow = btoks[yi]; + // same base: NumCmp (priority 3) / simplify 3c–3e territory + if (wpow->arg0() == upow->arg0()) + continue; + + expr* exp_n = get_power_exponent(upow); + expr* exp_m = get_power_exponent(wpow); + expr* u_base_e = get_power_base_expr(upow, m_seq); + expr* w_base_e = get_power_base_expr(wpow, m_seq); + if (!exp_n || !exp_m || !u_base_e || !w_base_e) + continue; + + const uint64_t key = (uint64_t(eq.m_lhs->id()) << 33) | + (uint64_t(eq.m_rhs->id()) << 1) | (fwd ? 1 : 0); + if (node->fw_applied(key)) + continue; + + // Mirror-space values (direction folded away: for fwd=false + // all strings are reversed, so the overlap is again at the + // "front"; real snodes are rebuilt via dir_concat + reverse). + zstring u_s, w_s; + const bool u_ground = ground_zstring(upow->arg0(), m_seq, u_s); + const bool w_ground = ground_zstring(wpow->arg0(), m_seq, w_s); + // ε-base powers are degenerate (handled by the simplify + // passes / power epsilon) — not our pattern. + if ((u_ground && u_s.empty()) || (w_ground && w_s.empty())) + continue; + zstring mu = fwd ? u_s : u_s.reverse(); + zstring mw = fwd ? w_s : w_s.reverse(); + zstring my; + for (unsigned i = 0; i < yi; ++i) { + unsigned val; + VERIFY(m_seq.is_const_char(to_app(btoks[i]->get_expr())->get_arg(0), val)); + my += zstring(val); + } + const unsigned Ly = my.length(); + + // V = sideA minus the head power; Z = sideB after W^m + euf::snode const* v_sn = nullptr; + { + euf::snode_vector atoks; + collect_tokens_dir(sideA, fwd, atoks); + SASSERT(!atoks.empty() && atoks[0] == upow); + for (unsigned i = 1; i < atoks.size(); ++i) + v_sn = dir_concat(m_sg, v_sn, atoks[i], fwd); + } + if (!v_sn) + v_sn = m_sg.mk_empty_seq(sideA->get_sort()); + euf::snode const* z_sn = nullptr; + for (unsigned i = yi + 1; i < btoks.size(); ++i) + z_sn = dir_concat(m_sg, z_sn, btoks[i], fwd); + if (!z_sn) + z_sn = m_sg.mk_empty_seq(sideB->get_sort()); + euf::snode const* y_sn = nullptr; + for (unsigned i = 0; i < yi; ++i) + y_sn = dir_concat(m_sg, y_sn, btoks[i], fwd); + + const expr_ref len_upow = compute_length_expr(upow); // n·|U| + const expr_ref len_wpow = compute_length_expr(wpow); // m·|W| + const expr_ref zero(a.mk_int(0), m); + const dep_tracker dep = eq.m_dep; + + // Ground feasibility of cases 2/3 (both require O ≥ T, and + // by F&W then Y ≺ U^ω and rot(U, Ly mod |U|)·W = W·rot(...)). + // gen23=false ⟹ cases 2/3 are unsat and are not generated. + bool gen23 = true; + if (u_ground && w_ground) { + const unsigned Lu = mu.length(); + for (unsigned i = 0; i < Ly && gen23; ++i) + gen23 = my[i] == mu[i % Lu]; + if (gen23) { + const unsigned r = Ly % Lu; + const zstring rot = mu.extract(r, Lu - r) + mu.extract(0, r); + gen23 = (rot + mw) == (mw + rot); + } + } + + // Refire guard: the symbolic case-1 child keeps the equation + // verbatim; without the mark the identical split would be + // re-emitted below it forever (arith splits escape the + // loop-cut). Set before mk_child so children inherit it. + node->mark_fw_applied(key); + + const unsigned Lu = mu.length(), Lw = mw.length(); + const bool ground = u_ground && w_ground && + (Ly + Lu + Lw - 1) / Lu + (Lu + Lw - 1) / Lw + 2 + + (gen23 ? Lu + Lw : 0) <= FW_ENUM_CAP; + + if (ground) { + // ---- ground fast path: all children progress ---- + const unsigned N = (Ly + Lu + Lw - 1) / Lu; // max n: n·Lu < Ly+Lu+Lw + const unsigned M = (Lu + Lw - 1) / Lw; // max m: m·Lw < Lu+Lw + const auto unroll = [&](euf::snode const* base, sort* srt, unsigned c) { + euf::snode const* r = c == 0 ? m_sg.mk_empty_seq(srt) : base; + for (unsigned i = 1; i < c; ++i) + r = m_sg.mk_concat(r, base); + return r; + }; + + // Case 1a: n = 0..N (⟺ n·Lu − Ly < T), unroll U^n. + for (unsigned c = 0; c <= N; ++c) { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, "fine-wilf n", true); + const nielsen_subst s(upow, unroll(upow->arg0(), upow->get_sort(), c), dep); + e->add_subst(s); + child->apply_subst(m_sg, s); + e->add_side_constraint(mk_constraint(a.mk_eq(exp_n, a.mk_int(c)), dep)); + } + // Case 1b: m = 0..M (⟺ m·Lw < T) ∧ n > N (disjoint from 1a). + for (unsigned c = 0; c <= M; ++c) { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, "fine-wilf m", true); + const nielsen_subst s(wpow, unroll(wpow->arg0(), wpow->get_sort(), c), dep); + e->add_subst(s); + child->apply_subst(m_sg, s); + e->add_side_constraint(mk_constraint(a.mk_eq(exp_m, a.mk_int(c)), dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, a.mk_int(N + 1)), dep)); + } + if (gen23) { + // Case 2: U^n ends inside W^m — cut W at mirror-phase p: + // n·Lu = Ly + k·Lw + p. Remainder: V = Q'·W^(m−k−1)·Z + // (p = 0: V = W^(m−k)·Z, covering the k = m boundary). + const expr_ref k_e = m_sk.mk("fw.k", eq.m_lhs->get_expr(), eq.m_rhs->get_expr(), + a.mk_int(fwd ? 1 : 0), a.mk_int()); + for (unsigned p = 0; p < Lw; ++p) { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, "fine-wilf elim L", true); + expr_ref rem_exp(p == 0 ? a.mk_sub(exp_m, k_e) + : a.mk_sub(exp_m, a.mk_add(k_e, a.mk_int(1))), m); + rem_exp = normalize_arith(m_rw, rem_exp); + euf::snode const* pow_sn = m_sg.mk(expr_ref(m_seq.str.mk_power(w_base_e, rem_exp), m)); + euf::snode const* rhs_new = dir_concat(m_sg, pow_sn, z_sn, fwd); + if (p > 0) { + const zstring q_m = mw.extract(p, Lw - p); + euf::snode const* qp_sn = m_sg.mk(m_seq.str.mk_string(fwd ? q_m : q_m.reverse())); + rhs_new = dir_concat(m_sg, qp_sn, rhs_new, fwd); + } + auto& eqs = child->str_eqs(); + eqs[eq_idx] = eqs.back(); + eqs.pop_back(); + eqs.push_back(str_eq(m, v_sn, rhs_new, dep)); + // n·Lu = Ly + k·Lw + p + e->add_side_constraint(mk_constraint(a.mk_eq(len_upow, + a.mk_add(a.mk_int(Ly + p), a.mk_mul(a.mk_int(Lw), k_e))), dep)); + // overlap ≥ T (disjoint from case 1) + e->add_side_constraint(mk_constraint( + a.mk_ge(len_upow, a.mk_int(Ly + Lu + Lw)), dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(k_e, zero), dep)); + e->add_side_constraint(mk_constraint( + a.mk_ge(exp_m, p == 0 ? k_e.get() : a.mk_add(k_e, a.mk_int(1))), dep)); + } + // Case 3: W^m ends strictly inside U^n — cut U at + // mirror-phase p: Ly + m·Lw = k·Lu + p. Remainder: + // Q''·U^(n−k−1)·V = Z (p = 0: U^(n−k)·V = Z). + const expr_ref k2_e = m_sk.mk("fw.k2", eq.m_lhs->get_expr(), eq.m_rhs->get_expr(), + a.mk_int(fwd ? 1 : 0), a.mk_int()); + for (unsigned p = 0; p < Lu; ++p) { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, "fine-wilf elim R", true); + expr_ref rem_exp(p == 0 ? a.mk_sub(exp_n, k2_e) + : a.mk_sub(exp_n, a.mk_add(k2_e, a.mk_int(1))), m); + rem_exp = normalize_arith(m_rw, rem_exp); + euf::snode const* pow_sn = m_sg.mk(expr_ref(m_seq.str.mk_power(u_base_e, rem_exp), m)); + euf::snode const* lhs_new = dir_concat(m_sg, pow_sn, v_sn, fwd); + if (p > 0) { + const zstring q_m = mu.extract(p, Lu - p); + euf::snode const* qq_sn = m_sg.mk(m_seq.str.mk_string(fwd ? q_m : q_m.reverse())); + lhs_new = dir_concat(m_sg, qq_sn, lhs_new, fwd); + } + auto& eqs = child->str_eqs(); + eqs[eq_idx] = eqs.back(); + eqs.pop_back(); + eqs.push_back(str_eq(m, lhs_new, z_sn, dep)); + // Ly + m·Lw = k·Lu + p + e->add_side_constraint(mk_constraint( + a.mk_eq(a.mk_add(a.mk_int(Ly), len_wpow), + a.mk_add(a.mk_int(p), a.mk_mul(a.mk_int(Lu), k2_e))), dep)); + // overlap ≥ T (disjoint from case 1) + e->add_side_constraint(mk_constraint( + a.mk_ge(len_wpow, a.mk_int(Lu + Lw)), dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(k2_e, zero), dep)); + // strict: W^m ends before U^n does + e->add_side_constraint(mk_constraint( + a.mk_ge(exp_n, a.mk_add(k2_e, a.mk_int(1))), dep)); + } + } + return true; + } + + // ---- symbolic path ---- + const expr_ref lu_e = compute_length_expr(upow->arg0()); + const expr_ref lw_e = compute_length_expr(wpow->arg0()); + const expr_ref t_e(a.mk_add(lu_e, lw_e), m); + const expr_ref ly_e(a.mk_int(Ly), m); + + // Case 1: small overlap — string constraints kept verbatim, + // only the (possibly nonlinear) bound is added. + { + nielsen_node* child = mk_child(node); + child->set_arith_split(); + nielsen_edge* e = mk_edge(node, child, "fine-wilf small", true); + e->add_side_constraint(mk_constraint( + m.mk_or(a.mk_lt(a.mk_sub(len_upow, ly_e), t_e), + a.mk_lt(len_wpow, t_e)), dep)); + } + if (gen23) { + // Case 2: U^n ends inside W^m. Fresh cuts R1 (overlap + // beyond Y) and R2 (rest of W^m): + // U^n = Y·R1, W^m = R1·R2, V = R2·Z. + { + const expr_ref r1_e = m_sk.mk("fw.r1", eq.m_lhs->get_expr(), eq.m_rhs->get_expr(), + a.mk_int(fwd ? 1 : 0), sideA->get_sort()); + const expr_ref r2_e = m_sk.mk("fw.r2", eq.m_lhs->get_expr(), eq.m_rhs->get_expr(), + a.mk_int(fwd ? 1 : 0), sideA->get_sort()); + euf::snode const* r1_sn = m_sg.mk(r1_e); + euf::snode const* r2_sn = m_sg.mk(r2_e); + const expr_ref len_r1(m_seq.str.mk_length(r1_e), m); + const expr_ref len_r2(m_seq.str.mk_length(r2_e), m); + + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, "fine-wilf elim L", false); + auto& eqs = child->str_eqs(); + eqs[eq_idx] = eqs.back(); + eqs.pop_back(); + eqs.push_back(str_eq(m, upow, dir_concat(m_sg, y_sn, r1_sn, fwd), dep)); + eqs.push_back(str_eq(m, wpow, dir_concat(m_sg, r1_sn, r2_sn, fwd), dep)); + eqs.push_back(str_eq(m, v_sn, dir_concat(m_sg, r2_sn, z_sn, fwd), dep)); + // |R1| = n·|U| − Ly and the F&W threshold + e->add_side_constraint(mk_constraint( + a.mk_eq(a.mk_add(ly_e, len_r1), len_upow), dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(len_r1, t_e), dep)); + // |R1| + |R2| = m·|W|; |R2| ≥ 0 covers the boundary + e->add_side_constraint(mk_constraint( + a.mk_eq(a.mk_add(len_r1, len_r2), len_wpow), dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(len_r2, zero), dep)); + } + // Case 3: W^m ends strictly inside U^n. Fresh cuts + // S1 = Y·W^m and S2 (rest of U^n): + // U^n = S1·S2, S1 = Y·W^m, Z = S2·V. + { + const expr_ref s1_e = m_sk.mk("fw.s1", eq.m_lhs->get_expr(), eq.m_rhs->get_expr(), + a.mk_int(fwd ? 1 : 0), sideA->get_sort()); + const expr_ref s2_e = m_sk.mk("fw.s2", eq.m_lhs->get_expr(), eq.m_rhs->get_expr(), + a.mk_int(fwd ? 1 : 0), sideA->get_sort()); + euf::snode const* s1_sn = m_sg.mk(s1_e); + euf::snode const* s2_sn = m_sg.mk(s2_e); + const expr_ref len_s1(m_seq.str.mk_length(s1_e), m); + const expr_ref len_s2(m_seq.str.mk_length(s2_e), m); + + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, "fine-wilf elim R", false); + auto& eqs = child->str_eqs(); + eqs[eq_idx] = eqs.back(); + eqs.pop_back(); + eqs.push_back(str_eq(m, upow, dir_concat(m_sg, s1_sn, s2_sn, fwd), dep)); + eqs.push_back(str_eq(m, s1_sn, dir_concat(m_sg, y_sn, wpow, fwd), dep)); + eqs.push_back(str_eq(m, z_sn, dir_concat(m_sg, s2_sn, v_sn, fwd), dep)); + // |S1| = Ly + m·|W|, m·|W| ≥ T, strictness |S2| ≥ 1, + // |S1| + |S2| = n·|U| + e->add_side_constraint(mk_constraint( + a.mk_eq(len_s1, a.mk_add(ly_e, len_wpow)), dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(len_wpow, t_e), dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(len_s2, a.mk_int(1)), dep)); + e->add_side_constraint(mk_constraint( + a.mk_eq(a.mk_add(len_s1, len_s2), len_upow), dep)); + } + } + return true; + } + } + } + return false; + } + // ----------------------------------------------------------------------- // Modifier: apply_const_num_unwinding // For a power token u^n facing a constant (char) head, @@ -6522,6 +6894,7 @@ namespace seq { st.update("nseq mod det", m_stats.m_mod_det); st.update("nseq mod power epsilon", m_stats.m_mod_power_epsilon); st.update("nseq mod num cmp", m_stats.m_mod_num_cmp); + st.update("nseq mod fine wilf", m_stats.m_mod_fine_wilf); st.update("nseq mod const num unwind", m_stats.m_mod_const_num_unwinding); st.update("nseq mod eq split", m_stats.m_mod_eq_split); st.update("nseq mod star intr", m_stats.m_mod_star_intr); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 437b8f25e1..69cfc7b93b 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -612,6 +612,14 @@ namespace seq { // into the resource/node budget and degrades to unknown — the sound // direction for an LP timeout. Sticky so it survives hot restart. bool m_is_arith_split = false; + // Fine & Wilf refire guard: directional keys of equations this node + // (or an ancestor, via clone_from) has already been F&W-split on + // (apply_fine_wilf). The symbolic small-overlap child keeps the + // equation verbatim (arith split) — without the guard the modifier + // would re-match it and emit the identical split forever, since + // arith-split nodes are exempt from the sibling loop-cut. + // Key: (lhs snode id << 33) | (rhs snode id << 1) | fwd. + svector m_fw_applied; // number of constraints inherited from the parent node at clone time. // constraints[0..m_parent_ic_count) are already asserted at the // parent's solver scope; only [m_parent_ic_count..end) need to be @@ -686,6 +694,10 @@ namespace seq { bool is_arith_split() const { return m_is_arith_split; } void set_arith_split() { m_is_arith_split = true; } + // Fine & Wilf refire guard (see m_fw_applied). + bool fw_applied(uint64_t key) const { return m_fw_applied.contains(key); } + void mark_fw_applied(uint64_t key) { m_fw_applied.push_back(key); } + // True if this node structurally aliases its parent's string signature // without being a recurrence: a factorization continuation (pending splits) // or an arithmetic-split child (pending LP resolution of its branch @@ -845,6 +857,7 @@ namespace seq { unsigned m_mod_power_epsilon = 0; unsigned m_mod_num_cmp = 0; unsigned m_mod_split_power_elim = 0; + unsigned m_mod_fine_wilf = 0; unsigned m_mod_const_num_unwinding = 0; unsigned m_mod_regex_if_split = 0; unsigned m_mod_eq_split = 0; @@ -929,6 +942,7 @@ namespace seq { unsigned m_max_nodes = 0; // 0 = unlimited bool m_parikh_enabled = true; bool m_signature_split = false; + bool m_fine_wilf = false; unsigned m_regex_factorization_threshold = 1; bool m_regex_factorization_eager = false; bool m_regex_dynamic_decomposition = true; @@ -1143,10 +1157,12 @@ namespace seq { void add_str_deq(euf::snode const* lhs, euf::snode const* rhs, sat::literal l) const; 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) 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; + // test-friendly overloads (no external dependency tracking); they + // create the root lazily — production callers (theory_nseq) use the + // enode/literal overloads after an explicit create_root() + 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); // access all nodes ptr_vector const& nodes() const { return m_nodes; } @@ -1166,6 +1182,8 @@ namespace seq { seq_parikh& parikh() const { return *m_parikh; } void set_signature_split(bool e) { m_signature_split = e; } + + void set_fine_wilf(bool e) { m_fine_wilf = e; } void set_regex_factorization_threshold(unsigned max) { m_regex_factorization_threshold = max; } void set_regex_factorization_eager(bool e) { m_regex_factorization_eager = e; } @@ -1561,6 +1579,27 @@ namespace seq { // cancellation deterministically. bool apply_split_power_elim(nielsen_node* node); + // Fine & Wilf overlap split: for an equation U^n·V = Y·W^m·Z (up to + // direction / side swap) with a directional head power U^n on one side + // and a concrete-char prefix Y (possibly empty) followed by a power W^m + // with a DIFFERENT base on the other, split on the overlap length + // O = min(n·|U| − |Y|, m·|W|) + // against the Fine & Wilf threshold T = |U| + |W| (the exact bound is + // T − gcd(|U|,|W|); dropping the gcd term is a sound weakening): + // Case 1 (O < T): one of the exponents is bounded. + // Case 2 (O ≥ T, LHS power ends first): U^n is eliminated. + // Case 3 (O ≥ T, RHS power ends first): W^m is eliminated. + // Ground bases: cases 2/3 are generated only if Y is a prefix of U^ω + // and rot(U, |Y| mod |U|) commutes with W (by F&W both are unsat + // otherwise), enumerating the cut position in the other base; case 1 + // enumerates the concretely-bounded exponent (all children progress). + // Symbolic bases: fresh cut variables axiomatize the alignment + // (U^n = Y·R1, W^m = R1·R2, V = R2·Z) and case 1 becomes an + // arith-split child guarded against refire (m_fw_applied). + // Preempts apply_const_num_unwinding's divergent one-copy peel loop on + // different-base power vs power heads. + bool apply_fine_wilf(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). bool apply_const_num_unwinding(nielsen_node* node); diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index af7d9b7d32..14daf55b99 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -1014,6 +1014,7 @@ namespace smt { m_nielsen.set_max_nodes(get_fparams().m_nseq_max_nodes); m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh); m_nielsen.set_signature_split(get_fparams().m_nseq_signature); + m_nielsen.set_fine_wilf(get_fparams().m_nseq_fine_wilf); m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold); m_nielsen.set_regex_factorization_eager(get_fparams().m_nseq_regex_factorization_eager); m_nielsen.set_regex_dynamic_decomposition(get_fparams().m_nseq_regex_dynamic_decomposition); diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 4563752812..443a1e25f6 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -103,6 +103,8 @@ add_executable(test-z3 nla_intervals.cpp nlsat.cpp no_overflow.cpp + nseq_basic.cpp + nseq_zipt.cpp object_allocator.cpp old_interval.cpp optional.cpp @@ -117,6 +119,7 @@ add_executable(test-z3 prime_generator.cpp psmt.cpp seq_regex_bisim.cpp + seq_nielsen.cpp proof_checker.cpp qe_arith.cpp mbp_qel.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 3a3cab41db..e25fb74d85 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -200,6 +200,9 @@ X(seq_split) \ X(fpa) \ X(seq_regex_bisim) \ + X(seq_nielsen) \ + X(nseq_basic) \ + X(nseq_zipt) \ X(term_enumeration) \ X(lcube) \ X(psmt) diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp index 797bbc17ff..306b8a0628 100644 --- a/src/test/nseq_basic.cpp +++ b/src/test/nseq_basic.cpp @@ -129,17 +129,16 @@ static void test_nseq_node_satisfied() { // empty node has no constraints => satisfied SASSERT(node->is_satisfied()); - // add a trivial equality + // a trivial equality is dropped already at insertion (add_str_eq) const euf::snode *empty = sg.mk_empty_seq(su.str.mk_string_sort()); const seq::dep_tracker dep = nullptr; const seq::str_eq eq(m, empty, empty, dep); node->add_str_eq(eq); - SASSERT(node->str_eqs().size() == 1); - SASSERT(!node->str_eqs()[0].is_trivial() || node->str_eqs()[0].m_lhs == node->str_eqs()[0].m_rhs); - // After simplification, trivial equalities should be removed + SASSERT(node->str_eqs().empty()); + SASSERT(node->is_satisfied()); const ptr_vector cur_path; const seq::simplify_result sr = node->simplify_and_init(cur_path); - + VERIFY(sr == seq::simplify_result::satisfied || sr == seq::simplify_result::proceed); std::cout << " ok\n"; } @@ -284,6 +283,93 @@ static void test_setup_seq_str_dispatches_nseq() { std::cout << " ok: setup_seq_str dispatched to setup_nseq for 'nseq'\n"; } +// ----------------------------------------------------------------------- +// Fine & Wilf end-to-end tests (full smt::context, real arithmetic). +// The equation shape U^n·V = Y·W^m·Z with different-base powers used to +// diverge under the const-num-unwinding peel; apply_fine_wilf (priority 3c, +// smt.nseq.fine_wilf) closes it. See specs/nseq-fine-wilf.md. +// ----------------------------------------------------------------------- + +// Shared builder: asserts "a"·(ba)^n·mid_l·u == (ab)^n·"a"·mid_r·v ∧ n ≥ 0 +// into ctx. mid_l/mid_r are ground infixes ("" = none). +static void assert_fine_wilf_eq(smt::context& ctx, ast_manager& m, + const char* mid_l, const char* mid_r) { + seq_util su(m); + arith_util au(m); + sort* str_sort = su.str.mk_string_sort(); + const expr_ref n(m.mk_const(symbol("n"), au.mk_int()), m); + const expr_ref u(m.mk_const(symbol("u"), str_sort), m); + const expr_ref v(m.mk_const(symbol("v"), str_sort), m); + const expr_ref pow_ba(su.str.mk_power(su.str.mk_string(zstring("ba")), n), m); + const expr_ref pow_ab(su.str.mk_power(su.str.mk_string(zstring("ab")), n), m); + + expr_ref lhs(su.str.mk_concat(su.str.mk_string(zstring("a")), pow_ba), m); + if (*mid_l) + lhs = su.str.mk_concat(lhs, su.str.mk_string(zstring(mid_l))); + lhs = su.str.mk_concat(lhs, u); + + expr_ref rhs(su.str.mk_concat(pow_ab, su.str.mk_string(zstring("a"))), m); + if (*mid_r) + rhs = su.str.mk_concat(rhs, su.str.mk_string(zstring(mid_r))); + rhs = su.str.mk_concat(rhs, v); + + ctx.assert_expr(expr_ref(au.mk_ge(n, au.mk_int(0)), m)); + ctx.assert_expr(expr_ref(m.mk_eq(lhs, rhs), m)); +} + +// UNSAT: "a"·(ba)^n·"ab"·u == (ab)^n·"a"·"ba"·v has no solution (after +// aligning the periodic parts the remainders force "ab"·u = "ba"·v with +// equal-position clash for every n). Diverges with fine_wilf disabled — +// this is the regression test for the peel loop. +static void test_nseq_fine_wilf_e2e_unsat() { + std::cout << "test_nseq_fine_wilf_e2e_unsat\n"; + ast_manager m; + reg_decl_plugins(m); + smt_params params; + params.m_string_solver = symbol("nseq"); + SASSERT(!params.m_nseq_fine_wilf); // opt-in feature: default off + params.m_nseq_fine_wilf = true; + smt::context ctx(m, params); + assert_fine_wilf_eq(ctx, m, "ab", "ba"); + const lbool r = ctx.check(); + SASSERT(r == l_false); + std::cout << " ok: unsat\n"; +} + +// SAT: the draft's test 1, "a"·(ba)^n·u == (ab)^n·"a"·v — u = v solves it +// for every n (a·(ba)^n = (ab)^n·a is the conjugation identity). +static void test_nseq_fine_wilf_e2e_sat() { + std::cout << "test_nseq_fine_wilf_e2e_sat\n"; + ast_manager m; + reg_decl_plugins(m); + smt_params params; + params.m_string_solver = symbol("nseq"); + params.m_nseq_fine_wilf = true; // opt-in (default off) + smt::context ctx(m, params); + assert_fine_wilf_eq(ctx, m, "", ""); + const lbool r = ctx.check(); + SASSERT(r == l_true); + std::cout << " ok: sat\n"; +} + +// Option off (the default): the SAT instance is still solved (the n = 0 +// peel branch closes it without Fine & Wilf), exercising the default +// smt.nseq.fine_wilf=false path end-to-end. (The UNSAT instance would +// diverge here — by design.) +static void test_nseq_fine_wilf_option_off() { + std::cout << "test_nseq_fine_wilf_option_off\n"; + ast_manager m; + reg_decl_plugins(m); + smt_params params; + params.m_string_solver = symbol("nseq"); + params.m_nseq_fine_wilf = false; // explicit for clarity (= the default) + smt::context ctx(m, params); + assert_fine_wilf_eq(ctx, m, "", ""); + const lbool r = ctx.check(); + SASSERT(r == l_true); + std::cout << " ok: sat with fine_wilf disabled\n"; +} + void tst_nseq_basic() { test_nseq_instantiation(); test_nseq_param_validation(); @@ -296,5 +382,8 @@ void tst_nseq_basic() { test_nseq_const_nielsen_solvable(); test_nseq_length_mismatch(); test_setup_seq_str_dispatches_nseq(); + test_nseq_fine_wilf_e2e_unsat(); + test_nseq_fine_wilf_e2e_sat(); + test_nseq_fine_wilf_option_off(); std::cout << "nseq_basic: all tests passed\n"; } diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index 8e570efe44..8de828c19f 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -163,10 +163,9 @@ static void test_nielsen_subst() { const seq::nielsen_subst s2(x, e, dep); SASSERT(s2.is_eliminating()); - // non-eliminating substitution: x -> concat(A, x) - euf::snode const* ax = sg.mk_concat(a, x); - const seq::nielsen_subst s3(x, ax, dep); - SASSERT(!s3.is_eliminating()); + // NOTE: non-eliminating substitutions (e.g. x -> A·x) are forbidden by + // construction — the nielsen_subst ctor asserts the variable does not + // occur in the replacement (add_subst_length_constraints relies on it). // eliminating substitution: x -> y (x not in y) const seq::nielsen_subst s4(x, y, dep); @@ -204,9 +203,10 @@ static void test_nielsen_node() { root->add_str_eq(seq::str_eq(m, sg.mk_concat(x, a), sg.mk_concat(a, y), dep)); SASSERT(root->str_eqs().size() == 2); - // regex membership - const expr_ref re_all(seq.re.mk_full_seq(str_sort), m); - euf::snode const* regex = sg.mk(re_all); + // regex membership (a universal regex like Σ* would be dropped as + // trivially true by add_str_mem — use a proper constraint) + const expr_ref re_a(seq.re.mk_to_re(seq.str.mk_string(zstring("A"))), m); + euf::snode const* regex = sg.mk(re_a); root->add_str_mem(seq::str_mem(m, x, regex, dep)); SASSERT(root->str_mems().size() == 1); @@ -277,9 +277,10 @@ static void test_nielsen_graph_populate() { SASSERT(ng.root()->str_eqs().size() == 1); SASSERT(ng.num_nodes() == 1); - // add regex membership: x in .* - const expr_ref re_all(seq.re.mk_full_seq(str_sort), m); - euf::snode const* regex = sg.mk(re_all); + // add regex membership: x in A (a full-seq membership x ∈ Σ* would be + // dropped as trivially true by add_str_mem) + const expr_ref re_a(seq.re.mk_to_re(seq.str.mk_string(zstring("A"))), m); + euf::snode const* regex = sg.mk(re_a); ng.add_str_mem(x, regex); SASSERT(ng.root()->str_mems().size() == 1); @@ -389,8 +390,10 @@ static void test_nielsen_expansion() { seq::nielsen_edge* edge1 = ng.mk_edge(root, child1, "test", true); edge1->add_subst(s1); - // branch 2: x -> Ax (non-eliminating, non-progress) - euf::snode const* ax = sg.mk_concat(a, x); + // branch 2: x -> A·x2 with a fresh tail (substitutions must be + // eliminating by construction; the edge is still non-progress) + euf::snode const* x2 = sg.mk_var(symbol("x2"), sg.get_str_sort()); + euf::snode const* ax = sg.mk_concat(a, x2); seq::nielsen_node* child2 = ng.mk_child(root); const seq::nielsen_subst s2(x, ax, dep); child2->apply_subst(sg, s2); @@ -424,9 +427,9 @@ static void test_multiple_memberships() { euf::snode const* x = sg.mk_var(symbol("x"), sg.get_str_sort()); - // x in .* - const expr_ref re_all(seq.re.mk_full_seq(str_sort), m); - euf::snode const* regex1 = sg.mk(re_all); + // x in A* (a full-seq membership would be dropped as trivially true) + const expr_ref re_astar(seq.re.mk_star(seq.re.mk_to_re(seq.str.mk_string(zstring("A")))), m); + euf::snode const* regex1 = sg.mk(re_astar); ng.add_str_mem(x, regex1); // x in re.union(to_re("A"), to_re("B")) @@ -490,17 +493,20 @@ static void test_eq_split_basic() { euf::snode const* xa = sg.mk_concat(x, a); euf::snode const* yb = sg.mk_concat(y, b); - // x·A = y·B — eq_split returns false (no valid split point), - // falls through to var_nielsen (priority 12) → 3 progress children + // x·A = y·B — eq_split returns false (no valid split point), falls + // through to var_nielsen (priority 12): five-way branch — 3 progress + // (x→ε, y→ε, x→y) + 2 non-progress (x longer / y longer) ng.add_str_eq(xa, yb); seq::nielsen_node* root = ng.root(); const bool extended = ng.generate_extensions(root); SASSERT(extended); - SASSERT(root->outgoing().size() == 3); - - // all children are progress (var_nielsen marks all as progress) - SASSERT(root->outgoing()[0]->is_progress()); + SASSERT(root->outgoing().size() == 5); + unsigned num_progress = 0; + for (seq::nielsen_edge const* e : root->outgoing()) + if (e->is_progress()) + ++num_progress; + SASSERT(num_progress == 3); } // test var vs var with solve: x·y = z·w is satisfiable (all vars can be ε) @@ -698,7 +704,9 @@ static void test_const_nielsen_solve_unsat() { SASSERT(result == seq::nielsen_graph::search_result::unsat); } -// test const_nielsen priority: A·x = y·B → const_nielsen (2 children), not var_nielsen (3) +// test priority for A·x = y·B: the det modifier's variable-vs-char +// look-ahead (sub-rule 4, y → A·tail) preempts const_nielsen and +// var_nielsen with a single deterministic progress child static void test_const_nielsen_priority_over_eq_split() { std::cout << "test_const_nielsen_priority_over_eq_split\n"; ast_manager m; @@ -723,8 +731,9 @@ static void test_const_nielsen_priority_over_eq_split() { const bool extended = ng.generate_extensions(root); SASSERT(extended); - // const_nielsen produces 2 children, not var_nielsen's 3 - SASSERT(root->outgoing().size() == 2); + SASSERT(root->outgoing().size() == 1); + SASSERT(strcmp(root->outgoing()[0]->rule_name(), "det") == 0); + SASSERT(root->outgoing()[0]->is_progress()); } // test const_nielsen tail direction: x·A = w·y @@ -769,7 +778,9 @@ static void test_const_nielsen_tail_char_var() { euf::snode_vector toks; s.m_replacement->collect_tokens(toks); SASSERT(toks.size() == 2); - SASSERT(toks[0]->is_var() && toks[0]->id() == y->id()); + // substitutions are eliminating by construction: the tail is a + // FRESH variable (y → y'·A), not y itself + SASSERT(toks[0]->is_var() && toks[0]->id() != y->id()); SASSERT(toks[1]->is_char() && toks[1]->id() == a->id()); saw_tail = true; SASSERT(!e->is_progress()); @@ -798,12 +809,13 @@ static void test_const_nielsen_not_applicable_both_vars() { euf::snode const* yb = sg.mk_concat(y, b); // x·A = y·B → both heads are vars → var_nielsen fires (priority 12) + // with its five-way branch (3 progress + 2 non-progress) ng.add_str_eq(xa, yb); seq::nielsen_node* root = ng.root(); const bool extended = ng.generate_extensions(root); SASSERT(extended); - SASSERT(root->outgoing().size() == 3); + SASSERT(root->outgoing().size() == 5); } // test const_nielsen solve: A·B·x = A·B·C → sat (x = C after two det cancels) @@ -863,10 +875,11 @@ static void test_regex_char_split_basic() { const auto sr = ng.root()->simplify_and_init({}); SASSERT(sr != seq::simplify_result::conflict); + // x ∈ "AB" is PRIMITIVE (single var, ground regex): the node is already + // satisfied — no modifier fires; the witness is left to seq_model. const bool extended = ng.generate_extensions(ng.root()); - SASSERT(extended); - // should have at least 2 children: x→'A'·z and x→ε - SASSERT(ng.root()->outgoing().size() >= 2); + SASSERT(!extended); + SASSERT(ng.root()->is_satisfied()); ng.display(std::cout); } @@ -910,12 +923,10 @@ static void test_regex_char_split_solve_multi_char() { seq::nielsen_graph ng(sg, solver, context_solver); euf::snode const* x = sg.mk_var(symbol("x"), sg.get_str_sort()); - const expr_ref ch_a(seq.str.mk_char('A'), m); - const expr_ref unit_a(seq.str.mk_unit(ch_a), m); - const expr_ref ch_b(seq.str.mk_char('B'), m); - const expr_ref unit_b(seq.str.mk_unit(ch_b), m); - const expr_ref ab(seq.str.mk_concat(unit_a, unit_b), m); - const expr_ref to_re_ab(seq.re.mk_to_re(ab), m); + // NB: build the regex over a string LITERAL (canonical form, as produced + // by th_rewriter through the theory); a to_re over a concat of units is + // not a canonical leaf and is not supported at this layer. + const expr_ref to_re_ab(seq.re.mk_to_re(seq.str.mk_string(zstring("AB"))), m); euf::snode const* regex = sg.mk(to_re_ab); ng.add_str_mem(x, regex); @@ -995,12 +1006,8 @@ static void test_regex_char_split_concat_str() { euf::snode const* y = sg.mk_var(symbol("y"), sg.get_str_sort()); euf::snode const* xy = sg.mk_concat(x, y); - const expr_ref ch_a(seq.str.mk_char('A'), m); - const expr_ref unit_a(seq.str.mk_unit(ch_a), m); - const expr_ref ch_b(seq.str.mk_char('B'), m); - const expr_ref unit_b(seq.str.mk_unit(ch_b), m); - const expr_ref ab(seq.str.mk_concat(unit_a, unit_b), m); - const expr_ref to_re_ab(seq.re.mk_to_re(ab), m); + // canonical literal-based regex (see test_regex_char_split_solve_multi_char) + const expr_ref to_re_ab(seq.re.mk_to_re(seq.str.mk_string(zstring("AB"))), m); euf::snode const* regex = sg.mk(to_re_ab); ng.add_str_mem(xy, regex); @@ -1281,12 +1288,16 @@ static void test_generate_extensions_no_applicable() { euf::snode const* a = sg.mk_char('A'); euf::snode const* b = sg.mk_char('B'); - // A = B → no variables involved → no modifier applies + // A = B → ground symbol clash. generate_extensions may only be called + // on a simplified, non-conflicting node (search_dfs simplifies first), + // so the modern expectation is: simplify detects the conflict and no + // extension is ever attempted. ng.add_str_eq(a, b); seq::nielsen_node* root = ng.root(); - const bool extended = ng.generate_extensions(root); - SASSERT(!extended); + const auto sr = root->simplify_and_init({}); + SASSERT(sr == seq::simplify_result::conflict); + SASSERT(root->is_currently_conflict()); SASSERT(root->outgoing().empty()); } @@ -1310,16 +1321,16 @@ static void test_generate_extensions_regex_only() { const expr_ref to_re_a(seq.re.mk_to_re(unit_a), m); euf::snode const* re_node = sg.mk(to_re_a); - // x ∈ to_re("A") → only regex_char_split can fire (no str_eq) + // x ∈ to_re("A") is a PRIMITIVE membership: the node is satisfied as-is + // (no modifier fires; the witness is left to seq_model) ng.add_str_mem(x, re_node); seq::nielsen_node* root = ng.root(); root->simplify_and_init({}); const bool extended = ng.generate_extensions(root); - SASSERT(extended); - // at least 1 child (epsilon branch) + possibly char branches - SASSERT(root->outgoing().size() >= 1); + SASSERT(!extended); + SASSERT(root->is_satisfied()); } // test: mixed constraints, x·A = x·B and y ∈ R → after simplify, A = B clash → unsat @@ -1359,7 +1370,8 @@ static void test_generate_extensions_mixed_det_first() { // solve() / search_dfs() tests // ----------------------------------------------------------------------- -// test solve on empty graph (no root) returns sat +// test solve on an empty constraint set returns sat (solve() requires an +// explicitly created root nowadays — theory_nseq calls create_root()) static void test_solve_empty_graph() { std::cout << "test_solve_empty_graph\n"; ast_manager m; @@ -1371,6 +1383,7 @@ static void test_solve_empty_graph() { seq::context_solver_i context_solver; seq::nielsen_graph ng(sg, solver, context_solver); SASSERT(!ng.root()); + ng.create_root(); const auto result = ng.solve(); SASSERT(result == seq::nielsen_graph::search_result::sat); } @@ -1459,7 +1472,7 @@ static void test_dep_tracker_get_set_bits() { dm.linearize(d1, bits1); SASSERT(bits1.size() == 1); SASSERT(std::holds_alternative(bits1[0])); - SASSERT(std::get(bits1[0]).index() == 5); + SASSERT(std::get(bits1[0]) == sat::literal(5)); // two leaves merged: sat::literal(3) and sat::literal(11) const seq::dep_tracker d2 = dm.mk_join( @@ -1471,9 +1484,9 @@ static void test_dep_tracker_get_set_bits() { bool has_3 = false, has_11 = false; for (auto const& d : bits2) { if (std::holds_alternative(d)) { - const unsigned idx = std::get(d).index(); - if (idx == 3) has_3 = true; - if (idx == 11) has_11 = true; + const sat::literal l = std::get(d); + if (l == sat::literal(3)) has_3 = true; + if (l == sat::literal(11)) has_11 = true; } } SASSERT(has_3); @@ -1489,9 +1502,9 @@ static void test_dep_tracker_get_set_bits() { bool has31 = false, has32 = false; for (auto const& d : bits3) { if (std::holds_alternative(d)) { - const unsigned idx = std::get(d).index(); - if (idx == 31) has31 = true; - if (idx == 32) has32 = true; + const sat::literal l = std::get(d); + if (l == sat::literal(31)) has31 = true; + if (l == sat::literal(32)) has32 = true; } } SASSERT(has31); @@ -1753,13 +1766,13 @@ static void test_simplify_empty_propagation() { euf::snode const* y = sg.mk_var(symbol("y"), sg.get_str_sort()); euf::snode const* xy = sg.mk_concat(x, y); - // ε = x·y → forces x=ε, y=ε → all trivial → satisfied - seq::nielsen_node* node = ng.mk_node(); - const seq::dep_tracker dep = nullptr; - node->add_str_eq(seq::str_eq(m, e, xy, dep)); - - const auto sr = node->simplify_and_init({}); - SASSERT(sr == seq::simplify_result::satisfied); + // ε = x·y → the det modifier's empty-side propagation (§8.1 sub-rule 1) + // forces x=ε, y=ε — nowadays a modifier step, not a simplify pass, so + // check the end-to-end result: solve → sat + ng.add_str_eq(e, xy); + const auto sr = ng.root()->simplify_and_init({}); + SASSERT(sr != seq::simplify_result::conflict); + SASSERT(ng.solve() == seq::nielsen_graph::search_result::sat); } // test simplify_and_init: empty vs concrete char → conflict @@ -1970,21 +1983,19 @@ static void test_simplify_brzozowski_rtl_suffix() { euf::snode const* xa = sg.mk_concat(x, a); euf::snode const* e = sg.mk_empty_seq(seq.str.mk_string_sort()); - const expr_ref ch_b(seq.str.mk_char('B'), m); - const expr_ref unit_b(seq.str.mk_unit(ch_b), m); - const expr_ref ch_a(seq.str.mk_char('A'), m); - const expr_ref unit_a(seq.str.mk_unit(ch_a), m); - const expr_ref ba(seq.str.mk_concat(unit_b, unit_a), m); - const expr_ref to_re_ba(seq.re.mk_to_re(ba), m); + // canonical literal-based regex (a to_re over a concat of units is not + // a canonical leaf at this layer) + const expr_ref to_re_ba(seq.re.mk_to_re(seq.str.mk_string(zstring("BA"))), m); euf::snode const* regex = sg.mk(to_re_ba); - // x·"A" ∈ to_re("BA") → RTL consume trailing 'A' → x ∈ to_re("B") + // x·"A" ∈ to_re("BA") → RTL consume trailing 'A' → x ∈ to_re("B"), + // which is primitive — the node is then satisfied seq::nielsen_node* node = ng.mk_node(); const seq::dep_tracker dep = nullptr; node->add_str_mem(seq::str_mem(m, xa, regex, dep)); const auto sr = node->simplify_and_init({}); - SASSERT(sr == seq::simplify_result::proceed); + SASSERT(sr == seq::simplify_result::satisfied); SASSERT(node->str_mems().size() == 1); SASSERT(node->str_mems()[0].m_str->is_var()); SASSERT(node->str_mems()[0].m_str->id() == x->id()); @@ -2014,7 +2025,7 @@ static void test_simplify_multiple_eqs() { seq::nielsen_node* node = ng.mk_node(); const seq::dep_tracker dep = nullptr; - // eq1: ε = ε (trivial → removed) + // eq1: ε = ε (trivial → dropped already at insertion by add_str_eq) node->add_str_eq(seq::str_eq(m, e, e, dep)); // eq2: A·x = A·y (prefix cancel → x = y) euf::snode const* ax = sg.mk_concat(a, x); @@ -2023,10 +2034,10 @@ static void test_simplify_multiple_eqs() { // eq3: x = z (non-trivial, kept) node->add_str_eq(seq::str_eq(m, x, z, dep)); - SASSERT(node->str_eqs().size() == 3); + SASSERT(node->str_eqs().size() == 2); const auto sr = node->simplify_and_init({}); SASSERT(sr == seq::simplify_result::proceed); - // eq1 removed, eq2 simplified to x=y, eq3 kept → 2 eqs remain + // eq2 simplified to x=y, eq3 kept → 2 eqs remain SASSERT(node->str_eqs().size() == 2); } @@ -2057,8 +2068,9 @@ static void test_det_cancel_child_eq() { SASSERT(result == seq::nielsen_graph::search_result::unsat); } -// test const_nielsen: verify children's substitutions target the variable -// A·x = y·B → char vs var: const_nielsen fires (2 children, both substitute y) +// test child substitutions for A·x = y·B: the det modifier's +// variable-vs-char look-ahead fires with a single child substituting +// y → A·y' (fresh tail) static void test_const_nielsen_child_substitutions() { std::cout << "test_const_nielsen_child_substitutions\n"; ast_manager m; @@ -2076,24 +2088,23 @@ static void test_const_nielsen_child_substitutions() { euf::snode const* ax = sg.mk_concat(a, x); euf::snode const* yb = sg.mk_concat(y, b); - // A·x = y·B → const_nielsen: 2 children, both substitute y + // A·x = y·B → det look-ahead: 1 child substituting y → A·y' ng.add_str_eq(ax, yb); seq::nielsen_node* root = ng.root(); const bool extended = ng.generate_extensions(root); SASSERT(extended); - SASSERT(root->outgoing().size() == 2); - - // both edges substitute y - for (unsigned i = 0; i < 2; ++i) { - SASSERT(root->outgoing()[i]->subst().size() == 1); - SASSERT(root->outgoing()[i]->subst()[0].m_var == y); - } - - // edge 0: y → ε (eliminating, replacement is empty) - SASSERT(root->outgoing()[0]->subst()[0].m_replacement->is_empty()); - // edge 1: y → A·fresh (replacement is non-empty) - SASSERT(!root->outgoing()[1]->subst()[0].m_replacement->is_empty()); + SASSERT(root->outgoing().size() == 1); + SASSERT(root->outgoing()[0]->subst().size() == 1); + seq::nielsen_subst const& s = root->outgoing()[0]->subst()[0]; + SASSERT(s.m_var == y); + SASSERT(!s.m_replacement->is_empty()); + // replacement starts with the matched char A and ends with a fresh var + euf::snode_vector toks; + s.m_replacement->collect_tokens(toks); + SASSERT(toks.size() == 2); + SASSERT(toks[0]->id() == a->id()); + SASSERT(toks[1]->is_var() && toks[1]->id() != y->id()); } // test var_nielsen: verify substitution structure — det fires for x = y (single var def) @@ -2584,10 +2595,10 @@ static void test_star_intr_no_backedge() { const auto sr = root->simplify_and_init({}); SASSERT(sr != seq::simplify_result::conflict); + // x ∈ "A" is a primitive membership: satisfied as-is, nothing fires const bool extended = ng.generate_extensions(root); - SASSERT(extended); - // regex_char_split fires (priority 9): at least 2 children (x→A·z, x→ε) - SASSERT(root->outgoing().size() >= 2); + SASSERT(!extended); + SASSERT(root->is_satisfied()); } // test_star_intr_with_backedge: backedge set → star_intr fires @@ -2725,11 +2736,11 @@ static void test_regex_var_split_basic() { const auto sr = root->simplify_and_init({}); SASSERT(sr != seq::simplify_result::conflict); + // x ∈ (A|B) is a primitive membership: satisfied as-is, nothing fires + // (the witness is enumerated by seq_model, not by graph splitting) const bool extended = ng.generate_extensions(root); - SASSERT(extended); - // Should produce children via regex_char_split or regex_var_split - SASSERT(root->outgoing().size() >= 2); - std::cout << " regex split generated " << root->outgoing().size() << " children\n"; + SASSERT(!extended); + SASSERT(root->is_satisfied()); } // test_power_split_no_power: no power tokens → modifier returns false @@ -3349,7 +3360,11 @@ static unsigned queried_ub(seq::nielsen_node* node, euf::snode const* var) { return ub.is_unsigned() ? ub.get_unsigned() : UINT_MAX; } -// test lower-bound constraints affect queried bounds +// Bounds are owned by the arithmetic side (context/sub solver) nowadays: +// nielsen_node::lower_bound/upper_bound consult the context solver and fall +// back to the conservative defaults (0 / unbounded) when it reports +// "unsupported" — node-local constraints do NOT feed the queries. These +// tests pin that contract plus the constraint-accumulation plumbing. static void test_add_lower_int_bound_basic() { std::cout << "test_add_lower_int_bound_basic\n"; ast_manager m; @@ -3363,34 +3378,30 @@ static void test_add_lower_int_bound_basic() { dummy_simple_solver solver; seq::context_solver_i context_solver; seq::nielsen_graph ng(sg, solver, context_solver); - ng.add_str_eq(x, x); // create root node + ng.create_root(); seq::nielsen_node* node = ng.root(); const seq::dep_tracker dep = nullptr; - // initially no bounds + // initially no bounds and no constraints SASSERT(queried_lb(node, x) == 0); SASSERT(queried_ub(node, x) == UINT_MAX); SASSERT(node->constraints().empty()); + // node constraints accumulate but do not affect the queried bounds + // (the default context solver reports "unsupported") add_len_ge(ng, node, x, 3, dep); - SASSERT(queried_lb(node, x) == 3); + SASSERT(queried_lb(node, x) == 0); SASSERT(node->constraints().size() == 1); SASSERT(node->constraints()[0].fml); - // weaker bound does not change the effective lower bound - add_len_ge(ng, node, x, 2, dep); - SASSERT(queried_lb(node, x) == 3); - SASSERT(node->constraints().size() == 2); - add_len_ge(ng, node, x, 5, dep); - SASSERT(queried_lb(node, x) == 5); - SASSERT(node->constraints().size() == 3); + SASSERT(node->constraints().size() == 2); std::cout << " ok\n"; } -// test upper-bound constraints affect queried bounds +// same contract for upper bounds static void test_add_upper_int_bound_basic() { std::cout << "test_add_upper_int_bound_basic\n"; ast_manager m; @@ -3403,7 +3414,7 @@ static void test_add_upper_int_bound_basic() { dummy_simple_solver solver; seq::context_solver_i context_solver; seq::nielsen_graph ng(sg, solver, context_solver); - ng.add_str_eq(x, x); + ng.create_root(); seq::nielsen_node* node = ng.root(); const seq::dep_tracker dep = nullptr; @@ -3411,23 +3422,18 @@ static void test_add_upper_int_bound_basic() { SASSERT(queried_ub(node, x) == UINT_MAX); add_len_le(ng, node, x, 10, dep); - SASSERT(queried_ub(node, x) == 10); + SASSERT(queried_ub(node, x) == UINT_MAX); SASSERT(node->constraints().size() == 1); SASSERT(node->constraints()[0].fml); - // weaker bound does not change the effective upper bound - add_len_le(ng, node, x, 20, dep); - SASSERT(queried_ub(node, x) == 10); - SASSERT(node->constraints().size() == 2); - add_len_le(ng, node, x, 5, dep); - SASSERT(queried_ub(node, x) == 5); - SASSERT(node->constraints().size() == 3); + SASSERT(node->constraints().size() == 2); std::cout << " ok\n"; } -// inconsistent local bounds are visible through lower_bound/upper_bound queries +// contradictory node-local length constraints do not surface through the +// bound queries (the arithmetic subsolver refutes them during search) static void test_add_bound_lb_gt_ub_conflict() { std::cout << "test_add_bound_lb_gt_ub_conflict\n"; ast_manager m; @@ -3440,19 +3446,21 @@ static void test_add_bound_lb_gt_ub_conflict() { dummy_simple_solver solver; seq::context_solver_i context_solver; seq::nielsen_graph ng(sg, solver, context_solver); - ng.add_str_eq(x, x); + ng.create_root(); seq::nielsen_node* node = ng.root(); const seq::dep_tracker dep = nullptr; add_len_le(ng, node, x, 3, dep); add_len_ge(ng, node, x, 5, dep); - SASSERT(queried_lb(node, x) > queried_ub(node, x)); + SASSERT(node->constraints().size() == 2); + SASSERT(queried_lb(node, x) == 0); + SASSERT(queried_ub(node, x) == UINT_MAX); std::cout << " ok\n"; } -// test clone_from: child inherits parent bounds +// test clone_from: child inherits parent constraints verbatim static void test_bounds_cloned() { std::cout << "test_bounds_cloned\n"; ast_manager m; @@ -3471,22 +3479,16 @@ static void test_bounds_cloned() { seq::nielsen_node* parent = ng.root(); const seq::dep_tracker dep = nullptr; - // set bounds on parent add_len_ge(ng, parent, x, 2, dep); add_len_le(ng, parent, x, 7, dep); add_len_ge(ng, parent, y, 1, dep); - // clone to child + // clone to child: constraints are copied, and the parent-inherited + // prefix is recorded (m_parent_ic_count semantics) seq::nielsen_node* child = ng.mk_child(parent); - - // child should have same bounds - SASSERT(queried_lb(child, x) == 2); - SASSERT(queried_ub(child, x) == 7); - SASSERT(queried_lb(child, y) == 1); - SASSERT(queried_ub(child, y) == UINT_MAX); - - // child's int_constraints should also be cloned (3 constraints: lb_x, ub_x, lb_y) SASSERT(child->constraints().size() == parent->constraints().size()); + for (unsigned i = 0; i < parent->constraints().size(); ++i) + SASSERT(child->constraints()[i].fml.get() == parent->constraints()[i].fml.get()); std::cout << " ok\n"; } @@ -3732,16 +3734,10 @@ static void test_simplify_unit_prefix_split() { const auto sr = node->simplify_and_init({}); SASSERT(sr == seq::simplify_result::proceed); - // original eq stripped to x==y, plus a new unit(a)==unit(b) eq - SASSERT(node->str_eqs().size() == 2); - // at least one eq has both sides as unit or var (the unit equality) - bool found_unit_eq = false; - for (auto const& eq : node->str_eqs()) { - if (eq.m_lhs && eq.m_rhs && - eq.m_lhs->is_char_or_unit() && eq.m_rhs->is_char_or_unit()) - found_unit_eq = true; - } - SASSERT(found_unit_eq); + // symbolic unit-vs-unit heads are NOT split off as a separate equality + // by simplify anymore — the equation is kept (unit unification is + // handled by the det modifier / char-range machinery during search) + SASSERT(node->str_eqs().size() == 1); std::cout << " ok\n"; } @@ -3819,19 +3815,300 @@ static void test_simplify_unit_suffix_split() { const auto sr = node->simplify_and_init({}); SASSERT(sr == seq::simplify_result::proceed); - // original eq stripped to x==y, plus a new unit(a)==unit(b) eq - SASSERT(node->str_eqs().size() == 2); - bool found_unit_eq = false; - for (auto const& eq : node->str_eqs()) { - if (eq.m_lhs && eq.m_rhs && - eq.m_lhs->is_char_or_unit() && eq.m_rhs->is_char_or_unit()) - found_unit_eq = true; - } - SASSERT(found_unit_eq); + // the unit-unit suffix is consumed by a char substitution — only x==y + // remains (see test_simplify_unit_prefix_split) + SASSERT(node->str_eqs().size() == 1); + std::cout << " ok\n"; +} + +// ----------------------------------------------------------------------- +// apply_fine_wilf tests (priority 3c): Fine & Wilf overlap splitting for +// different-base power heads. See specs/nseq-fine-wilf.md. +// ----------------------------------------------------------------------- + +// Shared setup: returns a power snode base^exp for a ground string base. +static euf::snode const* mk_ground_power(euf::sgraph& sg, seq_util& seq, ast_manager& m, + const char* base, expr* exp) { + const expr_ref base_e(seq.str.mk_string(zstring(base)), m); + const expr_ref pw(seq.str.mk_power(base_e, exp), m); + return sg.mk(pw); +} + +static unsigned count_edges_with_rule(seq::nielsen_node const* n, const char* prefix) { + unsigned cnt = 0; + for (seq::nielsen_edge const* e : n->outgoing()) + if (strncmp(e->rule_name(), prefix, strlen(prefix)) == 0) + ++cnt; + return cnt; +} + +// (ab)^n·U = (ba)^m·V — "ab" and "ba" do not commute, so the F&W cases 2/3 +// are pruned at generation time; only the bounded-exponent enumerations +// remain: n ∈ {0,1} (n·2 < 4) and m ∈ {0,1}, i.e. 4 progress children. +static void test_fine_wilf_noncommuting_children() { + std::cout << "test_fine_wilf_noncommuting_children\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + arith_util arith(m); + seq_util seq(m); + + dummy_simple_solver solver; + seq::context_solver_i context_solver; + seq::nielsen_graph ng(sg, solver, context_solver); + ng.set_fine_wilf(true); // opt-in (smt.nseq.fine_wilf defaults to off) + + expr* n_e = m.mk_const(symbol("n"), arith.mk_int()); + expr* m_e = m.mk_const(symbol("m"), arith.mk_int()); + euf::snode const* pw_ab = mk_ground_power(sg, seq, m, "ab", n_e); + euf::snode const* pw_ba = mk_ground_power(sg, seq, m, "ba", m_e); + euf::snode const* u = sg.mk_var(symbol("U"), sg.get_str_sort()); + euf::snode const* v = sg.mk_var(symbol("V"), sg.get_str_sort()); + + ng.add_str_eq(sg.mk_concat(pw_ab, u), sg.mk_concat(pw_ba, v)); + seq::nielsen_node* root = ng.root(); + + VERIFY(ng.generate_extensions(root)); + SASSERT(root->outgoing().size() == 4); + for (seq::nielsen_edge const* e : root->outgoing()) + SASSERT(e->is_progress()); + SASSERT(count_edges_with_rule(root, "fine-wilf n") == 2); + SASSERT(count_edges_with_rule(root, "fine-wilf m") == 2); + SASSERT(count_edges_with_rule(root, "fine-wilf elim") == 0); + std::cout << " ok\n"; +} + +// (ab)^n·U = (abab)^m·V — commuting roots (common primitive root "ab"), so +// all four blocks fire. With Lu/Lw ∈ {2,4} (which power plays "U" depends +// on str_eq's side canonicalization): bounded enumerations contribute +// N+1 = (Ly+Lu+Lw-1)/Lu + 1 and M+1 = (Lu+Lw-1)/Lw + 1 children (2+3 or +// 3+2), the case-2/3 cut enumerations Lw + Lu = 6 — 11 progress children. +static void test_fine_wilf_commuting_children() { + std::cout << "test_fine_wilf_commuting_children\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + arith_util arith(m); + seq_util seq(m); + + dummy_simple_solver solver; + seq::context_solver_i context_solver; + seq::nielsen_graph ng(sg, solver, context_solver); + ng.set_fine_wilf(true); // opt-in (smt.nseq.fine_wilf defaults to off) + + expr* n_e = m.mk_const(symbol("n"), arith.mk_int()); + expr* m_e = m.mk_const(symbol("m"), arith.mk_int()); + euf::snode const* pw_ab = mk_ground_power(sg, seq, m, "ab", n_e); + euf::snode const* pw_abab = mk_ground_power(sg, seq, m, "abab", m_e); + euf::snode const* u = sg.mk_var(symbol("U"), sg.get_str_sort()); + euf::snode const* v = sg.mk_var(symbol("V"), sg.get_str_sort()); + + ng.add_str_eq(sg.mk_concat(pw_ab, u), sg.mk_concat(pw_abab, v)); + seq::nielsen_node* root = ng.root(); + + VERIFY(ng.generate_extensions(root)); + SASSERT(root->outgoing().size() == 11); + for (seq::nielsen_edge const* e : root->outgoing()) + SASSERT(e->is_progress()); + SASSERT(count_edges_with_rule(root, "fine-wilf n") + + count_edges_with_rule(root, "fine-wilf m") == 5); + SASSERT(count_edges_with_rule(root, "fine-wilf elim") == 6); + std::cout << " ok\n"; +} + +// "a"·(ba)^n·U = (ab)^n·V — the draft's conjugation shape: ground prefix +// Y = "a" before the (ba)-power; rot("ab", 1) = "ba" = base(W), so the +// conjugate commutes and cases 2/3 fire alongside the enumerations: +// 3 + 2 + 2 + 2 = 9 children. +static void test_fine_wilf_ground_prefix() { + std::cout << "test_fine_wilf_ground_prefix\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + arith_util arith(m); + seq_util seq(m); + + dummy_simple_solver solver; + seq::context_solver_i context_solver; + seq::nielsen_graph ng(sg, solver, context_solver); + ng.set_fine_wilf(true); // opt-in (smt.nseq.fine_wilf defaults to off) + + expr* n_e = m.mk_const(symbol("n"), arith.mk_int()); + euf::snode const* pw_ba = mk_ground_power(sg, seq, m, "ba", n_e); + euf::snode const* pw_ab = mk_ground_power(sg, seq, m, "ab", n_e); + euf::snode const* a = sg.mk_char('a'); + euf::snode const* u = sg.mk_var(symbol("U"), sg.get_str_sort()); + euf::snode const* v = sg.mk_var(symbol("V"), sg.get_str_sort()); + + // "a"·(ba)^n·U = (ab)^n·V + ng.add_str_eq(sg.mk_concat(a, sg.mk_concat(pw_ba, u)), + sg.mk_concat(pw_ab, v)); + seq::nielsen_node* root = ng.root(); + + VERIFY(ng.generate_extensions(root)); + SASSERT(root->outgoing().size() == 9); + for (seq::nielsen_edge const* e : root->outgoing()) + SASSERT(e->is_progress()); + SASSERT(count_edges_with_rule(root, "fine-wilf n") == 3); + SASSERT(count_edges_with_rule(root, "fine-wilf m") == 2); + SASSERT(count_edges_with_rule(root, "fine-wilf elim L") == 2); + SASSERT(count_edges_with_rule(root, "fine-wilf elim R") == 2); + std::cout << " ok\n"; +} + +// (ab)^n·U = (ab)^m·V — SAME base: fine_wilf must not fire; NumCmp +// (priority 3) takes it with its two arith-split children. +static void test_fine_wilf_same_base_skipped() { + std::cout << "test_fine_wilf_same_base_skipped\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + arith_util arith(m); + seq_util seq(m); + + dummy_simple_solver solver; + seq::context_solver_i context_solver; + seq::nielsen_graph ng(sg, solver, context_solver); + ng.set_fine_wilf(true); // opt-in (smt.nseq.fine_wilf defaults to off) + + expr* n_e = m.mk_const(symbol("n"), arith.mk_int()); + expr* m_e = m.mk_const(symbol("m"), arith.mk_int()); + euf::snode const* pw_n = mk_ground_power(sg, seq, m, "ab", n_e); + euf::snode const* pw_m = mk_ground_power(sg, seq, m, "ab", m_e); + euf::snode const* u = sg.mk_var(symbol("U"), sg.get_str_sort()); + euf::snode const* v = sg.mk_var(symbol("V"), sg.get_str_sort()); + + ng.add_str_eq(sg.mk_concat(pw_n, u), sg.mk_concat(pw_m, v)); + seq::nielsen_node* root = ng.root(); + + VERIFY(ng.generate_extensions(root)); + SASSERT(root->outgoing().size() == 2); + SASSERT(count_edges_with_rule(root, "fine-wilf") == 0); + SASSERT(count_edges_with_rule(root, "power cmp") == 2); + for (seq::nielsen_edge const* e : root->outgoing()) + SASSERT(e->tgt()->is_arith_split()); + std::cout << " ok\n"; +} + +// smt.nseq.fine_wilf off (the default): the different-base power head falls +// back to the legacy const-num-unwinding peel (2 children). +static void test_fine_wilf_disabled_falls_through() { + std::cout << "test_fine_wilf_disabled_falls_through\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + arith_util arith(m); + seq_util seq(m); + + dummy_simple_solver solver; + seq::context_solver_i context_solver; + seq::nielsen_graph ng(sg, solver, context_solver); + ng.set_fine_wilf(false); + + expr* n_e = m.mk_const(symbol("n"), arith.mk_int()); + expr* m_e = m.mk_const(symbol("m"), arith.mk_int()); + euf::snode const* pw_ab = mk_ground_power(sg, seq, m, "ab", n_e); + euf::snode const* pw_ba = mk_ground_power(sg, seq, m, "ba", m_e); + euf::snode const* u = sg.mk_var(symbol("U"), sg.get_str_sort()); + euf::snode const* v = sg.mk_var(symbol("V"), sg.get_str_sort()); + + ng.add_str_eq(sg.mk_concat(pw_ab, u), sg.mk_concat(pw_ba, v)); + seq::nielsen_node* root = ng.root(); + + VERIFY(ng.generate_extensions(root)); + SASSERT(count_edges_with_rule(root, "fine-wilf") == 0); + SASSERT(count_edges_with_rule(root, "unwinding") == 2); + std::cout << " ok\n"; +} + +// Symbolic (variable) bases: x^n·U = y^m·V takes the symbolic path — +// one arith-split small-overlap child + the two cut-axiomatization +// children. Extending the arith-split child must NOT refire fine_wilf +// (the inherited m_fw_applied guard), falling through to the peel. +static void test_fine_wilf_symbolic_refire_guard() { + std::cout << "test_fine_wilf_symbolic_refire_guard\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + arith_util arith(m); + seq_util seq(m); + + dummy_simple_solver solver; + seq::context_solver_i context_solver; + seq::nielsen_graph ng(sg, solver, context_solver); + ng.set_fine_wilf(true); // opt-in (smt.nseq.fine_wilf defaults to off) + + expr* n_e = m.mk_const(symbol("n"), arith.mk_int()); + expr* m_e = m.mk_const(symbol("m"), arith.mk_int()); + euf::snode const* x = sg.mk_var(symbol("x"), sg.get_str_sort()); + euf::snode const* y = sg.mk_var(symbol("y"), sg.get_str_sort()); + const expr_ref pw_x_e(seq.str.mk_power(x->get_expr(), n_e), m); + const expr_ref pw_y_e(seq.str.mk_power(y->get_expr(), m_e), m); + euf::snode const* pw_x = sg.mk(pw_x_e); + euf::snode const* pw_y = sg.mk(pw_y_e); + euf::snode const* u = sg.mk_var(symbol("U"), sg.get_str_sort()); + euf::snode const* v = sg.mk_var(symbol("V"), sg.get_str_sort()); + + ng.add_str_eq(sg.mk_concat(pw_x, u), sg.mk_concat(pw_y, v)); + seq::nielsen_node* root = ng.root(); + + VERIFY(ng.generate_extensions(root)); + SASSERT(root->outgoing().size() == 3); + SASSERT(count_edges_with_rule(root, "fine-wilf small") == 1); + SASSERT(count_edges_with_rule(root, "fine-wilf elim L") == 1); + SASSERT(count_edges_with_rule(root, "fine-wilf elim R") == 1); + + // find the arith-split (case 1) child: same string constraints, guarded + seq::nielsen_node* small = nullptr; + for (seq::nielsen_edge* e : root->outgoing()) + if (strcmp(e->rule_name(), "fine-wilf small") == 0) + small = e->tgt(); + SASSERT(small && small->is_arith_split()); + + // the guard must divert the child to another modifier (the peel), not + // the identical fine-wilf split again + VERIFY(ng.generate_extensions(small)); + SASSERT(count_edges_with_rule(small, "fine-wilf") == 0); + SASSERT(small->outgoing().size() > 0); + std::cout << " ok\n"; +} + +// Solve-level: commuting roots are satisfiable (e.g. everything empty); +// the search must terminate through the fine-wilf children. +static void test_fine_wilf_solve_commuting_sat() { + std::cout << "test_fine_wilf_solve_commuting_sat\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + arith_util arith(m); + seq_util seq(m); + + dummy_simple_solver solver; + seq::context_solver_i context_solver; + seq::nielsen_graph ng(sg, solver, context_solver); + ng.set_fine_wilf(true); // opt-in (smt.nseq.fine_wilf defaults to off) + + expr* n_e = m.mk_const(symbol("n"), arith.mk_int()); + expr* m_e = m.mk_const(symbol("m"), arith.mk_int()); + euf::snode const* pw_ab = mk_ground_power(sg, seq, m, "ab", n_e); + euf::snode const* pw_abab = mk_ground_power(sg, seq, m, "abab", m_e); + euf::snode const* u = sg.mk_var(symbol("U"), sg.get_str_sort()); + euf::snode const* v = sg.mk_var(symbol("V"), sg.get_str_sort()); + + ng.add_str_eq(sg.mk_concat(pw_ab, u), sg.mk_concat(pw_abab, v)); + SASSERT(ng.solve() == seq::nielsen_graph::search_result::sat); std::cout << " ok\n"; } void tst_seq_nielsen() { + std::cout << std::unitbuf; // flush per write: locate crashes/assertions test_dep_tracker(); test_str_eq(); test_str_mem(); @@ -3951,4 +4228,12 @@ void tst_seq_nielsen() { test_simplify_unit_prefix_split(); test_simplify_unit_prefix_split_empty_rest(); test_simplify_unit_suffix_split(); + // Fine & Wilf overlap splitting (apply_fine_wilf, priority 3c) + test_fine_wilf_noncommuting_children(); + test_fine_wilf_commuting_children(); + test_fine_wilf_ground_prefix(); + test_fine_wilf_same_base_skipped(); + test_fine_wilf_disabled_falls_through(); + test_fine_wilf_symbolic_refire_guard(); + test_fine_wilf_solve_commuting_sat(); }