From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Sat, 6 Nov 2021 03:14:34 +0000 (-0300)
Subject: better traces in node converter (#7590)
X-Git-Tag: cvc5-1.0.0~869
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a0e1ac3b3b2cc048dae064358c4063a0b5969cc;p=cvc5.git

better traces in node converter (#7590)
---

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);