mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-07 00:09:28 +01:00
parent a18236bc7f 1d12a9c86d
commit cabdc1f64c
1 changed files with 12 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -100,33 +100,19 @@ 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());
if (p.size() == 1) {
if (!m_doms.contains(child)) {
m_doms.insert(child, p[0]);
change = true;
}
expr * new_idom = 0, *idom2 = 0;
for (auto& pred : p) {
if (m_doms.contains(pred)) {
new_idom = !new_idom ? pred : intersect(new_idom, pred);
}
}
else {
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);
}
}
if (!new_idom) {
m_doms.insert(child, p[0]);
TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(p[0], m) << "\n";);
change = true;
}
else if (!m_doms.find(child, idom2) || idom2 != new_idom) {
m_doms.insert(child, new_idom);
TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(new_idom, m) << "\n";);
change = true;
}
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;
}
}
iterations *= 2;