CVC3
expr_stream.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file expr_stream.cpp
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Mon Jun 16 13:57:29 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #include "pretty_printer.h"
22 #include "expr_stream.h"
23 #include "theory_core.h"
24 
25 using namespace std;
26 
27 namespace CVC3 {
28 
29  ExprStream::ExprStream(ExprManager *em)
30  : d_em(em), d_os(&cout), d_depth(em->printDepth()), d_currDepth(0),
31  d_lang(em->getOutputLang()),
32  d_indent(em->withIndentation()), d_col(em->indent()),
33  d_lineWidth(em->lineWidth()), d_indentReg(0), d_beginningOfLine(false),
34  d_dag(em->dagPrinting()), d_dagBuilt(false), d_idCounter(0),
35  d_nodag(false) {
36  d_indentStack.push_back(d_em->indent());
37  d_indentLast = d_indentStack.size();
38  d_dagPtr.push_back(0);
39  d_lastDagSize=d_dagPtr.size();
40  }
41 
42  //! Generating unique names in DAG expr
44  ostringstream name;
45  name << "v_" << d_idCounter++;
46  return name.str();
47  }
48 
49  static bool isTrivialExpr(const Expr& e) {
50  return (e.arity()==0 && !e.isClosure());
51  }
52 
53  //! Traverse the Expr, collect shared subexpressions in d_dagMap
54  void ExprStream::collectShared(const Expr& e, ExprMap<bool>& cache) {
55  // If seen before, and it's not something trivial, add to d_dagMap
56  if(!isTrivialExpr(e) && cache.count(e) > 0) {
57  if(d_dagMap.count(e) == 0) {
58  string s(newName());
59  if (d_lang == SMTLIB_LANG) {
60  Type type(e.getType());
61  if (type.isBool()) {
62  s = "$" + s;
63  }
64  else {
65  s = "?" + s;
66  }
67  }
68  else if (d_lang == SMTLIB_V2_LANG) {
69  s = "?" + s;
70  }
71  if (d_lang == TPTP_LANG) {
72 
73  s = to_upper( s);
74  }
75 
76  d_dagMap[e] = s;
77  d_newDagMap[e] = s;
78  d_dagStack.push_back(e);
79  }
80  return;
81  }
82  cache[e] = true;
83  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
84  collectShared(*i, cache);
85  d_dagBuilt = true;
86  }
87 
88  //! Wrap e into the top-level LET ... IN header from the dagMap
89  /*!
90  * We rely on the fact that d_dagMap is ordered by the Expr creation
91  * order, so earlier expressions cannot depend on later ones.
92  */
94  ExprManager* em = e.getEM();
95  if(d_newDagMap.size() == 0) return e;
96  vector<Expr> decls;
98  iend=d_newDagMap.end(); i!=iend; ++i) {
99  Expr var(em->newVarExpr((*i).second));
100  if(((*i).first).isType())
101  decls.push_back(Expr(LETDECL, var, em->newLeafExpr(TYPE),
102  (*i).first));
103  else
104  decls.push_back(Expr(LETDECL, var, (*i).first));
105  }
106  d_newDagMap.clear();
107  return Expr(LET, Expr(LETDECLS, decls), e);
108  }
109 
111  DebugAssert(d_indentStack.size() > 0
112  && d_indentStack.size() > d_indentLast,
113  "ExprStream::popIndent(): popped too much: "
114  "stack size = "+int2string(d_indentStack.size())
115  +", indentLast = "+int2string(d_indentLast));
116  if(d_indentStack.size() > 0 && d_indentStack.size() > d_indentLast)
117  d_indentStack.pop_back();
118  }
119 
120  //! Reset indentation to what it was at this level
122  while(d_indentStack.size() > d_indentLast)
123  d_indentStack.pop_back();
124  }
125 
126 
128  d_dagBuilt = false;
129  d_dagPtr.push_back(d_dagStack.size());
130  }
131 
134  "ExprStream::popDag: popping more than pushed");
135  DebugAssert(d_lastDagSize > 0, "ExprStream::popDag: this cannot happen!");
136  if(d_dagPtr.size() > d_lastDagSize) {
137  size_t size(d_dagPtr.back());
138  d_dagPtr.pop_back();
139  while(d_dagStack.size() > size) {
140  d_dagMap.erase(d_dagStack.back());
141  d_dagStack.pop_back();
142  }
143  d_newDagMap.clear();
144  }
145  }
146 
148  while(d_dagPtr.size() > d_lastDagSize) popDag();
149  }
150 
151  /*! \defgroup ExprStream_Op Overloaded operator<<
152  * \ingroup PrettyPrinting
153  * @{
154  */
155  //! Use manipulators which are functions over ExprStream&
157  ExprStream& (*manip)(ExprStream&)) {
158  return (*manip)(os);
159  }
160 
161  //! Print Expr
163  //os << "Printing in expr_stream";
164  // If the max print depth is reached, print "..."
165  if(os.d_depth >= 0 && os.d_currDepth > os.d_depth) return os << "...";
166  Expr e2(e);
167  // Don't LET-ify commands like ASSERT, QUERY, TRANSFORM
168  switch(e.getKind()) {
169  case QUERY:
170  case ASSERT:
171  case RESTART:
172  case TRANSFORM:
173  case TYPE:
174  case CONST:
175  os.d_nodag = true;
176  break;
177  default: break;
178  }
179  // Check cache for DAG printing
180  if(os.d_dag && !os.d_nodag &&
181  os.d_lang != SPASS_LANG) { // SPASS doesn't support LET
182  if(os.d_dagBuilt) {
184  if(i != os.d_dagMap.end()) {
185  ostringstream ss;
186  ss << (*i).second;
187  return os << ss.str();
188  }
189  } else {
190  // We are at the top level; build dagMap and print LET header
191  ExprMap<bool> cache;
192  os.collectShared(e, cache);
193  e2 = os.addLetHeader(e);
194  }
195  }
196  os.d_nodag=false;
197 
198  // Increase the depth before the (possibly) recursive call
199  os.d_currDepth++;
200  // Save the indentation stack position and register
201  int indentLast = os.d_indentLast;
202  int reg = os.d_indentReg;
203  size_t lastDagSize = os.d_lastDagSize;
204 
205  os.d_indentLast = os.d_indentStack.size();
206  os.d_lastDagSize = os.d_dagPtr.size();
207 
208  PrettyPrinter* pp = os.d_em->getPrinter();
209  // If no pretty-printer, or the language is AST, print the AST
210  if(pp == NULL || os.d_lang == AST_LANG) e2.printAST(os);
211  // Otherwise simply call the pretty-printer
212  else pp->print(os, e2);
213  // Restore the depth after the (possibly) recursive call
214  os.d_currDepth--;
215 
216  // Restore the indentation stack and register
217  os.resetIndent();
218  os.resetDag();
219  os.d_indentLast = indentLast;
220  os.d_indentReg = reg;
221  os.d_lastDagSize = lastDagSize;
222  return os;
223  }
224 
225  //! Print Type
227  return os << t.getExpr();
228  }
229 
230 
231  //! Print string
232  /*! This is where all the indentation is happening.
233 
234  The algorithm for determining whether to go to the next line is the
235  following:
236 
237  - If the new d_col does not exceed d_lineWidth/2 or current
238  indentation, don't bother.
239 
240  - If the difference between the new d_col and the current
241  indentation is less than d_lineWidth/4, don't bother either, so
242  that we don't get lots of very short lines clumped to the right
243  side.
244 
245  - Similarly, if the difference between the old d_col and the current
246  indentation is less than d_lineWidth/6, keep the same line.
247  Otherwise, for long atomic strings, we may get useless line breaks.
248 
249  - Otherwise, go to the next line.
250  */
251  ExprStream& operator<<(ExprStream& os, const string& s) {
252  // Save the old position
253  int oldCol(os.d_col);
254  // The new position after printing s
255  os.d_col += s.size();
256  if(os.d_indent) {
257  // Current indentation position
258  int n(os.d_indentStack.size()? os.d_indentStack.back() : 0);
259  // See if we need to go to the next line before printing.
260  if(2*os.d_col > os.d_lineWidth && 4*(os.d_col - n) > os.d_lineWidth
261  && 6*(oldCol - n) > os.d_lineWidth) {
262  os << endl;
263  // Recompute the new column
264  os.d_col += s.size();
265  }
266  }
267  *os.d_os << s;
268  os.d_beginningOfLine = false;
269  return os;
270  }
271 
272  //! Print char* string
273  ExprStream& operator<<(ExprStream& os, const char* s) {
274  return os << string(s);
275  }
276 
277  //! Print Rational
279  ostringstream ss;
280  ss << r;
281  return os << ss.str();
282  }
283 
284  //! Print int
286  ostringstream ss;
287  ss << i;
288  return os << ss.str();
289  }
290  /*! @} */ // End of group ExprStream_Op
291 
292  /*! \defgroup ExprStream_Manip Manipulators
293  * \ingroup PrettyPrinting
294  * @{
295  */
296 
297  //! Set the indentation to the current position
298  ExprStream& push(ExprStream& os) { os.pushIndent(); return os; }
299 
300  //! Restore the indentation
301  ExprStream& pop(ExprStream& os) { os.popIndent(); return os; }
302  //! Remember the current indentation and pop to the previous position
303  /*! There is only one register to save the previous position. If
304  you use popSave() more than once, only the latest position can be
305  restored with pushRestore(). */
307  os.d_indentReg = os.d_indentStack.size() ? os.d_indentStack.back() : 0;
308  os.popIndent();
309  return os;
310  }
311  //! Set the indentation to the position saved by popSave()
312  /*! There is only one register to save the previous position. Using
313  pushRestore() several times will set intendation to the same
314  position. */
316  os.pushIndent(os.d_indentReg);
317  return os;
318  }
319  //! Reset the indentation to the default at this level
320  ExprStream& reset(ExprStream& os) { os.resetIndent(); return os; }
321  //! Insert a single white space separator
322  /*! It is preferred to use 'space' rather than a string of spaces
323  (" ") because ExprStream needs to delete extra white space if it
324  decides to end the line. If you use strings for spaces, you'll
325  mess up the indentation. */
327  // Prevent " " to carry to the next line
328  if(!os.d_beginningOfLine) os << push << " " << pop;
329  return os;
330  }
331 
333  os.d_nodag = true;
334  return os;
335  }
336 
337  ExprStream& pushdag(ExprStream& os) { os.pushDag(); return os; }
338 
339  ExprStream& popdag(ExprStream& os) { os.popDag(); return os; }
340 
341  /*! @} */ // End of group ExprStream_Manip
342 
343 } // End of namespace CVC3
344 
345 namespace std {
346 
347  //! Print the end-of-line
348  /*!
349  * The new line will not necessarily start at column 0 because of
350  * indentation.
351  * \ingroup ExprStream_Manip
352  */
354  if(os.d_indent) {
355  // Current indentation
356  int n(os.d_indentStack.size()? os.d_indentStack.back() : 0);
357  // Create a string of n white spaces
358  string spaces(n, ' ');
359  (*os.d_os) << endl << spaces;
360  os.d_col = n;
361  } else {
362  (*os.d_os) << endl;
363  os.d_col = 0;
364  }
365  os.d_beginningOfLine = true;
366  return os;
367  }
368 }