mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Fix euf_seq_plugin class-aware simplifications

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-08 18:17:29 +00:00 • committed by GitHub
parent de4b5babb2
commit f4b04af699
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 90 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/ast/euf/euf_seq_plugin.cpp
View file

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

60
src/test/euf_seq_plugin.cpp
View file

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