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.

diff --git a/src/base/output.h b/src/base/output.h
index 7bfae7bca64a7e466ffda64e90672041991b6bb9..9ae5ad8db9775fd984a452512c9f984cf10ed332 100644 (file)
--- 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 */