Home
last modified time | relevance | path

Searched refs:m_post2expr (Results 1 – 4 of 4) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/tactic/core/
H A Ddom_simplify_tactic.cpp32 SASSERT(m_post2expr.empty()); in compute_post_order()
55 m_post2expr.push_back(e); in compute_post_order()
99 SASSERT(m_post2expr.empty() || m_post2expr.back() == e); in compute_dominators()
100 for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { in compute_dominators()
101 expr * child = m_post2expr[i]; in compute_dominators()
120 if (change && iterations > m_post2expr.size()) { in compute_dominators()
150 m_post2expr.reset(); in reset()
H A Ddom_simplify_tactic.h37 ptr_vector<expr> m_post2expr; variable
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/
H A Ddom_simplify_tactic.cpp32 SASSERT(m_post2expr.empty()); in compute_post_order()
55 m_post2expr.push_back(e); in compute_post_order()
99 SASSERT(m_post2expr.empty() || m_post2expr.back() == e); in compute_dominators()
100 for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { in compute_dominators()
101 expr * child = m_post2expr[i]; in compute_dominators()
120 if (change && iterations > m_post2expr.size()) { in compute_dominators()
150 m_post2expr.reset(); in reset()
H A Ddom_simplify_tactic.h37 ptr_vector<expr> m_post2expr; variable