From ba1df736cbaa200abf7a9ecf96f1d0d4554fb9e0 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 30 Jul 2013 19:06:23 -0400
Subject: [PATCH] SExpr pretty-printing for :all-options and :all-statistics.

---
 src/expr/command.cpp    |  3 ++
 src/printer/printer.cpp | 23 ++++++++++---
 src/printer/printer.h   | 71 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 93 insertions(+), 4 deletions(-)

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 3d5cec19b..d3e4b8553 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1257,6 +1257,9 @@ void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
     v.push_back(smtEngine->getInfo(d_flag));
     stringstream ss;
+    if(d_flag == "all-options" || d_flag == "all-statistics") {
+      ss << PrettySExprs(true);
+    }
     ss << SExpr(v);
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index f9d7c2a38..263ca50d7 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -31,6 +31,7 @@ using namespace std;
 namespace CVC4 {
 
 Printer* Printer::d_printers[language::output::LANG_MAX];
+const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
 
 Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   using namespace CVC4::language::output;
@@ -90,7 +91,7 @@ void Printer::toStream(std::ostream& out, const Result& r) const throw() {
   }
 }/* Printer::toStream() */
 
-void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+static void toStreamRec(std::ostream& out, const SExpr& sexpr, int indent) throw() {
   if(sexpr.isInteger()) {
     out << sexpr.getIntegerValue();
   } else if(sexpr.isRational()) {
@@ -111,19 +112,33 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
     }
     out << "\"" << s << "\"";
   } else {
-    out << '(';
     const vector<SExpr>& kids = sexpr.getChildren();
+    out << (indent > 0 && kids.size() > 1 ? "( " : "(");
     bool first = true;
     for(vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
       if(first) {
         first = false;
       } else {
-        out << ' ';
+        if(indent > 0) {
+          out << "\n" << string(indent, ' ');
+        } else {
+          out << ' ';
+        }
+      }
+      toStreamRec(out, *i, indent <= 0 || indent > 2 ? 0 : indent + 2);
+    }
+    if(indent > 0 && kids.size() > 1) {
+      out << '\n';
+      if(indent > 2) {
+        out << string(indent - 2, ' ');
       }
-      out << *i;
     }
     out << ')';
   }
+}/* toStreamRec() */
+
+void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+  toStreamRec(out, sexpr, PrettySExprs::getPrettySExprs(out) ? 2 : 0);
 }/* Printer::toStream(SExpr) */
 
 void Printer::toStream(std::ostream& out, const Model& m) const throw() {
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 */
-- 
2.30.2