mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

Fine & Wilf-based elimination of power-vs-power case (disabled by default for now)

Browse source
This commit is contained in:
CEisenhofer 2026-07-17 15:59:28 +02:00
parent 4f1f3ccc69
commit 3baad0f171
10 changed files with 961 additions and 164 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/params/smt_params.cpp
View file

@ -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);

1
src/params/smt_params.h
View file

@ -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;

1
src/params/smt_params_helper.pyg
View file

@ -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'),

383
src/smt/seq/seq_nielsen.cpp
View file

@ -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);

47
src/smt/seq/seq_nielsen.h
View file

@ -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<uint64_t> 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<nielsen_node> 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);

1
src/smt/theory_nseq.cpp
View file

@ -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);

3
src/test/CMakeLists.txt
View file

@ -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

3
src/test/main.cpp
View file

@ -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)

99
src/test/nseq_basic.cpp
View file

@ -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<seq::nielsen_edge> 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";
}

585
src/test/seq_nielsen.cpp
View file

@ -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<sat::literal>(bits1[0]));
SASSERT(std::get<sat::literal>(bits1[0]).index() == 5);
SASSERT(std::get<sat::literal>(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<sat::literal>(d)) {
const unsigned idx = std::get<sat::literal>(d).index();
if (idx == 3) has_3 = true;
if (idx == 11) has_11 = true;
const sat::literal l = std::get<sat::literal>(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<sat::literal>(d)) {
const unsigned idx = std::get<sat::literal>(d).index();
if (idx == 31) has31 = true;
if (idx == 32) has32 = true;
const sat::literal l = std::get<sat::literal>(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();
}