#include <expr_stream.h>
Collaboration diagram for CVC3::ExprStream:
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.
| 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] |
| 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().
Traverse the Expr, collect shared subexpressions in d_dagMap.
Definition at line 54 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(), CVC3::SMTLIB_LANG, and CVC3::TPTP_LANG.
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 90 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.
| 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 std::endl(), CVC3::nodag(), CVC3::operator<<(), CVC3::pop(), CVC3::popdag(), CVC3::popSave(), CVC3::push(), CVC3::pushdag(), CVC3::pushRestore(), CVC3::reset(), CVC3::space(), and 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::TheoryArith3::print(), CVC3::Expr::print(), and CVC3::Expr::toString().
| void CVC3::ExprStream::lang | ( | InputLanguage | l | ) | [inline] |
| int CVC3::ExprStream::depth | ( | ) | const [inline] |
| void CVC3::ExprStream::depth | ( | int | d | ) | [inline] |
| void CVC3::ExprStream::lineWidth | ( | int | w | ) | [inline] |
| 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(), 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.
| 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 107 of file expr_stream.cpp.
References d_indentLast, d_indentStack, and DebugAssert.
| void CVC3::ExprStream::resetIndent | ( | ) |
Reset indentation to what it was at this level.
Definition at line 118 of file expr_stream.cpp.
References d_indentLast, and d_indentStack.
Referenced by CVC3::Expr::print(), and CVC3::Expr::printAST().
| int CVC3::ExprStream::column | ( | ) | const [inline] |
| void CVC3::ExprStream::pushDag | ( | ) |
Recompute shared subexpression for the next Expr.
Definition at line 124 of file expr_stream.cpp.
References d_dagBuilt, d_dagPtr, and d_dagStack.
| void CVC3::ExprStream::popDag | ( | ) |
Delete shared subexpressions previously added with pushdag.
Definition at line 129 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 resetDag().
| void CVC3::ExprStream::resetDag | ( | ) |
Reset the DAG to what it was at this level.
Definition at line 144 of file expr_stream.cpp.
References d_dagPtr, d_lastDagSize, and popDag().
| ExprStream& operator<< | ( | ExprStream & | os, | |
| ExprStream &(*)(ExprStream &) | manip | |||
| ) | [friend] |
Use manipulators which are functions over ExprStream&.
Definition at line 153 of file expr_stream.cpp.
| ExprStream& operator<< | ( | ExprStream & | os, | |
| const Expr & | e | |||
| ) | [friend] |
| ExprStream& operator<< | ( | ExprStream & | os, | |
| const Type & | t | |||
| ) | [friend] |
| 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:
Definition at line 247 of file expr_stream.cpp.
| ExprStream& operator<< | ( | ExprStream & | os, | |
| const char * | s | |||
| ) | [friend] |
| ExprStream& operator<< | ( | ExprStream & | os, | |
| const Rational & | r | |||
| ) | [friend] |
| ExprStream& operator<< | ( | ExprStream & | os, | |
| int | i | |||
| ) | [friend] |
| ExprStream& push | ( | ExprStream & | os | ) | [friend] |
Set the indentation to the current position.
Definition at line 294 of file expr_stream.cpp.
Referenced by CVC3::SearchSatTheoryAPI::push(), CVC3::ContextManager::push(), and CVC3::space().
| ExprStream& pop | ( | ExprStream & | os | ) | [friend] |
Restore the indentation to the previous position.
Definition at line 297 of file expr_stream.cpp.
Referenced by CVC3::SearchSatTheoryAPI::pop(), CVC3::ContextManager::pop(), and CVC3::space().
| 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 302 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 311 of file expr_stream.cpp.
| ExprStream& reset | ( | ExprStream & | os | ) | [friend] |
| 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 322 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 328 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 333 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 335 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 349 of file expr_stream.cpp.
Referenced by std::endl(), and CVC3::operator<<().
ExprManager* CVC3::ExprStream::d_em [private] |
std::ostream* CVC3::ExprStream::d_os [private] |
int CVC3::ExprStream::d_depth [private] |
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] |
bool CVC3::ExprStream::d_indent [private] |
int CVC3::ExprStream::d_col [private] |
int CVC3::ExprStream::d_lineWidth [private] |
Try to format/indent for this line width
Definition at line 119 of file expr_stream.h.
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 ExprStream(), popIndent(), 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(), popIndent(), and resetIndent().
int CVC3::ExprStream::d_indentReg [private] |
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.
bool CVC3::ExprStream::d_dag [private] |
Print Expr as a DAG
Definition at line 131 of file expr_stream.h.
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(), 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(), 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(), 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(), 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] |
1.5.2