diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 6a2c730ca..7fdee401a 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -599,10 +599,11 @@ namespace seq {
return result;
}
- // Helper: render an snode as a human-readable label.
+ // Helper: render an snode as an HTML label for DOT output.
// Groups consecutive s_char tokens into quoted strings, renders s_var by name,
- // and falls back to mk_pp for other token kinds.
- static std::string snode_label(euf::snode const* n, ast_manager& m) {
+ // shows s_power with superscripts, s_unit by its inner expression,
+ // and falls back to mk_pp (HTML-escaped) for other token kinds.
+ static std::string snode_label_html(euf::snode const* n, ast_manager& m) {
if (!n) return "null";
seq_util seq(m);
@@ -621,7 +622,7 @@ namespace seq {
auto flush_chars = [&]() {
if (char_acc.empty()) return;
if (!first) result += " + ";
- result += "\"" + char_acc + "\"";
+ result += "\"" + dot_html_escape(char_acc) + "\"";
first = false;
char_acc.clear();
};
@@ -655,11 +656,33 @@ namespace seq {
if (!e) {
result += "#" + std::to_string(tok->id());
} else if (tok->is_var()) {
- result += to_app(e)->get_decl()->get_name().str();
+ result += dot_html_escape(to_app(e)->get_decl()->get_name().str());
+ } else if (tok->is_unit()) {
+ // seq.unit with non-literal character: show the character expression
+ expr* ch = to_app(e)->get_arg(0);
+ if (is_app(ch)) {
+ result += dot_html_escape(to_app(ch)->get_decl()->get_name().str());
+ } else {
+ std::ostringstream os;
+ os << mk_pp(ch, m);
+ result += dot_html_escape(os.str());
+ }
+ } else if (tok->is_power()) {
+ // seq.power(base, n): render as basen
+ std::string base_html = snode_label_html(tok->arg(0), m);
+ if (tok->arg(0)->length() > 1)
+ base_html = "(" + base_html + ")";
+ result += base_html;
+ result += "";
+ expr* exp_expr = to_app(e)->get_arg(1);
+ std::ostringstream os;
+ os << mk_pp(exp_expr, m);
+ result += dot_html_escape(os.str());
+ result += "";
} else {
std::ostringstream os;
os << mk_pp(e, m);
- result += os.str();
+ result += dot_html_escape(os.str());
}
}
flush_chars();
@@ -672,17 +695,17 @@ namespace seq {
// string equalities
for (auto const& eq : m_str_eq) {
if (!any) { out << "Cnstr:
"; any = true; }
- out << dot_html_escape(snode_label(eq.m_lhs, m))
+ out << snode_label_html(eq.m_lhs, m)
<< " = "
- << dot_html_escape(snode_label(eq.m_rhs, m))
+ << snode_label_html(eq.m_rhs, m)
<< "
";
}
// regex memberships
for (auto const& mem : m_str_mem) {
if (!any) { out << "Cnstr:
"; any = true; }
- out << dot_html_escape(snode_label(mem.m_str, m))
+ out << snode_label_html(mem.m_str, m)
<< " ∈ "
- << dot_html_escape(snode_label(mem.m_regex, m))
+ << snode_label_html(mem.m_regex, m)
<< "
";
}
// character ranges
@@ -790,9 +813,9 @@ namespace seq {
for (auto const& s : e->subst()) {
if (!first) out << "
";
first = false;
- out << dot_html_escape(snode_label(s.m_var, m))
+ out << snode_label_html(s.m_var, m)
<< " → " // mapping arrow
- << dot_html_escape(snode_label(s.m_replacement, m));
+ << snode_label_html(s.m_replacement, m);
}
for (auto const& cs : e->char_substs()) {
if (!first) out << "
";
@@ -861,8 +884,215 @@ namespace seq {
return false;
}
- simplify_result nielsen_node::simplify_and_init(nielsen_graph& g) {
+ // -----------------------------------------------------------------------
+ // Power simplification helpers (mirrors ZIPT's MergePowers,
+ // SimplifyPowerElim/CommPower, SimplifyPowerSingle)
+ // -----------------------------------------------------------------------
+
+ // Check if exponent b equals exponent a + diff for some rational constant diff.
+ // Uses syntactic matching on Z3 expression structure: pointer equality
+ // detects shared sub-expressions created during ConstNumUnwinding.
+ static bool get_const_power_diff(expr* b, expr* a, arith_util& arith, rational& diff) {
+ if (a == b) { diff = rational(0); return true; }
+ // b = (+ a k) ?
+ if (arith.is_add(b) && to_app(b)->get_num_args() == 2) {
+ rational val;
+ if (to_app(b)->get_arg(0) == a && arith.is_numeral(to_app(b)->get_arg(1), val))
+ { diff = val; return true; }
+ if (to_app(b)->get_arg(1) == a && arith.is_numeral(to_app(b)->get_arg(0), val))
+ { diff = val; return true; }
+ }
+ // a = (+ b k) → diff = -k
+ if (arith.is_add(a) && to_app(a)->get_num_args() == 2) {
+ rational val;
+ if (to_app(a)->get_arg(0) == b && arith.is_numeral(to_app(a)->get_arg(1), val))
+ { diff = -val; return true; }
+ if (to_app(a)->get_arg(1) == b && arith.is_numeral(to_app(a)->get_arg(0), val))
+ { diff = -val; return true; }
+ }
+ // b = (- a k) → diff = -k
+ if (arith.is_sub(b) && to_app(b)->get_num_args() == 2) {
+ rational val;
+ if (to_app(b)->get_arg(0) == a && arith.is_numeral(to_app(b)->get_arg(1), val))
+ { diff = -val; return true; }
+ }
+ // a = (- b k) → diff = k
+ if (arith.is_sub(a) && to_app(a)->get_num_args() == 2) {
+ rational val;
+ if (to_app(a)->get_arg(0) == b && arith.is_numeral(to_app(a)->get_arg(1), val))
+ { diff = val; return true; }
+ }
+ return false;
+ }
+
+ // Get the base expression of a power snode.
+ static expr* get_power_base_expr(euf::snode* power) {
+ if (!power || !power->is_power()) return nullptr;
+ expr* e = power->get_expr();
+ return (e && is_app(e) && to_app(e)->get_num_args() >= 2) ? to_app(e)->get_arg(0) : nullptr;
+ }
+
+ // Get the exponent expression of a power snode.
+ static expr* get_power_exp_expr(euf::snode* power) {
+ if (!power || !power->is_power()) return nullptr;
+ expr* e = power->get_expr();
+ return (e && is_app(e) && to_app(e)->get_num_args() >= 2) ? to_app(e)->get_arg(1) : nullptr;
+ }
+
+ // Merge adjacent tokens with the same power base on one side of an equation.
+ // Handles: char(c) · power(c^e) → power(c^(e+1)),
+ // power(c^e) · char(c) → power(c^(e+1)),
+ // power(c^e1) · power(c^e2) → power(c^(e1+e2)).
+ // Returns new snode if merging happened, nullptr otherwise.
+ static euf::snode* merge_adjacent_powers(euf::sgraph& sg, euf::snode* side) {
+ if (!side || side->is_empty() || side->is_token())
+ return nullptr;
+
+ euf::snode_vector tokens;
+ side->collect_tokens(tokens);
+ if (tokens.size() < 2) return nullptr;
+
+ ast_manager& m = sg.get_manager();
+ arith_util arith(m);
+ seq_util seq(m);
+
+ bool merged = false;
+ euf::snode_vector result;
+
+ unsigned i = 0;
+ while (i < tokens.size()) {
+ euf::snode* tok = tokens[i];
+
+ // Case 1: current is a power token — absorb following same-base tokens
+ if (tok->is_power()) {
+ expr* base_e = get_power_base_expr(tok);
+ expr* exp_acc = get_power_exp_expr(tok);
+ if (!base_e || !exp_acc) { result.push_back(tok); ++i; continue; }
+
+ bool local_merged = false;
+ unsigned j = i + 1;
+ while (j < tokens.size()) {
+ euf::snode* next = tokens[j];
+ if (next->is_power()) {
+ expr* nb = get_power_base_expr(next);
+ if (nb == base_e) {
+ exp_acc = arith.mk_add(exp_acc, get_power_exp_expr(next));
+ local_merged = true; ++j; continue;
+ }
+ }
+ if (next->is_char() && next->get_expr() == base_e) {
+ exp_acc = arith.mk_add(exp_acc, arith.mk_int(1));
+ local_merged = true; ++j; continue;
+ }
+ break;
+ }
+ if (local_merged) {
+ merged = true;
+ expr_ref new_pow(seq.str.mk_power(base_e, exp_acc), m);
+ result.push_back(sg.mk(new_pow));
+ } else {
+ result.push_back(tok);
+ }
+ i = j;
+ continue;
+ }
+
+ // Case 2: current is a char — check if next is a same-base power
+ if (tok->is_char() && tok->get_expr() && i + 1 < tokens.size()) {
+ euf::snode* next = tokens[i + 1];
+ if (next->is_power() && get_power_base_expr(next) == tok->get_expr()) {
+ expr* base_e = tok->get_expr();
+ // Use same arg order as Case 1: add(exp, 1), not add(1, exp),
+ // so that merging "c · c^e" and "c^e · c" both produce add(e, 1)
+ // and the resulting power expression is hash-consed identically.
+ expr* exp_acc = arith.mk_add(get_power_exp_expr(next), arith.mk_int(1));
+ unsigned j = i + 2;
+ while (j < tokens.size()) {
+ euf::snode* further = tokens[j];
+ if (further->is_power() && get_power_base_expr(further) == base_e) {
+ exp_acc = arith.mk_add(exp_acc, get_power_exp_expr(further));
+ ++j; continue;
+ }
+ if (further->is_char() && further->get_expr() == base_e) {
+ exp_acc = arith.mk_add(exp_acc, arith.mk_int(1));
+ ++j; continue;
+ }
+ break;
+ }
+ merged = true;
+ expr_ref new_pow(seq.str.mk_power(base_e, exp_acc), m);
+ result.push_back(sg.mk(new_pow));
+ i = j;
+ continue;
+ }
+ }
+
+ result.push_back(tok);
+ ++i;
+ }
+
+ if (!merged) return nullptr;
+
+ // Rebuild snode from merged token list
+ euf::snode* rebuilt = sg.mk_empty();
+ for (unsigned k = 0; k < result.size(); ++k) {
+ rebuilt = (k == 0) ? result[k] : sg.mk_concat(rebuilt, result[k]);
+ }
+ return rebuilt;
+ }
+
+ // Simplify constant-exponent powers: base^0 → ε, base^1 → base.
+ // Returns new snode if any simplification happened, nullptr otherwise.
+ static euf::snode* simplify_const_powers(euf::sgraph& sg, euf::snode* side) {
+ if (!side || side->is_empty()) return nullptr;
+
+ euf::snode_vector tokens;
+ side->collect_tokens(tokens);
+
+ ast_manager& m = sg.get_manager();
+ arith_util arith(m);
+
+ bool simplified = false;
+ euf::snode_vector result;
+
+ for (euf::snode* tok : tokens) {
+ if (tok->is_power()) {
+ expr* exp_e = get_power_exp_expr(tok);
+ rational val;
+ if (exp_e && arith.is_numeral(exp_e, val)) {
+ if (val.is_zero()) {
+ // base^0 → ε (skip this token entirely)
+ simplified = true;
+ continue;
+ }
+ if (val.is_one()) {
+ // base^1 → base
+ euf::snode* base_sn = tok->arg(0);
+ if (base_sn) {
+ result.push_back(base_sn);
+ simplified = true;
+ continue;
+ }
+ }
+ }
+ }
+ result.push_back(tok);
+ }
+
+ if (!simplified) return nullptr;
+
+ if (result.empty()) return sg.mk_empty();
+ euf::snode* rebuilt = result[0];
+ for (unsigned k = 1; k < result.size(); ++k)
+ rebuilt = sg.mk_concat(rebuilt, result[k]);
+ return rebuilt;
+ }
+
+ simplify_result nielsen_node::simplify_and_init(nielsen_graph& g, svector const& cur_path) {
euf::sgraph& sg = g.sg();
+ ast_manager& m = sg.get_manager();
+ arith_util arith(m);
+ seq_util seq(m);
bool changed = true;
while (changed) {
@@ -946,6 +1176,92 @@ namespace seq {
}
}
}
+
+ // pass 3: power simplification (mirrors ZIPT's LcpCompression +
+ // SimplifyPowerElim + SimplifyPowerSingle)
+ for (str_eq& eq : m_str_eq) {
+ if (eq.is_trivial() || !eq.m_lhs || !eq.m_rhs)
+ continue;
+
+ // 3a: simplify constant-exponent powers (base^0 → ε, base^1 → base)
+ if (euf::snode* s = simplify_const_powers(sg, eq.m_lhs))
+ { eq.m_lhs = s; changed = true; }
+ if (euf::snode* s = simplify_const_powers(sg, eq.m_rhs))
+ { eq.m_rhs = s; changed = true; }
+
+ // 3b: merge adjacent same-base tokens into combined powers
+ if (euf::snode* s = merge_adjacent_powers(sg, eq.m_lhs))
+ { eq.m_lhs = s; changed = true; }
+ if (euf::snode* s = merge_adjacent_powers(sg, eq.m_rhs))
+ { eq.m_rhs = s; changed = true; }
+
+ // 3c: power prefix elimination — when both sides start with a
+ // power of the same base, cancel the common power prefix.
+ // Mirrors ZIPT's SimplifyPowerElim + CommPower.
+ if (!eq.m_lhs || !eq.m_rhs) continue;
+ euf::snode* lh = eq.m_lhs->first();
+ euf::snode* rh = eq.m_rhs->first();
+ if (lh && rh && lh->is_power() && rh->is_power()) {
+ expr* lb = get_power_base_expr(lh);
+ expr* rb = get_power_base_expr(rh);
+ if (lb && rb && lb == rb) {
+ expr* lp = get_power_exp_expr(lh);
+ expr* rp = get_power_exp_expr(rh);
+ rational diff;
+ if (lp && rp && get_const_power_diff(rp, lp, arith, diff)) {
+ // rp = lp + diff (constant difference)
+ eq.m_lhs = sg.drop_first(eq.m_lhs);
+ eq.m_rhs = sg.drop_first(eq.m_rhs);
+ if (diff.is_pos()) {
+ // rp > lp: prepend base^diff to RHS
+ expr_ref de(arith.mk_int(diff), m);
+ expr_ref pw(seq.str.mk_power(lb, de), m);
+ eq.m_rhs = sg.mk_concat(sg.mk(pw), eq.m_rhs);
+ } else if (diff.is_neg()) {
+ // lp > rp: prepend base^(-diff) to LHS
+ expr_ref de(arith.mk_int(-diff), m);
+ expr_ref pw(seq.str.mk_power(lb, de), m);
+ eq.m_lhs = sg.mk_concat(sg.mk(pw), eq.m_lhs);
+ }
+ // diff == 0: both powers cancel completely
+ changed = true;
+ }
+ // 3d: LP-aware power prefix elimination
+ // When the exponent difference is non-constant, query the
+ // LP solver to determine which exponent is larger, and
+ // cancel deterministically. This avoids the branching
+ // that NumCmp would otherwise create, matching ZIPT's
+ // SimplifyPowerElim that calls node.IsLe()/node.IsLt().
+ else if (lp && rp && !cur_path.empty()) {
+ bool lp_le_rp = g.check_lp_le(lp, rp, this, cur_path);
+ bool rp_le_lp = g.check_lp_le(rp, lp, this, cur_path);
+ if (lp_le_rp || rp_le_lp) {
+ expr* smaller_exp = lp_le_rp ? lp : rp;
+ expr* larger_exp = lp_le_rp ? rp : lp;
+ eq.m_lhs = sg.drop_first(eq.m_lhs);
+ eq.m_rhs = sg.drop_first(eq.m_rhs);
+ if (lp_le_rp && rp_le_lp) {
+ // both ≤ → equal → both cancel completely
+ } else {
+ // strictly less: create diff power d = larger - smaller ≥ 1
+ expr_ref d(g.mk_fresh_int_var());
+ expr_ref one_e(arith.mk_int(1), m);
+ expr_ref zero_e(arith.mk_int(0), m);
+ expr_ref d_plus_smaller(arith.mk_add(d, smaller_exp), m);
+ // d ≥ 1 (strict inequality)
+ add_int_constraint(g.mk_int_constraint(d, one_e, int_constraint_kind::ge, eq.m_dep));
+ // d + smaller = larger
+ add_int_constraint(g.mk_int_constraint(d_plus_smaller, larger_exp, int_constraint_kind::eq, eq.m_dep));
+ expr_ref pw(seq.str.mk_power(lb, d), m);
+ euf::snode*& larger_side = lp_le_rp ? eq.m_rhs : eq.m_lhs;
+ larger_side = sg.mk_concat(sg.mk(pw), larger_side);
+ }
+ changed = true;
+ }
+ }
+ }
+ }
+ }
}
// consume leading concrete characters from str_mem via Brzozowski derivatives
@@ -1062,7 +1378,7 @@ namespace seq {
// Iterative deepening: increment by 1 on each failure.
// m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it.
- m_depth_bound = 3;
+ m_depth_bound = 10;
while (true) {
if (m_cancel_fn && m_cancel_fn()) {
#ifdef Z3DEBUG
@@ -1076,6 +1392,13 @@ namespace seq {
inc_run_idx();
svector cur_path;
search_result r = search_dfs(m_root, 0, cur_path);
+ IF_VERBOSE(1, verbose_stream() << "nseq iter=" << iter << " depth_bound=" << m_depth_bound
+ << " dfs_nodes=" << m_stats.m_num_dfs_nodes
+ << " max_depth=" << m_stats.m_max_depth
+ << " extensions=" << m_stats.m_num_extensions
+ << " arith_prune=" << m_stats.m_num_arith_infeasible
+ << " result=" << (r == search_result::sat ? "SAT" : r == search_result::unsat ? "UNSAT" : "UNKNOWN")
+ << "\n";);
if (r == search_result::sat) {
++m_stats.m_num_sat;
return r;
@@ -1084,10 +1407,8 @@ namespace seq {
++m_stats.m_num_unsat;
return r;
}
- // depth limit hit – increment bound by 1 and retry
- if (m_max_search_depth > 0 && m_depth_bound >= m_max_search_depth)
- break;
- ++m_depth_bound;
+ // depth limit hit – double the bound and retry
+ m_depth_bound *= 2;
}
++m_stats.m_num_unknown;
return search_result::unknown;
@@ -1116,7 +1437,7 @@ namespace seq {
node->set_eval_idx(m_run_idx);
// simplify constraints (idempotent after first call)
- simplify_result sr = node->simplify_and_init(*this);
+ simplify_result sr = node->simplify_and_init(*this, cur_path);
if (sr == simplify_result::conflict) {
++m_stats.m_num_simplify_conflict;
@@ -1133,6 +1454,7 @@ namespace seq {
// and verify they are jointly satisfiable using the LP solver
if (!cur_path.empty() && !check_int_feasibility(node, cur_path)) {
node->set_reason(backtrack_reason::arithmetic);
+ ++m_stats.m_num_arith_infeasible;
return search_result::unsat;
}
@@ -1851,10 +2173,15 @@ namespace seq {
if (!eq.m_lhs || !eq.m_rhs) continue;
euf::snode* lhead = eq.m_lhs->first();
euf::snode* rhead = eq.m_rhs->first();
- if (lhead && lhead->is_power() && rhead && rhead->is_char()) {
+ // Match power vs any non-variable, non-empty token (char, unit,
+ // power with different base, etc.).
+ // Same-base power vs power is handled by NumCmp (priority 3).
+ // Power vs variable is handled by PowerSplit (priority 11).
+ // Power vs empty is handled by PowerEpsilon (priority 2).
+ if (lhead && lhead->is_power() && rhead && !rhead->is_var() && !rhead->is_empty()) {
power = lhead; other_head = rhead; eq_out = &eq; return true;
}
- if (rhead && rhead->is_power() && lhead && lhead->is_char()) {
+ if (rhead && rhead->is_power() && lhead && !lhead->is_var() && !lhead->is_empty()) {
power = rhead; other_head = lhead; eq_out = &eq; return true;
}
}
@@ -1886,26 +2213,41 @@ namespace seq {
// -----------------------------------------------------------------------
// Modifier: apply_power_epsilon
- // For a power token u^n in an equation, branch:
+ // Fires only when one side of an equation is empty and the other side
+ // starts with a power token u^n. In that case, branch:
// (1) base u → ε (base is empty, so u^n = ε)
// (2) u^n → ε (the power is zero, replace power with empty)
- // mirrors ZIPT's PowerEpsilonModifier
+ // mirrors ZIPT's PowerEpsilonModifier (which requires LHS.IsEmpty())
// -----------------------------------------------------------------------
bool nielsen_graph::apply_power_epsilon(nielsen_node* node) {
- euf::snode *power = find_power_token(node);
+ // Match only when one equation side is empty and the other starts
+ // with a power. This mirrors ZIPT where PowerEpsilonModifier is
+ // constructed only inside the "if (LHS.IsEmpty())" branch of
+ // ExtendDir. When both sides are non-empty and a power faces a
+ // constant, ConstNumUnwinding (priority 4) handles it with both
+ // n=0 and n≥1 branches.
+ euf::snode* power = nullptr;
+ dep_tracker dep;
+ for (str_eq const& eq : node->str_eqs()) {
+ if (eq.is_trivial()) continue;
+ if (!eq.m_lhs || !eq.m_rhs) continue;
+ if (eq.m_lhs->is_empty() && eq.m_rhs->first() && eq.m_rhs->first()->is_power()) {
+ power = eq.m_rhs->first();
+ dep = eq.m_dep;
+ break;
+ }
+ if (eq.m_rhs->is_empty() && eq.m_lhs->first() && eq.m_lhs->first()->is_power()) {
+ power = eq.m_lhs->first();
+ dep = eq.m_dep;
+ break;
+ }
+ }
if (!power)
return false;
SASSERT(power->is_power() && power->num_args() >= 1);
euf::snode *base = power->arg(0);
- dep_tracker dep;
- for (str_eq const &eq : node->str_eqs()) {
- if (!eq.is_trivial()) {
- dep = eq.m_dep;
- break;
- }
- }
nielsen_node* child;
nielsen_edge* e;
@@ -1941,6 +2283,7 @@ namespace seq {
bool nielsen_graph::apply_num_cmp(nielsen_node* node) {
ast_manager& m = m_sg.get_manager();
arith_util arith(m);
+ seq_util& seq = m_sg.get_seq_util();
// Look for two power tokens with the same base on opposite sides
for (str_eq const& eq : node->str_eqs()) {
@@ -1954,35 +2297,68 @@ namespace seq {
// same base: compare the two powers
if (lhead->arg(0)->id() != rhead->arg(0)->id()) continue;
- // Get exponent expressions (m and n from u^m and u^n)
+ // Skip if the exponents differ by a constant — simplify_and_init's
+ // power prefix elimination already handles that case.
expr* exp_m = get_power_exponent(lhead);
expr* exp_n = get_power_exponent(rhead);
-
- // Branch 1: m <= n → cancel u^m from both sides
- // Side constraint: m <= n
- // After cancellation: ε·A = u^(n-m)·B
+ if (!exp_m || !exp_n) continue;
{
- nielsen_node* child = mk_child(node);
- nielsen_edge* e = mk_edge(node, child, true);
- nielsen_subst s(lhead, m_sg.mk_empty(), eq.m_dep);
- e->add_subst(s);
- child->apply_subst(m_sg, s);
- if (exp_m && exp_n)
- e->add_side_int(mk_int_constraint(exp_m, exp_n, int_constraint_kind::le, eq.m_dep));
+ rational diff;
+ if (get_const_power_diff(exp_n, exp_m, arith, diff))
+ continue; // handled by simplification
}
- // Branch 2: n < m → cancel u^n from both sides
- // Side constraint: n < m, i.e., n + 1 <= m, i.e., m >= n + 1
- // After cancellation: u^(m-n)·A = ε·B
+
+ expr* base_expr = get_power_base_expr(lhead);
+ if (!base_expr) continue;
+ expr* zero = arith.mk_int(0);
+ expr* one = arith.mk_int(1);
+
+ // Use fresh integer variables for the difference exponents to avoid
+ // LP solver issues when arith.mk_sub produces terms that simplify
+ // to constants after branch constraint propagation.
+
+ // Branch 1 (explored first): n < m → cancel u^n, leave u^d on LHS
+ // where d = m - n >= 1. Explored first because d≥1 means the
+ // difference power is non-empty, making progress in the equation.
{
+ expr_ref d(mk_fresh_int_var());
+ expr_ref diff_pow(seq.str.mk_power(base_expr, d), m);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
- nielsen_subst s(rhead, m_sg.mk_empty(), eq.m_dep);
- e->add_subst(s);
- child->apply_subst(m_sg, s);
- if (exp_m && exp_n) {
- expr_ref n_plus_1(arith.mk_add(exp_n, arith.mk_int(1)), m);
- e->add_side_int(mk_int_constraint(exp_m, n_plus_1, int_constraint_kind::ge, eq.m_dep));
- }
+ // u^n → ε
+ nielsen_subst s1(rhead, m_sg.mk_empty(), eq.m_dep);
+ e->add_subst(s1);
+ child->apply_subst(m_sg, s1);
+ // u^m → u^d
+ nielsen_subst s2(lhead, m_sg.mk(diff_pow), eq.m_dep);
+ e->add_subst(s2);
+ child->apply_subst(m_sg, s2);
+ // d >= 1
+ e->add_side_int(mk_int_constraint(d, one, int_constraint_kind::ge, eq.m_dep));
+ // d + n = m (defines d = m - n)
+ expr_ref d_plus_n(arith.mk_add(d, exp_n), m);
+ e->add_side_int(mk_int_constraint(d_plus_n, exp_m, int_constraint_kind::eq, eq.m_dep));
+ }
+ // Branch 2 (explored second): m <= n → cancel u^m, leave u^d on RHS
+ // where d = n - m >= 0
+ {
+ expr_ref d(mk_fresh_int_var());
+ expr_ref diff_pow(seq.str.mk_power(base_expr, d), m);
+ nielsen_node* child = mk_child(node);
+ nielsen_edge* e = mk_edge(node, child, true);
+ // u^m → ε
+ nielsen_subst s1(lhead, m_sg.mk_empty(), eq.m_dep);
+ e->add_subst(s1);
+ child->apply_subst(m_sg, s1);
+ // u^n → u^d
+ nielsen_subst s2(rhead, m_sg.mk(diff_pow), eq.m_dep);
+ e->add_subst(s2);
+ child->apply_subst(m_sg, s2);
+ // d >= 0
+ e->add_side_int(mk_int_constraint(d, zero, int_constraint_kind::ge, eq.m_dep));
+ // d + m = n (defines d = n - m)
+ expr_ref d_plus_m(arith.mk_add(d, exp_m), m);
+ e->add_side_int(mk_int_constraint(d_plus_m, exp_n, int_constraint_kind::eq, eq.m_dep));
}
return true;
}
@@ -2013,7 +2389,33 @@ namespace seq {
expr* zero = arith.mk_int(0);
expr* one = arith.mk_int(1);
- // Branch 1: n = 0 → replace power with ε (progress)
+ // Branch 1 (explored first): n >= 1 → peel one u: replace u^n with u · u^(n-1)
+ // Side constraint: n >= 1
+ // Create a proper nested power base^(n-1) instead of a fresh string variable.
+ // This preserves power structure so that simplify_and_init can merge and
+ // cancel adjacent same-base powers (mirroring ZIPT's SimplifyPowerUnwind).
+ // Explored first because the n≥1 branch is typically more productive
+ // for SAT instances (preserves power structure).
+ {
+ seq_util& seq = m_sg.get_seq_util();
+ expr* power_e = power->get_expr();
+ SASSERT(power_e);
+ expr* base_expr = to_app(power_e)->get_arg(0);
+ expr_ref n_minus_1(arith.mk_sub(exp_n, one), m);
+ expr_ref nested_pow(seq.str.mk_power(base_expr, n_minus_1), m);
+ euf::snode* nested_power_snode = m_sg.mk(nested_pow);
+
+ euf::snode* replacement = m_sg.mk_concat(base, nested_power_snode);
+ nielsen_node* child = mk_child(node);
+ nielsen_edge* e = mk_edge(node, child, false);
+ nielsen_subst s(power, replacement, eq->m_dep);
+ e->add_subst(s);
+ child->apply_subst(m_sg, s);
+ if (exp_n)
+ e->add_side_int(mk_int_constraint(exp_n, one, int_constraint_kind::ge, eq->m_dep));
+ }
+
+ // Branch 2 (explored second): n = 0 → replace power with ε (progress)
// Side constraint: n = 0
{
nielsen_node* child = mk_child(node);
@@ -2025,21 +2427,6 @@ namespace seq {
e->add_side_int(mk_int_constraint(exp_n, zero, int_constraint_kind::eq, eq->m_dep));
}
- // Branch 2: n >= 1 → peel one u: replace u^n with u · u^(n-1)
- // Side constraint: n >= 1
- // Use fresh power variable for u^(n-1)
- {
- euf::snode* fresh_power = mk_fresh_var();
- euf::snode* replacement = m_sg.mk_concat(base, fresh_power);
- nielsen_node* child = mk_child(node);
- nielsen_edge* e = mk_edge(node, child, false);
- nielsen_subst s(power, replacement, eq->m_dep);
- e->add_subst(s);
- child->apply_subst(m_sg, s);
- if (exp_n)
- e->add_side_int(mk_int_constraint(exp_n, one, int_constraint_kind::ge, eq->m_dep));
- }
-
return true;
}
@@ -2564,6 +2951,168 @@ namespace seq {
expr_ref nielsen_graph::int_constraint_to_expr(int_constraint const& ic) {
ast_manager& m = m_sg.get_manager();
arith_util arith(m);
+<<<<<<< Updated upstream
+=======
+
+ // If already mapped, return cached
+ unsigned eid = e->get_id();
+ lp::lpvar j;
+ if (m_expr2lpvar.find(eid, j))
+ return j;
+
+ // Check if this is a numeral — shouldn't be called with a numeral directly,
+ // but handle it gracefully by creating a fixed variable
+ rational val;
+ if (arith.is_numeral(e, val)) {
+ j = m_lp_solver->add_var(m_lp_ext_cnt++, true);
+ m_lp_solver->add_var_bound(j, lp::EQ, lp::mpq(val));
+ m_expr2lpvar.insert(eid, j);
+ return j;
+ }
+
+ // Decompose linear arithmetic: a + b → create LP term (1*a + 1*b)
+ expr* e1 = nullptr;
+ expr* e2 = nullptr;
+ if (arith.is_add(e, e1, e2)) {
+ lp::lpvar j1 = lp_ensure_var(e1);
+ lp::lpvar j2 = lp_ensure_var(e2);
+ if (j1 == lp::null_lpvar || j2 == lp::null_lpvar) return lp::null_lpvar;
+ vector> coeffs;
+ coeffs.push_back({lp::mpq(1), j1});
+ coeffs.push_back({lp::mpq(1), j2});
+ j = m_lp_solver->add_term(coeffs, m_lp_ext_cnt++);
+ m_expr2lpvar.insert(eid, j);
+ return j;
+ }
+
+ // Decompose: a - b → create LP term (1*a + (-1)*b)
+ if (arith.is_sub(e, e1, e2)) {
+ lp::lpvar j1 = lp_ensure_var(e1);
+ lp::lpvar j2 = lp_ensure_var(e2);
+ if (j1 == lp::null_lpvar || j2 == lp::null_lpvar) return lp::null_lpvar;
+ vector> coeffs;
+ coeffs.push_back({lp::mpq(1), j1});
+ coeffs.push_back({lp::mpq(-1), j2});
+ j = m_lp_solver->add_term(coeffs, m_lp_ext_cnt++);
+ m_expr2lpvar.insert(eid, j);
+ return j;
+ }
+
+ // Decompose: c * x where c is numeral → create LP term (c*x)
+ if (arith.is_mul(e, e1, e2)) {
+ rational coeff;
+ if (arith.is_numeral(e1, coeff)) {
+ lp::lpvar jx = lp_ensure_var(e2);
+ if (jx == lp::null_lpvar) return lp::null_lpvar;
+ vector> coeffs;
+ coeffs.push_back({lp::mpq(coeff), jx});
+ j = m_lp_solver->add_term(coeffs, m_lp_ext_cnt++);
+ m_expr2lpvar.insert(eid, j);
+ return j;
+ }
+ if (arith.is_numeral(e2, coeff)) {
+ lp::lpvar jx = lp_ensure_var(e1);
+ if (jx == lp::null_lpvar) return lp::null_lpvar;
+ vector> coeffs;
+ coeffs.push_back({lp::mpq(coeff), jx});
+ j = m_lp_solver->add_term(coeffs, m_lp_ext_cnt++);
+ m_expr2lpvar.insert(eid, j);
+ return j;
+ }
+ }
+
+ // Decompose: -x → create LP term (-1*x)
+ if (arith.is_uminus(e, e1)) {
+ lp::lpvar jx = lp_ensure_var(e1);
+ if (jx == lp::null_lpvar) return lp::null_lpvar;
+ vector> coeffs;
+ coeffs.push_back({lp::mpq(-1), jx});
+ j = m_lp_solver->add_term(coeffs, m_lp_ext_cnt++);
+ m_expr2lpvar.insert(eid, j);
+ return j;
+ }
+
+ // Leaf expression (variable, length, or other opaque term): map to fresh LP var
+ j = m_lp_solver->add_var(m_lp_ext_cnt++, true /* is_integer */);
+ m_expr2lpvar.insert(eid, j);
+ return j;
+ }
+
+ void nielsen_graph::lp_add_constraint(int_constraint const& ic) {
+ if (!m_lp_solver || !ic.m_lhs || !ic.m_rhs)
+ return;
+
+ ast_manager& m = m_sg.get_manager();
+ arith_util arith(m);
+
+ // We handle simple patterns:
+ // expr numeral → add_var_bound
+ // expr expr → create term (lhs - rhs) and bound to 0
+ rational val;
+ bool is_num_rhs = arith.is_numeral(ic.m_rhs, val);
+
+ if (is_num_rhs && (is_app(ic.m_lhs))) {
+ // Simple case: single variable or len(x) vs numeral
+ lp::lpvar j = lp_ensure_var(ic.m_lhs);
+ if (j == lp::null_lpvar) return;
+ lp::mpq rhs_val(val);
+ switch (ic.m_kind) {
+ case int_constraint_kind::eq:
+ m_lp_solver->add_var_bound(j, lp::EQ, rhs_val);
+ break;
+ case int_constraint_kind::le:
+ m_lp_solver->add_var_bound(j, lp::LE, rhs_val);
+ break;
+ case int_constraint_kind::ge:
+ m_lp_solver->add_var_bound(j, lp::GE, rhs_val);
+ break;
+ }
+ return;
+ }
+
+ // General case: create term lhs - rhs and bound it
+ // For now, handle single variable on LHS vs single variable on RHS
+ // (covers the common case of len(x) = len(y), n >= 0, etc.)
+ bool is_num_lhs = arith.is_numeral(ic.m_lhs, val);
+ if (is_num_lhs) {
+ // numeral expr → reverse and flip kind
+ lp::lpvar j = lp_ensure_var(ic.m_rhs);
+ if (j == lp::null_lpvar) return;
+ lp::mpq lhs_val(val);
+ switch (ic.m_kind) {
+ case int_constraint_kind::eq:
+ m_lp_solver->add_var_bound(j, lp::EQ, lhs_val);
+ break;
+ case int_constraint_kind::le:
+ // val <= rhs ⇔ rhs >= val
+ m_lp_solver->add_var_bound(j, lp::GE, lhs_val);
+ break;
+ case int_constraint_kind::ge:
+ // val >= rhs ⇔ rhs <= val
+ m_lp_solver->add_var_bound(j, lp::LE, lhs_val);
+ break;
+ }
+ return;
+ }
+
+ // Both sides are expressions: create term (lhs - rhs) with bound 0
+ lp::lpvar j_lhs = lp_ensure_var(ic.m_lhs);
+ lp::lpvar j_rhs = lp_ensure_var(ic.m_rhs);
+ if (j_lhs == lp::null_lpvar || j_rhs == lp::null_lpvar) return;
+
+ // If both sides map to the same LP variable, the constraint is
+ // trivially satisfied (lhs - rhs = 0). Skip to avoid the empty-term
+ // assertion in add_term.
+ if (j_lhs == j_rhs) return;
+
+ // Create a term: 1*lhs + (-1)*rhs
+ vector> coeffs;
+ coeffs.push_back({lp::mpq(1), j_lhs});
+ coeffs.push_back({lp::mpq(-1), j_rhs});
+ lp::lpvar term_j = m_lp_solver->add_term(coeffs, m_lp_ext_cnt++);
+
+ lp::mpq zero(0);
+>>>>>>> Stashed changes
switch (ic.m_kind) {
case int_constraint_kind::eq:
return expr_ref(m.mk_eq(ic.m_lhs, ic.m_rhs), m);
@@ -2626,6 +3175,61 @@ namespace seq {
return exp_snode ? exp_snode->get_expr() : nullptr;
}
+ bool nielsen_graph::check_lp_le(expr* a, expr* b, nielsen_node* node, svector const& cur_path) {
+ // Check if the path constraints entail a ≤ b.
+ // Strategy: add all constraints, then assert a > b (i.e. a - b ≥ 1).
+ // If infeasible, then a ≤ b is entailed.
+ //
+ // Uses fresh LP variables to avoid the add_term empty-term assertion
+ // that occurs when compound expressions share LP variables.
+ vector constraints;
+ collect_path_int_constraints(node, cur_path, constraints);
+ if (constraints.empty())
+ return false; // no constraints → can't determine
+
+ lp_solver_reset();
+ for (auto const& ic : constraints)
+ lp_add_constraint(ic);
+
+ // Create fresh LP variables to safely represent a - b ≥ 1
+ lp::lpvar fa = m_lp_solver->add_var(m_lp_ext_cnt++, true);
+ lp::lpvar fb = m_lp_solver->add_var(m_lp_ext_cnt++, true);
+
+ // fa = a (via fa - lp(a) = 0)
+ lp::lpvar ja = lp_ensure_var(a);
+ if (ja == lp::null_lpvar) return false;
+ if (fa != ja) {
+ vector> c1;
+ c1.push_back({lp::mpq(1), fa});
+ c1.push_back({lp::mpq(-1), ja});
+ lp::lpvar t1 = m_lp_solver->add_term(c1, m_lp_ext_cnt++);
+ m_lp_solver->add_var_bound(t1, lp::EQ, lp::mpq(0));
+ }
+
+ // fb = b (via fb - lp(b) = 0)
+ lp::lpvar jb = lp_ensure_var(b);
+ if (jb == lp::null_lpvar) return false;
+ if (fb != jb) {
+ vector> c2;
+ c2.push_back({lp::mpq(1), fb});
+ c2.push_back({lp::mpq(-1), jb});
+ lp::lpvar t2 = m_lp_solver->add_term(c2, m_lp_ext_cnt++);
+ m_lp_solver->add_var_bound(t2, lp::EQ, lp::mpq(0));
+ }
+
+ // Assert fa - fb ≥ 1 (i.e. a > b) using only fresh vars
+ {
+ vector> c3;
+ c3.push_back({lp::mpq(1), fa});
+ c3.push_back({lp::mpq(-1), fb});
+ lp::lpvar t3 = m_lp_solver->add_term(c3, m_lp_ext_cnt++);
+ m_lp_solver->add_var_bound(t3, lp::GE, lp::mpq(1));
+ }
+
+ lp::lp_status status = m_lp_solver->find_feasible_solution();
+ return status == lp::lp_status::INFEASIBLE; // a > b infeasible ⟹ a ≤ b
+ }
+
expr_ref nielsen_graph::mk_fresh_int_var() {
ast_manager& m = m_sg.get_manager();
arith_util arith(m);
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 1660be312..7beb16b38 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -613,8 +613,10 @@ namespace seq {
void apply_subst(euf::sgraph& sg, nielsen_subst const& s);
// simplify all constraints at this node and initialize status.
+ // cur_path provides the path from root to this node so that the
+ // LP solver can be queried for deterministic power cancellation.
// Returns proceed, conflict, satisfied, or restart.
- simplify_result simplify_and_init(nielsen_graph& g);
+ simplify_result simplify_and_init(nielsen_graph& g, svector const& cur_path);
// true if all str_eqs are trivial and there are no str_mems
bool is_satisfied() const;
@@ -660,6 +662,7 @@ namespace seq {
unsigned m_num_simplify_conflict = 0;
unsigned m_num_extensions = 0;
unsigned m_num_fresh_vars = 0;
+ unsigned m_num_arith_infeasible = 0;
unsigned m_max_depth = 0;
// modifier application counts
unsigned m_mod_det = 0;
@@ -681,6 +684,7 @@ namespace seq {
// the overall Nielsen transformation graph
// mirrors ZIPT's NielsenGraph
class nielsen_graph {
+ friend class nielsen_node;
euf::sgraph& m_sg;
region m_region;
ptr_vector m_nodes;
@@ -940,6 +944,10 @@ namespace seq {
// returns true if feasible, false if infeasible.
bool check_int_feasibility(nielsen_node* node, svector const& cur_path);
+ // check if path constraints entail a <= b.
+ // Strategy: add all path constraints + (a > b) and check for infeasibility.
+ bool check_lp_le(expr* a, expr* b, nielsen_node* node, svector const& cur_path);
+
// create an integer constraint: lhs rhs
int_constraint mk_int_constraint(expr* lhs, expr* rhs, int_constraint_kind kind, dep_tracker const& dep);
diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp
index c70afaf13..930749de3 100644
--- a/src/test/nseq_zipt.cpp
+++ b/src/test/nseq_zipt.cpp
@@ -598,75 +598,83 @@ static void test_zipt_parikh() {
static void test_tricky_str_equations() {
std::cout << "test_tricky_str_equations\n";
- // --- SAT: commutativity / rotation / symmetry ---
+ // ---------------------------------------------------------------
+ // SAT — Conjugacy equations: Xw₂ = w₁X
+ // SAT iff w₂ is a rotation of w₁. In that case w₁ = qp, w₂ = pq
+ // and X = (qp)^n · q is a family of solutions (n ≥ 0).
+ // All of these are UNSAT for X = ε (the ground parts don't match),
+ // so the solver must find a non-trivial witness.
+ // ---------------------------------------------------------------
- // XY = YX (classic commutativity; witness: X="ab", Y="abab")
- VERIFY(eq_sat("XY", "YX"));
+ // "ba" is a rotation of "ab" (p="b", q="a"). X = "a".
+ VERIFY(eq_sat("Xba", "abX"));
- // Xab = abX (X commutes with the word "ab"; witness: X="ab")
- VERIFY(eq_sat("Xab", "abX"));
+ // "cb" is a rotation of "bc" (p="c", q="b"). X = "b".
+ VERIFY(eq_sat("Xcb", "bcX"));
- // XaY = YaX (swap-symmetric; witness: X=Y=any, e.g. X=Y="b")
- VERIFY(eq_sat("XaY", "YaX"));
+ // "bca" is a rotation of "abc" (p="bc", q="a"). X = "a".
+ VERIFY(eq_sat("Xbca", "abcX"));
- // XYX = YXY (Markov-type; witness: X=Y)
- VERIFY(eq_sat("XYX", "YXY"));
+ // "cab" is a rotation of "abc" (p="c", q="ab"). X = "ab".
+ VERIFY(eq_sat("Xcab", "abcX"));
- // XYZ = ZYX (reverse-palindrome; witness: X="a",Y="b",Z="a")
- VERIFY(eq_sat("XYZ", "ZYX"));
+ // ---------------------------------------------------------------
+ // SAT — Power decomposition (ε NOT a solution)
+ // ---------------------------------------------------------------
- // XabY = YabX (rotation-like; witness: X="",Y="ab")
- VERIFY(eq_sat("XabY", "YabX"));
+ // XX = aa ⇒ X = "a". (ε gives "" ≠ "aa")
+ VERIFY(eq_sat("XX", "aa"));
- // aXYa = aYXa (cancel outer 'a'; reduces to XY=YX; witness: X=Y="")
- VERIFY(eq_sat("aXYa", "aYXa"));
+ // XbX = aba ⇒ 2|X| + 1 = 3 forces |X| = 1; X = "a".
+ // (ε gives "b" ≠ "aba")
+ VERIFY(eq_sat("XbX", "aba"));
- // XaXb = YaYb (both halves share variable; witness: X=Y)
- VERIFY(eq_sat("XaXb", "YaYb"));
+ // ---------------------------------------------------------------
+ // SAT — Multi-variable (ε NOT a solution)
+ // ---------------------------------------------------------------
- // abXba = Xabba (witness: X="" gives "abba"="abba")
- VERIFY(eq_sat("abXba", "Xabba"));
+ // X = "b", Y = "a" gives "baab" = "baab". (ε gives "ab" ≠ "ba")
+ VERIFY(eq_sat("XaYb", "bYaX"));
- // --- UNSAT: first-character mismatch ---
+ // X = "b", Y = "a" gives "abba" = "abba". (ε gives "ab" ≠ "ba")
+ VERIFY(eq_sat("abXY", "YXba"));
- // abXba = baXab (LHS starts 'a', RHS starts 'b')
- VERIFY(eq_unsat("abXba", "baXab"));
+ // ---------------------------------------------------------------
+ // UNSAT — Non-conjugate rotation
+ // Xw₂ = w₁X where w₂ is NOT a rotation of w₁.
+ // Heads are variable vs char, so never a trivial first-char clash.
+ // GPowerIntr introduces periodicity, then the period boundaries
+ // give a character mismatch.
+ // ---------------------------------------------------------------
- // XabX = XbaX (cancel X prefix/suffix → "ab"="ba"; 'a'≠'b')
- VERIFY(eq_unsat("XabX", "XbaX"));
+ // "cba" is the reverse of "abc", NOT a rotation.
+ // Rotations of "abc" are: abc, bca, cab.
+ VERIFY(eq_unsat("Xcba", "abcX"));
- // --- UNSAT: mismatch exposed after cancellation ---
+ // "acb" is a transposition of "abc", NOT a rotation.
+ VERIFY(eq_unsat("Xacb", "abcX"));
- // XaYb = XbYa (cancel X prefix → aYb=bYa; first char 'a'≠'b')
- VERIFY(eq_unsat("XaYb", "XbYa"));
+ // ---------------------------------------------------------------
+ // UNSAT — Induction via GPowerIntr
+ // One side starts with a variable that also appears on the other
+ // side behind a ground prefix → self-cycle. GPowerIntr forces
+ // periodicity; all period branches yield character mismatches.
+ // None of these has a trivial first-char or last-char clash.
+ // ---------------------------------------------------------------
- // XaYbX = XbYaX (cancel X prefix+suffix → aYb=bYa; first char 'a'≠'b')
- VERIFY(eq_unsat("XaYbX", "XbYaX"));
+ // Xa = bX: LHS head = X. Scan RHS: [b], X → self-cycle, base "b".
+ // X = b^n ⇒ b^n·a = b^{n+1} ⇒ last chars a ≠ b ⊥.
+ VERIFY(eq_unsat("Xa", "bX"));
- // XaXbX = XbXaX (cancel X prefix+suffix → aXb=bXa; first char 'a'≠'b')
- VERIFY(eq_unsat("XaXbX", "XbXaX"));
+ // acX = Xbc: RHS head = X. Scan LHS: [a,c], X → self-cycle, base "ac".
+ // X = (ac)^n ⇒ ac = bc ⊥ (a ≠ b).
+ // X = (ac)^n·a ⇒ aca = abc ⊥ (c ≠ b).
+ VERIFY(eq_unsat("acX", "Xbc"));
- // --- UNSAT: induction ---
-
- // aXb = Xba (forces X=a^n; final step requires a=b)
- VERIFY(eq_unsat("aXb", "Xba"));
-
- // XaY = YbX (a≠b; recursive unrolling forces a=b)
- VERIFY(eq_unsat("XaY", "YbX"));
-
- // --- UNSAT: length parity ---
-
- // XaX = YY (|XaX|=2|X|+1 is odd; |YY|=2|Y| is even)
- VERIFY(eq_unsat("XaX", "YY"));
-
- // XaaX = YbY (|XaaX|=2|X|+2 is even; |YbY|=2|Y|+1 is odd)
- VERIFY(eq_unsat("XaaX", "YbY"));
-
- // --- UNSAT: midpoint argument ---
-
- // XaX = YbY (equal length forces |X|=|Y|; midpoint position |X|
- // holds 'a' in LHS and 'b' in RHS, but 'a'≠'b')
- VERIFY(eq_unsat("XaX", "YbY"));
+ // bcX = Xab: RHS head = X. Scan LHS: [b,c], X → self-cycle, base "bc".
+ // X = (bc)^n ⇒ bc = ab ⊥ (b ≠ a).
+ // X = (bc)^n·b ⇒ bcb = bab ⊥ (c ≠ a).
+ VERIFY(eq_unsat("bcX", "Xab"));
std::cout << " ok\n";
}