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