ExprStream & CVC3::push | ( | ExprStream & | os | ) |
Set the indentation to the current position.
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(), CVC3::Expr::printAST(), and CVC3::TheoryArith::printRational().
ExprStream & CVC3::pop | ( | ExprStream & | os | ) |
Restore the indentation.
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::Expr::print(), and CVC3::Expr::printAST().
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().
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.
Referenced by CVC3::TheoryCore::print().
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.
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.
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(), CVC3::Expr::printAST(), and CVC3::TheoryArith::printRational().
ExprStream & CVC3::nodag | ( | ExprStream & | os | ) |
Referenced by CVC3::TheoryQuant::print(), CVC3::TheoryCore::print(), and CVC3::Expr::printAST().
ExprStream & CVC3::pushdag | ( | ExprStream & | os | ) |
Referenced by CVC3::TheoryUF::print(), CVC3::TheoryQuant::print(), and CVC3::TheoryArray::print().
ExprStream & CVC3::popdag | ( | ExprStream & | os | ) |
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.
Referenced by MiniSat::Solver::allClausesSatisfied(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::TheoryCore::assertFactCore(), 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(), CVC3::SearchEngineTheoremProducer::conflictClause(), MiniSat::Solver::curAssigns(), MiniSat::Solver::curClauses(), CVC3::TheoryQuant::debug(), CVC3::Translator::dump(), CVC3::Translator::dumpAssertion(), CVC3::Translator::dumpQuery(), CVC3::Translator::dumpQueryResult(), CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::evaluateNext(), CVC3::fatalError(), CVC3::SearchSat::findSplitterRec(), CVC3::Translator::finish(), generateSatProof(), CVC3::Scope::getMemory(), CVC3::SearchSat::getValue(), SAT::DPLLTBasic::handle_result(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::TheoryArithNew::kidsCanonical(), CVC3::TheoryArith3::kidsCanonical(), CVC3::CNF_TheoremProducer::learnedClauses(), main(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::SearchImplBase::newUserAssumption(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::operator<<(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::VCL::popScope(), CVC3::Expr::pprint(), CVC3::Expr::pprintnodag(), CVC3::Translator::preprocess(), CVC3::Translator::preprocess2(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::Theorem::print(), LFSCPrinter::print(), CVC3::Expr::print(), CVC3::MemoryTracker::print(), SAT::Clause::print(), CVC3::Assumptions::print(), LFSCPrinter::print_clause(), LFSCPrinter::print_helper(), 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(), CVC3::VCL::printStatistics(), SatSolver::PrintStatistics(), CVC3::VCCmd::printSymbols(), printUsage(), CVC3::VCCmd::processCommands(), MiniSat::Solver::protocolPropagation(), MiniSat::Solver::push(), CVC3::Theorem::recursivePrint(), CVC3::VCCmd::reportResult(), CVC3::SearchEngineTheoremProducer::satProof(), MiniSat::Solver::search(), SAT::DPLLTMiniSat::search(), sighandler(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::Translator::start(), CVC3::CommonTheoremProducer::substitutivityRule(), MiniSat::Solver::toString(), CVC3::SearchEngineFast::traceConflict(), and CVC3::TheoryArithOld::DifferenceLogicGraph::writeGraph().