Overloaded operator<<

Collaboration diagram for Overloaded operator<<:

Functions

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

  Use manipulators which are functions over ExprStream&.
  

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

  Print Expr.
  

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

  Print Type.
  

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

  Print string.
  

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

  Print char* string.
  

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

  Print Rational.
  

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

  Print int.
  

---

Function Documentation

ExprStream& CVC3::operator<<	(	ExprStream &	os,
		ExprStream &(*)(ExprStream &)	manip
	)

Use manipulators which are functions over ExprStream&.

Definition at line 156 of file expr_stream.cpp.

ExprStream& CVC3::operator<<	(	ExprStream &	os,
		const Expr &	e
	)

Print Expr.

Definition at line 162 of file expr_stream.cpp.

References CVC3::ExprStream::addLetHeader(), ASSERT, CVC3::AST_LANG, CVC3::ExprStream::collectShared(), CONST, CVC3::ExprStream::d_currDepth, CVC3::ExprStream::d_dag, CVC3::ExprStream::d_dagBuilt, CVC3::ExprStream::d_dagMap, CVC3::ExprStream::d_dagPtr, CVC3::ExprStream::d_depth, CVC3::ExprStream::d_em, CVC3::ExprStream::d_indentLast, CVC3::ExprStream::d_indentReg, CVC3::ExprStream::d_indentStack, CVC3::ExprStream::d_lang, CVC3::ExprStream::d_lastDagSize, CVC3::ExprStream::d_nodag, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getKind(), CVC3::ExprManager::getPrinter(), CVC3::PrettyPrinter::print(), CVC3::Expr::printAST(), QUERY, CVC3::ExprStream::resetDag(), CVC3::ExprStream::resetIndent(), RESTART, CVC3::SPASS_LANG, TRANSFORM, and TYPE.

ExprStream& CVC3::operator<<	(	ExprStream &	os,
		const Type &	t
	)

Print Type.

Definition at line 226 of file expr_stream.cpp.

References CVC3::Type::getExpr().

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

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.

References CVC3::ExprStream::d_beginningOfLine, CVC3::ExprStream::d_col, CVC3::ExprStream::d_indent, CVC3::ExprStream::d_indentStack, CVC3::ExprStream::d_lineWidth, CVC3::ExprStream::d_os, and std::endl().

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

Print char* string.

Definition at line 273 of file expr_stream.cpp.

ExprStream& CVC3::operator<<	(	ExprStream &	os,
		const Rational &	r
	)

Print Rational.

Definition at line 278 of file expr_stream.cpp.

ExprStream& CVC3::operator<<	(	ExprStream &	os,
		int	i
	)

Print int.

Definition at line 285 of file expr_stream.cpp.