mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Added rewrite cycle detection in demodulator/ufbv_rewriter. Partial fix for #1456.
This commit is contained in:
parent
450f3c9b45
commit
305212c021
|
@ -322,8 +322,27 @@ bool ufbv_rewriter::rewrite_visit_children(app * a) {
|
|||
while (j > 0) {
|
||||
expr * e = a->get_arg(--j);
|
||||
if (!m_rewrite_cache.contains(e) || !m_rewrite_cache.get(e).second) {
|
||||
m_rewrite_todo.push_back(e);
|
||||
res = false;
|
||||
bool recursive = false;
|
||||
unsigned sz = m_rewrite_todo.size();
|
||||
expr * v = e;
|
||||
if (m_rewrite_cache.contains(e)) {
|
||||
expr_bool_pair const & ebp = m_rewrite_cache.get(e);
|
||||
if (ebp.second)
|
||||
v = ebp.first;
|
||||
}
|
||||
for (unsigned i = sz; i > 0; i--) {
|
||||
if (m_rewrite_todo[i - 1] == v) {
|
||||
recursive = true;
|
||||
TRACE("demodulator", tout << "Detected demodulator cycle: " <<
|
||||
mk_pp(a, m_manager) << " --> " << mk_pp(v, m_manager) << std::endl;);
|
||||
m_rewrite_cache.insert(e, expr_bool_pair(v, true));
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!recursive) {
|
||||
m_rewrite_todo.push_back(e);
|
||||
res = false;
|
||||
}
|
||||
}
|
||||
}
|
||||
return res;
|
||||
|
@ -347,7 +366,8 @@ expr * ufbv_rewriter::rewrite(expr * n) {
|
|||
while (!m_rewrite_todo.empty()) {
|
||||
TRACE("demodulator_stack", tout << "STACK: " << std::endl;
|
||||
for ( unsigned i = 0; i<m_rewrite_todo.size(); i++)
|
||||
tout << std::dec << i << ": " << std::hex << (size_t)m_rewrite_todo[i] << std::endl;
|
||||
tout << std::dec << i << ": " << std::hex << (size_t)m_rewrite_todo[i] <<
|
||||
" = " << mk_pp(m_rewrite_todo[i], m_manager) << std::endl;
|
||||
);
|
||||
|
||||
expr * e = m_rewrite_todo.back();
|
||||
|
|
Loading…
Reference in a new issue