Collaboration diagram for Private methods:
size_t CVC3::ExprManager::HashString::operator() | ( | const std::string & | s | ) | const [inline, inherited] |
Definition at line 79 of file expr_manager.h.
CVC3::ExprManager::HashEV::HashEV | ( | ExprManager * | em | ) | [inline, inherited] |
Definition at line 119 of file expr_manager.h.
size_t CVC3::ExprManager::HashEV::operator() | ( | ExprValue * | ev | ) | const [inline, inherited] |
Definition at line 120 of file expr_manager.h.
virtual CVC3::ExprManager::TypeComputer::~TypeComputer | ( | ) | [inline, virtual, inherited] |
Definition at line 180 of file expr_manager.h.
virtual void CVC3::ExprManager::TypeComputer::computeType | ( | const Expr & | e | ) | [pure virtual, inherited] |
Compute the type of e.
Implemented in CVC3::TypeComputerCore.
Referenced by CVC3::ExprManager::computeType().
virtual void CVC3::ExprManager::TypeComputer::checkType | ( | const Expr & | e | ) | [pure virtual, inherited] |
Check that e is a valid Type expr.
Implemented in CVC3::TypeComputerCore.
Referenced by CVC3::ExprManager::checkType().
Cached recursive descent. Must be called only during rebuild().
Definition at line 209 of file expr_manager.cpp.
References CVC3::Expr::d_expr, CVC3::ExprManager::d_exprSet, CVC3::ExprManager::d_inRebuild, CVC3::ExprManager::d_rebuildCache, CVC3::ExprValue::d_type, DebugAssert, CVC3::MemoryManager::deleteData(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::end(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::find(), CVC3::Type::getExpr(), CVC3::ExprManager::getMM(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert(), CVC3::Type::isNull(), CVC3::ExprManager::nextIndex(), CVC3::ExprValue::rebuild(), CVC3::Expr::toString(), and CVC3::ExprManager::Type.
Referenced by CVC3::ExprValue::rebuild(), and CVC3::ExprManager::rebuild().
Return either an existing or a new ExprValue matching ev.
Definition at line 246 of file expr_manager.cpp.
References CVC3::ExprValue::copy(), CVC3::ExprManager::d_exprSet, DebugAssert, Hash::hash_set< _Key, _HashFcn, _EqualKey >::end(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::find(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert(), CVC3::ExprManager::isActive(), and CVC3::ExprManager::nextIndex().
Referenced by CVC3::Expr::Expr().
unsigned CVC3::ExprManager::getFlag | ( | ) | [inline, private, inherited] |
Return the current Expr flag counter.
Definition at line 204 of file expr_manager.h.
Referenced by CVC3::Expr::setFlag().
unsigned CVC3::ExprManager::nextFlag | ( | ) | [inline, private, inherited] |
Increment and return the Expr flag counter (this clears all the flags).
Definition at line 206 of file expr_manager.h.
References FatalAssert.
void ExprManager::computeType | ( | const Expr & | e | ) | [private, inherited] |
Compute the type of the Expr.
Definition at line 423 of file expr_manager.cpp.
References CVC3::ExprManager::TypeComputer::computeType(), CVC3::ExprManager::d_typeComputer, DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::getType(), and CVC3::Expr::isNull().
Referenced by CVC3::Expr::getType().
void ExprManager::checkType | ( | const Expr & | e | ) | [private, inherited] |
Check well-formedness of a type Expr.
Definition at line 430 of file expr_manager.cpp.
References CVC3::ExprManager::TypeComputer::checkType(), CVC3::ExprManager::d_typeComputer, DebugAssert, and CVC3::Expr::isValidType().
Referenced by CVC3::Type::Type().
ExprManager::ExprManager | ( | ContextManager * | cm, | |
const CLFlags & | flags | |||
) | [inherited] |
Constructor.
Definition at line 37 of file expr_manager.cpp.
References CVC3::BOOLEAN, CVC3::ExprManager::d_bool, CVC3::ExprManager::d_cm, CVC3::ExprManager::d_false, CVC3::ExprManager::d_inRebuild, CVC3::ExprManager::d_mm, CVC3::ExprManager::d_mmFlag, CVC3::ExprManager::d_notifyObj, CVC3::ExprManager::d_true, CVC3::EXPR_APPLY, CVC3::EXPR_BOUND_VAR, CVC3::EXPR_CLOSURE, CVC3::EXPR_NODE, CVC3::EXPR_RATIONAL, CVC3::EXPR_SKOLEM, CVC3::EXPR_STRING, CVC3::EXPR_SYMBOL, CVC3::EXPR_THEOREM, CVC3::EXPR_UCONST, CVC3::EXPR_VALUE, CVC3::FALSE_EXPR, CVC3::ContextManager::getCurrentContext(), IF_DEBUG, CVC3::ExprManager::newLeafExpr(), registerKinds(), CVC3::Expr::setType(), CVC3::TRUE_EXPR, and CVC3::Type::typeBool().
ExprManager::~ExprManager | ( | ) | [inherited] |
Destructor.
Definition at line 94 of file expr_manager.cpp.
References CVC3::ExprManager::clear(), CVC3::ExprManager::d_disableGC, CVC3::ExprManager::d_emptyVec, CVC3::ExprManager::d_mm, CVC3::ExprManager::d_notifyObj, FatalAssert, and TRACE_MSG.
void ExprManager::clear | ( | ) | [inherited] |
Free up all memory and delete all the expressions.
No more expressions can be created after this point, only destructors ~Expr() can be called.
This method is needed to dis-entangle the mutual dependency of ExprManager and ContextManager, when destructors of ExprValue (sub)classes need to delete backtracking objects, and deleting the ContextManager requires destruction of some remaining Exprs.
Definition at line 110 of file expr_manager.cpp.
References Hash::hash_set< _Key, _HashFcn, _EqualKey >::begin(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::clear(), CVC3::ExprManager::d_bool, CVC3::ExprManager::d_disableGC, CVC3::ExprManager::d_exprSet, CVC3::ExprManager::d_false, CVC3::ExprManager::d_mm, CVC3::ExprManager::d_nullExpr, CVC3::ExprManager::d_true, Hash::hash_set< _Key, _HashFcn, _EqualKey >::end(), CVC3::ExprManager::Expr, FatalAssert, IF_DEBUG, CVC3::ExprManager::isActive(), CVC3::Expr::isNull(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::size(), CVC3::TRACE, and TRACE_MSG.
Referenced by CVC3::ExprManager::~ExprManager(), and CVC3::VCL::~VCL().
bool ExprManager::isActive | ( | ) | [inherited] |
Check if the ExprManager is still active (clear() was not called).
Definition at line 153 of file expr_manager.cpp.
References CVC3::ExprManager::d_disableGC.
Referenced by CVC3::ExprManager::clear(), CVC3::ExprManager::installExprValue(), CVC3::ExprManager::newExprValue(), CVC3::Theorem::print(), and CVC3::ExprManager::rebuild().
void ExprManager::gc | ( | ExprValue * | ev | ) | [inherited] |
Garbage collect the ExprValue pointer.
Definition at line 157 of file expr_manager.cpp.
References CVC3::ExprManager::d_disableGC, CVC3::ExprManager::d_exprSet, CVC3::ExprManager::d_mm, CVC3::ExprManager::d_postponed, CVC3::ExprManager::d_postponeGC, and Hash::hash_set< _Key, _HashFcn, _EqualKey >::erase().
Referenced by CVC3::ExprValue::decRefcount().
void CVC3::ExprManager::postponeGC | ( | ) | [inline, inherited] |
Postpone deletion of garbage-collected expressions.
Definition at line 238 of file expr_manager.h.
Referenced by CVC3::ExprManagerNotifyObj::notifyPre().
void ExprManager::resumeGC | ( | ) | [inherited] |
Resume deletion of garbage-collected expressions.
Definition at line 170 of file expr_manager.cpp.
References CVC3::ExprManager::d_mm, CVC3::ExprManager::d_postponed, and CVC3::ExprManager::d_postponeGC.
Referenced by CVC3::ExprManagerNotifyObj::notify().
Rebuild the Expr with this ExprManager if it belongs to another ExprManager.
Definition at line 184 of file expr_manager.cpp.
References CVC3::ExprManager::d_inRebuild, CVC3::ExprManager::d_rebuildCache, DebugAssert, CVC3::Expr::getEM(), IF_DEBUG, CVC3::ExprManager::isActive(), CVC3::Expr::isNull(), and CVC3::ExprManager::rebuildRec().
Referenced by CVC3::VCL::importExpr(), CVC3::VCL::importType(), CVC3::Op::Op(), and CVC3::Expr::rebuild().
ExprIndex CVC3::ExprManager::nextIndex | ( | ) | [inline, inherited] |
Return the next Expr index.
It should be used only by ExprValue() constructor
Definition at line 249 of file expr_manager.h.
Referenced by CVC3::ExprManager::newExprValue(), and CVC3::ExprManager::rebuildRec().
ExprIndex CVC3::ExprManager::lastIndex | ( | ) | [inline, inherited] |
void CVC3::ExprManager::clearFlags | ( | ) | [inline, inherited] |
Clears the generic Expr flag in all Exprs.
Definition at line 253 of file expr_manager.h.
Referenced by CVC3::Expr::clearFlags(), and hasBoundVar().
const Expr& CVC3::ExprManager::boolExpr | ( | ) | [inline, inherited] |
const Expr& CVC3::ExprManager::falseExpr | ( | ) | [inline, inherited] |
FALSE Expr.
Definition at line 259 of file expr_manager.h.
Referenced by CVC3::CoreTheoremProducer::AndToIte(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::TheorySimulate::computeTCC(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::CommonTheoremProducer::contradictionRule(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::VCL::falseExpr(), CVC3::Theory::falseExpr(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteOr(), and CVC3::CoreTheoremProducer::rewriteOrSubterms().
const Expr& CVC3::ExprManager::trueExpr | ( | ) | [inline, inherited] |
TRUE Expr.
Definition at line 261 of file expr_manager.h.
Referenced by CVC3::CoreTheoremProducer::AndToIte(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryCore::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryArithNew::computeTypePred(), CVC3::Theory::computeTypePred(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::ArithTheoremProducerOld::dummyTheorem(), CVC3::ArithTheoremProducer::dummyTheorem(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::VCL::trueExpr(), CVC3::Theory::trueExpr(), CVC3::CommonTheoremProducer::trueTheorem(), and CVC3::QuantTheoremProducer::universalInst().
const std::vector<Expr>& CVC3::ExprManager::getEmptyVector | ( | ) | [inline, inherited] |
References to empty objects (used in ExprValue).
Definition at line 263 of file expr_manager.h.
Referenced by CVC3::ExprValue::getKids(), and CVC3::Expr::getKids().
const Expr& CVC3::ExprManager::getNullExpr | ( | ) | [inline, inherited] |
Expr CVC3::ExprManager::newExpr | ( | ExprValue * | ev | ) | [inline, inherited] |
Return either an existing or a new Expr matching ev.
Definition at line 270 of file expr_manager.h.
Referenced by CVC3::ExprManager::newBoundVarExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::ExprManager::newLeafExpr(), CVC3::ExprManager::newRatExpr(), CVC3::ExprManager::newSkolemExpr(), CVC3::ExprManager::newStringExpr(), CVC3::ExprManager::newSymbolExpr(), CVC3::ExprManager::newTheoremExpr(), and CVC3::ExprManager::newVarExpr().
Expr CVC3::ExprManager::newLeafExpr | ( | const Op & | op | ) | [inline, inherited] |
Definition at line 420 of file expr_manager.h.
References DebugAssert, CVC3::Expr::getEM(), CVC3::Op::getExpr(), CVC3::Op::getKind(), CVC3::Expr::isNull(), and CVC3::ExprManager::newExpr().
Referenced by CVC3::ExprStream::addLetHeader(), CVC3::VCL::checkContinue(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::ExprManager::ExprManager(), CVC3::VCL::getAssumptions(), CVC3::VCL::getAssumptionsTCC(), CVC3::VCL::getAssumptionsUsed(), CVC3::VCL::getClosure(), CVC3::VCL::getConcreteModel(), CVC3::VCL::getCounterExample(), CVC3::VCL::getProof(), CVC3::VCL::getProofClosure(), CVC3::VCL::getProofTCC(), CVC3::VCL::getTCC(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::VCL::pop(), CVC3::VCL::popScope(), CVC3::VCL::push(), CVC3::VCL::pushScope(), CVC3::CommonTheoremProducer::substitutivityRule(), and CVC3::TheoremProducer::TheoremProducer().
Expr CVC3::ExprManager::newStringExpr | ( | const std::string & | s | ) | [inline, inherited] |
Definition at line 434 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::Translator::finish(), and CVC3::VCL::stringExpr().
Expr CVC3::ExprManager::newRatExpr | ( | const Rational & | r | ) | [inline, inherited] |
Definition at line 437 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::CommonTheoremProducer::andElim(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::Translator::preprocessRec(), CVC3::TheoryBitvector::rat(), CVC3::TheoryArith::rat(), CVC3::BitvectorTheoremProducer::rat(), CVC3::ArithTheoremProducerOld::rat(), CVC3::ArithTheoremProducer::rat(), CVC3::VCL::ratExpr(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), and CVC3::TheoryArith::rewriteToDiff().
Expr CVC3::ExprManager::newSkolemExpr | ( | const Expr & | e, | |
int | i | |||
) | [inline, inherited] |
Definition at line 440 of file expr_manager.h.
References DebugAssert, CVC3::Expr::getEM(), and CVC3::ExprManager::newExpr().
Referenced by CVC3::Expr::skolemExpr().
Expr CVC3::ExprManager::newVarExpr | ( | const std::string & | s | ) | [inline, inherited] |
Definition at line 444 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::ExprStream::addLetHeader(), CVC3::TheoryQuant::checkSat(), CVC3::Theory::lookupVar(), CVC3::TheoremProducer::newPf(), and CVC3::Theory::newVar().
Expr CVC3::ExprManager::newSymbolExpr | ( | const std::string & | s, | |
int | kind | |||
) | [inline, inherited] |
Definition at line 447 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::TheoryDatatype::dataType(), CVC3::Theory::newFunction(), CVC3::Theory::newVar(), and CVC3::Translator::printArrayExpr().
Expr CVC3::ExprManager::newBoundVarExpr | ( | const std::string & | name, | |
const std::string & | uid | |||
) | [inline, inherited] |
Definition at line 450 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::VCL::boundVarExpr(), CVC3::TheoryUF::computeModel(), CVC3::VCL::createOp(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::ExprManager::newBoundVarExpr(), CVC3::TheoremProducer::newLabel(), CVC3::Theory::newSubtypeExpr(), and CVC3::CommonTheoremProducer::varIntroRule().
Expr CVC3::ExprManager::newBoundVarExpr | ( | const std::string & | name, | |
const std::string & | uid, | |||
const Type & | type | |||
) | [inline, inherited] |
Definition at line 454 of file expr_manager.h.
References CVC3::ARROW, DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Type::isNull(), CVC3::Expr::lookupType(), CVC3::ExprManager::newBoundVarExpr(), and CVC3::Expr::setType().
Expr CVC3::ExprManager::newBoundVarExpr | ( | const Type & | type | ) | [inline, inherited] |
Expr CVC3::ExprManager::newClosureExpr | ( | int | kind, | |
const std::vector< Expr > & | vars, | |||
const Expr & | body | |||
) | [inline, inherited] |
Definition at line 472 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::arrayLiteral(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryQuant::computeTCC(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::VCL::existsExpr(), CVC3::VCL::forallExpr(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::VCL::lambdaExpr(), CVC3::TheoryUF::lambdaExpr(), CVC3::TheoremProducer::newPf(), CVC3::Theory::newSubtypeExpr(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::Expr::recursiveSubst(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), and CVC3::CommonTheoremProducer::varIntroRule().
Expr CVC3::ExprManager::newTheoremExpr | ( | const Theorem & | thm | ) | [inline, inherited] |
Expr CVC3::ExprManager::andExpr | ( | const std::vector< Expr > & | children | ) | [inline, inherited] |
Expr CVC3::ExprManager::orExpr | ( | const std::vector< Expr > & | children | ) | [inline, inherited] |
size_t CVC3::ExprManager::hash | ( | const Expr & | e | ) | const [inline, inherited] |
Hash function for a single Expr.
Definition at line 490 of file expr_manager.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::hash(), and CVC3::Expr::isNull().
ContextManager* CVC3::ExprManager::getCM | ( | ) | const [inline, inherited] |
Context* CVC3::ExprManager::getCurrentContext | ( | ) | const [inline, inherited] |
int CVC3::ExprManager::scopelevel | ( | ) | [inline, inherited] |
void CVC3::ExprManager::setTM | ( | TheoremManager * | tm | ) | [inline, inherited] |
TheoremManager* CVC3::ExprManager::getTM | ( | ) | const [inline, inherited] |
Fetch the TheoremManager.
Definition at line 306 of file expr_manager.h.
Referenced by CVC3::Theorem::clearAllFlags(), CVC3::Theorem::getCachedValue(), CVC3::Theorem::getExpandFlag(), CVC3::Theorem::getLitFlag(), CVC3::Theorem::isFlagged(), CVC3::Theorem::setCachedValue(), CVC3::Theorem::setExpandFlag(), CVC3::Theorem::setFlag(), CVC3::Theorem::setLitFlag(), CVC3::Theorem::withAssumptions(), and CVC3::Theorem::withProof().
MemoryManager* CVC3::ExprManager::getMM | ( | size_t | MMIndex | ) | [inline, inherited] |
Return a MemoryManager for the given ExprValue type.
Definition at line 309 of file expr_manager.h.
References DebugAssert.
Referenced by CVC3::ExprTheorem::copy(), CVC3::ExprClosure::copy(), CVC3::ExprApplyTmp::copy(), CVC3::ExprApply::copy(), CVC3::ExprBoundVar::copy(), CVC3::ExprSymbol::copy(), CVC3::ExprVar::copy(), CVC3::ExprRational::copy(), CVC3::ExprSkolem::copy(), CVC3::ExprString::copy(), CVC3::ExprNode::copy(), CVC3::ExprNodeTmp::copy(), CVC3::ExprValue::copy(), CVC3::BVConstExpr::copy(), CVC3::ExprValue::getMM(), and CVC3::ExprManager::rebuildRec().
unsigned CVC3::ExprManager::getSimpCacheTag | ( | ) | const [inline, inherited] |
Get the simplifier's cache tag.
Definition at line 314 of file expr_manager.h.
Referenced by CVC3::Expr::setSimpCache(), and CVC3::Expr::validSimpCache().
void CVC3::ExprManager::invalidateSimpCache | ( | ) | [inline, inherited] |
Invalidate the simplifier's cache tag.
Definition at line 316 of file expr_manager.h.
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::CoreNotifyObj::notify(), and CVC3::TheoryCore::setFindLiteral().
void CVC3::ExprManager::registerTypeComputer | ( | TypeComputer * | typeComputer | ) | [inline, inherited] |
Register type computer.
Definition at line 319 of file expr_manager.h.
Referenced by CVC3::TheoryCore::TheoryCore().
int CVC3::ExprManager::printDepth | ( | ) | const [inline, inherited] |
bool CVC3::ExprManager::withIndentation | ( | ) | const [inline, inherited] |
int CVC3::ExprManager::lineWidth | ( | ) | const [inline, inherited] |
int CVC3::ExprManager::indent | ( | ) | const [inline, inherited] |
Get initial indentation.
Definition at line 329 of file expr_manager.h.
Referenced by CVC3::ExprStream::ExprStream(), CVC3::Expr::indent(), and CVC3::Theorem::print().
int ExprManager::indent | ( | int | n, | |
bool | permanent = false | |||
) | [inherited] |
Set initial indentation. Returns the previous permanent value.
Definition at line 324 of file expr_manager.cpp.
References CVC3::ExprManager::d_indent, and CVC3::ExprManager::d_indentTransient.
int ExprManager::incIndent | ( | int | n, | |
bool | permanent = false | |||
) | [inherited] |
Increment the current transient indentation by n.
If the second argument is true, sets the result as permanent.
Definition at line 335 of file expr_manager.cpp.
References CVC3::ExprManager::d_indent, and CVC3::ExprManager::d_indentTransient.
Referenced by CVC3::Theorem::print().
void CVC3::ExprManager::restoreIndent | ( | ) | [inline, inherited] |
Set transient indentation to permanent.
Definition at line 337 of file expr_manager.h.
Referenced by CVC3::operator<<().
InputLanguage ExprManager::getInputLang | ( | ) | const [inherited] |
Get the input language for printing.
Definition at line 344 of file expr_manager.cpp.
References CVC3::ExprManager::d_inputLang, and CVC3::getLanguage().
Referenced by CVC3::VCCmd::evaluateCommand(), and main().
InputLanguage ExprManager::getOutputLang | ( | ) | const [inherited] |
Get the output language for printing.
Definition at line 350 of file expr_manager.cpp.
References CVC3::ExprManager::d_inputLang, CVC3::ExprManager::d_outputLang, and CVC3::getLanguage().
Referenced by CVC3::Translator::dump(), CVC3::Translator::dumpAssertion(), CVC3::Translator::dumpQuery(), CVC3::Translator::dumpQueryResult(), CVC3::Translator::finish(), CVC3::Translator::fixConstName(), main(), CVC3::Translator::printArrayExpr(), CVC3::VCCmd::reportResult(), and CVC3::Translator::start().
bool CVC3::ExprManager::dagPrinting | ( | ) | const [inline, inherited] |
PrettyPrinter* CVC3::ExprManager::getPrinter | ( | ) | const [inline, inherited] |
Return the pretty-printer if there is one; otherwise return NULL.
Definition at line 346 of file expr_manager.h.
Referenced by CVC3::operator<<().
void ExprManager::newKind | ( | int | kind, | |
const std::string & | name, | |||
bool | isType = false | |||
) | [inherited] |
Register a new kind.
The kind may already be registered under the same name, but if the name is different, it's an error.
If the new kind is supposed to represent a type, set isType to true.
Definition at line 357 of file expr_manager.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), CVC3::ExprManager::d_kindMap, CVC3::ExprManager::d_kindMapByName, CVC3::ExprManager::d_typeKinds, DebugAssert, and Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert().
Referenced by registerKinds(), CVC3::TheoremManager::TheoremManager(), CVC3::TheoryArithNew::TheoryArithNew(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::TheoryArray::TheoryArray(), CVC3::TheoryBitvector::TheoryBitvector(), CVC3::TheoryDatatype::TheoryDatatype(), CVC3::TheoryRecords::TheoryRecords(), and CVC3::TheoryUF::TheoryUF().
void ExprManager::registerPrettyPrinter | ( | PrettyPrinter & | printer | ) | [inherited] |
Register the pretty-printer (can only do it if none registered).
The pointer is NOT owned by ExprManager. Delete it yourself.
Definition at line 381 of file expr_manager.cpp.
References CVC3::ExprManager::d_prettyPrinter, and DebugAssert.
Referenced by CVC3::TheoryCore::TheoryCore().
void ExprManager::unregisterPrettyPrinter | ( | ) | [inherited] |
Tell ExprManager that the printer is no longer valid.
Definition at line 388 of file expr_manager.cpp.
References CVC3::ExprManager::d_prettyPrinter, and FatalAssert.
Referenced by CVC3::TheoryCore::~TheoryCore().
bool CVC3::ExprManager::isKindRegistered | ( | int | kind | ) | [inline, inherited] |
Returns true if kind is built into CVC or has been registered via newKind.
Definition at line 367 of file expr_manager.h.
Referenced by CVC3::ExprValue::ExprValue().
bool CVC3::ExprManager::isTypeKind | ( | int | kind | ) | [inline, inherited] |
Check if a kind represents a type.
Definition at line 369 of file expr_manager.h.
Referenced by CVC3::Expr::isType().
const string & ExprManager::getKindName | ( | int | kind | ) | [inherited] |
Return the name associated with a kind. The kind must already be registered.
Definition at line 395 of file expr_manager.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), CVC3::ExprManager::d_kindMap, and DebugAssert.
Referenced by CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::Theory::registerKinds(), and CVC3::Theory::theoryOf().
int ExprManager::getKind | ( | const std::string & | name | ) | [inherited] |
Return a kind associated with a name. Returns NULL_KIND if not found.
Definition at line 402 of file expr_manager.cpp.
References CVC3::ExprManager::d_kindMapByName, and CVC3::NULL_KIND.
Referenced by CVC3::VCCmd::evaluateCommand(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryUF::parseExprOp(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), and CVC3::TheoryArithNew::parseExprOp().
size_t ExprManager::registerSubclass | ( | size_t | sizeOfSubclass | ) | [inherited] |
Register a new subclass of ExprValue.
Takes the size (in bytes) of the new subclass and returns the unique index of that subclass. Subsequent calls to the subclass's getMMIndex() must return that index.
Definition at line 411 of file expr_manager.cpp.
References CVC3::ExprManager::d_mm, CVC3::ExprManager::d_mmFlag, and FatalAssert.
Referenced by CVC3::TheoryBitvector::TheoryBitvector().
CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj | ( | ExprManager * | em, | |
Context * | cxt | |||
) | [inline, inherited] |
void ExprManagerNotifyObj::notifyPre | ( | void | ) | [virtual, inherited] |
Reimplemented from CVC3::ContextNotifyObj.
Definition at line 602 of file expr_manager.cpp.
References CVC3::ExprManagerNotifyObj::d_em, and CVC3::ExprManager::postponeGC().
void ExprManagerNotifyObj::notify | ( | void | ) | [virtual, inherited] |
Reimplemented from CVC3::ContextNotifyObj.
Definition at line 607 of file expr_manager.cpp.
References CVC3::ExprManagerNotifyObj::d_em, and CVC3::ExprManager::resumeGC().
size_t CVC3::ExprManager::hash | ( | const ExprValue * | ev | ) | const [inline, private, inherited] |
Definition at line 480 of file expr_manager.h.
References DebugAssert, and CVC3::ExprValue::hash().
Referenced by CVC3::Expr::hash().
bool CVC3::ExprManager::EqEV::operator() | ( | const ExprValue * | ev1, | |
const ExprValue * | ev2 | |||
) | const [inline, inherited] |
Definition at line 485 of file expr_manager.h.