mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

dom_simplifier: fix dominator computation

Browse source
This commit is contained in:
Nuno Lopes 2017-10-06 18:19:37 +01:00
parent 31c6b3eb5b
commit 1d12a9c86d
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -95,17 +95,17 @@ bool expr_dominators::compute_dominators() {
for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) {
expr * child = m_post2expr[i];
ptr_vector<expr> const& p = m_parents[child];
SASSERT(!p.empty());
expr * new_idom = 0, *idom2 = 0;
for (unsigned j = 0; j < p.size(); ++j) {
if (!new_idom) {
m_doms.find(p[j], new_idom);
}
else if (m_doms.find(p[j], idom2)) {
new_idom = intersect(new_idom, idom2);
for (auto& pred : p) {
if (m_doms.contains(pred)) {
new_idom = !new_idom ? pred : intersect(new_idom, pred);
}
}
if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) {
if (!new_idom) {
m_doms.insert(child, p[0]);
change = true;
}
else if (!m_doms.find(child, idom2) || idom2 != new_idom) {
m_doms.insert(child, new_idom);
change = true;
}