From c92b9fbd07d1db4641c3c49fc5dd8e98be25f3e6 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 19 Jan 2022 10:02:48 -0800 Subject: [PATCH] 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. --- src/theory/arith/arith_rewriter.cpp | 30 +++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) 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) -- 2.30.2