00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
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
00053 void ExprStream::collectShared(const Expr& e, ExprMap<bool>& cache) {
00054
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
00080
00081
00082
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
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
00143
00144
00145
00146
00147 ExprStream& operator<<(ExprStream& os,
00148 ExprStream& (*manip)(ExprStream&)) {
00149 return (*manip)(os);
00150 }
00151
00152
00153 ExprStream& operator<<(ExprStream& os, const Expr& e) {
00154
00155
00156 if(os.d_depth >= 0 && os.d_currDepth > os.d_depth) return os << "...";
00157 Expr e2(e);
00158
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
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
00180 ExprMap<bool> cache;
00181 os.collectShared(e, cache);
00182 e2 = os.addLetHeader(e);
00183 }
00184 }
00185 os.d_nodag=false;
00186
00187
00188 os.d_currDepth++;
00189
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
00199 if(pp == NULL || os.d_lang == AST_LANG) e2.printAST(os);
00200
00201 else pp->print(os, e2);
00202
00203 os.d_currDepth--;
00204
00205
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
00215 ExprStream& operator<<(ExprStream& os, const Type& t) {
00216 return os << t.getExpr();
00217 }
00218
00219
00220
00221
00222
00223
00224
00225
00226
00227
00228
00229
00230
00231
00232
00233
00234
00235
00236
00237
00238
00239
00240 ExprStream& operator<<(ExprStream& os, const string& s) {
00241
00242 int oldCol(os.d_col);
00243
00244 os.d_col += s.size();
00245 if(os.d_indent) {
00246
00247 int n(os.d_indentStack.size()? os.d_indentStack.back() : 0);
00248
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
00253 os.d_col += s.size();
00254 }
00255 }
00256 *os.d_os << s;
00257 os.d_beginningOfLine = false;
00258 return os;
00259 }
00260
00261
00262 ExprStream& operator<<(ExprStream& os, const char* s) {
00263 return os << string(s);
00264 }
00265
00266
00267 ExprStream& operator<<(ExprStream& os, const Rational& r) {
00268 ostringstream ss;
00269 ss << r;
00270 return os << ss.str();
00271 }
00272
00273
00274 ExprStream& operator<<(ExprStream& os, int i) {
00275 ostringstream ss;
00276 ss << i;
00277 return os << ss.str();
00278 }
00279
00280
00281
00282
00283
00284
00285
00286
00287 ExprStream& push(ExprStream& os) { os.pushIndent(); return os; }
00288
00289
00290 ExprStream& pop(ExprStream& os) { os.popIndent(); return os; }
00291
00292
00293
00294
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
00301
00302
00303
00304 ExprStream& pushRestore(ExprStream& os) {
00305 os.pushIndent(os.d_indentReg);
00306 return os;
00307 }
00308
00309 ExprStream& reset(ExprStream& os) { os.resetIndent(); return os; }
00310
00311
00312
00313
00314
00315 ExprStream& space(ExprStream& os) {
00316
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
00331
00332 }
00333
00334 namespace std {
00335
00336
00337
00338
00339
00340
00341
00342 CVC3::ExprStream& endl(CVC3::ExprStream& os) {
00343 if(os.d_indent) {
00344
00345 int n(os.d_indentStack.size()? os.d_indentStack.back() : 0);
00346
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 }