mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 13:54:53 +00:00
Code Activity

Merge pull request #8860 from Z3Prover/copilot/fix-c3-branch-issue

Browse source 
Remove unimplemented `is_subsumed_by` from `nielsen_node` and tests
This commit is contained in:
Nikolaj Bjorner 2026-03-04 13:04:47 -08:00 • committed by GitHub
commit e3d592becb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 177 deletions
Download patch file Download diff file Expand all files Collapse all files

177
src/test/seq_nielsen.cpp
View file

@ -1529,177 +1529,6 @@ static void test_solve_eval_idx_tracking() {
SASSERT(root->eval_idx() == ng.run_idx());
}
// test is_subsumed_by: node with superset of constraints is subsumed
static void test_is_subsumed_by_basic() {
std::cout << "test_is_subsumed_by_basic\n";
ast_manager m;
reg_decl_plugins(m);
euf::egraph eg(m);
euf::sgraph sg(m, eg);
seq::nielsen_graph ng(sg);
euf::snode* x = sg.mk_var(symbol("x"));
euf::snode* y = sg.mk_var(symbol("y"));
euf::snode* z = sg.mk_var(symbol("z"));
seq::dep_tracker dep(4, 0);
// node1 has {x=y, x=z}
seq::nielsen_node* n1 = ng.mk_node();
n1->add_str_eq(seq::str_eq(x, y, dep));
n1->add_str_eq(seq::str_eq(x, z, dep));
// node2 has {x=y} (subset of node1)
seq::nielsen_node* n2 = ng.mk_node();
n2->add_str_eq(seq::str_eq(x, y, dep));
// n1 is subsumed by n2 (n2's constraints are a subset of n1's)
SASSERT(n1->is_subsumed_by(*n2));
// n2 is NOT subsumed by n1 (n1 has x=z which n2 doesn't)
SASSERT(!n2->is_subsumed_by(*n1));
}
// test is_subsumed_by: trivial equations are skipped
static void test_is_subsumed_by_trivial_skip() {
std::cout << "test_is_subsumed_by_trivial_skip\n";
ast_manager m;
reg_decl_plugins(m);
euf::egraph eg(m);
euf::sgraph sg(m, eg);
seq::nielsen_graph ng(sg);
euf::snode* x = sg.mk_var(symbol("x"));
euf::snode* y = sg.mk_var(symbol("y"));
euf::snode* e = sg.mk_empty();
seq::dep_tracker dep(4, 0);
// node1 has {x=y}
seq::nielsen_node* n1 = ng.mk_node();
n1->add_str_eq(seq::str_eq(x, y, dep));
// node2 has {x=y, ε=ε} (extra trivial eq)
seq::nielsen_node* n2 = ng.mk_node();
n2->add_str_eq(seq::str_eq(x, y, dep));
n2->add_str_eq(seq::str_eq(e, e, dep));
// n1 is subsumed by n2 (n2's non-trivial constraints ⊆ n1's)
SASSERT(n1->is_subsumed_by(*n2));
// n2 is also subsumed by n1 (n1's constraints ⊆ n2's)
SASSERT(n2->is_subsumed_by(*n1));
}
// test is_subsumed_by: non-matching constraints
static void test_is_subsumed_by_no_match() {
std::cout << "test_is_subsumed_by_no_match\n";
ast_manager m;
reg_decl_plugins(m);
euf::egraph eg(m);
euf::sgraph sg(m, eg);
seq::nielsen_graph ng(sg);
euf::snode* x = sg.mk_var(symbol("x"));
euf::snode* y = sg.mk_var(symbol("y"));
euf::snode* z = sg.mk_var(symbol("z"));
seq::dep_tracker dep(4, 0);
// node1 has {x=y}
seq::nielsen_node* n1 = ng.mk_node();
n1->add_str_eq(seq::str_eq(x, y, dep));
// node2 has {x=z} (different constraint)
seq::nielsen_node* n2 = ng.mk_node();
n2->add_str_eq(seq::str_eq(x, z, dep));
SASSERT(!n1->is_subsumed_by(*n2));
SASSERT(!n2->is_subsumed_by(*n1));
}
// test is_subsumed_by: identical constraint sets
static void test_is_subsumed_by_exact_match() {
std::cout << "test_is_subsumed_by_exact_match\n";
ast_manager m;
reg_decl_plugins(m);
euf::egraph eg(m);
euf::sgraph sg(m, eg);
seq::nielsen_graph ng(sg);
euf::snode* x = sg.mk_var(symbol("x"));
euf::snode* y = sg.mk_var(symbol("y"));
seq::dep_tracker dep(4, 0);
seq::nielsen_node* n1 = ng.mk_node();
n1->add_str_eq(seq::str_eq(x, y, dep));
seq::nielsen_node* n2 = ng.mk_node();
n2->add_str_eq(seq::str_eq(x, y, dep));
// identical sets: mutual subsumption
SASSERT(n1->is_subsumed_by(*n2));
SASSERT(n2->is_subsumed_by(*n1));
}
// test is_subsumed_by with str_mem constraints
static void test_is_subsumed_by_str_mem() {
std::cout << "test_is_subsumed_by_str_mem\n";
ast_manager m;
reg_decl_plugins(m);
euf::egraph eg(m);
euf::sgraph sg(m, eg);
seq_util seq(m);
sort_ref str_sort(seq.str.mk_string_sort(), m);
seq::nielsen_graph ng(sg);
euf::snode* x = sg.mk_var(symbol("x"));
euf::snode* e = sg.mk_empty();
expr_ref re_all(seq.re.mk_full_seq(str_sort), m);
euf::snode* regex = sg.mk(re_all);
seq::dep_tracker dep(4, 0);
// node1 has {x ∈ re_all, x=x_eq}
seq::nielsen_node* n1 = ng.mk_node();
n1->add_str_mem(seq::str_mem(x, regex, e, 0, dep));
euf::snode* y = sg.mk_var(symbol("y"));
n1->add_str_eq(seq::str_eq(x, y, dep));
// node2 has {x ∈ re_all} only (subset)
seq::nielsen_node* n2 = ng.mk_node();
n2->add_str_mem(seq::str_mem(x, regex, e, 0, dep));
SASSERT(n1->is_subsumed_by(*n2));
SASSERT(!n2->is_subsumed_by(*n1));
}
// test is_subsumed_by: empty node subsumes everything
static void test_is_subsumed_by_empty() {
std::cout << "test_is_subsumed_by_empty\n";
ast_manager m;
reg_decl_plugins(m);
euf::egraph eg(m);
euf::sgraph sg(m, eg);
seq::nielsen_graph ng(sg);
euf::snode* x = sg.mk_var(symbol("x"));
euf::snode* y = sg.mk_var(symbol("y"));
seq::dep_tracker dep(4, 0);
// node1 has {x=y}
seq::nielsen_node* n1 = ng.mk_node();
n1->add_str_eq(seq::str_eq(x, y, dep));
// node2 is empty
seq::nielsen_node* n2 = ng.mk_node();
// n1 is subsumed by empty n2 (empty set is subset of everything)
SASSERT(n1->is_subsumed_by(*n2));
// n2 is NOT subsumed by n1 (n1 has x=y which n2 doesn't)
SASSERT(!n2->is_subsumed_by(*n1));
}
// -----------------------------------------------------------------------
// Direct simplify_and_init tests
@ -3332,12 +3161,6 @@ void tst_seq_nielsen() {
test_solve_mixed_eq_mem_sat();
test_solve_children_failed_reason();
test_solve_eval_idx_tracking();
test_is_subsumed_by_basic();
test_is_subsumed_by_trivial_skip();
test_is_subsumed_by_no_match();
test_is_subsumed_by_exact_match();
test_is_subsumed_by_str_mem();
test_is_subsumed_by_empty();
test_simplify_prefix_cancel();
test_simplify_symbol_clash();
test_simplify_empty_propagation();