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 #8863 from Z3Prover/copilot/simplify-seq-nielsen-code

Browse source 
seq_nielsen: extract handle_empty_side() to eliminate duplicated empty-propagation logic
This commit is contained in:
Nikolaj Bjorner 2026-03-04 20:46:39 -08:00 • committed by GitHub
commit 1f203742cc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 38 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -514,6 +514,33 @@ namespace seq {
// nielsen_node: simplify_and_init
// -----------------------------------------------------------------------
bool nielsen_node::handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side,
dep_tracker const& dep, bool& changed) {
euf::snode_vector tokens;
non_empty_side->collect_tokens(tokens);
bool all_vars_or_opaque = true;
bool has_char = false;
for (euf::snode* t : tokens) {
if (t->is_char()) has_char = true;
else if (!t->is_var() && t->kind() != euf::snode_kind::s_other) {
all_vars_or_opaque = false; break;
}
}
if (has_char || !all_vars_or_opaque) {
m_is_general_conflict = true;
m_reason = backtrack_reason::symbol_clash;
return true;
}
for (euf::snode* t : tokens) {
if (t->is_var()) {
nielsen_subst s(t, sg.mk_empty(), dep);
apply_subst(sg, s);
changed = true;
}
}
return false;
}
simplify_result nielsen_node::simplify_and_init(nielsen_graph& g) {
euf::sgraph& sg = g.sg();
bool changed = true;
@ -556,53 +583,13 @@ namespace seq {
// one side empty, the other not empty => conflict or substitution
if (eq.m_lhs->is_empty() && !eq.m_rhs->is_empty()) {
euf::snode_vector tokens;
eq.m_rhs->collect_tokens(tokens);
bool all_vars_or_opaque = true;
bool has_char = false;
for (euf::snode* t : tokens) {
if (t->is_char()) has_char = true;
else if (!t->is_var() && t->kind() != euf::snode_kind::s_other) {
all_vars_or_opaque = false; break;
}
}
if (has_char || !all_vars_or_opaque) {
m_is_general_conflict = true;
m_reason = backtrack_reason::symbol_clash;
if (handle_empty_side(sg, eq.m_rhs, eq.m_dep, changed))
return simplify_result::conflict;
}
for (euf::snode* t : tokens) {
if (t->is_var()) {
nielsen_subst s(t, sg.mk_empty(), eq.m_dep);
apply_subst(sg, s);
changed = true;
}
}
continue;
}
if (eq.m_rhs->is_empty() && !eq.m_lhs->is_empty()) {
euf::snode_vector tokens;
eq.m_lhs->collect_tokens(tokens);
bool all_vars_or_opaque = true;
bool has_char = false;
for (euf::snode* t : tokens) {
if (t->is_char()) has_char = true;
else if (!t->is_var() && t->kind() != euf::snode_kind::s_other) {
all_vars_or_opaque = false; break;
}
}
if (has_char || !all_vars_or_opaque) {
m_is_general_conflict = true;
m_reason = backtrack_reason::symbol_clash;
if (handle_empty_side(sg, eq.m_lhs, eq.m_dep, changed))
return simplify_result::conflict;
}
for (euf::snode* t : tokens) {
if (t->is_var()) {
nielsen_subst s(t, sg.mk_empty(), eq.m_dep);
apply_subst(sg, s);
changed = true;
}
}
continue;
}

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

@ -502,6 +502,15 @@ namespace seq {
// render constraint set as an HTML fragment for DOT node labels.
// mirrors ZIPT's NielsenNode.ToHtmlString()
std::ostream& display_html(std::ostream& out, ast_manager& m) const;
private:
// Helper: handle one empty vs one non-empty side of a string equality.
// Collects tokens from non_empty_side; if any token causes a conflict
// (is a concrete character or an unexpected kind), sets conflict flags
// and returns true. Otherwise substitutes all variables to empty,
// sets changed=true, and returns false.
bool handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side,
dep_tracker const& dep, bool& changed);
};
// search statistics collected during Nielsen graph solving