mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

#6523 - contains_ptr bug regarding etable reinserts

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-29 10:44:36 -08:00
parent 1d4644f718
commit e972eb33b2
3 changed files with 29 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -69,7 +69,7 @@ namespace euf {
}
enode_bool_pair egraph::insert_table(enode* p) {
TRACE("euf", tout << bpp(p) << "\n");
TRACE("euf", tout << "insert_table " << bpp(p) << "\n");
//SASSERT(!m_table.contains_ptr(p));
auto rc = m_table.insert(p);
p->m_cg = rc.first;
@ -83,7 +83,12 @@ namespace euf {
void egraph::reinsert_equality(enode* p) {
SASSERT(p->is_equality());
if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root())
add_literal(p, nullptr);
queue_literal(p, nullptr);
}
void egraph::queue_literal(enode* p, enode* ante) {
if (m_on_propagate_literal)
m_to_add_literal.push_back({ p, ante });
}
void egraph::force_push() {
@ -164,19 +169,14 @@ namespace euf {
if (!ante)
m_on_propagate_literal(n, ante);
else if (m.is_true(ante->get_expr()) || m.is_false(ante->get_expr())) {
for (enode* k : enode_class(n)) {
if (k != ante) {
//verbose_stream() << "eq: " << k->value() << " " <<ante->value() << "\n";
m_on_propagate_literal(k, ante);
}
}
for (enode* k : enode_class(n))
if (k != ante)
m_on_propagate_literal(k, ante);
}
else {
for (enode* k : enode_class(n)) {
if (k->value() != ante->value()) {
//verbose_stream() << "eq: " << k->value() << " " <<ante->value() << "\n";
m_on_propagate_literal(k, ante);
}
if (k->value() != ante->value())
m_on_propagate_literal(k, ante);
}
}
}
@ -352,6 +352,7 @@ namespace euf {
if (num_scopes <= m_num_scopes) {
m_num_scopes -= num_scopes;
m_to_merge.reset();
m_to_add_literal.reset();
return;
}
num_scopes -= m_num_scopes;
@ -434,6 +435,7 @@ namespace euf {
m_scopes.shrink(old_lim);
m_region.pop_scope(num_scopes);
m_to_merge.reset();
m_to_add_literal.reset();
SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
@ -494,6 +496,7 @@ namespace euf {
void egraph::remove_parents(enode* r) {
TRACE("euf", tout << bpp(r) << "\n");
DEBUG_CODE(for (enode* p : enode_parents(r)) SASSERT(!p->is_marked1()); );
for (enode* p : enode_parents(r)) {
if (p->is_marked1())
continue;
@ -582,11 +585,17 @@ namespace euf {
bool egraph::propagate() {
SASSERT(m_num_scopes == 0 || m_to_merge.empty());
force_push();
unsigned j = 0;
for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
auto const& w = m_to_merge[i];
merge(w.a, w.b, justification::congruence(w.commutativity, m_congruence_timestamp++));
for (; j < m_to_add_literal.size() && m.limit().inc() && !inconsistent(); ++j) {
auto const& [p, ante] = m_to_add_literal[j];
add_literal(p, ante);
}
}
m_to_merge.reset();
m_to_add_literal.reset();
return
(m_new_th_eqs_qhead < m_new_th_eqs.size()) ||
inconsistent();

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

@ -90,6 +90,11 @@ namespace euf {
to_merge(enode* a, enode* b, bool c) : a(a), b(b), commutativity(c) {}
};
struct to_add_literal {
enode* p, *ante;
to_add_literal(enode* p, enode* ante) : p(p), ante(ante) {}
};
struct stats {
unsigned m_num_merge;
unsigned m_num_th_eqs;
@ -162,6 +167,7 @@ namespace euf {
};
ast_manager& m;
svector<to_merge> m_to_merge;
svector<to_add_literal> m_to_add_literal;
etable m_table;
region m_region;
svector<update_record> m_updates;
@ -207,6 +213,7 @@ namespace euf {
void add_th_diseqs(theory_id id, theory_var v1, enode* r);
bool th_propagates_diseqs(theory_id id) const;
void add_literal(enode* n, enode* ante);
void queue_literal(enode* n, enode* ante);
void undo_eq(enode* r1, enode* n1, unsigned r2_num_parents);
void undo_add_th_var(enode* n, theory_id id);
enode* mk_enode(expr* f, unsigned generation, unsigned num_args, enode * const* args);

2
src/ast/euf/euf_etable.cpp
View file

@ -203,7 +203,6 @@ namespace euf {
SASSERT(n->num_args() > 0);
enode * n_prime;
void * t = get_table(n);
//verbose_stream() << "insert " << n << "\n";
switch (static_cast<table_kind>(GET_TAG(t))) {
case UNARY:
n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n);
@ -238,6 +237,7 @@ namespace euf {
UNTAG(table*, t)->erase(n);
break;
}
CTRACE("euf", contains_ptr(n), display(tout));
SASSERT(!contains_ptr(n));
}