1 files changed, 71 insertions, 0 deletions
diff --git a/src/printer/printer.h b/src/printer/printer.h
index f73441966..e4bc7ce09 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -91,6 +91,77 @@ public:
 
 };/* class Printer */
 
+/**
+ * IOStream manipulator to pretty-print SExprs.
+ */
+class PrettySExprs {
+  /**
+   * The allocated index in ios_base for our setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  bool d_prettySExprs;
+
+public:
+  /**
+   * Construct a PrettySExprs with the given setting.
+   */
+  PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {}
+
+  inline void applyPrettySExprs(std::ostream& out) {
+    out.iword(s_iosIndex) = d_prettySExprs;
+  }
+
+  static inline bool getPrettySExprs(std::ostream& out) {
+    return out.iword(s_iosIndex);
+  }
+
+  static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) {
+    out.iword(s_iosIndex) = prettySExprs;
+  }
+
+  /**
+   * Set the pretty-sexprs state on the output stream for the current
+   * stack scope.  This makes sure the old state is reset on the
+   * stream after normal OR exceptional exit from the scope, using the
+   * RAII C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    bool d_oldPrettySExprs;
+
+  public:
+
+    inline Scope(std::ostream& out, bool prettySExprs) :
+      d_out(out),
+      d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
+      PrettySExprs::setPrettySExprs(out, prettySExprs);
+    }
+
+    inline ~Scope() {
+      PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs);
+    }
+
+  };/* class PrettySExprs::Scope */
+
+};/* class PrettySExprs */
+
+/**
+ * Sets the default pretty-sexprs setting for an ostream.  Use like this:
+ *
+ *   // let out be an ostream, s an SExpr
+ *   out << PrettySExprs(true) << s << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
+  ps.applyPrettySExprs(out);
+  return out;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PRINTER__PRINTER_H */