diff options
Diffstat (limited to 'src/printer/printer.h')
-rw-r--r-- | src/printer/printer.h | 71 |
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 */ |