From: Gereon Kremer <gkremer@stanford.edu>
Date: Wed, 19 Jan 2022 18:02:48 +0000 (-0800)
Subject: Make tracing for arithmetic rewriter more consistent and useful (#7960)
X-Git-Tag: cvc5-1.0.0~526
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c92b9fbd07d1db4641c3c49fc5dd8e98be25f3e6;p=cvc5.git

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 1fcb71643..c698490b0 100644
--- 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)