CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::ExprStream Class Reference

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

#include <expr_stream.h>

Public Member Functions

 ExprStream (ExprManager *em)
 Default constructor. More...
 
 ~ExprStream ()
 Destructor. More...
 
void os (std::ostream &os)
 Set a new output stream. More...
 
InputLanguage lang () const
 Get the current output language. More...
 
void lang (InputLanguage l)
 Set the output language. More...
 
int depth () const
 Get the printing depth. More...
 
void depth (int d)
 Set the printing depth. More...
 
void lineWidth (int w)
 Set the line width. More...
 
bool dagFlag (bool flag=true)
 Set the DAG flag (return previous value) More...
 
void pushIndent ()
 Set the indentation to the current column. More...
 
void pushIndent (int pos)
 Set the indentation to the given absolute position. More...
 
void popIndent ()
 Restore the indentation (user cannot pop more than pushed) More...
 
void resetIndent ()
 Reset indentation to what it was at this level. More...
 
int column () const
 Return the current column position. More...
 
void pushDag ()
 Recompute shared subexpression for the next Expr. More...
 
void popDag ()
 Delete shared subexpressions previously added with pushdag. More...
 
void resetDag ()
 Reset the DAG to what it was at this level. More...
 

Private Member Functions

std::string newName ()
 Generating unique names in DAG expr. More...
 
void collectShared (const Expr &e, ExprMap< bool > &cache)
 Traverse the Expr, collect shared subexpressions in d_dagMap. More...
 
Expr addLetHeader (const Expr &e)
 Wrap e into the top-level LET ... IN header from the dagMap. More...
 

Private Attributes

ExprManagerd_em
 The ExprManager to use. More...
 
std::ostream * d_os
 The ostream to print into. More...
 
int d_depth
 Printing only upto this depth; -1 == unlimited. More...
 
int d_currDepth
 Current depth of Expr. More...
 
InputLanguage d_lang
 Output language. More...
 
bool d_indent
 Whether to print with indentations. More...
 
int d_col
 Current column in a line. More...
 
int d_lineWidth
 
std::vector< int > d_indentStack
 Indentation stack. More...
 
size_t d_indentLast
 The lowest position of the indent stack the user can pop. More...
 
int d_indentReg
 Indentation register for popSave() and pushRestore() More...
 
bool d_beginningOfLine
 Whether it is a beginning of line (for eating up extra spaces) More...
 
bool d_dag
 
ExprMap< std::string > d_dagMap
 Mapping subexpressions to names for DAG printing. More...
 
ExprMap< std::string > d_newDagMap
 New subexpressions not yet printed in a LET header. More...
 
std::vector< Exprd_dagStack
 Stack of shared subexpressions (same as in d_dagMap) More...
 
std::vector< size_t > d_dagPtr
 Stack of pointers to d_dagStack for pushing/popping shared subexprs. More...
 
size_t d_lastDagSize
 The smallest size of d_dagPtr the user can `popDag'. More...
 
bool d_dagBuilt
 Flag whether the dagMap is already built. More...
 
int d_idCounter
 Counter for generating unique LET var names. More...
 
bool d_nodag
 nodag() manipulator has been applied More...
 

Friends

ExprStreamoperator<< (ExprStream &os, ExprStream &(*manip)(ExprStream &))
 Use manipulators which are functions over ExprStream&. More...
 
ExprStreamoperator<< (ExprStream &os, const Expr &e)
 Print Expr. More...
 
ExprStreamoperator<< (ExprStream &os, const Type &t)
 Print Type. More...
 
ExprStreamoperator<< (ExprStream &os, const std::string &s)
 Print string. More...
 
ExprStreamoperator<< (ExprStream &os, const char *s)
 Print char* string. More...
 
ExprStreamoperator<< (ExprStream &os, const Rational &r)
 Print Rational. More...
 
ExprStreamoperator<< (ExprStream &os, int i)
 Print int. More...
 
ExprStreampush (ExprStream &os)
 Set the indentation to the current position. More...
 
ExprStreampop (ExprStream &os)
 Restore the indentation to the previous position. More...
 
ExprStreampopSave (ExprStream &os)
 Remember the current indentation and pop to the previous position. More...
 
ExprStreampushRestore (ExprStream &os)
 Set the indentation to the position saved by popSave() More...
 
ExprStreamreset (ExprStream &os)
 Reset the indentation to the default at this level. More...
 
ExprStreamspace (ExprStream &os)
 Insert a single white space separator. More...
 
ExprStreamnodag (ExprStream &os)
 Print the next top-level expression node without DAG-ifying. More...
 
ExprStreampushdag (ExprStream &os)
 Recompute shared subexpression for the next Expr. More...
 
ExprStreampopdag (ExprStream &os)
 Delete shared subexpressions previously added with pushdag. More...
 
ExprStreamstd::endl (ExprStream &os)
 Print the end-of-line. More...
 

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

ExprManager* CVC3::ExprStream::d_em
private

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<<().

int CVC3::ExprStream::d_depth
private

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

Definition at line 114 of file expr_stream.h.

Referenced by CVC3::operator<<().

int CVC3::ExprStream::d_currDepth
private

Current depth of Expr.

Definition at line 115 of file expr_stream.h.

Referenced by CVC3::operator<<().

InputLanguage CVC3::ExprStream::d_lang
private

Output language.

Definition at line 116 of file expr_stream.h.

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

bool CVC3::ExprStream::d_indent
private

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<<().

int CVC3::ExprStream::d_lineWidth
private

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().

size_t CVC3::ExprStream::d_indentLast
private

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().

int CVC3::ExprStream::d_indentReg
private

Indentation register for popSave() and pushRestore()

Definition at line 128 of file expr_stream.h.

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

bool CVC3::ExprStream::d_beginningOfLine
private

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().

size_t CVC3::ExprStream::d_lastDagSize
private

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().

bool CVC3::ExprStream::d_dagBuilt
private

Flag whether the dagMap is already built.

Definition at line 143 of file expr_stream.h.

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

int CVC3::ExprStream::d_idCounter
private

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: