CVC3

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