CVC3: CVC3::ExprStream Class Reference

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:

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

Constructor & Destructor Documentation

CVC3::ExprStream::ExprStream ( ExprManager * em )

Default constructor.

Definition at line 28 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 42 of file expr_stream.cpp.

References d_idCounter.

Referenced by collectShared().

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

Traverse the Expr, collect shared subexpressions in d_dagMap.

Definition at line 53 of file expr_stream.cpp.

References CVC3::Expr::begin(), CVC3::ExprMap< Data >::count(), d_dagBuilt, d_dagMap, d_dagStack, d_lang, d_newDagMap, CVC3::Expr::end(), CVC3::isTrivialExpr(), newName(), and CVC3::SMTLIB_LANG.

Referenced by CVC3::operator<<().

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

References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::clear(), d_newDagMap, CVC3::ExprMap< Data >::end(), CVC3::Expr::getEM(), CVC3::LET, CVC3::LETDECL, CVC3::LETDECLS, CVC3::ExprManager::newLeafExpr(), CVC3::ExprManager::newVarExpr(), CVC3::ExprMap< Data >::size(), and CVC3::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.

Referenced by CVC3::Expr::toString().

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

Get the current output language.

Definition at line 165 of file expr_stream.h.

Referenced by CVC3::TheoryUF::print(), CVC3::TheorySimulate::print(), CVC3::TheoryRecords::print(), CVC3::TheoryQuant::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryArray::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryArithNew::print(), CVC3::Expr::print(), and CVC3::Expr::toString().

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.

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

Set the DAG flag.

Definition at line 175 of file expr_stream.h.

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

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

References d_indentLast, d_indentStack, and DebugAssert.

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

void CVC3::ExprStream::resetIndent ( )

Reset indentation to what it was at this level.

Definition at line 112 of file expr_stream.cpp.

References d_indentLast, and d_indentStack.

Referenced by 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 118 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 123 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 138 of file expr_stream.cpp.

References d_dagPtr, d_lastDagSize, and popDag().

Friends And Related Function Documentation

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

Use manipulators which are functions over ExprStream&.

Definition at line 147 of file expr_stream.cpp.

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

Print Expr.

Definition at line 153 of file expr_stream.cpp.

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

Print Type.

Definition at line 215 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 240 of file expr_stream.cpp.

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

Print char* string.

Definition at line 262 of file expr_stream.cpp.

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

Print Rational.

Definition at line 267 of file expr_stream.cpp.

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

Print int.

Definition at line 274 of file expr_stream.cpp.

ExprStream& push ( ExprStream & os ) [friend]

Set the indentation to the current position.

Definition at line 287 of file expr_stream.cpp.

ExprStream& pop ( ExprStream & os ) [friend]

Restore the indentation to the previous position.

Definition at line 290 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 295 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 304 of file expr_stream.cpp.

ExprStream& reset ( ExprStream & os ) [friend]

Reset the indentation to the default at this level.

Definition at line 309 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 315 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 321 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 326 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 328 of file expr_stream.cpp.

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

Print the end-of-line.

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

Definition at line 342 of file expr_stream.cpp.

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