CVC3  2.4.1
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 }
int arity() const
Definition: expr.h:1201
ExprStream & popSave(ExprStream &os)
Remember the current indentation and pop to the previous position.
ExprStream & pop(ExprStream &os)
Restore the indentation.
std::ostream * d_os
The ostream to print into.
Definition: expr_stream.h:113
for output in SPASS format
Definition: lang.h:49
int d_depth
Printing only upto this depth; -1 == unlimited.
Definition: expr_stream.h:114
iterator begin() const
Begin iterator.
Definition: expr.h:1211
ExprStream & nodag(ExprStream &os)
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
Definition: expr.cpp:400
void pushDag()
Recompute shared subexpression for the next Expr.
bool d_indent
Whether to print with indentations.
Definition: expr_stream.h:117
void clear()
Definition: expr_map.h:175
Data structure of expressions in CVC3.
Definition: expr.h:133
static bool isTrivialExpr(const Expr &e)
Definition: expr_stream.cpp:49
ExprManager * getEM() const
Definition: expr.h:1156
ExprStream & reset(ExprStream &os)
Reset the indentation to the default at this level.
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
iterator find(const Expr &e)
Definition: expr_map.h:194
Definition: kinds.h:227
Definition: kinds.h:225
std::string newName()
Generating unique names in DAG expr.
Definition: expr_stream.cpp:43
bool d_dagBuilt
Flag whether the dagMap is already built.
Definition: expr_stream.h:143
for output in TPTP format
Definition: lang.h:46
ExprMap< std::string > d_newDagMap
New subexpressions not yet printed in a LET header.
Definition: expr_stream.h:135
MS C++ specific settings.
Definition: type.h:42
SMT-LIB v2 format.
Definition: lang.h:52
STL namespace.
iterator begin()
Definition: expr_map.h:190
void pushIndent()
Set the indentation to the current column.
Definition: expr_stream.h:179
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Definition: kinds.h:240
bool d_beginningOfLine
Whether it is a beginning of line (for eating up extra spaces)
Definition: expr_stream.h:130
#define DebugAssert(cond, str)
Definition: debug.h:408
size_t size() const
Definition: expr_map.h:171
ExprManager * d_em
The ExprManager to use.
Definition: expr_stream.h:112
size_t d_lastDagSize
The smallest size of d_dagPtr the user can `popDag'.
Definition: expr_stream.h:141
void resetDag()
Reset the DAG to what it was at this level.
Definition: kinds.h:97
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
ExprStream & pushdag(ExprStream &os)
bool d_nodag
nodag() manipulator has been applied
Definition: expr_stream.h:147
const Expr & getExpr() const
Definition: type.h:52
bool isClosure() const
Definition: expr.h:1007
size_t count(const Expr &e) const
Definition: expr_map.h:173
std::vector< size_t > d_dagPtr
Stack of pointers to d_dagStack for pushing/popping shared subexprs.
Definition: expr_stream.h:139
int d_idCounter
Counter for generating unique LET var names.
Definition: expr_stream.h:145
void popDag()
Delete shared subexpressions previously added with pushdag.
ExprMap< std::string > d_dagMap
Mapping subexpressions to names for DAG printing.
Definition: expr_stream.h:133
ExprStream & pushRestore(ExprStream &os)
Set the indentation to the position saved by popSave()
Expr newLeafExpr(const Op &op)
Definition: expr_manager.h:454
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
void resetIndent()
Reset indentation to what it was at this level.
PrettyPrinter * getPrinter() const
Return the pretty-printer if there is one; otherwise return NULL.
Definition: expr_manager.h:371
std::string int2string(int n)
Definition: cvc_util.h:46
Expression Manager.
Definition: expr_manager.h:58
void popIndent()
Restore the indentation (user cannot pop more than pushed)
int d_indentReg
Indentation register for popSave() and pushRestore()
Definition: expr_stream.h:128
ExprStream & popdag(ExprStream &os)
Expr addLetHeader(const Expr &e)
Wrap e into the top-level LET ... IN header from the dagMap.
Definition: expr_stream.cpp:93
int indent() const
Get initial indentation.
Definition: expr_manager.h:354
Definition: kinds.h:94
void collectShared(const Expr &e, ExprMap< bool > &cache)
Traverse the Expr, collect shared subexpressions in d_dagMap.
Definition: expr_stream.cpp:54
int d_col
Current column in a line.
Definition: expr_stream.h:118
int d_currDepth
Current depth of Expr.
Definition: expr_stream.h:115
std::string to_upper(const std::string &src)
Definition: cvc_util.h:30
SMT-LIB format.
Definition: lang.h:34
Expr newVarExpr(const std::string &s)
Definition: expr_manager.h:478
InputLanguage d_lang
Output language.
Definition: expr_stream.h:116
virtual ExprStream & print(ExprStream &os, const Expr &e)=0
The pretty-printer which subclasses must implement.
size_t d_indentLast
The lowest position of the indent stack the user can pop.
Definition: expr_stream.h:126
Definition: kinds.h:93
Definition: kinds.h:53
Definition: expr.cpp:35
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
std::vector< int > d_indentStack
Indentation stack.
Definition: expr_stream.h:124
iterator end()
Definition: expr_map.h:191
void erase(const Expr &e)
Definition: expr_map.h:178
Abstract API to a pretty-printer for Expr.
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
std::vector< Expr > d_dagStack
Stack of shared subexpressions (same as in d_dagMap)
Definition: expr_stream.h:137
iterator end() const
End iterator.
Definition: expr.h:1217