Patch by Dan Liew: "Moved PrintContext class out of ExprPrinter.cpp so

it can be used by other classes. It has also been improved so it can
be used with the soon to be added ExprSMTLIBPrinter classes."



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166555 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 92 insertions, 42 deletions

diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h
new file mode 100644
index 00000000..a9e91925
--- /dev/null
+++ b/include/klee/util/PrintContext.h
@@ -0,0 +1,91 @@
+#ifndef PRINTCONTEXT_H_
+#define PRINTCONTEXT_H_
+
+#include <ostream>
+#include <sstream>
+#include <string>
+#include <stack>
+#include <iomanip>
+
+/// PrintContext - Helper class for pretty printing.
+/// It provides a basic wrapper around std::ostream that keeps track of
+/// how many characters have been used on the current line.
+///
+/// It also provides an optional way keeping track of the various levels of indentation
+/// by using a stack.
+/// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
+class PrintContext {
+private:
+  std::ostream &os;
+  std::stringstream ss;
+  std::string newline;
+
+  ///This is used to keep track of the stack of indentations used by
+  /// \sa breakLineI()
+  /// \sa pushIndent()
+  /// \sa popIndent()
+  std::stack<unsigned int> indentStack;
+
+public:
+  /// Number of characters on the current line.
+  unsigned pos;
+
+  PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
+  {
+	  indentStack.push(pos);
+  }
+
+  void setNewline(const std::string &_newline) {
+    newline = _newline;
+  }
+
+  void breakLine(unsigned indent=0) {
+    os << newline;
+    if (indent)
+      os << std::setw(indent) << ' ';
+    pos = indent;
+  }
+
+  ///Break line using the indent on the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& breakLineI()
+  {
+	  breakLine(indentStack.top());
+	  return *this;
+  }
+
+  ///Add the current position on the line to the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& pushIndent()
+  {
+	  indentStack.push(pos);
+	  return *this;
+  }
+
+  ///Pop the top off the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& popIndent()
+  {
+	  indentStack.pop();
+	  return *this;
+  }
+
+  /// write - Output a string to the stream and update the
+  /// position. The stream should not have any newlines.
+  void write(const std::string &s) {
+    os << s;
+    pos += s.length();
+  }
+
+  template <typename T>
+  PrintContext &operator<<(T elt) {
+    ss.str("");
+    ss << elt;
+    write(ss.str());
+    return *this;
+  }
+
+};
+
+
+#endif /* PRINTCONTEXT_H_ */
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 6e7ccd2d..ac1d1d01 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -7,6 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "klee/util/PrintContext.h"
 #include "klee/util/ExprPPrinter.h"
 
 #include "klee/Constraints.h"
@@ -38,48 +39,6 @@ namespace {
   PCAllConstWidths("pc-all-const-widths",  llvm::cl::init(false));
 }
 
-/// PrintContext - Helper class for storing extra information for
-/// the pretty printer.
-class PrintContext {
-private:
-  std::ostream &os;
-  std::stringstream ss;
-  std::string newline;
-
-public:
-  /// Number of characters on the current line.
-  unsigned pos;
-
-public:
-  PrintContext(std::ostream &_os) : os(_os), newline("\n"), pos(0) {}
-
-  void setNewline(const std::string &_newline) {
-    newline = _newline;
-  }
-
-  void breakLine(unsigned indent=0) {
-    os << newline;
-    if (indent)
-      os << std::setw(indent) << ' ';
-    pos = indent;
-  }
-
-  /// write - Output a string to the stream and update the
-  /// position. The stream should not have any newlines.
-  void write(const std::string &s) {
-    os << s;
-    pos += s.length();
-  }
-
-  template <typename T>
-  PrintContext &operator<<(T elt) {
-    ss.str("");
-    ss << elt;
-    write(ss.str());
-    return *this;
-  }
-};
-
 class PPrinter : public ExprPPrinter {
 public:
   std::set<const Array*> usedArrays;