expr_stream.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr_stream.cpp
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Mon Jun 16 13:57:29 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  */
00019 /*****************************************************************************/
00020 
00021 #include "pretty_printer.h"
00022 #include "expr_stream.h"
00023 
00024 using namespace std;
00025 
00026 namespace CVC3 {
00027 
00028   ExprStream::ExprStream(ExprManager *em)
00029     : d_em(em), d_os(&cout), d_depth(em->printDepth()), d_currDepth(0),
00030       d_lang(em->getOutputLang()),
00031       d_indent(em->withIndentation()), d_col(em->indent()),
00032       d_lineWidth(em->lineWidth()), d_indentReg(0), d_beginningOfLine(false),
00033       d_dag(em->dagPrinting()), d_dagBuilt(false), d_idCounter(0),
00034       d_nodag(false) {
00035     d_indentStack.push_back(d_em->indent());
00036     d_indentLast = d_indentStack.size();
00037     d_dagPtr.push_back(0);
00038     d_lastDagSize=d_dagPtr.size();
00039   }
00040 
00041   //! Generating unique names in DAG expr
00042   string ExprStream::newName() {
00043     ostringstream name;
00044     name << "cvc_" << d_idCounter++;
00045     return name.str();
00046   }
00047 
00048   static bool isTrivialExpr(const Expr& e) {
00049     return (e.arity()==0 && !e.isClosure());
00050   }
00051 
00052   //! Traverse the Expr, collect shared subexpressions in d_dagMap
00053   void ExprStream::collectShared(const Expr& e, ExprMap<bool>& cache) {
00054     // If seen before, and it's not something trivial, add to d_dagMap
00055     if(!isTrivialExpr(e) && cache.count(e) > 0) {
00056       if(d_dagMap.count(e) == 0) {
00057   string s(newName());
00058         if (d_lang == SMTLIB_LANG) {
00059           Type type(e.getType());
00060           if (type.isBool()) {
00061             s = "$" + s;
00062           }
00063           else {
00064             s = "?" + s;
00065           }
00066         }
00067   d_dagMap[e] = s;
00068   d_newDagMap[e] = s;
00069   d_dagStack.push_back(e);
00070       }
00071       return;
00072     }
00073     cache[e] = true;
00074     for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
00075       collectShared(*i, cache);
00076     d_dagBuilt = true;
00077   }
00078 
00079   //! Wrap e into the top-level LET ... IN header from the dagMap
00080   /*! 
00081    * We rely on the fact that d_dagMap is ordered by the Expr creation
00082    * order, so earlier expressions cannot depend on later ones.
00083    */
00084   Expr ExprStream::addLetHeader(const Expr& e) {
00085     ExprManager* em = e.getEM();
00086     if(d_newDagMap.size() == 0) return e;
00087     vector<Expr> decls;
00088     for(ExprMap<string>::iterator i=d_newDagMap.begin(),
00089     iend=d_newDagMap.end(); i!=iend; ++i) {
00090       Expr var(em->newVarExpr((*i).second));
00091       if(((*i).first).isType())
00092   decls.push_back(Expr(LETDECL, var, em->newLeafExpr(TYPE),
00093                              (*i).first));
00094       else
00095   decls.push_back(Expr(LETDECL, var, (*i).first));
00096     }
00097     d_newDagMap.clear();
00098     return Expr(LET, Expr(LETDECLS, decls), e);
00099   }
00100 
00101   void ExprStream::popIndent() {
00102     DebugAssert(d_indentStack.size() > 0
00103     && d_indentStack.size() > d_indentLast,
00104     "ExprStream::popIndent(): popped too much: "
00105     "stack size = "+int2string(d_indentStack.size())
00106     +", indentLast = "+int2string(d_indentLast));
00107     if(d_indentStack.size() > 0 && d_indentStack.size() > d_indentLast)
00108       d_indentStack.pop_back();
00109   }
00110 
00111   //! Reset indentation to what it was at this level
00112   void ExprStream::resetIndent() {
00113     while(d_indentStack.size() > d_indentLast)
00114       d_indentStack.pop_back();
00115   }
00116 
00117 
00118   void ExprStream::pushDag() {
00119     d_dagBuilt = false;
00120     d_dagPtr.push_back(d_dagStack.size());
00121   }
00122 
00123   void ExprStream::popDag() {
00124     DebugAssert(d_dagPtr.size() > d_lastDagSize,
00125     "ExprStream::popDag: popping more than pushed");
00126     DebugAssert(d_lastDagSize > 0, "ExprStream::popDag: this cannot happen!");
00127     if(d_dagPtr.size() > d_lastDagSize) {
00128       size_t size(d_dagPtr.back());
00129       d_dagPtr.pop_back();
00130       while(d_dagStack.size() > size) {
00131   d_dagMap.erase(d_dagStack.back());
00132   d_dagStack.pop_back();
00133       }
00134       d_newDagMap.clear();
00135     }
00136   }
00137 
00138   void ExprStream::resetDag() {
00139     while(d_dagPtr.size() > d_lastDagSize) popDag();
00140   }
00141 
00142   /*! \defgroup ExprStream_Op Overloaded operator<< 
00143    * \ingroup PrettyPrinting
00144    * @{
00145    */
00146   //! Use manipulators which are functions over ExprStream&
00147   ExprStream& operator<<(ExprStream& os,
00148        ExprStream& (*manip)(ExprStream&)) {
00149     return (*manip)(os);
00150   }
00151 
00152   //! Print Expr
00153   ExprStream& operator<<(ExprStream& os, const Expr& e) {
00154     //os << "Printing in expr_stream";
00155     // If the max print depth is reached, print "..."
00156     if(os.d_depth >= 0 && os.d_currDepth > os.d_depth) return os << "...";
00157     Expr e2(e);
00158     // Don't LET-ify commands like ASSERT, QUERY, TRANSFORM
00159     switch(e.getKind()) {
00160     case QUERY:
00161     case ASSERT:
00162     case TRANSFORM:
00163     case TYPE:
00164     case CONST:
00165       os.d_nodag = true;
00166       break;
00167     default: break;
00168     }
00169     // Check cache for DAG printing
00170     if(os.d_dag && !os.d_nodag) {
00171       if(os.d_dagBuilt) {
00172   ExprMap<string>::iterator i(os.d_dagMap.find(e));
00173   if(i != os.d_dagMap.end()) {
00174     ostringstream ss;
00175     ss << (*i).second;
00176     return os << ss.str();
00177   }
00178       } else {
00179   // We are at the top level; build dagMap and print LET header
00180   ExprMap<bool> cache;
00181   os.collectShared(e, cache);
00182   e2 = os.addLetHeader(e);
00183       }
00184     }
00185     os.d_nodag=false;
00186 
00187     // Increase the depth before the (possibly) recursive call
00188     os.d_currDepth++;
00189     // Save the indentation stack position and register
00190     int indentLast = os.d_indentLast;
00191     int reg = os.d_indentReg;
00192     size_t lastDagSize = os.d_lastDagSize;
00193 
00194     os.d_indentLast = os.d_indentStack.size();
00195     os.d_lastDagSize = os.d_dagPtr.size();
00196 
00197     PrettyPrinter* pp = os.d_em->getPrinter();
00198     // If no pretty-printer, or the language is AST, print the AST
00199     if(pp == NULL || os.d_lang == AST_LANG) e2.printAST(os);
00200     // Otherwise simply call the pretty-printer
00201     else pp->print(os, e2);
00202     // Restore the depth after the (possibly) recursive call
00203     os.d_currDepth--;
00204 
00205     // Restore the indentation stack and register
00206     os.resetIndent();
00207     os.resetDag();
00208     os.d_indentLast = indentLast;
00209     os.d_indentReg = reg;
00210     os.d_lastDagSize = lastDagSize;
00211     return os;
00212   }
00213 
00214   //! Print Type
00215   ExprStream& operator<<(ExprStream& os, const Type& t) {
00216     return os << t.getExpr();
00217   }
00218 
00219 
00220   //! Print string
00221   /*! This is where all the indentation is happening.
00222 
00223   The algorithm for determining whether to go to the next line is the
00224   following:
00225   
00226   - If the new d_col does not exceed d_lineWidth/2 or current
00227     indentation, don't bother.
00228   
00229   - If the difference between the new d_col and the current
00230     indentation is less than d_lineWidth/4, don't bother either, so
00231     that we don't get lots of very short lines clumped to the right
00232     side.
00233 
00234   - Similarly, if the difference between the old d_col and the current
00235     indentation is less than d_lineWidth/6, keep the same line.
00236     Otherwise, for long atomic strings, we may get useless line breaks.
00237   
00238   - Otherwise, go to the next line.
00239   */
00240   ExprStream& operator<<(ExprStream& os, const string& s) {
00241     // Save the old position
00242     int oldCol(os.d_col);
00243     // The new position after printing s
00244     os.d_col += s.size();
00245     if(os.d_indent) {
00246       // Current indentation position
00247       int n(os.d_indentStack.size()? os.d_indentStack.back() : 0);
00248       // See if we need to go to the next line before printing.
00249       if(2*os.d_col > os.d_lineWidth && 4*(os.d_col - n) > os.d_lineWidth
00250    && 6*(oldCol - n) > os.d_lineWidth) {
00251   os << endl;
00252   // Recompute the new column
00253   os.d_col += s.size();
00254       }
00255     }
00256     *os.d_os << s;
00257     os.d_beginningOfLine = false;
00258     return os;
00259   }
00260 
00261   //! Print char* string
00262   ExprStream& operator<<(ExprStream& os, const char* s) {
00263     return os << string(s);
00264   }
00265 
00266   //! Print Rational
00267   ExprStream& operator<<(ExprStream& os, const Rational& r) {
00268     ostringstream ss;
00269     ss << r;
00270     return os << ss.str();
00271   }
00272 
00273   //! Print int
00274   ExprStream& operator<<(ExprStream& os, int i) {
00275     ostringstream ss;
00276     ss << i;
00277     return os << ss.str();
00278   }
00279   /*! @} */ // End of group ExprStream_Op
00280 
00281   /*! \defgroup ExprStream_Manip Manipulators 
00282    * \ingroup PrettyPrinting
00283    * @{
00284    */
00285 
00286   //! Set the indentation to the current position
00287   ExprStream& push(ExprStream& os) { os.pushIndent(); return os; }
00288 
00289   //! Restore the indentation
00290   ExprStream& pop(ExprStream& os) { os.popIndent(); return os; }
00291   //! Remember the current indentation and pop to the previous position
00292   /*! There is only one register to save the previous position.  If
00293     you use popSave() more than once, only the latest position can be
00294     restored with pushRestore(). */
00295   ExprStream& popSave(ExprStream& os) {
00296     os.d_indentReg = os.d_indentStack.size() ? os.d_indentStack.back() : 0;
00297     os.popIndent();
00298     return os;
00299   }
00300   //! Set the indentation to the position saved by popSave()
00301   /*! There is only one register to save the previous position.  Using
00302     pushRestore() several times will set intendation to the same
00303     position. */
00304   ExprStream& pushRestore(ExprStream& os) {
00305     os.pushIndent(os.d_indentReg);
00306     return os;
00307   }
00308   //! Reset the indentation to the default at this level
00309   ExprStream& reset(ExprStream& os) { os.resetIndent(); return os; }
00310   //! Insert a single white space separator
00311   /*! It is preferred to use 'space' rather than a string of spaces
00312     (" ") because ExprStream needs to delete extra white space if it
00313     decides to end the line.  If you use strings for spaces, you'll
00314     mess up the indentation. */
00315   ExprStream& space(ExprStream& os) {
00316     // Prevent " " to carry to the next line
00317     if(!os.d_beginningOfLine) os << push << " " << pop;
00318     return os;
00319   }
00320 
00321   ExprStream& nodag(ExprStream& os) {
00322     os.d_nodag = true;
00323     return os;
00324   }
00325 
00326   ExprStream& pushdag(ExprStream& os) { os.pushDag(); return os; }
00327 
00328   ExprStream& popdag(ExprStream& os) { os.popDag(); return os; }
00329 
00330   /*! @} */ // End of group ExprStream_Manip
00331 
00332 } // End of namespace CVC3
00333 
00334 namespace std {
00335 
00336   //! Print the end-of-line
00337   /*! 
00338    * The new line will not necessarily start at column 0 because of
00339    * indentation.
00340    * \ingroup ExprStream_Manip 
00341    */
00342   CVC3::ExprStream& endl(CVC3::ExprStream& os) {
00343     if(os.d_indent) {
00344       // Current indentation
00345       int n(os.d_indentStack.size()? os.d_indentStack.back() : 0);
00346       // Create a string of n white spaces
00347       string spaces(n, ' ');
00348       (*os.d_os) << endl << spaces;
00349       os.d_col = n;
00350     } else {
00351       (*os.d_os) << endl;
00352       os.d_col = 0;
00353     }
00354     os.d_beginningOfLine = true;
00355     return os;
00356   }
00357 }

Generated on Tue Jul 3 14:33:37 2007 for CVC3 by  doxygen 1.5.1