CVC3  2.4.1
expr_stream.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file expr_stream.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Mon Jun 16 10:59:18 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  * Declaration of class ExprStream, an output stream to pretty-print
19  * Expr in various nice output formats (presentation/internal/other
20  * languages, outo-indentation, bounded depth printing, DAG-ified
21  * printing, etc, etc...).
22  *
23  * This stream is most useful for the decision procedure designer when
24  * writing a pretty-printer (Theory::print() method). ExprStream
25  * carries information about the current output language, and all the
26  * indentation and depth pretty-printing is done automagically by the
27  * operator<<().
28  *
29  */
30 /*****************************************************************************/
31 
32 #ifndef _cvc3__expr_stream_h_
33 #define _cvc3__expr_stream_h_
34 
35 #include "os.h"
36 #include "expr.h"
37 
38 namespace CVC3 {
39  class ExprStream;
40 }
41 
42 namespace std {
44 }
45 
46 namespace CVC3 {
47 
48  /*! \defgroup PrettyPrinting Pretty-printing related classes and methods
49  * \ingroup BuildingBlocks
50  * If you are writing a theory-specific pretty-printer, please read
51  * carefully all the documentation about class ExprStream and its
52  * manipulators.
53  *
54  * @{
55  */
56 
57  //! Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
58  /*! Use this class as a standard ostream for Expr, string, int,
59  Rational, manipulators like endl, and it will do the expected
60  thing. Additionally, it has methods to access the current
61  printing flags.
62 
63  In order for the indentation engine to work correctly, you must
64  use the manipulators properly.
65 
66  Never use "\\n" in a string; always use endl manipulator, which
67  knows about indentation and will do the right thing.
68 
69  Always assume that the object you are printing may start printing
70  on a new line from the current indentation position. Therefore,
71  no string should start with an empty space (otherwise parts of
72  your expression will be mis-indented). If you need a white space
73  separator, or an operator surrounded by spaces, like os << " = ",
74  use os << space << "= " instead. The 'space' manipulator adds one
75  white space only if it's not at the beginning of a newly indented
76  line. Think of it as a logical white-space separator with
77  intelligent behavior, rather than a stupid hard space like " ".
78 
79  Indentation can be set to the current position with os << push,
80  and restored to the previous with os << pop. You do not need to
81  restore it before exiting your print function, ExprStream knows
82  how to restore it automatically. For example, you can write:
83 
84  os << "(" << push << e[0] << space << "+ " << e[1] << push << ")";
85 
86  to print (PLUS a b) as "(a + b)". Notice the second 'push' before
87  the closing paren. This is intentional (not a typo), and prevents
88  the paren ")" from jumping to the next line by itself. ExprStream
89  will not go to the next line if the current position is too close
90  to the indentation, since this will not give the expression a
91  better look.
92 
93  The indentation level is not restored in this example, and that is
94  fine, ExprStream will take care of that.
95 
96  For complex expressions like IF-THEN-ELSE, you may want to
97  remember the indentation to which you want to return later. You
98  can save the current indentation position with os << popSave, and
99  restore it later with os << pushRestore. These manipulators are
100  similar to pop and push, but 'pushRestore' will set the new
101  indentation level to the one popped by the last popSave instead of
102  the current one. At the moment, there is only one register for
103  saving an indentation position, so multiple pushRestore will not
104  work as you would expect (maybe this should be fixed?..).
105 
106  For concrete examples, see TheoryCore::print() and
107  TheoryArith::print().
108 
109  */
111  private:
112  ExprManager* d_em; //!< The ExprManager to use
113  std::ostream* d_os; //!< The ostream to print into
114  int d_depth; //!< Printing only upto this depth; -1 == unlimited
115  int d_currDepth; //!< Current depth of Expr
116  InputLanguage d_lang; //!< Output language
117  bool d_indent; //!< Whether to print with indentations
118  int d_col; //!< Current column in a line
119  int d_lineWidth; //!< Try to format/indent for this line width
120  //! Indentation stack
121  /*! The user code can set the indentation to the current d_col by
122  pushing the new value on the stack. This value is popped
123  automatically when returning from the recursive call. */
124  std::vector<int> d_indentStack;
125  //! The lowest position of the indent stack the user can pop
126  size_t d_indentLast;
127  //! Indentation register for popSave() and pushRestore()
129  //! Whether it is a beginning of line (for eating up extra spaces)
131  bool d_dag; //!< Print Expr as a DAG
132  //! Mapping subexpressions to names for DAG printing
134  //! New subexpressions not yet printed in a LET header
136  //! Stack of shared subexpressions (same as in d_dagMap)
137  std::vector<Expr> d_dagStack;
138  //! Stack of pointers to d_dagStack for pushing/popping shared subexprs
139  std::vector<size_t> d_dagPtr;
140  //! The smallest size of d_dagPtr the user can `popDag'
142  //! Flag whether the dagMap is already built
144  //! Counter for generating unique LET var names
146  //! nodag() manipulator has been applied
147  bool d_nodag;
148  //! Generating unique names in DAG expr
149  std::string newName();
150  //! Traverse the Expr, collect shared subexpressions in d_dagMap
151  void collectShared(const Expr& e, ExprMap<bool>& cache);
152  //! Wrap e into the top-level LET ... IN header from the dagMap
153  Expr addLetHeader(const Expr& e);
154  public:
155  //! Default constructor
156  ExprStream(ExprManager *em);
157  //! Destructor
159  //! Set a new output stream
160  /*! Note, that there is no method to access the ostream. This is
161  done on purpose, so that DP designers had to use only ExprStream
162  to print everything in their versions of Theory::print(). */
163  void os(std::ostream& os) { d_os = &os; }
164  //! Get the current output language
165  InputLanguage lang() const { return d_lang; }
166  //! Set the output language
167  void lang(InputLanguage l) { d_lang = l; }
168  //! Get the printing depth
169  int depth() const { return d_depth; }
170  //! Set the printing depth
171  void depth(int d) { d_depth = d; }
172  //! Set the line width
173  void lineWidth(int w) { d_lineWidth = w; }
174  //! Set the DAG flag (return previous value)
175  bool dagFlag(bool flag = true) { bool old = d_dag; d_dag = flag; return old; }
176  //! Set the indentation to the current column
177  /*! The value will be restorted automatically after the DP print()
178  function returns */
179  void pushIndent() { d_indentStack.push_back(d_col); }
180  //! Set the indentation to the given absolute position
181  /*! The value will be restorted automatically after the DP print()
182  function returns */
183  void pushIndent(int pos) { d_indentStack.push_back(pos); }
184  //! Restore the indentation (user cannot pop more than pushed)
185  void popIndent();
186  //! Reset indentation to what it was at this level
187  void resetIndent();
188  //! Return the current column position
189  int column() const { return d_col; }
190  //! Recompute shared subexpression for the next Expr
191  void pushDag();
192  //! Delete shared subexpressions previously added with pushdag
193  void popDag();
194  //! Reset the DAG to what it was at this level
195  void resetDag();
196 
197  // The printing action
198 
199  //! Use manipulators which are functions over ExprStream&
200  friend ExprStream& operator<<(ExprStream& os,
201  ExprStream& (*manip)(ExprStream&));
202  //! Print Expr
203  friend ExprStream& operator<<(ExprStream& os, const Expr& e);
204  //! Print Type
205  friend ExprStream& operator<<(ExprStream& os, const Type& t);
206  //! Print string
207  friend ExprStream& operator<<(ExprStream& os, const std::string& s);
208  //! Print char* string
209  friend ExprStream& operator<<(ExprStream& os, const char* s);
210  //! Print Rational
211  friend ExprStream& operator<<(ExprStream& os, const Rational& r);
212  //! Print int
213  friend ExprStream& operator<<(ExprStream& os, int i);
214 
215  //! Set the indentation to the current position
216  friend ExprStream& push(ExprStream& os);
217  //! Restore the indentation to the previous position
218  friend ExprStream& pop(ExprStream& os);
219  //! Remember the current indentation and pop to the previous position
220  friend ExprStream& popSave(ExprStream& os);
221  //! Set the indentation to the position saved by popSave()
222  friend ExprStream& pushRestore(ExprStream& os);
223  //! Reset the indentation to the default at this level
224  friend ExprStream& reset(ExprStream& os);
225  //! Insert a single white space separator
226  /*! It is preferred to use 'space' rather than a string of spaces
227  (" ") because ExprStream needs to delete extra white space if it
228  decides to end the line. If you use strings for spaces, you'll
229  mess up the indentation. */
230  friend ExprStream& space(ExprStream& os);
231  //! Print the next top-level expression node without DAG-ifying
232  /*!
233  * DAG-printing will resume for the children of the node. This is
234  * useful when printing definitions in the header of a DAGified
235  * LET expressions: defs have names, but must be printed expanded.
236  */
237  friend ExprStream& nodag(ExprStream& os);
238  //! Recompute shared subexpression for the next Expr
239  /*!
240  * For some constructs with bound variables (notably,
241  * quantifiers), shared subexpressions are not computed, because
242  * they cannot be defined outside the scope of bound variables.
243  * If this manipulator is applied before an expression within the
244  * scope of bound vars, these internal subexpressions will then be
245  * computed.
246  */
247  friend ExprStream& pushdag(ExprStream& os);
248  //! Delete shared subexpressions previously added with pushdag
249  /*!
250  * Similar to push/pop, shared subexpressions are automatically
251  * deleted upon a return from a recursive call, so popdag is not
252  * necessary after a pushdag in theory-specific print() functions.
253  * Also, you cannot pop more than you pushed an the current
254  * recursion level.
255  */
256  friend ExprStream& popdag(ExprStream& os);
257  //! Print the end-of-line
258  /*! The new line will not necessarily start at column 0 because of
259  indentation.
260 
261  The name endl will be introduced in namespace std, otherwise
262  CVC3::endl would overshadow std::endl, wreaking havoc...
263  */
264  friend ExprStream& std::endl(ExprStream& os);
265  }; // end of class ExprStream
266 
267  /*! @} */ // End of group PrettyPrinting
268 
269 ExprStream& push(ExprStream& os);
270 ExprStream& pop(ExprStream& os);
271 ExprStream& popSave(ExprStream& os);
272 ExprStream& pushRestore(ExprStream& os);
273 ExprStream& reset(ExprStream& os);
274 ExprStream& space(ExprStream& os);
275 ExprStream& nodag(ExprStream& os);
276 ExprStream& pushdag(ExprStream& os);
277 ExprStream& popdag(ExprStream& os);
278 
279 
280 } // End of namespace CVC3
281 
282 /*
283 namespace std {
284  CVC3::ExprStream& endl(CVC3::ExprStream& os);
285 }
286 */
287 
288 #endif
ExprStream & popSave(ExprStream &os)
Remember the current indentation and pop to the previous position.
ExprStream & pop(ExprStream &os)
Restore the indentation.
std::ostream * d_os
The ostream to print into.
Definition: expr_stream.h:113
int d_depth
Printing only upto this depth; -1 == unlimited.
Definition: expr_stream.h:114
ExprStream & nodag(ExprStream &os)
bool d_indent
Whether to print with indentations.
Definition: expr_stream.h:117
Data structure of expressions in CVC3.
Definition: expr.h:133
#define CVC_DLL
Definition: type.h:43
ExprStream & reset(ExprStream &os)
Reset the indentation to the default at this level.
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
InputLanguage
Different input languages.
Definition: lang.h:30
bool d_dagBuilt
Flag whether the dagMap is already built.
Definition: expr_stream.h:143
ExprMap< std::string > d_newDagMap
New subexpressions not yet printed in a LET header.
Definition: expr_stream.h:135
MS C++ specific settings.
Definition: type.h:42
STL namespace.
void pushIndent(int pos)
Set the indentation to the given absolute position.
Definition: expr_stream.h:183
void pushIndent()
Set the indentation to the current column.
Definition: expr_stream.h:179
ExprStream & space(ExprStream &os)
Insert a single white space separator.
bool d_beginningOfLine
Whether it is a beginning of line (for eating up extra spaces)
Definition: expr_stream.h:130
ExprManager * d_em
The ExprManager to use.
Definition: expr_stream.h:112
size_t d_lastDagSize
The smallest size of d_dagPtr the user can `popDag'.
Definition: expr_stream.h:141
void depth(int d)
Set the printing depth.
Definition: expr_stream.h:171
int column() const
Return the current column position.
Definition: expr_stream.h:189
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
ExprStream & pushdag(ExprStream &os)
bool d_nodag
nodag() manipulator has been applied
Definition: expr_stream.h:147
void lang(InputLanguage l)
Set the output language.
Definition: expr_stream.h:167
~ExprStream()
Destructor.
Definition: expr_stream.h:158
std::vector< size_t > d_dagPtr
Stack of pointers to d_dagStack for pushing/popping shared subexprs.
Definition: expr_stream.h:139
void lineWidth(int w)
Set the line width.
Definition: expr_stream.h:173
int d_idCounter
Counter for generating unique LET var names.
Definition: expr_stream.h:145
ExprMap< std::string > d_dagMap
Mapping subexpressions to names for DAG printing.
Definition: expr_stream.h:133
void os(std::ostream &os)
Set a new output stream.
Definition: expr_stream.h:163
ExprStream & pushRestore(ExprStream &os)
Set the indentation to the position saved by popSave()
Abstraction over different operating systems.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
int depth() const
Get the printing depth.
Definition: expr_stream.h:169
Expression Manager.
Definition: expr_manager.h:58
int d_indentReg
Indentation register for popSave() and pushRestore()
Definition: expr_stream.h:128
ExprStream & popdag(ExprStream &os)
int d_col
Current column in a line.
Definition: expr_stream.h:118
int d_currDepth
Current depth of Expr.
Definition: expr_stream.h:115
Definition of the API to expression package. See class Expr for details.
InputLanguage d_lang
Output language.
Definition: expr_stream.h:116
size_t d_indentLast
The lowest position of the indent stack the user can pop.
Definition: expr_stream.h:126
Definition: expr.cpp:35
InputLanguage lang() const
Get the current output language.
Definition: expr_stream.h:165
std::vector< int > d_indentStack
Indentation stack.
Definition: expr_stream.h:124
bool dagFlag(bool flag=true)
Set the DAG flag (return previous value)
Definition: expr_stream.h:175
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
std::vector< Expr > d_dagStack
Stack of shared subexpressions (same as in d_dagMap)
Definition: expr_stream.h:137