From f4b04af6996b6e8fa624b7175586ab6d383fbed8 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 8 Jun 2026 18:17:29 +0000 Subject: [PATCH] Fix euf_seq_plugin class-aware simplifications --- src/ast/euf/euf_seq_plugin.cpp | 45 ++++++++++++++++--------- src/test/euf_seq_plugin.cpp | 60 ++++++++++++++++++++++++++++++++++ 2 files changed, 90 insertions(+), 15 deletions(-) diff --git a/src/ast/euf/euf_seq_plugin.cpp b/src/ast/euf/euf_seq_plugin.cpp index 7db7de370..feb544cc0 100644 --- a/src/ast/euf/euf_seq_plugin.cpp +++ b/src/ast/euf/euf_seq_plugin.cpp @@ -183,22 +183,22 @@ namespace euf { propagate_simplify(n); } - // Re-apply identity and absorption rules over all tracked concat nodes. - // This handles the case where the merge caused a child to become equivalent - // to an identity (ε) or absorbing element (∅) that was not known at - // registration time (e.g. b ~ "" discovered after concat(x, b) was registered). - // Also re-simplifies RE concat nodes when a child's root has become full_seq, - // to handle nullable absorption through nested concats: - // concat(.*, concat(v, w)) = concat(.*, w) when v is nullable but w is not. + // Re-apply identity and absorption rules over tracked concat nodes whose + // children are affected by this merge. This handles the case where a child + // becomes equivalent to an identity (ε) or absorbing element (∅) after + // registration (e.g. b ~ "" discovered after concat(x, b) was registered). + enode* merged_root = a->get_root(); for (enode* n : m_concats) { enode *na, *nb; - if (is_str_concat(n, na, nb)) { + if (is_str_concat(n, na, nb) && + (na->get_root() == merged_root || nb->get_root() == merged_root)) { if (is_str_empty(na)) push_merge(n, nb); else if (is_str_empty(nb)) push_merge(n, na); } - if (is_re_concat(n, na, nb)) { + if (is_re_concat(n, na, nb) && + (na->get_root() == merged_root || nb->get_root() == merged_root)) { if (is_re_epsilon(na)) push_merge(n, nb); else if (is_re_epsilon(nb)) @@ -207,8 +207,6 @@ namespace euf { push_merge(n, na); // absorb: concat(∅, b) = ∅ else if (is_re_empty(nb)) push_merge(n, nb); // absorb: concat(a, ∅) = ∅ - else if (is_full_seq(na->get_root()) || is_full_seq(nb->get_root())) - propagate_simplify(n); } } } @@ -270,11 +268,17 @@ namespace euf { // Rule 2: Nullable absorption by .* // concat(.*, v) = .* when v is nullable - if (is_full_seq(a) && is_nullable(b)) + auto find_full_seq = [this](enode* e) { + for (enode* c : enode_class(e)) + if (is_full_seq(c)) + return true; + return false; + }; + if (find_full_seq(a) && is_nullable(b)) push_merge(n, a); // concat(v, .*) = .* when v is nullable - if (is_nullable(a) && is_full_seq(b)) + if (is_nullable(a) && find_full_seq(b)) push_merge(n, b); // concat(.*, concat(v, w)) = concat(.*, w) when v nullable @@ -304,10 +308,21 @@ namespace euf { } bool seq_plugin::same_star_body(enode* a, enode* b) { - if (!is_star(a) || !is_star(b)) + enode* star_a = nullptr, *star_b = nullptr; + for (enode* c : enode_class(a)) + if (is_star(c)) { + star_a = c; + break; + } + for (enode* c : enode_class(b)) + if (is_star(c)) { + star_b = c; + break; + } + if (!star_a || !star_b) return false; // re.star(x) and re.star(y) have congruent bodies if x ~ y - return a->get_arg(0)->get_root() == b->get_arg(0)->get_root(); + return star_a->get_arg(0)->get_root() == star_b->get_arg(0)->get_root(); } bool seq_plugin::same_loop_body(enode* a, enode* b, diff --git a/src/test/euf_seq_plugin.cpp b/src/test/euf_seq_plugin.cpp index 05ef2dbf2..3f97c0e77 100644 --- a/src/test/euf_seq_plugin.cpp +++ b/src/test/euf_seq_plugin.cpp @@ -290,6 +290,64 @@ static void test_seq_plugin_loop_merge() { std::cout << g << "\n"; } +// test seq_plugin: star simplification should work when class contains a star +// but the concat children themselves are non-star representatives. +static void test_seq_plugin_star_merge_class_member() { + std::cout << "test_seq_plugin_star_merge_class_member\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + euf::egraph& g = sg.get_egraph(); + seq_util seq(m); + sort_ref str_sort(seq.str.mk_string_sort(), m); + sort_ref re_sort(seq.re.mk_re(str_sort), m); + + expr_ref x(m.mk_const("x", str_sort), m); + expr_ref v(m.mk_const("v", re_sort), m); + expr_ref star_x(seq.re.mk_star(seq.re.mk_to_re(x)), m); + expr_ref vv(seq.re.mk_concat(v, v), m); + + auto* nv = get_node(g, seq, v); + auto* nstar = get_node(g, seq, star_x); + auto* nvv = get_node(g, seq, vv); + g.propagate(); + + // v is equivalent to re.*(to_re(x)), so concat(v, v) should simplify to v. + g.merge(nv, nstar, nullptr); + g.propagate(); + SASSERT(nvv->get_root() == nv->get_root()); +} + +// test seq_plugin: nullable absorption by .* should work when .* is only +// present as a member of the equivalence class. +static void test_seq_plugin_full_seq_class_member() { + std::cout << "test_seq_plugin_full_seq_class_member\n"; + ast_manager m; + reg_decl_plugins(m); + euf::egraph eg(m); + euf::sgraph sg(m, eg); + euf::egraph& g = sg.get_egraph(); + seq_util seq(m); + sort_ref str_sort(seq.str.mk_string_sort(), m); + sort_ref re_sort(seq.re.mk_re(str_sort), m); + + expr_ref v(m.mk_const("v", re_sort), m); + expr_ref full(seq.re.mk_full_seq(str_sort), m); + expr_ref eps(seq.re.mk_epsilon(str_sort), m); + expr_ref veps(seq.re.mk_concat(v, eps), m); + + auto* nv = get_node(g, seq, v); + auto* nfull = get_node(g, seq, full); + auto* nveps = get_node(g, seq, veps); + g.propagate(); + + // v is equivalent to .*, and epsilon is nullable, so concat(v, epsilon) = v. + g.merge(nv, nfull, nullptr); + g.propagate(); + SASSERT(nveps->get_root() == nv->get_root()); +} + void tst_euf_seq_plugin() { s_var = 0; test_sgraph_basic(); s_var = 0; test_sgraph_backtrack(); @@ -300,4 +358,6 @@ void tst_euf_seq_plugin() { s_var = 0; test_sgraph_egraph_sync(); s_var = 0; test_seq_plugin_identity_after_merge(); s_var = 0; test_seq_plugin_loop_merge(); + s_var = 0; test_seq_plugin_star_merge_class_member(); + s_var = 0; test_seq_plugin_full_seq_class_member(); }