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),
100 if(((*i).first).isType())
113 "ExprStream::popIndent(): popped too much: "
134 "ExprStream::popDag: popping more than pushed");
187 return os << ss.str();
212 else pp->
print(os, e2);
253 int oldCol(os.
d_col);
255 os.
d_col += s.size();
264 os.
d_col += s.size();
274 return os << string(s);
281 return os << ss.str();
288 return os << ss.str();
358 string spaces(n,
' ');
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.
for output in SPASS format
int d_depth
Printing only upto this depth; -1 == unlimited.
iterator begin() const
Begin iterator.
ExprStream & nodag(ExprStream &os)
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
void pushDag()
Recompute shared subexpression for the next Expr.
bool d_indent
Whether to print with indentations.
Data structure of expressions in CVC3.
static bool isTrivialExpr(const Expr &e)
ExprManager * getEM() const
ExprStream & reset(ExprStream &os)
Reset the indentation to the default at this level.
ostream & operator<<(ostream &os, const Expr &e)
iterator find(const Expr &e)
std::string newName()
Generating unique names in DAG expr.
bool d_dagBuilt
Flag whether the dagMap is already built.
for output in TPTP format
ExprMap< std::string > d_newDagMap
New subexpressions not yet printed in a LET header.
MS C++ specific settings.
void pushIndent()
Set the indentation to the current column.
ExprStream & space(ExprStream &os)
Insert a single white space separator.
bool d_beginningOfLine
Whether it is a beginning of line (for eating up extra spaces)
#define DebugAssert(cond, str)
ExprManager * d_em
The ExprManager to use.
size_t d_lastDagSize
The smallest size of d_dagPtr the user can `popDag'.
void resetDag()
Reset the DAG to what it was at this level.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
ExprStream & pushdag(ExprStream &os)
bool d_nodag
nodag() manipulator has been applied
const Expr & getExpr() const
size_t count(const Expr &e) const
std::vector< size_t > d_dagPtr
Stack of pointers to d_dagStack for pushing/popping shared subexprs.
int d_idCounter
Counter for generating unique LET var names.
void popDag()
Delete shared subexpressions previously added with pushdag.
ExprMap< std::string > d_dagMap
Mapping subexpressions to names for DAG printing.
ExprStream & pushRestore(ExprStream &os)
Set the indentation to the position saved by popSave()
Expr newLeafExpr(const Op &op)
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
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.
std::string int2string(int n)
void popIndent()
Restore the indentation (user cannot pop more than pushed)
int d_indentReg
Indentation register for popSave() and pushRestore()
ExprStream & popdag(ExprStream &os)
Expr addLetHeader(const Expr &e)
Wrap e into the top-level LET ... IN header from the dagMap.
int indent() const
Get initial indentation.
void collectShared(const Expr &e, ExprMap< bool > &cache)
Traverse the Expr, collect shared subexpressions in d_dagMap.
int d_col
Current column in a line.
int d_currDepth
Current depth of Expr.
std::string to_upper(const std::string &src)
Expr newVarExpr(const std::string &s)
InputLanguage d_lang
Output language.
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.
Type getType() const
Get the type. Recursively compute if necessary.
std::vector< int > d_indentStack
Indentation stack.
void erase(const Expr &e)
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)
iterator end() const
End iterator.