Refactoring Options Handler & Library Cycle Breaking

What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.

The Problem:
The build order of CVC4 used to be [roughly] specified as:
  options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.

The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.

The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)

The build order of CVC4 can now be [roughly] specified as
  base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.

More details about the directories:

base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.

options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .

util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.

expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.

smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.

What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.

1 files changed, 590 insertions, 0 deletions

diff --git a/src/base/output.h b/src/base/output.h
new file mode 100644
index 000000000..0974591db
--- /dev/null
+++ b/src/base/output.h
@@ -0,0 +1,590 @@
+/*********************                                                        */
+/*! \file output.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Tim King, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Output utility classes and functions
+ **
+ ** Output utility classes and functions.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef __CVC4__OUTPUT_H
+#define __CVC4__OUTPUT_H
+
+#include <ios>
+#include <iostream>
+#include <streambuf>
+#include <string>
+#include <cstdio>
+#include <cstdarg>
+#include <set>
+#include <utility>
+
+namespace CVC4 {
+
+template <class T, class U>
+std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) CVC4_PUBLIC;
+
+template <class T, class U>
+std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
+  return out << "[" << p.first << "," << p.second << "]";
+}
+
+/**
+ * A utility class to provide (essentially) a "/dev/null" streambuf.
+ * If debugging support is compiled in, but debugging for
+ * e.g. "parser" is off, then Debug("parser") returns a stream
+ * attached to a null_streambuf instance so that output is directed to
+ * the bit bucket.
+ */
+class CVC4_PUBLIC null_streambuf : public std::streambuf {
+public:
+  /* Overriding overflow() just ensures that EOF isn't returned on the
+   * stream.  Perhaps this is not so critical, but recommended; this
+   * way the output stream looks like it's functioning, in a non-error
+   * state. */
+  int overflow(int c) { return c; }
+};/* class null_streambuf */
+
+/** A null stream-buffer singleton */
+extern null_streambuf null_sb;
+/** A null output stream singleton */
+extern std::ostream null_os CVC4_PUBLIC;
+
+class CVC4_PUBLIC CVC4ostream {
+  static const std::string s_tab;
+  static const int s_indentIosIndex;
+
+  /** The underlying ostream */
+  std::ostream* d_os;
+  /** Are we in the first column? */
+  bool d_firstColumn;
+
+  /** The endl manipulator (why do we need to keep this?) */
+  std::ostream& (*const d_endl)(std::ostream&);
+
+  // do not allow use
+  CVC4ostream& operator=(const CVC4ostream&);
+
+public:
+  CVC4ostream() :
+    d_os(NULL),
+    d_firstColumn(false),
+    d_endl(&std::endl) {
+  }
+  explicit CVC4ostream(std::ostream* os) :
+    d_os(os),
+    d_firstColumn(true),
+    d_endl(&std::endl) {
+  }
+
+  void pushIndent() {
+    if(d_os != NULL) {
+      ++d_os->iword(s_indentIosIndex);
+    }
+  }
+  void popIndent() {
+    if(d_os != NULL) {
+      long& indent = d_os->iword(s_indentIosIndex);
+      if(indent > 0) {
+        --indent;
+      }
+    }
+  }
+
+  CVC4ostream& flush() {
+    if(d_os != NULL) {
+      d_os->flush();
+    }
+    return *this;
+  }
+
+  bool isConnected() { return d_os != NULL; }
+  operator std::ostream&() { return isConnected() ? *d_os : null_os; }
+
+  template <class T>
+  CVC4ostream& operator<<(T const& t) CVC4_PUBLIC;
+
+  // support manipulators, endl, etc..
+  CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+
+      if(pf == d_endl) {
+        d_firstColumn = true;
+      }
+    }
+    return *this;
+  }
+  CVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+    }
+    return *this;
+  }
+  CVC4ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+    }
+    return *this;
+  }
+  CVC4ostream& operator<<(CVC4ostream& (*pf)(CVC4ostream&)) {
+    return pf(*this);
+  }
+};/* class CVC4ostream */
+
+inline CVC4ostream& push(CVC4ostream& stream) {
+  stream.pushIndent();
+  return stream;
+}
+
+inline CVC4ostream& pop(CVC4ostream& stream) {
+  stream.popIndent();
+  return stream;
+}
+
+template <class T>
+CVC4ostream& CVC4ostream::operator<<(T const& t) {
+  if(d_os != NULL) {
+    if(d_firstColumn) {
+      d_firstColumn = false;
+      long indent = d_os->iword(s_indentIosIndex);
+      for(long i = 0; i < indent; ++i) {
+        d_os = &(*d_os << s_tab);
+      }
+    }
+    d_os = &(*d_os << t);
+  }
+  return *this;
+}
+
+/**
+ * Does nothing; designed for compilation of non-debug/non-trace
+ * builds.  None of these should ever be called in such builds, but we
+ * offer this to the compiler so it doesn't complain.
+ */
+class CVC4_PUBLIC NullC {
+public:
+  operator bool() { return false; }
+  operator CVC4ostream() { return CVC4ostream(); }
+  operator std::ostream&() { return null_os; }
+};/* class NullC */
+
+extern NullC nullCvc4Stream CVC4_PUBLIC;
+
+/** The debug output class */
+class CVC4_PUBLIC DebugC {
+  std::set<std::string> d_tags;
+  std::ostream* d_os;
+
+public:
+  explicit DebugC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+  int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+
+  CVC4ostream operator()(const char* tag) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+  CVC4ostream operator()(std::string tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+  bool on (std::string tag) { d_tags.insert(tag); return true; }
+  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+  bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
+
+  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+};/* class DebugC */
+
+/** The warning output class */
+class CVC4_PUBLIC WarningC {
+  std::set< std::pair<const char*, size_t> > d_alreadyWarned;
+  std::ostream* d_os;
+
+public:
+  explicit WarningC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
+
+  // This function supports the WarningOnce() macro, which allows you
+  // to easily indicate that a warning should be emitted, but only
+  // once for a given run of CVC4.
+  bool warnOnce(const char* file, size_t line) {
+    std::pair<const char*, size_t> pr = std::make_pair(file, line);
+    if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) {
+      // signal caller not to warn again
+      return false;
+    }
+
+    // okay warn this time, but don't do it again
+    d_alreadyWarned.insert(pr);
+    return true;
+  }
+
+};/* class WarningC */
+
+/** The message output class */
+class CVC4_PUBLIC MessageC {
+  std::ostream* d_os;
+
+public:
+  explicit MessageC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
+};/* class MessageC */
+
+/** The notice output class */
+class CVC4_PUBLIC NoticeC {
+  std::ostream* d_os;
+
+public:
+  explicit NoticeC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
+};/* class NoticeC */
+
+/** The chat output class */
+class CVC4_PUBLIC ChatC {
+  std::ostream* d_os;
+
+public:
+  explicit ChatC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
+};/* class ChatC */
+
+/** The trace output class */
+class CVC4_PUBLIC TraceC {
+  std::ostream* d_os;
+  std::set<std::string> d_tags;
+
+public:
+  explicit TraceC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+  int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+
+  CVC4ostream operator()(const char* tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  CVC4ostream operator()(std::string tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+  bool on (std::string tag) { d_tags.insert(tag); return true; }
+  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+  bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
+
+  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+};/* class TraceC */
+
+/** The dump output class */
+class CVC4_PUBLIC DumpOutC {
+  std::set<std::string> d_tags;
+  std::ostream* d_os;
+
+public:
+  /**
+   * A copy of cout for use by the dumper.  This is important because
+   * it has different settings (e.g., the expr printing depth is always
+   * unlimited). */
+  static std::ostream dump_cout;
+
+  explicit DumpOutC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+  int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+
+  CVC4ostream operator()(const char* tag) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+  CVC4ostream operator()(std::string tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+  bool on (std::string tag) { d_tags.insert(tag); return true; }
+  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+  bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
+
+  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+};/* class DumpOutC */
+
+/** The debug output singleton */
+extern DebugC DebugChannel CVC4_PUBLIC;
+/** The warning output singleton */
+extern WarningC WarningChannel CVC4_PUBLIC;
+/** The message output singleton */
+extern MessageC MessageChannel CVC4_PUBLIC;
+/** The notice output singleton */
+extern NoticeC NoticeChannel CVC4_PUBLIC;
+/** The chat output singleton */
+extern ChatC ChatChannel CVC4_PUBLIC;
+/** The trace output singleton */
+extern TraceC TraceChannel CVC4_PUBLIC;
+/** The dump output singleton */
+extern DumpOutC DumpOutChannel CVC4_PUBLIC;
+
+#ifdef CVC4_MUZZLE
+
+#  define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
+#  define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+#  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
+#  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
+#  define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+#  define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
+
+inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int WarningC::printf(const char* fmt, ...) { return 0; }
+inline int MessageC::printf(const char* fmt, ...) { return 0; }
+inline int NoticeC::printf(const char* fmt, ...) { return 0; }
+inline int ChatC::printf(const char* fmt, ...) { return 0; }
+inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
+
+#else /* CVC4_MUZZLE */
+
+#  if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+#    define Debug ::CVC4::DebugChannel
+#  else /* CVC4_DEBUG && CVC4_TRACING */
+#    define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
+inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_DEBUG && CVC4_TRACING */
+#  define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+#  define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
+#  define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
+#  ifdef CVC4_TRACING
+#    define Trace ::CVC4::TraceChannel
+#  else /* CVC4_TRACING */
+#    define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_TRACING */
+#  ifdef CVC4_DUMPING
+#    define DumpOut ::CVC4::DumpOutChannel
+#  else /* CVC4_DUMPING */
+#    define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
+inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_DUMPING */
+
+#endif /* CVC4_MUZZLE */
+
+// Disallow e.g. !Debug("foo").isOn() forms
+// because the ! will apply before the ? .
+// If a compiler error has directed you here,
+// just parenthesize it e.g. !(Debug("foo").isOn())
+class __cvc4_true {
+  void operator!() CVC4_UNUSED;
+  void operator~() CVC4_UNUSED;
+  void operator-() CVC4_UNUSED;
+  void operator+() CVC4_UNUSED;
+public:
+  inline operator bool() { return true; }
+};/* __cvc4_true */
+
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+
+class CVC4_PUBLIC 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(const char* 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 /* CVC4_DEBUG && CVC4_TRACING */
+
+class CVC4_PUBLIC ScopedDebug {
+public:
+  ScopedDebug(std::string tag, bool newSetting = true) {}
+  ScopedDebug(const char* tag, bool newSetting = true) {}
+};/* class ScopedDebug */
+
+#endif /* CVC4_DEBUG && CVC4_TRACING */
+
+#ifdef CVC4_TRACING
+
+class CVC4_PUBLIC 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(const char* 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 /* CVC4_TRACING */
+
+class CVC4_PUBLIC ScopedTrace {
+public:
+  ScopedTrace(std::string tag, bool newSetting = true) {}
+  ScopedTrace(const char* tag, bool newSetting = true) {}
+};/* class ScopedTrace */
+
+#endif /* CVC4_TRACING */
+
+/**
+ * Pushes an indentation level on construction, pop on destruction.
+ * Useful for tracing recursive functions especially, but also can be
+ * used for clearly separating different phases of an algorithm,
+ * or iterations of a loop, or... etc.
+ */
+class CVC4_PUBLIC IndentedScope {
+  CVC4ostream d_out;
+public:
+  inline IndentedScope(CVC4ostream out);
+  inline ~IndentedScope();
+};/* class IndentedScope */
+
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; }
+inline IndentedScope::~IndentedScope() { d_out << pop; }
+#else /* CVC4_DEBUG && CVC4_TRACING */
+inline IndentedScope::IndentedScope(CVC4ostream out) {}
+inline IndentedScope::~IndentedScope() {}
+#endif /* CVC4_DEBUG && CVC4_TRACING */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OUTPUT_H */