mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

reset visited (fast mark) to not clash with occurs

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-17 17:36:21 +09:00
parent 6662afdd26
commit 59b7845c7d
4 changed files with 19 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/euf/euf_egraph.cpp
View file

@ -451,7 +451,7 @@ namespace euf {
add_literal(n1, false); add_literal(n1, false);
if (n1->is_equality() && n1->value() == l_false) if (n1->is_equality() && n1->value() == l_false)
new_diseq(n1); new_diseq(n1);
remove_parents(r1, r2); remove_parents(r1);
push_eq(r1, n1, r2->num_parents()); push_eq(r1, n1, r2->num_parents());
merge_justification(n1, n2, j); merge_justification(n1, n2, j);
for (enode* c : enode_class(n1)) for (enode* c : enode_class(n1))
@ -464,8 +464,8 @@ namespace euf {
cb(r2, r1); cb(r2, r1);
} }
void egraph::remove_parents(enode* r1, enode* r2) { void egraph::remove_parents(enode* r) {
for (enode* p : enode_parents(r1)) { for (enode* p : enode_parents(r)) {
if (p->is_marked1()) if (p->is_marked1())
continue; continue;
if (p->merge_enabled()) { if (p->merge_enabled()) {

2
src/ast/euf/euf_egraph.h
View file

@ -220,7 +220,7 @@ namespace euf {
void merge_th_eq(enode* n, enode* root); void merge_th_eq(enode* n, enode* root);
void merge_justification(enode* n1, enode* n2, justification j); void merge_justification(enode* n1, enode* n2, justification j);
void reinsert_parents(enode* r1, enode* r2); void reinsert_parents(enode* r1, enode* r2);
void remove_parents(enode* r1, enode* r2); void remove_parents(enode* r);
void unmerge_justification(enode* n1); void unmerge_justification(enode* n1);
void reinsert_equality(enode* p); void reinsert_equality(enode* p);
void update_children(enode* n); void update_children(enode* n);

22
src/ast/simplifiers/euf_completion.cpp
View file

@ -80,18 +80,22 @@ namespace euf {
}; };
for (unsigned i = m_qhead; i < sz; ++i) { for (unsigned i = m_qhead; i < sz; ++i) {
auto [f,d] = m_fmls[i](); expr* x, * y;
auto* n = mk_enode(f); auto [f, d] = m_fmls[i]();
if (m.is_eq(f)) { if (m.is_eq(f, x, y)) {
m_egraph.merge(n->get_arg(0), n->get_arg(1), d); enode* a = mk_enode(x);
add_children(n->get_arg(0)); enode* b = mk_enode(y);
add_children(n->get_arg(1)); m_egraph.merge(a, b, d);
add_children(a);
add_children(b);
} }
if (m.is_not(f)) { else if (m.is_not(f, f)) {
m_egraph.merge(n->get_arg(0), m_ff, d); enode* n = mk_enode(f);
add_children(n->get_arg(0)); m_egraph.merge(n, m_ff, d);
add_children(n);
} }
else { else {
enode* n = mk_enode(f);
m_egraph.merge(n, m_tt, d); m_egraph.merge(n, m_tt, d);
add_children(n); add_children(n);
} }

3
src/ast/simplifiers/solve_eqs.cpp
View file

@ -129,7 +129,8 @@ namespace euf {
todo.push_back(var2id(e)); todo.push_back(var2id(e));
} }
m_todo.reset(); m_todo.reset();
visited.reset();
if (!is_safe) { if (!is_safe) {
todo.shrink(todo_sz); todo.shrink(todo_sz);
continue; continue;