mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-21 09:29:35 +00:00
Code Activity

Don't add duplicate equations and membership constraints to Nielsen root

Browse source
This commit is contained in:
CEisenhofer 2026-05-06 16:38:26 +02:00
parent e62ba9b60b
commit 712cd68e8c
2 changed files with 21 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -460,12 +460,24 @@ namespace seq {
dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r)); dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
str_eq eq(lhs, rhs, dep); str_eq eq(lhs, rhs, dep);
eq.sort(); eq.sort();
// check if root node contains this equation already
if (std::ranges::any_of(m_root->str_eqs(), [&](const str_eq& e) {
return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs;
}))
// already present, no need to add again
return;
m_root->add_str_eq(eq); m_root->add_str_eq(eq);
} }
void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) { void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) {
if (!root()) if (!root())
create_root(); create_root();
// check if root node contains this membership constraint already
if (std::ranges::any_of(m_root->str_mems(), [&](const str_mem& e) {
return e.m_regex == regex && e.m_str == str;
}))
// already present, no need to add again
return;
dep_tracker dep = m_dep_mgr.mk_leaf(l); dep_tracker dep = m_dep_mgr.mk_leaf(l);
m_root->add_str_mem(str_mem(str, regex, dep)); m_root->add_str_mem(str_mem(str, regex, dep));
} }

9
src/smt/theory_nseq.cpp
View file

@ -992,6 +992,15 @@ namespace smt {
#ifdef Z3DEBUG #ifdef Z3DEBUG
std::cout << "Conflict with " << lits.size() << " literals and " << eqs.size() << " equalities" << std::endl; std::cout << "Conflict with " << lits.size() << " literals and " << eqs.size() << " equalities" << std::endl;
std::cout << "The root node contained " << m_nielsen.root()->str_mems().size() << " memberships and " << m_nielsen.root()->str_eqs().size() << " equalities" << std::endl; std::cout << "The root node contained " << m_nielsen.root()->str_mems().size() << " memberships and " << m_nielsen.root()->str_eqs().size() << " equalities" << std::endl;
unsigned idx = 0;
for (auto& eq : m_nielsen.root()->str_eqs()) {
std::cout << "[" << (idx++) << "]: " << seq::eq_pp(eq, m);
}
idx = 0;
for (auto& mem : m_nielsen.root()->str_mems()) {
std::cout << "[" << (idx++) << "]: " << seq::mem_pp(m, mem);
}
std::flush(std::cout);
#endif #endif
} }