CVCL::ExprStream Class Reference
[Pretty-printing related classes and methods]

Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING! More...

#include <expr_stream.h>

Collaboration diagram for CVCL::ExprStream:

[legend]List of all members.

Public Member Functions

• ExprStream (ExprManager *em)

  Default constructor.
  

• ~ExprStream ()

  Destructor.
  

• void os (std::ostream &os)

  Set a new output stream.
  

• InputLanguage lang () const

  Get the current output language.
  

• void lang (InputLanguage l)

  Set the output language.
  

• int depth () const

  Get the printing depth.
  

• void depth (int d)

  Set the printing depth.
  

• void lineWidth (int w)

  Set the line width.
  

• void dagFlag (bool flag=true)

  Set the DAG flag.
  

• void pushIndent ()

  Set the indentation to the current column.
  

• void pushIndent (int pos)

  Set the indentation to the given absolute position.
  

• void popIndent ()

  Restore the indentation (user cannot pop more than pushed).
  

• void resetIndent ()

  Reset indentation to what it was at this level.
  

• int column () const

  Return the current column position.
  

• void pushDag ()

  Recompute shared subexpression for the next Expr.
  

• void popDag ()

  Delete shared subexpressions previously added with pushdag.
  

• void resetDag ()

  Reset the DAG to what it was at this level.
  

• const Expr & getParent ()

  Get parent of current expr being printed.
  

Private Member Functions

• std::string newName ()

  Generating unique names in DAG expr.
  

• void collectShared (const Expr &e, ExprMap< bool > &cache)

  Traverse the Expr, collect shared subexpressions in d_dagMap.
  

• Expr addLetHeader (const Expr &e)

  Wrap e into the top-level LET ... IN header from the dagMap.
  

Private Attributes

• ExprManager * d_em

  The ExprManager to use.
  

• std::ostream * d_os

  The ostream to print into.
  

• int d_depth

  Printing only upto this depth; -1 == unlimited.
  

• int d_currDepth

  Current depth of Expr.
  

• InputLanguage d_lang

  Output language.
  

• bool d_indent

  Whether to print with indentations.
  

• int d_col

  Current column in a line.
  

• int d_lineWidth
• std::vector< int > d_indentStack

  Indentation stack.
  

• size_t d_indentLast

  The lowest position of the indent stack the user can pop.
  

• int d_indentReg

  Indentation register for popSave() and pushRestore().
  

• bool d_beginningOfLine

  Whether it is a beginning of line (for eating up extra spaces).
  

• bool d_dag
• ExprMap< std::string > d_dagMap

  Mapping subexpressions to names for DAG printing.
  

• ExprMap< std::string > d_newDagMap

  New subexpressions not yet printed in a LET header.
  

• std::vector< Expr > d_dagStack

  Stack of shared subexpressions (same as in d_dagMap).
  

• std::vector< size_t > d_dagPtr

  Stack of pointers to d_dagStack for pushing/popping shared subexprs.
  

• size_t d_lastDagSize

  The smallest size of d_dagPtr the user can `popDag'.
  

• bool d_dagBuilt

  Flag whether the dagMap is already built.
  

• int d_idCounter

  Counter for generating unique LET var names.
  

• bool d_nodag

  nodag() manipulator has been applied
  

• Expr d_parent

  Parent of current expr being printed.
  

• Expr d_current

  Current expr being printed.
  

Friends

• ExprStream & operator<< (ExprStream &os, ExprStream &(*manip)(ExprStream &))

  Use manipulators which are functions over ExprStream&.
  

• ExprStream & operator<< (ExprStream &os, const Expr &e)

  Print Expr.
  

• ExprStream & operator<< (ExprStream &os, const Type &t)

  Print Type.
  

• ExprStream & operator<< (ExprStream &os, const std::string &s)

  Print string.
  

• ExprStream & operator<< (ExprStream &os, const char *s)

  Print char* string.
  

• ExprStream & operator<< (ExprStream &os, const Rational &r)

  Print Rational.
  

• ExprStream & operator<< (ExprStream &os, int i)

  Print int.
  

• ExprStream & push (ExprStream &os)

  Set the indentation to the current position.
  

• ExprStream & pop (ExprStream &os)

  Restore the indentation to the previous position.
  

• ExprStream & popSave (ExprStream &os)

  Remember the current indentation and pop to the previous position.
  

• ExprStream & pushRestore (ExprStream &os)

  Set the indentation to the position saved by popSave().
  

• ExprStream & reset (ExprStream &os)

  Reset the indentation to the default at this level.
  

• ExprStream & space (ExprStream &os)

  Insert a single white space separator.
  

• ExprStream & nodag (ExprStream &os)

  Print the next top-level expression node without DAG-ifying.
  

• ExprStream & pushdag (ExprStream &os)

  Recompute shared subexpression for the next Expr.
  

• ExprStream & popdag (ExprStream &os)

  Delete shared subexpressions previously added with pushdag.
  

• ExprStream & endl (ExprStream &os)

  Print the end-of-line.
  

---

Detailed Description

Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!

Use this class as a standard ostream for Expr, string, int, Rational, manipulators like endl, and it will do the expected thing. Additionally, it has methods to access the current printing flags.

In order for the indentation engine to work correctly, you must use the manipulators properly.

Never use "\\n" in a string; always use endl manipulator, which knows about indentation and will do the right thing.

Always assume that the object you are printing may start printing on a new line from the current indentation position. Therefore, no string should start with an empty space (otherwise parts of your expression will be mis-indented). If you need a white space separator, or an operator surrounded by spaces, like os << " = ", use os << space << "= " instead. The 'space' manipulator adds one white space only if it's not at the beginning of a newly indented line. Think of it as a logical white-space separator with intelligent behavior, rather than a stupid hard space like " ".

Indentation can be set to the current position with os << push, and restored to the previous with os << pop. You do not need to restore it before exiting your print function, ExprStream knows how to restore it automatically. For example, you can write:

os << "(" << push << e[0] << space << "+ " << e[1] << push << ")";

to print (PLUS a b) as "(a + b)". Notice the second 'push' before the closing paren. This is intentional (not a typo), and prevents the paren ")" from jumping to the next line by itself. ExprStream will not go to the next line if the current position is too close to the indentation, since this will not give the expression a better look.

The indentation level is not restored in this example, and that is fine, ExprStream will take care of that.

For complex expressions like IF-THEN-ELSE, you may want to remember the indentation to which you want to return later. You can save the current indentation position with os << popSave, and restore it later with os << pushRestore. These manipulators are similar to pop and push, but 'pushRestore' will set the new indentation level to the one popped by the last popSave instead of the current one. At the moment, there is only one register for saving an indentation position, so multiple pushRestore will not work as you would expect (maybe this should be fixed?..).

For concrete examples, see TheoryCore::print() and TheoryArith::print().

Definition at line 117 of file expr_stream.h.

---

Constructor & Destructor Documentation

CVCL::ExprStream::ExprStream (  ExprManager *  em  )

Default constructor. Definition at line 39 of file expr_stream.cpp. References d_dagPtr, d_em, d_indentLast, d_indentStack, d_lastDagSize, and CVCL::ExprManager::indent().

CVCL::ExprStream::~ExprStream (   )  [inline]

Destructor. Definition at line 169 of file expr_stream.h.

---

Member Function Documentation

string CVCL::ExprStream::newName (   )  [private]

Generating unique names in DAG expr. Definition at line 53 of file expr_stream.cpp. References d_idCounter. Referenced by collectShared().

void CVCL::ExprStream::collectShared (  const Expr &  e, ExprMap< bool > &  cache )  [private]

Traverse the Expr, collect shared subexpressions in d_dagMap. Definition at line 79 of file expr_stream.cpp. References CVCL::Expr::begin(), CVCL::ExprMap< Data >::count(), d_dagBuilt, d_dagMap, d_dagStack, d_lang, d_newDagMap, CVCL::Expr::end(), CVCL::Type::isBool(), CVCL::isTrivialExpr(), newName(), and CVCL::SMTLIB_LANG. Referenced by CVCL::operator<<().

Expr CVCL::ExprStream::addLetHeader (  const Expr &  e  )  [private]

Wrap e into the top-level LET ... IN header from the dagMap. We rely on the fact that d_dagMap is ordered by the Expr creation order, so earlier expressions cannot depend on later ones. Definition at line 110 of file expr_stream.cpp. References CVCL::ExprMap< Data >::begin(), CVCL::ExprMap< Data >::clear(), d_newDagMap, CVCL::ExprMap< Data >::end(), CVCL::Expr::getEM(), CVCL::LET, CVCL::LETDECL, CVCL::LETDECLS, CVCL::ExprManager::newLeafExpr(), CVCL::ExprManager::newVarExpr(), CVCL::ExprMap< Data >::size(), and CVCL::TYPE. Referenced by CVCL::operator<<().

void CVCL::ExprStream::os (  std::ostream &  os  )  [inline]

Set a new output stream. Note, that there is no method to access the ostream. This is done on purpose, so that DP designers had to use only ExprStream to print everything in their versions of Theory::print(). Definition at line 174 of file expr_stream.h. References d_os. Referenced by CVCL::operator<<(), and CVCL::Expr::toString().

InputLanguage CVCL::ExprStream::lang (   )  const [inline]

Get the current output language. Definition at line 176 of file expr_stream.h. References d_lang. Referenced by CVCL::TheoryUF::print(), CVCL::TheorySimulate::print(), CVCL::TheoryRecords::print(), CVCL::TheoryQuant::print(), CVCL::TheoryDatatype::print(), TheoryCore::print(), CVCL::TheoryBitvector::print(), CVCL::TheoryArray::print(), CVCL::TheoryArith::print(), CVCL::Expr::print(), and CVCL::Expr::toString().

void CVCL::ExprStream::lang (  InputLanguage  l  )  [inline]

Set the output language. Definition at line 178 of file expr_stream.h. References d_lang.

int CVCL::ExprStream::depth (   )  const [inline]

Get the printing depth. Definition at line 180 of file expr_stream.h. References d_depth.

void CVCL::ExprStream::depth (  int  d  )  [inline]

Set the printing depth. Definition at line 182 of file expr_stream.h. References d_depth.

void CVCL::ExprStream::lineWidth (  int  w  )  [inline]

Set the line width. Definition at line 184 of file expr_stream.h. References d_lineWidth.

void CVCL::ExprStream::dagFlag (  bool  flag = true  )  [inline]

Set the DAG flag. Definition at line 186 of file expr_stream.h. References d_dag. Referenced by CVCL::Expr::pprintnodag(), and CVCL::Expr::print().

void CVCL::ExprStream::pushIndent (   )  [inline]

Set the indentation to the current column. The value will be restorted automatically after the DP print() function returns Definition at line 190 of file expr_stream.h. References d_col, and d_indentStack. Referenced by CVCL::push(), and CVCL::pushRestore().

void CVCL::ExprStream::pushIndent (  int  pos  )  [inline]

Set the indentation to the given absolute position. The value will be restorted automatically after the DP print() function returns Definition at line 194 of file expr_stream.h. References d_indentStack.

void CVCL::ExprStream::popIndent (   )

Restore the indentation (user cannot pop more than pushed). Definition at line 127 of file expr_stream.cpp. References d_indentLast, d_indentStack, and CVCL::int2string(). Referenced by CVCL::pop(), and CVCL::popSave().

void CVCL::ExprStream::resetIndent (   )

Reset indentation to what it was at this level. Definition at line 138 of file expr_stream.cpp. References d_indentLast, and d_indentStack. Referenced by CVCL::operator<<(), CVCL::Expr::print(), CVCL::Expr::printAST(), and CVCL::reset().

int CVCL::ExprStream::column (   )  const [inline]

Return the current column position. Definition at line 200 of file expr_stream.h. References d_col.

void CVCL::ExprStream::pushDag (   )

Recompute shared subexpression for the next Expr. Definition at line 144 of file expr_stream.cpp. References d_dagBuilt, d_dagPtr, and d_dagStack. Referenced by CVCL::pushdag().

void CVCL::ExprStream::popDag (   )

Delete shared subexpressions previously added with pushdag. Definition at line 149 of file expr_stream.cpp. References CVCL::ExprMap< Data >::clear(), d_dagMap, d_dagPtr, d_dagStack, d_lastDagSize, d_newDagMap, and CVCL::ExprMap< Data >::erase(). Referenced by CVCL::popdag(), and resetDag().

void CVCL::ExprStream::resetDag (   )

Reset the DAG to what it was at this level. Definition at line 164 of file expr_stream.cpp. References d_dagPtr, d_lastDagSize, and popDag(). Referenced by CVCL::operator<<().

const Expr& CVCL::ExprStream::getParent (   )  [inline]

Get parent of current expr being printed. Definition at line 208 of file expr_stream.h. References d_parent. Referenced by CVCL::TheoryArith::print().

---

Friends And Related Function Documentation

ExprStream& operator<< (  ExprStream &  os, ExprStream &(*)(ExprStream &)  manip )  [friend]

Use manipulators which are functions over ExprStream&. Definition at line 173 of file expr_stream.cpp.

ExprStream& operator<< (  ExprStream &  os, const Expr &  e )  [friend]

Print Expr. Definition at line 179 of file expr_stream.cpp.

ExprStream& operator<< (  ExprStream &  os, const Type &  t )  [friend]

Print Type. Definition at line 247 of file expr_stream.cpp.

ExprStream& operator<< (  ExprStream &  os, const std::string &  s )  [friend]

Print string.

ExprStream& operator<< (  ExprStream &  os, const char *  s )  [friend]

Print char* string. Definition at line 294 of file expr_stream.cpp.

ExprStream& operator<< (  ExprStream &  os, const Rational &  r )  [friend]

Print Rational. Definition at line 299 of file expr_stream.cpp.

ExprStream& operator<< (  ExprStream &  os, int  i )  [friend]

Print int. Definition at line 306 of file expr_stream.cpp.

ExprStream& push (  ExprStream &  os  )  [friend]

Set the indentation to the current position. Definition at line 319 of file expr_stream.cpp.

ExprStream& pop (  ExprStream &  os  )  [friend]

Restore the indentation to the previous position. Definition at line 322 of file expr_stream.cpp.

ExprStream& popSave (  ExprStream &  os  )  [friend]

Remember the current indentation and pop to the previous position. There is only one register to save the previous position. If you use popSave() more than once, only the latest position can be restored with pushRestore(). Definition at line 327 of file expr_stream.cpp.

ExprStream& pushRestore (  ExprStream &  os  )  [friend]

Set the indentation to the position saved by popSave(). There is only one register to save the previous position. Using pushRestore() several times will set intendation to the same position. Definition at line 336 of file expr_stream.cpp.

ExprStream& reset (  ExprStream &  os  )  [friend]

Reset the indentation to the default at this level. Definition at line 341 of file expr_stream.cpp.

ExprStream& space (  ExprStream &  os  )  [friend]

Insert a single white space separator. It is preferred to use 'space' rather than a string of spaces (" ") because ExprStream needs to delete extra white space if it decides to end the line. If you use strings for spaces, you'll mess up the indentation. Definition at line 347 of file expr_stream.cpp.

ExprStream& nodag (  ExprStream &  os  )  [friend]

Print the next top-level expression node without DAG-ifying. DAG-printing will resume for the children of the node. This is useful when printing definitions in the header of a DAGified LET expressions: defs have names, but must be printed expanded. Definition at line 353 of file expr_stream.cpp.

ExprStream& pushdag (  ExprStream &  os  )  [friend]

Recompute shared subexpression for the next Expr. For some constructs with bound variables (notably, quantifiers), shared subexpressions are not computed, because they cannot be defined outside the scope of bound variables. If this manipulator is applied before an expression within the scope of bound vars, these internal subexpressions will then be computed. Definition at line 358 of file expr_stream.cpp.

ExprStream& popdag (  ExprStream &  os  )  [friend]

Delete shared subexpressions previously added with pushdag. Similar to push/pop, shared subexpressions are automatically deleted upon a return from a recursive call, so popdag is not necessary after a pushdag in theory-specific print() functions. Also, you cannot pop more than you pushed an the current recursion level. Definition at line 360 of file expr_stream.cpp.

ExprStream& endl (  CVCL::ExprStream &  os  )  [friend]

Print the end-of-line. The new line will not necessarily start at column 0 because of indentation. Definition at line 374 of file expr_stream.cpp.

---

Member Data Documentation

ExprManager* CVCL::ExprStream::d_em [private]

The ExprManager to use. Definition at line 119 of file expr_stream.h. Referenced by ExprStream(), and CVCL::operator<<().

std::ostream* CVCL::ExprStream::d_os [private]

The ostream to print into. Definition at line 120 of file expr_stream.h. Referenced by std::endl(), CVCL::operator<<(), and os().

int CVCL::ExprStream::d_depth [private]

Printing only upto this depth; -1 == unlimited. Definition at line 121 of file expr_stream.h. Referenced by depth(), and CVCL::operator<<().

int CVCL::ExprStream::d_currDepth [private]

Current depth of Expr. Definition at line 122 of file expr_stream.h. Referenced by CVCL::operator<<().

InputLanguage CVCL::ExprStream::d_lang [private]

Output language. Definition at line 123 of file expr_stream.h. Referenced by collectShared(), lang(), and CVCL::operator<<().

bool CVCL::ExprStream::d_indent [private]

Whether to print with indentations. Definition at line 124 of file expr_stream.h. Referenced by std::endl(), and CVCL::operator<<().

int CVCL::ExprStream::d_col [private]

Current column in a line. Definition at line 125 of file expr_stream.h. Referenced by column(), std::endl(), CVCL::operator<<(), and pushIndent().

int CVCL::ExprStream::d_lineWidth [private]

Try to format/indent for this line width Definition at line 126 of file expr_stream.h. Referenced by lineWidth(), and CVCL::operator<<().

std::vector<int> CVCL::ExprStream::d_indentStack [private]

Indentation stack. The user code can set the indentation to the current d_col by pushing the new value on the stack. This value is popped automatically when returning from the recursive call. Definition at line 131 of file expr_stream.h. Referenced by std::endl(), ExprStream(), CVCL::operator<<(), popIndent(), CVCL::popSave(), pushIndent(), and resetIndent().

size_t CVCL::ExprStream::d_indentLast [private]

The lowest position of the indent stack the user can pop. Definition at line 133 of file expr_stream.h. Referenced by ExprStream(), CVCL::operator<<(), popIndent(), and resetIndent().

int CVCL::ExprStream::d_indentReg [private]

Indentation register for popSave() and pushRestore(). Definition at line 135 of file expr_stream.h. Referenced by CVCL::operator<<(), CVCL::popSave(), and CVCL::pushRestore().

bool CVCL::ExprStream::d_beginningOfLine [private]

Whether it is a beginning of line (for eating up extra spaces). Definition at line 137 of file expr_stream.h. Referenced by std::endl(), CVCL::operator<<(), and CVCL::space().

bool CVCL::ExprStream::d_dag [private]

Print Expr as a DAG Definition at line 138 of file expr_stream.h. Referenced by dagFlag(), and CVCL::operator<<().

ExprMap<std::string> CVCL::ExprStream::d_dagMap [private]

Mapping subexpressions to names for DAG printing. Definition at line 140 of file expr_stream.h. Referenced by collectShared(), CVCL::operator<<(), and popDag().

ExprMap<std::string> CVCL::ExprStream::d_newDagMap [private]

New subexpressions not yet printed in a LET header. Definition at line 142 of file expr_stream.h. Referenced by addLetHeader(), collectShared(), and popDag().

std::vector<Expr> CVCL::ExprStream::d_dagStack [private]

Stack of shared subexpressions (same as in d_dagMap). Definition at line 144 of file expr_stream.h. Referenced by collectShared(), popDag(), and pushDag().

std::vector<size_t> CVCL::ExprStream::d_dagPtr [private]

Stack of pointers to d_dagStack for pushing/popping shared subexprs. Definition at line 146 of file expr_stream.h. Referenced by ExprStream(), CVCL::operator<<(), popDag(), pushDag(), and resetDag().

size_t CVCL::ExprStream::d_lastDagSize [private]

The smallest size of d_dagPtr the user can `popDag'. Definition at line 148 of file expr_stream.h. Referenced by ExprStream(), CVCL::operator<<(), popDag(), and resetDag().

bool CVCL::ExprStream::d_dagBuilt [private]

Flag whether the dagMap is already built. Definition at line 150 of file expr_stream.h. Referenced by collectShared(), CVCL::operator<<(), and pushDag().

int CVCL::ExprStream::d_idCounter [private]

Counter for generating unique LET var names. Definition at line 152 of file expr_stream.h. Referenced by newName().

bool CVCL::ExprStream::d_nodag [private]

nodag() manipulator has been applied Definition at line 154 of file expr_stream.h. Referenced by CVCL::nodag(), and CVCL::operator<<().

Expr CVCL::ExprStream::d_parent [private]

Parent of current expr being printed. Definition at line 156 of file expr_stream.h. Referenced by getParent(), and CVCL::operator<<().

Expr CVCL::ExprStream::d_current [private]

Current expr being printed. Definition at line 158 of file expr_stream.h. Referenced by CVCL::operator<<().

---

The documentation for this class was generated from the following files:

• expr_stream.h
• expr_stream.cpp

---