mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fix issue in #4655

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-24 17:45:50 -07:00
parent c722962124
commit 22aee4d08d
5 changed files with 83 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -16,6 +16,7 @@ Author:
--*/
#include "ast/euf/euf_egraph.h"
#include "ast/ast_pp.h"
namespace euf {
@ -59,6 +60,7 @@ namespace euf {
}
void egraph::reinsert_equality(enode* p) {
SASSERT(is_equality(p));
if (p->get_arg(0)->get_root() == p->get_arg(1)->get_root())
m_new_eqs.push_back(p);
}
@ -162,10 +164,10 @@ namespace euf {
if (r1 == r2)
return;
if (r1->interpreted() && r2->interpreted()) {
set_conflict(r1, r2, j);
set_conflict(n1, n2, j);
return;
}
if ((r1->class_size() > r2->class_size() && !r1->interpreted()) || r2->interpreted()) {
if ((r1->class_size() > r2->class_size() && !r2->interpreted()) || r1->interpreted()) {
std::swap(r1, r2);
std::swap(n1, n2);
}
@ -237,41 +239,6 @@ namespace euf {
SASSERT(n1->get_root()->m_target == nullptr);
}
template <typename T>
void egraph::explain(ptr_vector<T>& justifications) {
SASSERT(m_inconsistent);
SASSERT(m_todo.empty());
m_todo.push_back(m_n1);
m_todo.push_back(m_n2);
auto push_congruence = [&](enode* p, enode* q) {
SASSERT(p->get_decl() == q->get_decl());
for (enode* arg : enode_args(p))
m_todo.push_back(arg);
for (enode* arg : enode_args(q))
m_todo.push_back(arg);
};
auto explain_node = [&](enode* n) {
if (!n->m_target)
return;
if (n->is_marked1())
return;
n->mark1();
if (n->m_justification.is_external())
justifications.push_back(n->m_justification.ext<T>());
else if (n->m_justification.is_congruence())
push_congruence(n, n->m_target);
n = n->m_target;
if (!n->is_marked1())
m_todo.push_back(n);
};
if (m_justification.is_external())
justifications.push_back(m_justification.ext<T>());
for (unsigned i = 0; i < m_todo.size(); ++i)
explain_node(m_todo[i]);
for (enode* n : m_todo)
n->unmark1();
}
void egraph::invariant() {
for (enode* n : m_nodes)
n->invariant();

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

@ -99,8 +99,44 @@ namespace euf {
bool inconsistent() const { return m_inconsistent; }
enode_vector const& new_eqs() const { return m_new_eqs; }
template <typename T>
void explain(ptr_vector<T>& justifications);
void explain(ptr_vector<T>& justifications) {
SASSERT(m_inconsistent);
SASSERT(m_todo.empty());
auto push_congruence = [&](enode* p, enode* q) {
SASSERT(p->get_decl() == q->get_decl());
for (enode* arg : enode_args(p))
m_todo.push_back(arg);
for (enode* arg : enode_args(q))
m_todo.push_back(arg);
};
auto explain_node = [&](enode* n) {
if (!n->m_target)
return;
if (n->is_marked1())
return;
n->mark1();
if (n->m_justification.is_external())
justifications.push_back(n->m_justification.ext<T>());
else if (n->m_justification.is_congruence())
push_congruence(n, n->m_target);
n = n->m_target;
if (!n->is_marked1())
m_todo.push_back(n);
};
m_todo.push_back(m_n1);
m_todo.push_back(m_n2);
if (m_justification.is_external())
justifications.push_back(m_justification.ext<T>());
else if (m_justification.is_congruence())
push_congruence(m_n1, m_n2);
for (unsigned i = 0; i < m_todo.size(); ++i)
explain_node(m_todo[i]);
for (enode* n : m_todo)
n->unmark1();
m_todo.reset();
}
void invariant();
std::ostream& display(std::ostream& out) const;
};

1
src/ast/euf/euf_enode.h
View file

@ -63,6 +63,7 @@ namespace euf {
n->m_root = n;
n->m_commutative = num_args == 2 && is_app(f) && to_app(f)->get_decl()->is_commutative();
for (unsigned i = 0; i < num_args; ++i) {
SASSERT(to_app(f)->get_arg(i) == args[i]->get_owner());
n->m_args[i] = args[i];
}
return n;