mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-20 15:40:37 +00:00
Code Activity

Better tracking for debugging

Browse source
This commit is contained in:
CEisenhofer 2026-06-01 19:50:34 +02:00
parent 2da7c7b3db
commit 5b41c6eb9f
5 changed files with 153 additions and 116 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/ast/euf/euf_sgraph.cpp
View file

@ -677,33 +677,57 @@ namespace euf {
if (!re->has_projection())
return mk(m_rewriter.mk_derivative(ch, re_expr));
// Minimal language-preserving simplifications that never inspect a
// projection's arguments (so the opaque skolem and its inner state id
// are preserved for the oracle's r ∈ Q test).
// Language-preserving combinators that DISTRIBUTE over ite. The
// symbolic-character derivative of a regex is a linear form: a
// *top-level* ite dispatching on character predicates over the (single)
// symbolic char, with ordinary derivative regexes at the leaves. Both
// projection leaves (via wrap_proj) and projection-free subterms (via
// mk_derivative) already yield top-level ites; if the surrounding
// Boolean/concat operators did not push themselves into the ite leaves,
// the ite would end up *buried* (e.g. ~(ite(...)·Σ*)) where
// apply_regex_if_split — which only matches a top-level ite — can no
// longer resolve the symbolic char, stalling the constraint and causing
// unbounded variable unwinding. Distributing keeps the result a proper
// top-level linear form, exactly as the standard mk_derivative does.
// These combinators also fold the trivial regex identities so the
// projection skolem and its inner state id are preserved verbatim.
auto is_empty = [&](expr* r) { return m_seq.re.is_empty(r); };
auto is_full = [&](expr* r) { return m_seq.re.is_full_seq(r); };
auto is_eps = [&](expr* r) { return m_seq.re.is_epsilon(r); };
auto mk_union = [&](expr* x, expr* y) -> expr* {
auto is_ite = [&](expr* r, expr*& c, expr*& t, expr*& e) { return m.is_ite(r, c, t, e); };
std::function<expr*(expr*, expr*)> mk_union = [&](expr* x, expr* y) -> expr* {
expr *c = nullptr, *t = nullptr, *e = nullptr;
if (is_ite(x, c, t, e)) return m.mk_ite(c, mk_union(t, y), mk_union(e, y));
if (is_ite(y, c, t, e)) return m.mk_ite(c, mk_union(x, t), mk_union(x, e));
if (is_empty(x)) return y;
if (is_empty(y)) return x;
if (x == y) return x;
if (is_full(x) || is_full(y)) return m_seq.re.mk_full_seq(re_sort);
return m_seq.re.mk_union(x, y);
};
auto mk_inter = [&](expr* x, expr* y) -> expr* {
std::function<expr*(expr*, expr*)> mk_inter = [&](expr* x, expr* y) -> expr* {
expr *c = nullptr, *t = nullptr, *e = nullptr;
if (is_ite(x, c, t, e)) return m.mk_ite(c, mk_inter(t, y), mk_inter(e, y));
if (is_ite(y, c, t, e)) return m.mk_ite(c, mk_inter(x, t), mk_inter(x, e));
if (is_empty(x) || is_empty(y)) return m_seq.re.mk_empty(re_sort);
if (is_full(x)) return y;
if (is_full(y)) return x;
if (x == y) return x;
return m_seq.re.mk_inter(x, y);
};
auto mk_concat = [&](expr* x, expr* y) -> expr* {
std::function<expr*(expr*, expr*)> mk_concat = [&](expr* x, expr* y) -> expr* {
expr *c = nullptr, *t = nullptr, *e = nullptr;
if (is_ite(x, c, t, e)) return m.mk_ite(c, mk_concat(t, y), mk_concat(e, y));
if (is_ite(y, c, t, e)) return m.mk_ite(c, mk_concat(x, t), mk_concat(x, e));
if (is_empty(x) || is_empty(y)) return m_seq.re.mk_empty(re_sort);
if (is_eps(x)) return y;
if (is_eps(y)) return x;
return m_seq.re.mk_concat(x, y);
};
auto mk_compl = [&](expr* x) -> expr* {
std::function<expr*(expr*)> mk_compl = [&](expr* x) -> expr* {
expr *c = nullptr, *t = nullptr, *e = nullptr;
if (is_ite(x, c, t, e)) return m.mk_ite(c, mk_compl(t), mk_compl(e));
if (is_empty(x)) return m_seq.re.mk_full_seq(re_sort);
if (is_full(x)) return m_seq.re.mk_empty(re_sort);
expr* inner = nullptr;

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

@ -220,8 +220,8 @@ namespace seq {
// nielsen_edge
// -----------------------------------------------
nielsen_edge::nielsen_edge(nielsen_node* src, nielsen_node* tgt, const bool is_progress):
m_src(src), m_tgt(tgt),
nielsen_edge::nielsen_edge(nielsen_node* src, nielsen_node* tgt, const char* rule, const bool is_progress):
m_src(src), m_tgt(tgt), m_rule_name(rule),
m_is_progress(is_progress) { }
void nielsen_edge::add_subst(nielsen_subst const& s) {
@ -514,10 +514,11 @@ namespace seq {
return child;
}
nielsen_edge* nielsen_graph::mk_edge(nielsen_node* src, nielsen_node* tgt, const bool is_progress) {
nielsen_edge* nielsen_graph::mk_edge(nielsen_node *src, nielsen_node *tgt, const char *rule,
const bool is_progress) {
SASSERT(src != nullptr);
SASSERT(tgt != nullptr);
nielsen_edge* e = alloc(nielsen_edge, src, tgt, is_progress);
nielsen_edge* e = alloc(nielsen_edge, src, tgt, rule, is_progress);
m_edges.push_back(e);
src->add_outgoing(e);
return e;
@ -1707,6 +1708,29 @@ namespace seq {
}
}
// Empty-language check for *primitive* memberships whose regex contains a
// projection operator. The regex widening pass below skips primitives,
// and is_contradiction only fires once the string side is empty. But a
// cycle decomposition constrains the remainder x'' by ~((π(r)∩~ε)·Σ*),
// and deriving this through the cycle can collapse it to the empty
// language: e.g. ~(π(r)·Σ*) ≡ ∅ because π(r) is nullable (r ∈ F), so
// π(r)·Σ* ≡ Σ*. Such a constraint is unsatisfiable, but without this
// eager check the variable would be unwound depth-deep before the
// conflict surfaces — the source of the multi-cycle-SCC blow-up. The
// check is cheap: is_empty_bfs on these projection regexes settles in a
// couple of states (a nullable projection short-circuits to non-empty).
SASSERT(m_graph.m_seq_regex);
for (str_mem const& mem : m_str_mem) {
if (!mem.is_primitive() || !mem.m_regex->has_projection())
continue;
if (m_graph.m_seq_regex->is_empty_bfs(mem.m_regex) == l_true) {
TRACE(seq, tout << "empty primitive projection regex " << mem_pp(mem, m) << "\n");
set_general_conflict();
set_conflict(backtrack_reason::regex, mem.m_dep);
return simplify_result::conflict;
}
}
// remove trivial membership constraints once again
unsigned wj = 0;
for (unsigned j = 0; j < m_str_mem.size(); ++j) {
@ -1904,7 +1928,7 @@ namespace seq {
return search_result::unknown;
#ifdef Z3DEBUG
if (m_stats.m_num_dfs_nodes % 200 == 0) {
if (m_stats.m_num_dfs_nodes % 50 == 0) {
std::string dot = to_dot();
std::cout << "";
}
@ -2097,7 +2121,7 @@ namespace seq {
if (l->is_empty() || r->is_empty()) {
euf::snode* non_empty_side = l->is_empty() ? r : l;
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "det", true);
euf::snode_vector tokens;
non_empty_side->collect_tokens(tokens);
@ -2107,7 +2131,7 @@ namespace seq {
for (euf::snode* t : tokens) {
if (t->is_var()) {
nielsen_subst s(t, m_sg.mk_empty_seq(t->get_sort()), nullptr, eq.m_dep);
nielsen_subst s(t, m_sg.mk_empty_seq(t->get_sort()), eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
} else if (t->is_power()) {
@ -2115,7 +2139,7 @@ namespace seq {
expr* pow_base = nullptr, *pow_exp = nullptr;
if (seq().str.is_power(expr_node, pow_base, pow_exp) && pow_exp)
e->add_side_constraint(mk_constraint(a.mk_eq(pow_exp, a.mk_int(0)), eq.m_dep));
nielsen_subst s(t, m_sg.mk_empty_seq(t->get_sort()), nullptr, eq.m_dep);
nielsen_subst s(t, m_sg.mk_empty_seq(t->get_sort()), eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
}
@ -2140,7 +2164,7 @@ namespace seq {
break;
else if (lt->is_char_or_unit() && rt->is_char_or_unit()) {
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "det", true);
if (lt->is_char()) {
std::swap(lt, rt);
@ -2157,7 +2181,7 @@ namespace seq {
if (lt->is_char())
std::swap(lt, rt);
nielsen_subst subst(lt, rt, m_sg.mk(a.mk_int(1)), eq.m_dep);
nielsen_subst subst(lt, rt, eq.m_dep);
e->add_subst(subst);
child->apply_subst(m_sg, subst);
@ -2181,7 +2205,7 @@ namespace seq {
break;
else if (lt->is_char_or_unit() && rt->is_char_or_unit()) {
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "det", true);
euf::snode* lhs_rest = m_sg.drop_right(l, suffix + 1);
euf::snode* rhs_rest = m_sg.drop_right(r, suffix + 1);
@ -2192,7 +2216,7 @@ namespace seq {
if (lt->is_char())
std::swap(lt, rt);
nielsen_subst subst(lt, rt, nullptr, eq.m_dep);
nielsen_subst subst(lt, rt, eq.m_dep);
e->add_subst(subst);
child->apply_subst(m_sg, subst);
@ -2222,8 +2246,8 @@ namespace seq {
if (m.are_equal(base_head->get_expr(), other_head->get_expr())) continue;
// Directional base/head mismatch -> force exponent 0 and power -> ε.
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_subst s(pow_head, m_sg.mk_empty_seq(pow_head->get_sort()), nullptr, eq.m_dep);
nielsen_edge* e = mk_edge(node, child, "det", true);
nielsen_subst s(pow_head, m_sg.mk_empty_seq(pow_head->get_sort()), eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
expr* pow_exp = get_power_exp_expr(pow_head, m_seq);
@ -2377,11 +2401,9 @@ namespace seq {
}
euf::snode* tail = get_tail(var_node, compute_length_expr(prefix_sn).get(), fwd);
euf::snode* replacement = dir_concat(m_sg, prefix_sn, tail, fwd);
nielsen_subst s(var_node, replacement,
mk_rewrite(a.mk_sub(compute_length_expr(var_node), compute_length_expr(prefix_sn))),
eq.m_dep);
nielsen_subst s(var_node, replacement, eq.m_dep);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "det", true);
e->add_side_constraint(mk_constraint(a.mk_ge(compute_length_expr(tail), a.mk_int(0)), eq.m_dep));
e->add_subst(s);
child->apply_subst(m_sg, s);
@ -2412,8 +2434,8 @@ namespace seq {
if (var) {
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_subst s(var, def, nullptr, eq.m_dep);
nielsen_edge* e = mk_edge(node, child, "det", true);
nielsen_subst s(var, def, eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
return true;
@ -2439,8 +2461,8 @@ namespace seq {
euf::snode* var_head = lhead->is_var() ? lhead : (rhead->is_var() ? rhead : nullptr);
if (char_head && var_head) {
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
const nielsen_subst s1(var_head, m_sg.mk_empty_seq(var_head->get_sort()), nullptr, eq.m_dep);
nielsen_edge* e = mk_edge(node, child, "nielsen const 0", true);
const nielsen_subst s1(var_head, m_sg.mk_empty_seq(var_head->get_sort()), eq.m_dep);
e->add_subst(s1);
child->apply_subst(m_sg, s1);
@ -2448,9 +2470,9 @@ namespace seq {
euf::snode* tail = get_tail(var_head, a.mk_int(1), fwd);
euf::snode* replacement = dir_concat(m_sg, char_head, tail, fwd);
child = mk_child(node);
e = mk_edge(node, child, false);
e = mk_edge(node, child, "nielsen const >", false);
e->add_side_constraint(mk_constraint(a.mk_ge(compute_length_expr(tail), a.mk_int(0)), eq.m_dep));
const nielsen_subst s2(var_head, replacement, mk_rewrite(a.mk_sub(compute_length_expr(var_head), a.mk_int(1))), eq.m_dep);
const nielsen_subst s2(var_head, replacement, eq.m_dep);
e->add_subst(s2);
child->apply_subst(m_sg, s2);
return true;
@ -2478,16 +2500,16 @@ namespace seq {
// child 1: x → ε (progress)
{
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
const nielsen_subst s(lhead, m_sg.mk_empty_seq(lhead->get_sort()), nullptr, eq.m_dep);
nielsen_edge* e = mk_edge(node, child, "nielsen var =l", true);
const nielsen_subst s(lhead, m_sg.mk_empty_seq(lhead->get_sort()), eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
}
// child 2: y → ε (progress)
{
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
const nielsen_subst s(rhead, m_sg.mk_empty_seq(rhead->get_sort()), nullptr, eq.m_dep);
nielsen_edge* e = mk_edge(node, child, "nielsen var =r", true);
const nielsen_subst s(rhead, m_sg.mk_empty_seq(rhead->get_sort()), eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
}
@ -2495,10 +2517,8 @@ namespace seq {
{
euf::snode* replacement = dir_concat(m_sg, rhead, get_tail(lhead, compute_length_expr(rhead).get(), fwd), fwd);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
const nielsen_subst s(lhead, replacement,
mk_rewrite(a.mk_sub(compute_length_expr(lhead), compute_length_expr(rhead))),
eq.m_dep);
nielsen_edge* e = mk_edge(node, child, "nielsen var >", false);
const nielsen_subst s(lhead, replacement, eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
}
@ -2506,10 +2526,8 @@ namespace seq {
{
euf::snode* replacement = dir_concat(m_sg, lhead, get_tail(rhead, compute_length_expr(lhead).get(), fwd), fwd);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
const nielsen_subst s(rhead, replacement,
mk_rewrite(a.mk_sub(compute_length_expr(rhead), compute_length_expr(lhead))),
eq.m_dep);
nielsen_edge* e = mk_edge(node, child, "nielsen var <", false);
const nielsen_subst s(rhead, replacement, eq.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
}
@ -2754,7 +2772,7 @@ namespace seq {
// Create single progress child.
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "eq split", true);
// Remove the original equation and add the two new ones.
auto& eqs = child->str_eqs();
@ -3052,16 +3070,16 @@ namespace seq {
// This makes u^n = ε^n = ε for any n.
if (base->is_var()) {
child = mk_child(node);
e = mk_edge(node, child, true);
const nielsen_subst s1(base, m_sg.mk_empty_seq(base->get_sort()), nullptr, dep);
e = mk_edge(node, child, "power power 0", true);
const nielsen_subst s1(base, m_sg.mk_empty_seq(base->get_sort()), dep);
e->add_subst(s1);
child->apply_subst(m_sg, s1);
}
// Branch 2: replace the power token itself with ε (n = 0 semantics)
child = mk_child(node);
e = mk_edge(node, child, true);
const nielsen_subst s2(power, m_sg.mk_empty_seq(power->get_sort()), nullptr, dep);
e = mk_edge(node, child, "power base 0", true);
const nielsen_subst s2(power, m_sg.mk_empty_seq(power->get_sort()), dep);
e->add_subst(s2);
child->apply_subst(m_sg, s2);
@ -3108,13 +3126,13 @@ namespace seq {
// Branch 1 (explored first): n < m (add constraint c ≥ p + 1)
{
nielsen_edge *e = mk_edge(node, mk_child(node), true);
nielsen_edge *e = mk_edge(node, mk_child(node), "power cmp <", true);
const expr_ref n_plus_1(a.mk_add(exp_n, a.mk_int(1)), m);
e->add_side_constraint(mk_constraint(a.mk_ge(exp_m, n_plus_1), eq.m_dep));
}
// Branch 2 (explored second): m <= n (add constraint p ≥ c)
{
nielsen_edge *e = mk_edge(node, mk_child(node), true);
nielsen_edge *e = mk_edge(node, mk_child(node), "power cmp >=", true);
e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, exp_m), eq.m_dep));
}
return true;
@ -3174,13 +3192,13 @@ namespace seq {
// Branch 1: pow_exp < count (i.e., count >= pow_exp + 1)
{
nielsen_edge *e = mk_edge(node, mk_child(node), true);
nielsen_edge *e = mk_edge(node, mk_child(node), "power elim >", true);
const expr_ref pow_plus1(a.mk_add(pow_exp, a.mk_int(1)), m);
e->add_side_constraint(mk_constraint(a.mk_ge(norm_count, pow_plus1), eq.m_dep));
}
// Branch 2: count <= pow_exp (i.e., pow_exp >= count)
{
nielsen_edge *e = mk_edge(node, mk_child(node), true);
nielsen_edge *e = mk_edge(node, mk_child(node), "power elim <=", true);
e->add_side_constraint(mk_constraint(a.mk_ge(pow_exp, norm_count), eq.m_dep));
}
return true;
@ -3216,8 +3234,8 @@ namespace seq {
// Branch 1 (explored first): n = 0 → replace power with ε (progress)
// Side constraint: n = 0
nielsen_node *child = mk_child(node);
nielsen_edge *e = mk_edge(node, child, true);
const nielsen_subst s1(power, m_sg.mk_empty_seq(power->get_sort()), nullptr, eq->m_dep);
nielsen_edge *e = mk_edge(node, child, "unwinding 0", true);
const nielsen_subst s1(power, m_sg.mk_empty_seq(power->get_sort()), eq->m_dep);
e->add_subst(s1);
child->apply_subst(m_sg, s1);
if (exp_n)
@ -3240,8 +3258,8 @@ namespace seq {
euf::snode* replacement = dir_concat(m_sg, base, nested_power_snode, fwd);
child = mk_child(node);
e = mk_edge(node, child, true);
const nielsen_subst s2(power, replacement, nullptr, eq->m_dep);
e = mk_edge(node, child, "unwinding >", true);
const nielsen_subst s2(power, replacement, eq->m_dep);
e->add_subst(s2);
child->apply_subst(m_sg, s2);
if (exp_n)
@ -3374,7 +3392,7 @@ namespace seq {
SASSERT(tail);
nielsen_node* child = mk_child(node);
mk_edge(node, child, true);
mk_edge(node, child, "cycle subs", true);
auto& child_mems = child->str_mems();
for (unsigned k = 0; k < child_mems.size(); ++k) {
@ -3453,8 +3471,8 @@ namespace seq {
nielsen_node* child = mk_child(node);
SASSERT(child->m_str_mem[mi] == mem);
nielsen_edge* e = mk_edge(node, child, false);
const nielsen_subst s(x, xp_xpp, nullptr, mem.m_dep);
nielsen_edge* e = mk_edge(node, child, "cycle decomp", false);
const nielsen_subst s(x, xp_xpp, mem.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
@ -3486,6 +3504,9 @@ namespace seq {
<< " stabilizer=" << mk_pp(stabilizer_re->get_expr(), m)
<< " xpp_re=" << xpp_re << "\n");
#ifdef Z3DEBUG
std::string dot = partial_dfa_to_dot(mem.m_regex, false);
#endif
return true;
}
return false;
@ -3746,7 +3767,7 @@ namespace seq {
for (auto& [m_p, m_q, m_dep] : feasible) {
nielsen_node* child = mk_child(node);
mk_edge(node, child, true);
mk_edge(node, child, "regex fact", true);
// remove the original mem from child
auto& child_mems = child->str_mems();
@ -3881,8 +3902,8 @@ namespace seq {
replacement = prefix_sn ? dir_concat(m_sg, power_snode, prefix_sn, fwd) : power_snode;
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_subst s(var, replacement, nullptr, eq.m_dep); // TODO review - ensure var does not occur in replacement.
nielsen_edge* e = mk_edge(node, child, "power intr", true);
nielsen_subst s(var, replacement, eq.m_dep); // TODO review - ensure var does not occur in replacement.
e->add_subst(s);
child->apply_subst(m_sg, s);
@ -4035,7 +4056,7 @@ namespace seq {
for (unsigned branch = 0; branch < 2; ++branch) {
nielsen_node* child = mk_child(node);
mk_edge(node, child, true);
mk_edge(node, child, "signature split", true);
auto& child_eqs = child->str_eqs();
child_eqs[eq_idx] = child_eqs.back();
@ -4087,7 +4108,7 @@ namespace seq {
// No ite remaining: leaf → create child node with regex updated to r
euf::snode *new_regex_snode = m_sg.mk(r);
nielsen_node *child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "regex if", true);
for (const auto f : cs) {
e->add_side_constraint(constraint(f, mem.m_dep, m));
}
@ -4148,21 +4169,15 @@ namespace seq {
if (mem.is_primitive())
continue;
euf::snode* first = mem.m_str->first();
if (!first || !first->is_var())
continue;
// Compute minterms from the regex
euf::snode_vector minterms;
m_sg.compute_minterms(mem.m_regex, minterms);
VERIFY(!minterms.empty());
SASSERT(first);
// std::cout << "Considering regex: " << spp(mem.m_regex, m) << std::endl;
// Branch 1: x → ε (progress)
{
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
const nielsen_subst s(first, m_sg.mk_empty_seq(first->get_sort()), nullptr, mem.m_dep);
nielsen_edge* e = mk_edge(node, child, "regex var split", true);
const nielsen_subst s(first, m_sg.mk_empty_seq(first->get_sort()), mem.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
}
@ -4180,9 +4195,9 @@ namespace seq {
euf::snode* tail = get_tail(first, 1, true);
euf::snode* replacement = m_sg.mk_concat(fresh_char, tail);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
nielsen_edge* e = mk_edge(node, child, "regex var split", false);
const nielsen_subst s(first, replacement, mk_rewrite(a.mk_sub(compute_length_expr(first), a.mk_int(1))), mem.m_dep);
const nielsen_subst s(first, replacement, mem.m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
@ -4267,8 +4282,8 @@ namespace seq {
replacement = prefix_sn ? dir_concat(m_sg, power_m_sn, prefix_sn, fwd) : power_m_sn;
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_subst s(var_head, replacement, nullptr, eq->m_dep); // TODO review - ensure var does not occur in replacement.
nielsen_edge* e = mk_edge(node, child, "power split", true);
nielsen_subst s(var_head, replacement, eq->m_dep); // TODO review - ensure var does not occur in replacement.
e->add_subst(s);
child->apply_subst(m_sg, s);
@ -4291,10 +4306,8 @@ namespace seq {
{
euf::snode* replacement = dir_concat(m_sg, power, var_head, fwd);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
const nielsen_subst s(var_head, replacement,
mk_rewrite(a.mk_sub(compute_length_expr(var_head), compute_length_expr(power))),
eq->m_dep);
nielsen_edge* e = mk_edge(node, child, "power split", false);
const nielsen_subst s(var_head, replacement, eq->m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
}
@ -4331,8 +4344,8 @@ namespace seq {
// Side constraint: n = 0
{
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
const nielsen_subst s(power, m_sg.mk_empty_seq(power->get_sort()), nullptr, eq->m_dep);
nielsen_edge* e = mk_edge(node, child, "unwinding eq 0", true);
const nielsen_subst s(power, m_sg.mk_empty_seq(power->get_sort()), eq->m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, zero), eq->m_dep));
@ -4346,8 +4359,8 @@ namespace seq {
euf::snode* power_snode = m_sg.mk(power_expr);
euf::snode* replacement = dir_concat(m_sg, base, power_snode, fwd);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
const nielsen_subst s(power, replacement, nullptr, eq->m_dep); // TODO review - ensure var does not occur in replacement.
nielsen_edge* e = mk_edge(node, child, "unwinding eq >", false);
const nielsen_subst s(power, replacement, eq->m_dep); // TODO review - ensure var does not occur in replacement.
e->add_subst(s);
child->apply_subst(m_sg, s);
e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, one), eq->m_dep));
@ -4375,8 +4388,8 @@ namespace seq {
// Side constraint: n = 0
{
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
const nielsen_subst s(power, m_sg.mk_empty_seq(power->get_sort()), nullptr, mem->m_dep);
nielsen_edge* e = mk_edge(node, child, "unwinding mem 0", true);
const nielsen_subst s(power, m_sg.mk_empty_seq(power->get_sort()), mem->m_dep);
e->add_subst(s);
child->apply_subst(m_sg, s);
e->add_side_constraint(mk_constraint(a.mk_eq(exp_n, zero), mem->m_dep));
@ -4390,8 +4403,8 @@ namespace seq {
euf::snode* replacement = dir_concat(m_sg, base, power_snode, fwd);
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, false);
const nielsen_subst s(power, replacement, nullptr, mem->m_dep); // TODO review - ensure var does not occur in replacement.
nielsen_edge* e = mk_edge(node, child, "unwinding mem >", false);
const nielsen_subst s(power, replacement, mem->m_dep); // TODO review - ensure var does not occur in replacement.
e->add_subst(s);
child->apply_subst(m_sg, s);
e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, one), mem->m_dep));
@ -4433,7 +4446,7 @@ namespace seq {
// Branch 1: |u| < |v|
{
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "diseq I", true);
child->m_str_deq.pop_back();
expr_ref cmp(this->a.mk_lt(u_len, v_len), m);
m_rw(cmp);
@ -4442,7 +4455,7 @@ namespace seq {
// Branch 2: |v| < |u|
{
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "diseq II", true);
child->m_str_deq.pop_back();
expr_ref cmp(this->a.mk_lt(v_len, u_len), m);
m_rw(cmp);
@ -4451,7 +4464,7 @@ namespace seq {
// Branch 3: u = wau' && v = wbv' && |u'| = |v'| && a != b
{
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
nielsen_edge* e = mk_edge(node, child, "diseq III", true);
child->m_str_deq.pop_back();
child->add_str_eq(u_eq);
child->add_str_eq(v_eq);

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

@ -503,12 +503,11 @@ namespace seq {
struct nielsen_subst {
euf::snode* m_var;
euf::snode* m_replacement;
// euf::snode *m_length = nullptr; // representation of length if this is a sequence variable, null otherwise.
dep_tracker m_dep;
nielsen_subst(): m_var(nullptr), m_replacement(nullptr), m_dep(nullptr) {}
nielsen_subst(euf::snode* var, euf::snode* repl, euf::snode* length, dep_tracker const& dep):
m_var(var), m_replacement(repl)/*, m_length(length)*/, m_dep(dep) {
nielsen_subst(euf::snode* var, euf::snode* repl, dep_tracker const& dep):
m_var(var), m_replacement(repl), m_dep(dep) {
SASSERT(var != nullptr);
SASSERT(repl != nullptr);
// var may be s_var or s_power; sgraph::subst uses pointer identity matching
@ -582,15 +581,18 @@ namespace seq {
class nielsen_edge {
nielsen_node* m_src;
nielsen_node* m_tgt;
const char* const m_rule_name;
vector<nielsen_subst> m_subst;
vector<constraint> m_side_constraints; // side constraints: integer equalities/inequalities
bool m_is_progress; // does this edge represent progress?
bool m_len_constraints_computed = false; // lazily computed substitution length constraints
public:
nielsen_edge(nielsen_node* src, nielsen_node* tgt, bool is_progress);
nielsen_edge(nielsen_node* src, nielsen_node* tgt, const char* rule, bool is_progress);
nielsen_node* src() const { return m_src; }
nielsen_node* tgt() const { return m_tgt; }
const char* rule_name() const { return m_rule_name; }
void set_tgt(nielsen_node* tgt) { m_tgt = tgt; }
@ -989,7 +991,7 @@ namespace seq {
nielsen_node* mk_child(nielsen_node* parent);
// edge management
nielsen_edge* mk_edge(nielsen_node* src, nielsen_node* tgt, bool is_progress);
nielsen_edge* mk_edge(nielsen_node *src, nielsen_node *tgt, const char *rule, bool is_progress);
// root node access
nielsen_node* root() const { return m_root; }

8
src/smt/seq/seq_nielsen_pp.cpp
View file

@ -744,18 +744,16 @@ namespace seq {
out << " " << n->id() << " -> " << e->tgt()->id() << " [label=<";
// edge label: substitutions joined by <br/>
bool first = true;
out << "[" << e->rule_name() << "]";
for (auto const& s : e->subst()) {
if (!first) out << "<br/>";
first = false;
out << "<br/>";
out << snode_label_html(s.m_var, m)
<< " &#8594; " // mapping arrow
<< snode_label_html(s.m_replacement, m);
}
// side constraints: integer equalities/inequalities
for (auto const& ic : e->side_constraints()) {
if (!first) out << "<br/>";
first = false;
out << "<br/>";
out << "<font color=\"gray\">"
<< constraint_html(ic, names, next_id, m)
<< "</font>";

28
src/test/seq_nielsen.cpp
View file

@ -156,20 +156,20 @@ static void test_nielsen_subst() {
euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
seq::dep_tracker dep = nullptr;
seq::nielsen_subst s1(x, a, nullptr, dep);
seq::nielsen_subst s1(x, a, dep);
SASSERT(s1.is_eliminating());
// eliminating substitution: x -> empty
seq::nielsen_subst s2(x, e, nullptr, dep);
seq::nielsen_subst s2(x, e, dep);
SASSERT(s2.is_eliminating());
// non-eliminating substitution: x -> concat(A, x)
euf::snode* ax = sg.mk_concat(a, x);
seq::nielsen_subst s3(x, ax, nullptr, dep);
seq::nielsen_subst s3(x, ax, dep);
SASSERT(!s3.is_eliminating());
// eliminating substitution: x -> y (x not in y)
seq::nielsen_subst s4(x, y, nullptr, dep);
seq::nielsen_subst s4(x, y, dep);
SASSERT(s4.is_eliminating());
}
@ -243,8 +243,8 @@ static void test_nielsen_edge() {
seq::nielsen_node* child = ng.mk_child(parent);
// create edge with substitution x -> A
seq::nielsen_edge* edge = ng.mk_edge(parent, child, true);
edge->add_subst(seq::nielsen_subst(x, a, nullptr, dep));
seq::nielsen_edge* edge = ng.mk_edge(parent, child, "test", true);
edge->add_subst(seq::nielsen_subst(x, a, dep));
SASSERT(edge->src() == parent);
SASSERT(edge->tgt() == child);
@ -322,7 +322,7 @@ static void test_nielsen_subst_apply() {
node->add_str_eq(seq::str_eq(xa, by, dep));
// apply substitution x -> empty
seq::nielsen_subst s(x, e, nullptr, dep);
seq::nielsen_subst s(x, e, dep);
node->apply_subst(sg, s);
// after x -> empty: lhs should be just A, rhs still concat(B, y)
@ -385,17 +385,17 @@ static void test_nielsen_expansion() {
// branch 1: x -> eps (eliminating, progress)
euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
seq::nielsen_node* child1 = ng.mk_child(root);
seq::nielsen_subst s1(x, e, nullptr, dep);
seq::nielsen_subst s1(x, e, dep);
child1->apply_subst(sg, s1);
seq::nielsen_edge* edge1 = ng.mk_edge(root, child1, true);
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* ax = sg.mk_concat(a, x);
seq::nielsen_node* child2 = ng.mk_child(root);
seq::nielsen_subst s2(x, ax, nullptr, dep);
seq::nielsen_subst s2(x, ax, dep);
child2->apply_subst(sg, s2);
seq::nielsen_edge* edge2 = ng.mk_edge(root, child2, false);
seq::nielsen_edge* edge2 = ng.mk_edge(root, child2, "test", false);
edge2->add_subst(s2);
SASSERT(ng.num_nodes() == 3);
@ -3584,7 +3584,7 @@ static void test_subst_does_not_propagate_bounds_single_var() {
// apply substitution x → a·y
euf::snode* ay = sg.mk_concat(a, y);
seq::nielsen_subst s(x, ay, nullptr, dep);
seq::nielsen_subst s(x, ay, dep);
node->apply_subst(sg, s);
// No local propagation anymore: y keeps conservative defaults.
@ -3619,7 +3619,7 @@ static void test_subst_no_immediate_bound_conflict() {
// apply substitution x → a·b (no eager bound check at this stage)
euf::snode* ab = sg.mk_concat(a, b);
seq::nielsen_subst s(x, ab, nullptr, dep);
seq::nielsen_subst s(x, ab, dep);
node->apply_subst(sg, s);
SASSERT(!node->is_general_conflict());
@ -3752,7 +3752,7 @@ static void test_subst_does_not_propagate_bounds_multi_var() {
// apply substitution x → y·z (two vars, no constants)
euf::snode* yz = sg.mk_concat(y, z);
seq::nielsen_subst s(x, yz, nullptr, dep);
seq::nielsen_subst s(x, yz, dep);
node->apply_subst(sg, s);
SASSERT(queried_ub(node, y) == UINT_MAX);