Collaboration diagram for Manipulators:

Functions

ExprStream & CVC3::push (ExprStream &os)
Set the indentation to the current position.
ExprStream & CVC3::pop (ExprStream &os)
Restore the indentation.
ExprStream & CVC3::popSave (ExprStream &os)
Remember the current indentation and pop to the previous position.
ExprStream & CVC3::pushRestore (ExprStream &os)
Set the indentation to the position saved by popSave()
ExprStream & CVC3::reset (ExprStream &os)
Reset the indentation to the default at this level.
ExprStream & CVC3::space (ExprStream &os)
Insert a single white space separator.
ExprStream & CVC3::nodag (ExprStream &os)
ExprStream & CVC3::pushdag (ExprStream &os)
ExprStream & CVC3::popdag (ExprStream &os)
CVC3::ExprStream & std::endl (CVC3::ExprStream &os)
Print the end-of-line.

Function Documentation

ExprStream & CVC3::push ( ExprStream & os )

ExprStream & CVC3::pop ( ExprStream & os )

Restore the indentation.

Restore the indentation to the previous position.

Definition at line 301 of file expr_stream.cpp.

References CVC3::ExprStream::popIndent().

Referenced by CVC3::VCL::assertFormula(), CVC3::SearchSat::check(), CVC3::VCL::pop(), 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::Expr::print(), CVC3::Translator::printArrayExpr(), CVC3::Expr::printAST(), CVC3::TheoryCore::printSmtLibShared(), CVC3::TheoryBitvector::printSmtLibShared(), CVC3::VCL::push(), CVC3::VCL::query(), and CVC3::space().

ExprStream & CVC3::popSave ( ExprStream & os )

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.

References CVC3::ExprStream::d_indentReg, CVC3::ExprStream::d_indentStack, and CVC3::ExprStream::popIndent().

Referenced by CVC3::TheoryCore::print().

ExprStream & CVC3::pushRestore ( ExprStream & os )

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.

References CVC3::ExprStream::d_indentReg, and CVC3::ExprStream::pushIndent().

Referenced by CVC3::TheoryCore::print().

ExprStream & CVC3::reset ( ExprStream & os )

Reset the indentation to the default at this level.

Definition at line 320 of file expr_stream.cpp.

References CVC3::ExprStream::resetIndent().

ExprStream & CVC3::space ( ExprStream & os )

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.

References CVC3::ExprStream::d_beginningOfLine, CVC3::pop(), and CVC3::push().

ExprStream & CVC3::nodag ( ExprStream & os )

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.

References CVC3::ExprStream::d_nodag.

Referenced by CVC3::TheoryQuant::print(), CVC3::TheoryCore::print(), CVC3::Translator::printArrayExpr(), and CVC3::Expr::printAST().

ExprStream & CVC3::pushdag ( ExprStream & os )

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.

References CVC3::ExprStream::pushDag().

Referenced by CVC3::TheoryUF::print(), CVC3::TheoryQuant::print(), and CVC3::TheoryArray::print().

ExprStream & CVC3::popdag ( ExprStream & os )

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.

References CVC3::ExprStream::popDag().

Referenced by CVC3::TheoryUF::print(), CVC3::TheoryQuant::print(), and CVC3::TheoryArray::print().

CVC3::ExprStream & std::endl ( CVC3::ExprStream & os )

Print the end-of-line.

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

Definition at line 353 of file expr_stream.cpp.

References CVC3::ExprStream::d_beginningOfLine, CVC3::ExprStream::d_col, CVC3::ExprStream::d_indent, CVC3::ExprStream::d_indentStack, and CVC3::ExprStream::d_os.

Referenced by Abort(), MiniSat::Solver::allClausesSatisfied(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::TheoryCore::assertFactCore(), CSolver::back_track(), CVC3::SearchSat::check(), CVC3::Scope::check(), MiniSat::Solver::checkClause(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArithOld::checkSat(), MiniSat::Solver::checkWatched(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CDatabase::compact_lit_pool(), CSolver::conflict_analysis_zchaff(), CVC3::SearchEngineTheoremProducer::conflictClause(), LFSCConvert::convert(), MiniSat::Solver::curAssigns(), MiniSat::Solver::curClauses(), LFSCConvert::cvc3_to_lfsc(), CVC3::TheoryQuant::debug(), CSolver::decide_next_branch(), CSolver::delete_unrelevant_clauses(), CDatabase::detail_dump_cl(), LFSCConvert::do_bso(), CDatabase::dump(), CVariable::dump(), CClause::dump(), CSolver::dump_assignment_stack(), CVC3::Translator::dumpQueryResult(), CDatabase::enlarge_lit_pool(), CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::evaluateNext(), CVC3::fatalError(), CVC3::SearchSat::findSplitterRec(), CVC3::Translator::finish(), generateSatProof(), get_knd_result(), CVC3::Scope::getMemory(), CVC3::SearchSat::getValue(), LFSCObj::getY(), SAT::DPLLTBasic::handle_result(), Obj::indent(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::TheoryArithNew::kidsCanonical(), CVC3::TheoryArith3::kidsCanonical(), CVC3::CNF_TheoremProducer::learnedClauses(), main(), LFSCLraPoly::Make(), LFSCProof::Make_CNF(), LFSCConvert::make_let_proof(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::SearchImplBase::newUserAssumption(), TReturn::normalize_to_tf(), TReturn::normalize_tr(), TReturn::normalize_tret(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::operator<<(), CDatabase::output_lit_pool_state(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::VCL::popScope(), CVC3::Expr::pprint(), CVC3::Expr::pprintnodag(), CVC3::Theorem::pprintxnodag(), CSolver::preprocess(), CVC3::Translator::preprocess(), CVC3::Translator::preprocess2(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryArithOld::print(), CVC3::Expr::print(), CVC3::MemoryTracker::print(), SAT::Clause::print(), CVC3::Assumptions::print(), Obj::print_error(), LFSCPrinter::print_LFSC(), LFSCPfLet::print_pf(), LFSCPrinter::print_terms_h(), Obj::print_warning(), CVC3::Statistics::printAll(), CVC3::Expr::printAST(), CVC3::VCCmd::printCounterExample(), MiniSat::Derivation::printDerivation(), MiniSat::Solver::printDIMACS(), CVC3::VCL::printExpr(), CVC3::VCCmd::printModel(), printSatProof(), MiniSat::Solver::printState(), SatSolver::PrintStatistics(), CVC3::VCCmd::printSymbols(), printUsage(), CVC3::VCCmd::processCommands(), MiniSat::Solver::protocolPropagation(), MiniSat::Solver::push(), LFSCObj::queryMt(), CSolver::queue_implication(), CVC3::VCCmd::reportResult(), CSolver::restart(), CSolver::run_periodic_functions(), CVC3::SearchEngineTheoremProducer::satProof(), MiniSat::Solver::search(), SAT::DPLLTMiniSat::search(), CSolver::set_var_value(), sighandler(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::Translator::start(), CVC3::CommonTheoremProducer::substitutivityRule(), MiniSat::Solver::toString(), CVC3::SearchEngineFast::traceConflict(), TReturn::TReturn(), CSolver::unset_var_value(), Warning(), and CVC3::TheoryArithOld::DifferenceLogicGraph::writeGraph().