00001 /*****************************************************************************/ 00002 /*! 00003 * \file expr_stream.h 00004 * 00005 * Author: Sergey Berezin 00006 * 00007 * Created: Mon Jun 16 10:59:18 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 * Declaration of class ExprStream, an output stream to pretty-print 00019 * Expr in various nice output formats (presentation/internal/other 00020 * languages, outo-indentation, bounded depth printing, DAG-ified 00021 * printing, etc, etc...). 00022 * 00023 * This stream is most useful for the decision procedure designer when 00024 * writing a pretty-printer (Theory::print() method). ExprStream 00025 * carries information about the current output language, and all the 00026 * indentation and depth pretty-printing is done automagically by the 00027 * operator<<(). 00028 * 00029 */ 00030 /*****************************************************************************/ 00031 00032 #ifndef _cvc3__expr_stream_h_ 00033 #define _cvc3__expr_stream_h_ 00034 00035 #include "os.h" 00036 #include "expr.h" 00037 00038 namespace CVC3 { 00039 class ExprStream; 00040 } 00041 00042 namespace std { 00043 CVC3::ExprStream& endl(CVC3::ExprStream& os); 00044 } 00045 00046 namespace CVC3 { 00047 00048 /*! \defgroup PrettyPrinting Pretty-printing related classes and methods 00049 * \ingroup BuildingBlocks 00050 * If you are writing a theory-specific pretty-printer, please read 00051 * carefully all the documentation about class ExprStream and its 00052 * manipulators. 00053 * 00054 * @{ 00055 */ 00056 00057 //! Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING! 00058 /*! Use this class as a standard ostream for Expr, string, int, 00059 Rational, manipulators like endl, and it will do the expected 00060 thing. Additionally, it has methods to access the current 00061 printing flags. 00062 00063 In order for the indentation engine to work correctly, you must 00064 use the manipulators properly. 00065 00066 Never use "\\n" in a string; always use endl manipulator, which 00067 knows about indentation and will do the right thing. 00068 00069 Always assume that the object you are printing may start printing 00070 on a new line from the current indentation position. Therefore, 00071 no string should start with an empty space (otherwise parts of 00072 your expression will be mis-indented). If you need a white space 00073 separator, or an operator surrounded by spaces, like os << " = ", 00074 use os << space << "= " instead. The 'space' manipulator adds one 00075 white space only if it's not at the beginning of a newly indented 00076 line. Think of it as a logical white-space separator with 00077 intelligent behavior, rather than a stupid hard space like " ". 00078 00079 Indentation can be set to the current position with os << push, 00080 and restored to the previous with os << pop. You do not need to 00081 restore it before exiting your print function, ExprStream knows 00082 how to restore it automatically. For example, you can write: 00083 00084 os << "(" << push << e[0] << space << "+ " << e[1] << push << ")"; 00085 00086 to print (PLUS a b) as "(a + b)". Notice the second 'push' before 00087 the closing paren. This is intentional (not a typo), and prevents 00088 the paren ")" from jumping to the next line by itself. ExprStream 00089 will not go to the next line if the current position is too close 00090 to the indentation, since this will not give the expression a 00091 better look. 00092 00093 The indentation level is not restored in this example, and that is 00094 fine, ExprStream will take care of that. 00095 00096 For complex expressions like IF-THEN-ELSE, you may want to 00097 remember the indentation to which you want to return later. You 00098 can save the current indentation position with os << popSave, and 00099 restore it later with os << pushRestore. These manipulators are 00100 similar to pop and push, but 'pushRestore' will set the new 00101 indentation level to the one popped by the last popSave instead of 00102 the current one. At the moment, there is only one register for 00103 saving an indentation position, so multiple pushRestore will not 00104 work as you would expect (maybe this should be fixed?..). 00105 00106 For concrete examples, see TheoryCore::print() and 00107 TheoryArith::print(). 00108 00109 */ 00110 class CVC_DLL ExprStream { 00111 private: 00112 ExprManager* d_em; //!< The ExprManager to use 00113 std::ostream* d_os; //!< The ostream to print into 00114 int d_depth; //!< Printing only upto this depth; -1 == unlimited 00115 int d_currDepth; //!< Current depth of Expr 00116 InputLanguage d_lang; //!< Output language 00117 bool d_indent; //!< Whether to print with indentations 00118 int d_col; //!< Current column in a line 00119 int d_lineWidth; //!< Try to format/indent for this line width 00120 //! Indentation stack 00121 /*! The user code can set the indentation to the current d_col by 00122 pushing the new value on the stack. This value is popped 00123 automatically when returning from the recursive call. */ 00124 std::vector<int> d_indentStack; 00125 //! The lowest position of the indent stack the user can pop 00126 size_t d_indentLast; 00127 //! Indentation register for popSave() and pushRestore() 00128 int d_indentReg; 00129 //! Whether it is a beginning of line (for eating up extra spaces) 00130 bool d_beginningOfLine; 00131 bool d_dag; //!< Print Expr as a DAG 00132 //! Mapping subexpressions to names for DAG printing 00133 ExprMap<std::string> d_dagMap; 00134 //! New subexpressions not yet printed in a LET header 00135 ExprMap<std::string> d_newDagMap; 00136 //! Stack of shared subexpressions (same as in d_dagMap) 00137 std::vector<Expr> d_dagStack; 00138 //! Stack of pointers to d_dagStack for pushing/popping shared subexprs 00139 std::vector<size_t> d_dagPtr; 00140 //! The smallest size of d_dagPtr the user can `popDag' 00141 size_t d_lastDagSize; 00142 //! Flag whether the dagMap is already built 00143 bool d_dagBuilt; 00144 //! Counter for generating unique LET var names 00145 int d_idCounter; 00146 //! nodag() manipulator has been applied 00147 bool d_nodag; 00148 //! Generating unique names in DAG expr 00149 std::string newName(); 00150 //! Traverse the Expr, collect shared subexpressions in d_dagMap 00151 void collectShared(const Expr& e, ExprMap<bool>& cache); 00152 //! Wrap e into the top-level LET ... IN header from the dagMap 00153 Expr addLetHeader(const Expr& e); 00154 public: 00155 //! Default constructor 00156 ExprStream(ExprManager *em); 00157 //! Destructor 00158 ~ExprStream() { } 00159 //! Set a new output stream 00160 /*! Note, that there is no method to access the ostream. This is 00161 done on purpose, so that DP designers had to use only ExprStream 00162 to print everything in their versions of Theory::print(). */ 00163 void os(std::ostream& os) { d_os = &os; } 00164 //! Get the current output language 00165 InputLanguage lang() const { return d_lang; } 00166 //! Set the output language 00167 void lang(InputLanguage l) { d_lang = l; } 00168 //! Get the printing depth 00169 int depth() const { return d_depth; } 00170 //! Set the printing depth 00171 void depth(int d) { d_depth = d; } 00172 //! Set the line width 00173 void lineWidth(int w) { d_lineWidth = w; } 00174 //! Set the DAG flag 00175 void dagFlag(bool flag = true) { d_dag = flag; } 00176 //! Set the indentation to the current column 00177 /*! The value will be restorted automatically after the DP print() 00178 function returns */ 00179 void pushIndent() { d_indentStack.push_back(d_col); } 00180 //! Set the indentation to the given absolute position 00181 /*! The value will be restorted automatically after the DP print() 00182 function returns */ 00183 void pushIndent(int pos) { d_indentStack.push_back(pos); } 00184 //! Restore the indentation (user cannot pop more than pushed) 00185 void popIndent(); 00186 //! Reset indentation to what it was at this level 00187 void resetIndent(); 00188 //! Return the current column position 00189 int column() const { return d_col; } 00190 //! Recompute shared subexpression for the next Expr 00191 void pushDag(); 00192 //! Delete shared subexpressions previously added with pushdag 00193 void popDag(); 00194 //! Reset the DAG to what it was at this level 00195 void resetDag(); 00196 00197 // The printing action 00198 00199 //! Use manipulators which are functions over ExprStream& 00200 friend ExprStream& operator<<(ExprStream& os, 00201 ExprStream& (*manip)(ExprStream&)); 00202 //! Print Expr 00203 friend ExprStream& operator<<(ExprStream& os, const Expr& e); 00204 //! Print Type 00205 friend ExprStream& operator<<(ExprStream& os, const Type& t); 00206 //! Print string 00207 friend ExprStream& operator<<(ExprStream& os, const std::string& s); 00208 //! Print char* string 00209 friend ExprStream& operator<<(ExprStream& os, const char* s); 00210 //! Print Rational 00211 friend ExprStream& operator<<(ExprStream& os, const Rational& r); 00212 //! Print int 00213 friend ExprStream& operator<<(ExprStream& os, int i); 00214 00215 //! Set the indentation to the current position 00216 friend ExprStream& push(ExprStream& os); 00217 //! Restore the indentation to the previous position 00218 friend ExprStream& pop(ExprStream& os); 00219 //! Remember the current indentation and pop to the previous position 00220 friend ExprStream& popSave(ExprStream& os); 00221 //! Set the indentation to the position saved by popSave() 00222 friend ExprStream& pushRestore(ExprStream& os); 00223 //! Reset the indentation to the default at this level 00224 friend ExprStream& reset(ExprStream& os); 00225 //! Insert a single white space separator 00226 /*! It is preferred to use 'space' rather than a string of spaces 00227 (" ") because ExprStream needs to delete extra white space if it 00228 decides to end the line. If you use strings for spaces, you'll 00229 mess up the indentation. */ 00230 friend ExprStream& space(ExprStream& os); 00231 //! Print the next top-level expression node without DAG-ifying 00232 /*! 00233 * DAG-printing will resume for the children of the node. This is 00234 * useful when printing definitions in the header of a DAGified 00235 * LET expressions: defs have names, but must be printed expanded. 00236 */ 00237 friend ExprStream& nodag(ExprStream& os); 00238 //! Recompute shared subexpression for the next Expr 00239 /*! 00240 * For some constructs with bound variables (notably, 00241 * quantifiers), shared subexpressions are not computed, because 00242 * they cannot be defined outside the scope of bound variables. 00243 * If this manipulator is applied before an expression within the 00244 * scope of bound vars, these internal subexpressions will then be 00245 * computed. 00246 */ 00247 friend ExprStream& pushdag(ExprStream& os); 00248 //! Delete shared subexpressions previously added with pushdag 00249 /*! 00250 * Similar to push/pop, shared subexpressions are automatically 00251 * deleted upon a return from a recursive call, so popdag is not 00252 * necessary after a pushdag in theory-specific print() functions. 00253 * Also, you cannot pop more than you pushed an the current 00254 * recursion level. 00255 */ 00256 friend ExprStream& popdag(ExprStream& os); 00257 //! Print the end-of-line 00258 /*! The new line will not necessarily start at column 0 because of 00259 indentation. 00260 00261 The name endl will be introduced in namespace std, otherwise 00262 CVC3::endl would overshadow std::endl, wreaking havoc... 00263 */ 00264 friend ExprStream& std::endl(ExprStream& os); 00265 }; // end of class ExprStream 00266 00267 /*! @} */ // End of group PrettyPrinting 00268 00269 ExprStream& push(ExprStream& os); 00270 ExprStream& pop(ExprStream& os); 00271 ExprStream& popSave(ExprStream& os); 00272 ExprStream& pushRestore(ExprStream& os); 00273 ExprStream& reset(ExprStream& os); 00274 ExprStream& space(ExprStream& os); 00275 ExprStream& nodag(ExprStream& os); 00276 ExprStream& pushdag(ExprStream& os); 00277 ExprStream& popdag(ExprStream& os); 00278 00279 00280 } // End of namespace CVC3 00281 00282 /* 00283 namespace std { 00284 CVC3::ExprStream& endl(CVC3::ExprStream& os); 00285 } 00286 */ 00287 00288 #endif