From 59b7845c7dc765a9c19074c43d288daccd753d68 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 17 Nov 2022 17:36:21 +0900
Subject: [PATCH] reset visited (fast mark) to not clash with occurs
---
src/ast/euf/euf_egraph.cpp | 6 +++---
src/ast/euf/euf_egraph.h | 2 +-
src/ast/simplifiers/euf_completion.cpp | 22 +++++++++++++---------
src/ast/simplifiers/solve_eqs.cpp | 3 ++-
4 files changed, 19 insertions(+), 14 deletions(-)
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index c8605b297..666a7fad6 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -451,7 +451,7 @@ namespace euf {
add_literal(n1, false);
if (n1->is_equality() && n1->value() == l_false)
new_diseq(n1);
- remove_parents(r1, r2);
+ remove_parents(r1);
push_eq(r1, n1, r2->num_parents());
merge_justification(n1, n2, j);
for (enode* c : enode_class(n1))
@@ -464,8 +464,8 @@ namespace euf {
cb(r2, r1);
}
- void egraph::remove_parents(enode* r1, enode* r2) {
- for (enode* p : enode_parents(r1)) {
+ void egraph::remove_parents(enode* r) {
+ for (enode* p : enode_parents(r)) {
if (p->is_marked1())
continue;
if (p->merge_enabled()) {
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 53aaf481a..d6bcb9cd3 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -220,7 +220,7 @@ namespace euf {
void merge_th_eq(enode* n, enode* root);
void merge_justification(enode* n1, enode* n2, justification j);
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 reinsert_equality(enode* p);
void update_children(enode* n);
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 9860b48b2..ac1ecc47a 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -80,18 +80,22 @@ namespace euf {
};
for (unsigned i = m_qhead; i < sz; ++i) {
- auto [f,d] = m_fmls[i]();
- auto* n = mk_enode(f);
- if (m.is_eq(f)) {
- m_egraph.merge(n->get_arg(0), n->get_arg(1), d);
- add_children(n->get_arg(0));
- add_children(n->get_arg(1));
+ expr* x, * y;
+ auto [f, d] = m_fmls[i]();
+ if (m.is_eq(f, x, y)) {
+ enode* a = mk_enode(x);
+ enode* b = mk_enode(y);
+ m_egraph.merge(a, b, d);
+ add_children(a);
+ add_children(b);
}
- if (m.is_not(f)) {
- m_egraph.merge(n->get_arg(0), m_ff, d);
- add_children(n->get_arg(0));
+ else if (m.is_not(f, f)) {
+ enode* n = mk_enode(f);
+ m_egraph.merge(n, m_ff, d);
+ add_children(n);
}
else {
+ enode* n = mk_enode(f);
m_egraph.merge(n, m_tt, d);
add_children(n);
}
diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index f66f64b6d..5090e1b43 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -129,7 +129,8 @@ namespace euf {
todo.push_back(var2id(e));
}
m_todo.reset();
-
+ visited.reset();
+
if (!is_safe) {
todo.shrink(todo_sz);
continue;