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

fix some basic mistakes in dominator code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-28 20:11:46 -07:00
parent 597f77cd77
commit 8d8e4cbc51
1 changed files with 13 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -69,7 +69,7 @@ private:
m_post2expr.push_back(e); m_post2expr.push_back(e);
todo.pop_back(); todo.pop_back();
for (expr* arg : *a) { for (expr* arg : *a) {
add_edge(m_parents, a, arg); add_edge(m_parents, arg, a);
} }
} }
} }
@ -83,12 +83,17 @@ private:
unsigned n1 = m_expr2post[x]; unsigned n1 = m_expr2post[x];
unsigned n2 = m_expr2post[y]; unsigned n2 = m_expr2post[y];
while (n1 != n2) { while (n1 != n2) {
if (n1 < n2) if (n1 < n2) {
n1 = m_doms[n1]; x = m_doms[x];
else if (n1 > n2) n1 = m_expr2post[x];
n2 = m_doms[n2]; }
else if (n1 > n2) {
y = m_doms[y];
n2 = m_expr2post[y];
}
} }
return n1; SASSERT(x == y);
return x;
} }
void compute_dominators() { void compute_dominators() {
@ -111,6 +116,7 @@ private:
} }
if (!m_doms.find(child, idom2) || idom2 != new_idom) { if (!m_doms.find(child, idom2) || idom2 != new_idom) {
m_doms.insert(child, new_idom); m_doms.insert(child, new_idom);
change = true;
} }
} }
} }
@ -118,10 +124,7 @@ private:
void extract_tree() { void extract_tree() {
for (auto const& kv : m_doms) { for (auto const& kv : m_doms) {
expr * child = kv.m_key; add_edge(m_tree, kv.m_value, kv.m_key);
for (expr * parent : kv.m_value) {
add_edge(m_tree, parent, child);
}
} }
} }