Overloaded operator<<
[Pretty-printing related classes and methods]

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

References CVC3::ExprStream::os().

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

Print Expr.

Definition at line 159 of file expr_stream.cpp.

References CVC3::ASSERT, CVC3::AST_LANG, CVC3::CONST, CVC3::ExprStream::d_currDepth, CVC3::Expr::getKind(), CVC3::ExprStream::os(), CVC3::PrettyPrinter::print(), CVC3::Expr::printAST(), CVC3::QUERY, CVC3::RESTART, CVC3::TRANSFORM, and CVC3::TYPE.

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

Print Type.

Definition at line 222 of file expr_stream.cpp.

References CVC3::Type::getExpr(), and CVC3::ExprStream::os().

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

References CVC3::ExprStream::endl, and CVC3::ExprStream::os().

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

Print char* string.

Definition at line 269 of file expr_stream.cpp.

References CVC3::ExprStream::os().

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

Print Rational.

Definition at line 274 of file expr_stream.cpp.

References CVC3::ExprStream::os().

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

Print int.

Definition at line 281 of file expr_stream.cpp.

References CVC3::ExprStream::os().

---