CVC3
Public Member Functions | Private Member Functions | Private Attributes | Friends

CVC3::ExprStream Class Reference

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

#include <expr_stream.h>

Collaboration diagram for CVC3::ExprStream:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Friends


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 110 of file expr_stream.h.


Constructor & Destructor Documentation

CVC3::ExprStream::ExprStream ( ExprManager em)

Default constructor.

Definition at line 29 of file expr_stream.cpp.

References d_dagPtr, d_em, d_indentLast, d_indentStack, d_lastDagSize, and CVC3::ExprManager::indent().

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

Destructor.

Definition at line 158 of file expr_stream.h.


Member Function Documentation

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

Generating unique names in DAG expr.

Definition at line 43 of file expr_stream.cpp.

References d_idCounter.

Referenced by collectShared().

void CVC3::ExprStream::collectShared ( const Expr e,
ExprMap< bool > &  cache 
) [private]
Expr CVC3::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 93 of file expr_stream.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::clear(), d_newDagMap, CVC3::ExprMap< Data >::end(), CVC3::Expr::getEM(), LET, LETDECL, LETDECLS, CVC3::ExprManager::newLeafExpr(), CVC3::ExprManager::newVarExpr(), CVC3::ExprMap< Data >::size(), and TYPE.

Referenced by CVC3::operator<<().

void CVC3::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 163 of file expr_stream.h.

References os().

Referenced by CVC3::operator<<(), os(), and CVC3::Expr::toString().

InputLanguage CVC3::ExprStream::lang ( ) const [inline]
void CVC3::ExprStream::lang ( InputLanguage  l) [inline]

Set the output language.

Definition at line 167 of file expr_stream.h.

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

Get the printing depth.

Definition at line 169 of file expr_stream.h.

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

Set the printing depth.

Definition at line 171 of file expr_stream.h.

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

Set the line width.

Definition at line 173 of file expr_stream.h.

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

Set the DAG flag (return previous value)

Definition at line 175 of file expr_stream.h.

Referenced by CVC3::Expr::pprintnodag(), CVC3::TheoryUF::print(), CVC3::Expr::print(), and CVC3::VCCmd::printSymbols().

void CVC3::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 179 of file expr_stream.h.

Referenced by CVC3::push(), and CVC3::pushRestore().

void CVC3::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 183 of file expr_stream.h.

void CVC3::ExprStream::popIndent ( )

Restore the indentation (user cannot pop more than pushed)

Definition at line 110 of file expr_stream.cpp.

References d_indentLast, d_indentStack, DebugAssert, and CVC3::int2string().

Referenced by CVC3::pop(), and CVC3::popSave().

void CVC3::ExprStream::resetIndent ( )

Reset indentation to what it was at this level.

Definition at line 121 of file expr_stream.cpp.

References d_indentLast, and d_indentStack.

Referenced by CVC3::operator<<(), CVC3::Expr::print(), CVC3::Expr::printAST(), and CVC3::reset().

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

Return the current column position.

Definition at line 189 of file expr_stream.h.

void CVC3::ExprStream::pushDag ( )

Recompute shared subexpression for the next Expr.

Definition at line 127 of file expr_stream.cpp.

References d_dagBuilt, d_dagPtr, and d_dagStack.

Referenced by CVC3::pushdag().

void CVC3::ExprStream::popDag ( )

Delete shared subexpressions previously added with pushdag.

Definition at line 132 of file expr_stream.cpp.

References CVC3::ExprMap< Data >::clear(), d_dagMap, d_dagPtr, d_dagStack, d_lastDagSize, d_newDagMap, DebugAssert, and CVC3::ExprMap< Data >::erase().

Referenced by CVC3::popdag(), and resetDag().

void CVC3::ExprStream::resetDag ( )

Reset the DAG to what it was at this level.

Definition at line 147 of file expr_stream.cpp.

References d_dagPtr, d_lastDagSize, and popDag().

Referenced by CVC3::operator<<().


Friends And Related Function Documentation

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

Use manipulators which are functions over ExprStream&.

Definition at line 156 of file expr_stream.cpp.

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

Print Expr.

Definition at line 162 of file expr_stream.cpp.

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

Print Type.

Definition at line 226 of file expr_stream.cpp.

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

Print string.

This is where all the indentation is happening.

The algorithm for determining whether to go to the next line is the following:

  • If the new d_col does not exceed d_lineWidth/2 or current indentation, don't bother.
  • If the difference between the new d_col and the current indentation is less than d_lineWidth/4, don't bother either, so that we don't get lots of very short lines clumped to the right side.
  • Similarly, if the difference between the old d_col and the current indentation is less than d_lineWidth/6, keep the same line. Otherwise, for long atomic strings, we may get useless line breaks.
  • Otherwise, go to the next line.

Definition at line 251 of file expr_stream.cpp.

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

Print char* string.

Definition at line 273 of file expr_stream.cpp.

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

Print Rational.

Definition at line 278 of file expr_stream.cpp.

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

Print int.

Definition at line 285 of file expr_stream.cpp.

ExprStream& push ( ExprStream os) [friend]

Set the indentation to the current position.

Definition at line 298 of file expr_stream.cpp.

ExprStream& pop ( ExprStream os) [friend]

Restore the indentation to the previous position.

Definition at line 301 of file expr_stream.cpp.

Referenced by CVC3::VCL::popScope().

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 306 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 315 of file expr_stream.cpp.

ExprStream& reset ( ExprStream os) [friend]

Reset the indentation to the default at this level.

Definition at line 320 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 326 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 332 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 337 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 339 of file expr_stream.cpp.

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

Print the end-of-line.

The new line will not necessarily start at column 0 because of indentation.

The name endl will be introduced in namespace std, otherwise CVC3::endl would overshadow std::endl, wreaking havoc...


Member Data Documentation

The ExprManager to use.

Definition at line 112 of file expr_stream.h.

Referenced by ExprStream(), and CVC3::operator<<().

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

The ostream to print into.

Definition at line 113 of file expr_stream.h.

Referenced by std::endl(), and CVC3::operator<<().

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

Definition at line 114 of file expr_stream.h.

Referenced by CVC3::operator<<().

Current depth of Expr.

Definition at line 115 of file expr_stream.h.

Referenced by CVC3::operator<<().

Output language.

Definition at line 116 of file expr_stream.h.

Referenced by collectShared(), and CVC3::operator<<().

Whether to print with indentations.

Definition at line 117 of file expr_stream.h.

Referenced by std::endl(), and CVC3::operator<<().

int CVC3::ExprStream::d_col [private]

Current column in a line.

Definition at line 118 of file expr_stream.h.

Referenced by std::endl(), and CVC3::operator<<().

Try to format/indent for this line width

Definition at line 119 of file expr_stream.h.

Referenced by CVC3::operator<<().

std::vector<int> CVC3::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 124 of file expr_stream.h.

Referenced by std::endl(), ExprStream(), CVC3::operator<<(), popIndent(), CVC3::popSave(), and resetIndent().

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

Definition at line 126 of file expr_stream.h.

Referenced by ExprStream(), CVC3::operator<<(), popIndent(), and resetIndent().

Indentation register for popSave() and pushRestore()

Definition at line 128 of file expr_stream.h.

Referenced by CVC3::operator<<(), CVC3::popSave(), and CVC3::pushRestore().

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

Definition at line 130 of file expr_stream.h.

Referenced by std::endl(), CVC3::operator<<(), and CVC3::space().

bool CVC3::ExprStream::d_dag [private]

Print Expr as a DAG

Definition at line 131 of file expr_stream.h.

Referenced by CVC3::operator<<().

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

Mapping subexpressions to names for DAG printing.

Definition at line 133 of file expr_stream.h.

Referenced by collectShared(), CVC3::operator<<(), and popDag().

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

New subexpressions not yet printed in a LET header.

Definition at line 135 of file expr_stream.h.

Referenced by addLetHeader(), collectShared(), and popDag().

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

Stack of shared subexpressions (same as in d_dagMap)

Definition at line 137 of file expr_stream.h.

Referenced by collectShared(), popDag(), and pushDag().

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

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

Definition at line 139 of file expr_stream.h.

Referenced by ExprStream(), CVC3::operator<<(), popDag(), pushDag(), and resetDag().

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

Definition at line 141 of file expr_stream.h.

Referenced by ExprStream(), CVC3::operator<<(), popDag(), and resetDag().

Flag whether the dagMap is already built.

Definition at line 143 of file expr_stream.h.

Referenced by collectShared(), CVC3::operator<<(), and pushDag().

Counter for generating unique LET var names.

Definition at line 145 of file expr_stream.h.

Referenced by newName().

bool CVC3::ExprStream::d_nodag [private]

nodag() manipulator has been applied

Definition at line 147 of file expr_stream.h.

Referenced by CVC3::nodag(), and CVC3::operator<<().


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