From 9ae093ec410f8dd224500113e3438bc748a19603 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 10 Dec 2021 11:08:58 -0800
Subject: [PATCH] Some cleanup around trace and debug (#7792)

Some minor cleanup in our output routines. While ScopedDebug and ScopedTrace are never used at all (and don't seem to make much sense considering how we use Debug and Trace), IndentedScope may be useful in some more places.
---
 src/base/output.h | 92 ++---------------------------------------------
 1 file changed, 2 insertions(+), 90 deletions(-)

diff --git a/src/base/output.h b/src/base/output.h
index 7bfae7bca..9ae5ad8db 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -357,82 +357,6 @@ class __cvc5_true
   inline operator bool() { return true; }
 }; /* __cvc5_true */
 
-#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
-
-class ScopedDebug
-{
-  std::string d_tag;
-  bool d_oldSetting;
-
-public:
-
-  ScopedDebug(std::string tag, bool newSetting = true) :
-    d_tag(tag) {
-    d_oldSetting = Debug.isOn(d_tag);
-    if(newSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-
-  ~ScopedDebug() {
-    if(d_oldSetting) {
-      Debug.on(d_tag);
-    } else {
-      Debug.off(d_tag);
-    }
-  }
-}; /* class ScopedDebug */
-
-#else /* CVC5_DEBUG && CVC5_TRACING */
-
-class ScopedDebug
-{
- public:
-  ScopedDebug(std::string tag, bool newSetting = true) {}
-}; /* class ScopedDebug */
-
-#endif /* CVC5_DEBUG && CVC5_TRACING */
-
-#ifdef CVC5_TRACING
-
-class ScopedTrace
-{
-  std::string d_tag;
-  bool d_oldSetting;
-
-public:
-
-  ScopedTrace(std::string tag, bool newSetting = true) :
-    d_tag(tag) {
-    d_oldSetting = Trace.isOn(d_tag);
-    if(newSetting) {
-      Trace.on(d_tag);
-    } else {
-      Trace.off(d_tag);
-    }
-  }
-
-  ~ScopedTrace() {
-    if(d_oldSetting) {
-      Trace.on(d_tag);
-    } else {
-      Trace.off(d_tag);
-    }
-  }
-}; /* class ScopedTrace */
-
-#else /* CVC5_TRACING */
-
-class ScopedTrace
-{
- public:
-  ScopedTrace(std::string tag, bool newSetting = true) {}
-}; /* class ScopedTrace */
-
-#endif /* CVC5_TRACING */
-
 /**
  * Pushes an indentation level on construction, pop on destruction.
  * Useful for tracing recursive functions especially, but also can be
@@ -442,23 +366,11 @@ class ScopedTrace
 class IndentedScope
 {
   Cvc5ostream d_out;
-
  public:
-  inline IndentedScope(Cvc5ostream out);
-  inline ~IndentedScope();
+  inline IndentedScope(Cvc5ostream out) : d_out(out) { d_out << push; }
+  inline ~IndentedScope() { d_out << pop; }
 }; /* class IndentedScope */
 
-#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
-inline IndentedScope::IndentedScope(Cvc5ostream out) : d_out(out)
-{
-  d_out << push;
-}
-inline IndentedScope::~IndentedScope() { d_out << pop; }
-#else  /* CVC5_DEBUG && CVC5_TRACING */
-inline IndentedScope::IndentedScope(Cvc5ostream out) {}
-inline IndentedScope::~IndentedScope() {}
-#endif /* CVC5_DEBUG && CVC5_TRACING */
-
 }  // namespace cvc5
 
 #endif /* CVC5__OUTPUT_H */
-- 
2.30.2