mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 20:58:54 +00:00
Code Activity

use idom for checking dominator relationships

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-07 14:35:44 +01:00
parent b898b07795
commit deba7d4d6e
2 changed files with 18 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -257,11 +257,14 @@ expr_ref dom_simplify_tactic::simplify_arg(expr * e) {
return r; return r;
} }
/**
\brief simplify e recursively.
*/
expr_ref dom_simplify_tactic::simplify_rec(expr * e0) { expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
expr_ref r(m); expr_ref r(m);
expr* e = 0; expr* e = 0;
TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << "\n";);
if (!m_result.find(e0, e)) { if (!m_result.find(e0, e)) {
e = e0; e = e0;
} }
@ -408,6 +411,12 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
SASSERT(scope_level() == 0); SASSERT(scope_level() == 0);
} }
/**
\brief determine if a is dominated by b.
Walk the immediate dominators of a upwards until hitting b or a term that is deeper than b.
Save intermediary results in a cache to avoid recomputations.
*/
bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
if (a == b) if (a == b)
return true; return true;
@ -416,15 +425,14 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
if (m_subexpr_cache.find(a, b, r)) if (m_subexpr_cache.find(a, b, r))
return r; return r;
for (expr * e : tree(b)) { if (get_depth(a) >= get_depth(b)) {
if (is_subexpr(a, e)) {
m_subexpr_cache.insert(a, b, true);
return true;
}
}
m_subexpr_cache.insert(a, b, false);
return false; return false;
} }
SASSERT(a != idom(a) && get_depth(idom(a)) > get_depth(a));
r = is_subexpr(idom(a), b);
m_subexpr_cache.insert(a, b, r);
return r;
}
ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) { ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
if (auto p = m_dominators.get_tree().find_core(e)) if (auto p = m_dominators.get_tree().find_core(e))

2
src/tactic/core/dom_simplify_tactic.h
View file

@ -57,6 +57,7 @@ public:
bool compile(unsigned sz, expr * const* es); bool compile(unsigned sz, expr * const* es);
tree_t const& get_tree() { return m_tree; } tree_t const& get_tree() { return m_tree; }
void reset(); void reset();
expr* idom(expr *e) const { return m_doms[e]; }
std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out);
}; };
@ -113,6 +114,7 @@ class dom_simplify_tactic : public tactic {
void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); } void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
ptr_vector<expr> const & tree(expr * e); ptr_vector<expr> const & tree(expr * e);
expr* idom(expr *e) const { return m_dominators.idom(e); }
unsigned scope_level() { return m_scope_level; } unsigned scope_level() { return m_scope_level; }
void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); } void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); }