Make tracing for arithmetic rewriter more consistent and useful (#7960)

Tracing in the arithmetic rewriter was very inconsistent and oftentimes not particularly helpful. This adds a general trace showing all top-level calls to the arithmetic rewriter.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 1fcb71643284349550954921e3814ee8d26de080..c698490b0ef234370aabf2ae8ce97de3460fa193 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -62,30 +62,32 @@ ArithRewriter::ArithRewriter(OperatorElim& oe) : d_opElim(oe) {}
 
 RewriteResponse ArithRewriter::preRewrite(TNode t)
 {
+  Trace("arith-rewriter") << "preRewrite(" << t << ")" << std::endl;
   if (isAtom(t))
   {
-    return preRewriteAtom(t);
+    auto res = preRewriteAtom(t);
+    Trace("arith-rewriter")
+        << res.d_status << " -> " << res.d_node << std::endl;
+    return res;
   }
-  return preRewriteTerm(t);
+  auto res = preRewriteTerm(t);
+  Trace("arith-rewriter") << res.d_status << " -> " << res.d_node << std::endl;
+  return res;
 }
 
 RewriteResponse ArithRewriter::postRewrite(TNode t)
 {
+  Trace("arith-rewriter") << "postRewrite(" << t << ")" << std::endl;
   if (isAtom(t))
   {
-    RewriteResponse response = postRewriteAtom(t);
-    if (Debug.isOn("arith::rewriter") && response.d_status == REWRITE_DONE)
-    {
-      Comparison::parseNormalForm(response.d_node);
-    }
-    return response;
-  }
-  RewriteResponse response = postRewriteTerm(t);
-  if (Debug.isOn("arith::rewriter") && response.d_status == REWRITE_DONE)
-  {
-    Polynomial::parsePolynomial(response.d_node);
+    auto res = postRewriteAtom(t);
+    Trace("arith-rewriter")
+        << res.d_status << " -> " << res.d_node << std::endl;
+    return res;
   }
-  return response;
+  auto res = postRewriteTerm(t);
+  Trace("arith-rewriter") << res.d_status << " -> " << res.d_node << std::endl;
+  return res;
 }
 
 RewriteResponse ArithRewriter::preRewriteAtom(TNode atom)