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

Canceling out common variables is a simplification step now

Browse source
This commit is contained in:
CEisenhofer 2026-03-05 18:17:04 +01:00
parent 272000a466
commit 5a95b40bdb
1 changed files with 14 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -618,26 +618,11 @@ namespace seq {
changed = true; changed = true;
} }
// pass 2: detect symbol clashes and empty-propagation // pass 2: detect symbol clashes, empty-propagation, and prefix cancellation
for (str_eq& eq : m_str_eq) { for (str_eq& eq : m_str_eq) {
if (!eq.m_lhs || !eq.m_rhs) if (!eq.m_lhs || !eq.m_rhs)
continue; continue;
// both sides start with a concrete character: check match
if (eq.m_lhs->is_char() && eq.m_rhs->is_char()) {
if (eq.m_lhs->id() != eq.m_rhs->id()) {
// symbol clash
m_is_general_conflict = true;
m_reason = backtrack_reason::symbol_clash;
return simplify_result::conflict;
}
// same char: drop from both sides
eq.m_lhs = sg.drop_first(eq.m_lhs);
eq.m_rhs = sg.drop_first(eq.m_rhs);
changed = true;
continue;
}
// one side empty, the other not empty => conflict or substitution // one side empty, the other not empty => conflict or substitution
if (eq.m_lhs->is_empty() && !eq.m_rhs->is_empty()) { if (eq.m_lhs->is_empty() && !eq.m_rhs->is_empty()) {
if (handle_empty_side(sg, eq.m_rhs, eq.m_dep, changed)) if (handle_empty_side(sg, eq.m_rhs, eq.m_dep, changed))
@ -650,20 +635,28 @@ namespace seq {
continue; continue;
} }
// prefix matching: lhs and rhs both start with the same char => cancel // prefix cancellation: strip any common leading tokens.
// Same char or same variable on both sides can always be cancelled.
// Two different concrete characters is a symbol clash.
{ {
euf::snode_vector lhs_toks, rhs_toks; euf::snode_vector lhs_toks, rhs_toks;
eq.m_lhs->collect_tokens(lhs_toks); eq.m_lhs->collect_tokens(lhs_toks);
eq.m_rhs->collect_tokens(rhs_toks); eq.m_rhs->collect_tokens(rhs_toks);
unsigned prefix = 0; unsigned prefix = 0;
while (prefix < lhs_toks.size() && prefix < rhs_toks.size() && while (prefix < lhs_toks.size() && prefix < rhs_toks.size()) {
lhs_toks[prefix]->is_char() && rhs_toks[prefix]->is_char()) { euf::snode* lt = lhs_toks[prefix];
if (lhs_toks[prefix]->id() != rhs_toks[prefix]->id()) { euf::snode* rt = rhs_toks[prefix];
if (lt->id() == rt->id() && (lt->is_char() || lt->is_var())) {
// identical token on both sides: cancel
++prefix;
} else if (lt->is_char() && rt->is_char()) {
// different concrete characters: symbol clash
m_is_general_conflict = true; m_is_general_conflict = true;
m_reason = backtrack_reason::symbol_clash; m_reason = backtrack_reason::symbol_clash;
return simplify_result::conflict; return simplify_result::conflict;
} else {
break;
} }
++prefix;
} }
if (prefix > 0) { if (prefix > 0) {
eq.m_lhs = sg.drop_left(eq.m_lhs, prefix); eq.m_lhs = sg.drop_left(eq.m_lhs, prefix);
@ -884,23 +877,6 @@ namespace seq {
euf::snode* lhead = lhs_toks[0]; euf::snode* lhead = lhs_toks[0];
euf::snode* rhead = rhs_toks[0]; euf::snode* rhead = rhs_toks[0];
// same-head variable cancellation: x·A = x·B → A = B
if (lhead->is_var() && lhead->id() == rhead->id()) {
euf::snode* ltail = m_sg.drop_first(eq.m_lhs);
euf::snode* rtail = m_sg.drop_first(eq.m_rhs);
nielsen_node* child = mk_child(node);
// replace the equation with the tails
for (str_eq& ceq : child->str_eqs()) {
if (ceq.m_lhs == eq.m_lhs && ceq.m_rhs == eq.m_rhs) {
ceq.m_lhs = ltail;
ceq.m_rhs = rtail;
break;
}
}
mk_edge(node, child, true);
return true;
}
// variable definition: x = t where x ∉ vars(t) → subst x → t // variable definition: x = t where x ∉ vars(t) → subst x → t
if (lhead->is_var() && eq.m_rhs->is_empty()) { if (lhead->is_var() && eq.m_rhs->is_empty()) {
nielsen_node* child = mk_child(node); nielsen_node* child = mk_child(node);