diff options
| -rw-r--r-- | src/expr/node_converter.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp index eabe1d4f1..b72aa99f6 100644 --- a/src/expr/node_converter.cpp +++ b/src/expr/node_converter.cpp @@ -52,6 +52,8 @@ Node NodeConverter::convert(Node n) d_preCache[cur] = curp; if (!curp.isNull()) { + Trace("nconv-debug2") + << "..pre-rewrite changed " << cur << " into " << curp << std::endl; visit.push_back(cur); visit.push_back(curp); } @@ -74,6 +76,7 @@ Node NodeConverter::convert(Node n) } else if (it->second.isNull()) { + Trace("nconv-debug2") << "..post-visit " << cur << std::endl; it = d_preCache.find(cur); Assert(it != d_preCache.end()); if (!it->second.isNull()) @@ -82,6 +85,8 @@ Node NodeConverter::convert(Node n) Assert(d_cache.find(it->second) != d_cache.end()); Node ret = d_cache[it->second]; addToCache(cur, ret); + Trace("nconv-debug2") + << "..from cache changed " << cur << " into " << ret << std::endl; } else { @@ -107,6 +112,8 @@ Node NodeConverter::convert(Node n) if (childChanged) { ret = nm->mkNode(ret.getKind(), children); + Trace("nconv-debug2") << "..from children changed " << cur << " into " + << ret << std::endl; } // run the callback for the current application Node cret = postConvert(ret); @@ -114,6 +121,8 @@ Node NodeConverter::convert(Node n) { AlwaysAssert(cret.getType().isComparableTo(ret.getType())) << "Converting " << ret << " to " << cret << " changes type"; + Trace("nconv-debug2") << "..post-rewrite changed " << ret << " into " + << cret << std::endl; ret = cret; } addToCache(cur, ret); |