CVC3

expr_stream.h

Go to the documentation of this file.
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 (return previous value)
00175     bool dagFlag(bool flag = true) { bool old = d_dag; d_dag = flag; return old; }
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