mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

fix parent list

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-10 06:07:05 -07:00 • committed by Arie Gurfinkel
parent a6848c79b7
commit ad153592a2
1 changed files with 29 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/qe/qe_term_graph.cpp
View file

@ -61,7 +61,7 @@ namespace qe {
if (!is_app(a)) return; if (!is_app(a)) return;
for (expr* e : *to_app(a)) { for (expr* e : *to_app(a)) {
term* t = app2term[e->get_id()]; term* t = app2term[e->get_id()];
t->m_parents.push_back(this); t->get_root().m_parents.push_back(this);
m_children.push_back(t); m_children.push_back(t);
} }
} }
@ -659,12 +659,20 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl
m_term2app.reset(); m_term2app.reset();
m_pinned.reset(); m_pinned.reset();
ptr_vector<term> worklist(m_terms);
obj_hashtable<expr> roots; obj_hashtable<expr> roots;
ptr_vector<term> worklist;
for (term * t : m_terms) {
if (t->is_root()) {
worklist.push_back(t);
t->set_mark(true);
}
}
while (!worklist.empty()) { while (!worklist.empty()) {
term* t = worklist.back(); term* t = worklist.back();
worklist.pop_back(); worklist.pop_back();
if (!t->is_root() || m_term2app.contains(t->get_id())) continue; SASSERT(t->is_root());
t->set_mark(false);
if (m_term2app.contains(t->get_id())) continue;
term* r = t; term* r = t;
roots.reset(); roots.reset();
expr_ref rep(m), other(m); expr_ref rep(m), other(m);
@ -700,17 +708,29 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl
// update the representative of t to the preferred one. // update the representative of t to the preferred one.
// used by mk_pure to determine representative of child. // used by mk_pure to determine representative of child.
m_term2app.insert(t->get_id(), rep); m_term2app.insert(t->get_id(), rep);
// TBD: add_parent in merge ensures that #if 1
// congruence closure root t contains all parents. // The root should contain all parents relative to the equivalence class.
// TBD: could tune this by using marking to only add roots to worklist if not already there. // To ensure this, merge uses add_parent on the chosen root with respect to the old root.
// To enable adding terms after merge the constructor for terms also has to ensure
// that new terms are added as parents of the roots of their children.
for (term * p : term::parents(t)) {
p = &p->get_root();
if (!p->is_marked()) {
p->set_mark(true);
worklist.push_back(p);
}
}
#else
r = t; r = t;
do { do {
for (term * p : term::parents(r)) { for (term * p : term::parents(r)) {
worklist.push_back(p); worklist.push_back(&p->get_root());
} }
r = &r->get_next(); r = &r->get_next();
} }
while (r != t); while (r != t);
#endif
} }
} }
// walk other predicates than equalities // walk other predicates than equalities
@ -725,6 +745,7 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl
// theory aware core minimization // theory aware core minimization
m_term2app.reset(); m_term2app.reset();
m_pinned.reset(); m_pinned.reset();
reset_marks();
return result; return result;
} }