CVC3
|
![]() |
Functions | |
size_t | CVC3::ExprManager::HashString::operator() (const std::string &s) const |
CVC3::ExprManager::HashEV::HashEV (ExprManager *em) | |
size_t | CVC3::ExprManager::HashEV::operator() (ExprValue *ev) const |
bool | CVC3::ExprManager::EqEV::operator() (const ExprValue *ev1, const ExprValue *ev2) const |
CVC3::ExprManager::TypeComputer::TypeComputer () | |
virtual | CVC3::ExprManager::TypeComputer::~TypeComputer () |
virtual void | CVC3::ExprManager::TypeComputer::computeType (const Expr &e)=0 |
Compute the type of e. | |
virtual void | CVC3::ExprManager::TypeComputer::checkType (const Expr &e)=0 |
Check that e is a valid Type expr. | |
virtual Cardinality | CVC3::ExprManager::TypeComputer::finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)=0 |
Get information related to finiteness of a type. | |
Expr | CVC3::ExprManager::rebuildRec (const Expr &e) |
Cached recursive descent. Must be called only during rebuild() | |
ExprValue * | CVC3::ExprManager::newExprValue (ExprValue *ev) |
Return either an existing or a new ExprValue matching ev. | |
unsigned | CVC3::ExprManager::getFlag () |
Return the current Expr flag counter. | |
unsigned | CVC3::ExprManager::nextFlag () |
Increment and return the Expr flag counter (this clears all the flags) | |
void | CVC3::ExprManager::computeType (const Expr &e) |
Compute the type of the Expr. | |
void | CVC3::ExprManager::checkType (const Expr &e) |
Check well-formedness of a type Expr. | |
Cardinality | CVC3::ExprManager::finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize) |
Get information related to finiteness of a type. | |
CVC3::ExprManager::ExprManager (ContextManager *cm, const CLFlags &flags) | |
Constructor. | |
CVC3::ExprManager::~ExprManager () | |
Destructor. | |
void | CVC3::ExprManager::clear () |
Free up all memory and delete all the expressions. | |
bool | CVC3::ExprManager::isActive () |
Check if the ExprManager is still active (clear() was not called) | |
void | CVC3::ExprManager::gc (ExprValue *ev) |
Garbage collect the ExprValue pointer. | |
void | CVC3::ExprManager::postponeGC () |
Postpone deletion of garbage-collected expressions. | |
void | CVC3::ExprManager::resumeGC () |
Resume deletion of garbage-collected expressions. | |
Expr | CVC3::ExprManager::rebuild (const Expr &e) |
Rebuild the Expr with this ExprManager if it belongs to another ExprManager. | |
ExprIndex | CVC3::ExprManager::nextIndex () |
Return the next Expr index. | |
ExprIndex | CVC3::ExprManager::lastIndex () |
void | CVC3::ExprManager::clearFlags () |
Clears the generic Expr flag in all Exprs. | |
const Expr & | CVC3::ExprManager::boolExpr () |
BOOLEAN Expr. | |
const Expr & | CVC3::ExprManager::falseExpr () |
FALSE Expr. | |
const Expr & | CVC3::ExprManager::trueExpr () |
TRUE Expr. | |
const std::vector< Expr > & | CVC3::ExprManager::getEmptyVector () |
References to empty objects (used in ExprValue) | |
const Expr & | CVC3::ExprManager::getNullExpr () |
References to empty objects (used in ExprValue) | |
Expr | CVC3::ExprManager::newExpr (ExprValue *ev) |
Return either an existing or a new Expr matching ev. | |
Expr | CVC3::ExprManager::newLeafExpr (const Op &op) |
Expr | CVC3::ExprManager::newStringExpr (const std::string &s) |
Expr | CVC3::ExprManager::newRatExpr (const Rational &r) |
Expr | CVC3::ExprManager::newSkolemExpr (const Expr &e, int i) |
Expr | CVC3::ExprManager::newVarExpr (const std::string &s) |
Expr | CVC3::ExprManager::newSymbolExpr (const std::string &s, int kind) |
Expr | CVC3::ExprManager::newBoundVarExpr (const std::string &name, const std::string &uid) |
Expr | CVC3::ExprManager::newBoundVarExpr (const std::string &name, const std::string &uid, const Type &type) |
Expr | CVC3::ExprManager::newBoundVarExpr (const Type &type) |
Expr | CVC3::ExprManager::newClosureExpr (int kind, const Expr &var, const Expr &body) |
Expr | CVC3::ExprManager::newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body) |
Expr | CVC3::ExprManager::newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const Expr &trigger) |
Expr | CVC3::ExprManager::newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers) |
Expr | CVC3::ExprManager::newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers) |
Expr | CVC3::ExprManager::andExpr (const std::vector< Expr > &children) |
Expr | CVC3::ExprManager::orExpr (const std::vector< Expr > &children) |
size_t | CVC3::ExprManager::hash (const Expr &e) const |
Hash function for a single Expr. | |
ContextManager * | CVC3::ExprManager::getCM () const |
Fetch our ContextManager. | |
Context * | CVC3::ExprManager::getCurrentContext () const |
Get the current context from our ContextManager. | |
int | CVC3::ExprManager::scopelevel () |
Get current scope level. | |
void | CVC3::ExprManager::setTM (TheoremManager *tm) |
Set the TheoremManager. | |
TheoremManager * | CVC3::ExprManager::getTM () const |
Fetch the TheoremManager. | |
MemoryManager * | CVC3::ExprManager::getMM (size_t MMIndex) |
Return a MemoryManager for the given ExprValue type. | |
unsigned | CVC3::ExprManager::getSimpCacheTag () const |
Get the simplifier's cache tag. | |
void | CVC3::ExprManager::invalidateSimpCache () |
Invalidate the simplifier's cache tag. | |
void | CVC3::ExprManager::registerTypeComputer (TypeComputer *typeComputer) |
Register type computer. | |
int | CVC3::ExprManager::printDepth () const |
Get printing depth. | |
bool | CVC3::ExprManager::withIndentation () const |
Whether to print with indentation. | |
int | CVC3::ExprManager::lineWidth () const |
Suggested line width for printing with indentation. | |
int | CVC3::ExprManager::indent () const |
Get initial indentation. | |
int | CVC3::ExprManager::indent (int n, bool permanent=false) |
Set initial indentation. Returns the previous permanent value. | |
int | CVC3::ExprManager::incIndent (int n, bool permanent=false) |
Increment the current transient indentation by n. | |
void | CVC3::ExprManager::restoreIndent () |
Set transient indentation to permanent. | |
InputLanguage | CVC3::ExprManager::getInputLang () const |
Get the input language for printing. | |
InputLanguage | CVC3::ExprManager::getOutputLang () const |
Get the output language for printing. | |
bool | CVC3::ExprManager::dagPrinting () const |
Whether to print Expr's as DAGs. | |
PrettyPrinter * | CVC3::ExprManager::getPrinter () const |
Return the pretty-printer if there is one; otherwise return NULL. | |
void | CVC3::ExprManager::newKind (int kind, const std::string &name, bool isType=false) |
Register a new kind. | |
void | CVC3::ExprManager::registerPrettyPrinter (PrettyPrinter &printer) |
Register the pretty-printer (can only do it if none registered) | |
void | CVC3::ExprManager::unregisterPrettyPrinter () |
Tell ExprManager that the printer is no longer valid. | |
bool | CVC3::ExprManager::isKindRegistered (int kind) |
Returns true if kind is built into CVC or has been registered via newKind. | |
bool | CVC3::ExprManager::isTypeKind (int kind) |
Check if a kind represents a type. | |
const std::string & | CVC3::ExprManager::getKindName (int kind) |
Return the name associated with a kind. The kind must already be registered. | |
int | CVC3::ExprManager::getKind (const std::string &name) |
Return a kind associated with a name. Returns NULL_KIND if not found. | |
size_t | CVC3::ExprManager::registerSubclass (size_t sizeOfSubclass) |
Register a new subclass of ExprValue. | |
unsigned long | CVC3::ExprManager::getMemory (int verbosity) |
Calculate memory usage. | |
CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj (ExprManager *em, Context *cxt) | |
Constructor. | |
void | CVC3::ExprManagerNotifyObj::notifyPre (void) |
void | CVC3::ExprManagerNotifyObj::notify (void) |
unsigned long | CVC3::ExprManagerNotifyObj::getMemory (int verbosity) |
size_t | CVC3::ExprManager::hash (const ExprValue *ev) const |
Variables | |
std::hash< char * > | CVC3::ExprManager::HashString::h |
ExprManager * | CVC3::ExprManager::HashEV::d_em |
ExprManager * | CVC3::ExprManagerNotifyObj::d_em |
|
inline |
Definition at line 79 of file expr_manager.h.
|
inline |
Definition at line 119 of file expr_manager.h.
|
inline |
Definition at line 120 of file expr_manager.h.
|
inline |
Definition at line 537 of file expr_manager.h.
|
inline |
Definition at line 185 of file expr_manager.h.
|
inlinevirtual |
Definition at line 186 of file expr_manager.h.
|
pure virtual |
Compute the type of e.
Implemented in CVC3::TypeComputerCore.
Referenced by CVC3::ExprManager::computeType().
|
pure virtual |
Check that e is a valid Type expr.
Implemented in CVC3::TypeComputerCore.
Referenced by CVC3::ExprManager::checkType().
|
pure virtual |
Get information related to finiteness of a type.
Implemented in CVC3::TypeComputerCore.
Referenced by CVC3::ExprManager::finiteTypeInfo().
Cached recursive descent. Must be called only during rebuild()
Definition at line 251 of file expr_manager.cpp.
References CVC3::Expr::d_expr, CVC3::ExprManager::d_exprSet, CVC3::ExprManager::d_rebuildCache, CVC3::ExprValue::d_type, DebugAssert, CVC3::MemoryManager::deleteData(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::end(), CVC3::ExprHashMap< Data >::end(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::find(), CVC3::ExprHashMap< Data >::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 288 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().
|
inlineprivate |
Return the current Expr flag counter.
Definition at line 213 of file expr_manager.h.
Referenced by CVC3::Expr::setFlag().
|
inlineprivate |
Increment and return the Expr flag counter (this clears all the flags)
Definition at line 215 of file expr_manager.h.
References FatalAssert.
|
private |
Compute the type of the Expr.
Definition at line 465 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().
|
private |
Check well-formedness of a type Expr.
Definition at line 472 of file expr_manager.cpp.
References CVC3::ExprManager::TypeComputer::checkType(), CVC3::ExprManager::d_typeComputer, DebugAssert, and CVC3::Expr::isValidType().
Referenced by CVC3::Type::Type().
|
private |
Get information related to finiteness of a type.
Definition at line 479 of file expr_manager.cpp.
References CVC3::ExprManager::d_typeComputer, DebugAssert, and CVC3::ExprManager::TypeComputer::finiteTypeInfo().
Referenced by CVC3::Expr::typeCard(), CVC3::Expr::typeEnumerateFinite(), and CVC3::Expr::typeSizeFinite().
ExprManager::ExprManager | ( | ContextManager * | cm, |
const CLFlags & | flags | ||
) |
Constructor.
Definition at line 70 of file expr_manager.cpp.
References BOOLEAN, CVC3::ExprManager::d_bool, CVC3::ExprManager::d_cm, CVC3::ExprManager::d_false, 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_UCONST, CVC3::EXPR_VALUE, FALSE_EXPR, CVC3::ContextManager::getCurrentContext(), IF_DEBUG, CVC3::ExprManager::newLeafExpr(), registerKinds(), CVC3::Expr::setType(), TRUE_EXPR, and CVC3::Type::typeBool().
Referenced by CVC3::ExprManager::getMemory().
ExprManager::~ExprManager | ( | ) |
Destructor.
Definition at line 125 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 | ( | ) |
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 141 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, CVC3::ExprValue::getMMIndex(), IF_DEBUG, CVC3::ExprManager::isActive(), CVC3::Expr::isNull(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::size(), TRACE, and TRACE_MSG.
Referenced by CVC3::ExprManager::~ExprManager().
bool ExprManager::isActive | ( | ) |
Check if the ExprManager is still active (clear() was not called)
Definition at line 184 of file expr_manager.cpp.
References CVC3::ExprManager::d_disableGC.
Referenced by CVC3::ExprManager::clear(), CVC3::ExprManager::newExprValue(), CVC3::Theorem::print(), and CVC3::ExprManager::rebuild().
void ExprManager::gc | ( | ExprValue * | ev | ) |
Garbage collect the ExprValue pointer.
Definition at line 188 of file expr_manager.cpp.
References CVC3::ExprManager::d_disableGC, CVC3::ExprManager::d_exprSet, CVC3::ExprManager::d_inGC, CVC3::ExprManager::d_mm, CVC3::ExprManager::d_pending, CVC3::ExprManager::d_postponed, CVC3::ExprManager::d_postponeGC, Hash::hash_set< _Key, _HashFcn, _EqualKey >::erase(), FatalAssert, CVC3::ExprValue::getMMIndex(), and IF_DEBUG.
Referenced by CVC3::Expr::~Expr().
|
inline |
Postpone deletion of garbage-collected expressions.
Definition at line 257 of file expr_manager.h.
void ExprManager::resumeGC | ( | ) |
Resume deletion of garbage-collected expressions.
Definition at line 212 of file expr_manager.cpp.
References CVC3::ExprManager::d_mm, CVC3::ExprManager::d_postponed, CVC3::ExprManager::d_postponeGC, and CVC3::ExprValue::getMMIndex().
Rebuild the Expr with this ExprManager if it belongs to another ExprManager.
Definition at line 226 of file expr_manager.cpp.
References CVC3::ExprHashMap< Data >::clear(), CVC3::ExprManager::d_rebuildCache, DebugAssert, CVC3::Expr::getEM(), IF_DEBUG, CVC3::ExprManager::isActive(), CVC3::Expr::isNull(), CVC3::ExprManager::rebuildRec(), and CVC3::ExprHashMap< Data >::size().
Referenced by CVC3::Op::Op(), and CVC3::Expr::rebuild().
|
inline |
Return the next Expr index.
It should be used only by ExprValue() constructor
Definition at line 268 of file expr_manager.h.
Referenced by CVC3::ExprManager::newExprValue(), and CVC3::ExprManager::rebuildRec().
|
inline |
Definition at line 269 of file expr_manager.h.
Referenced by CVC3::Expr::hasLastIndex().
|
inline |
Clears the generic Expr flag in all Exprs.
Definition at line 272 of file expr_manager.h.
Referenced by CVC3::Expr::clearFlags(), and IF_DEBUG().
|
inline |
BOOLEAN Expr.
Definition at line 276 of file expr_manager.h.
Referenced by CVC3::TheoryCore::parseExprOp(), and CVC3::Type::typeBool().
|
inline |
FALSE Expr.
Definition at line 278 of file expr_manager.h.
Referenced by CVC3::TheorySimulate::computeTCC(), CVC3::SearchEngineTheoremProducer::confAndrAF(), CVC3::SearchEngineTheoremProducer::confAndrAT(), CVC3::SearchEngineTheoremProducer::confIffr(), CVC3::SearchEngineTheoremProducer::confIterIfThen(), CVC3::SearchEngineTheoremProducer::confIterThenElse(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::CommonTheoremProducer::contradictionRule(), LFSCConvert::cvc3_to_lfsc(), CVC3::Theory::falseExpr(), CVC3::CommonTheoremProducer::iffNotFalse(), CVC3::CommonTheoremProducer::notToIff(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryCore::print(), LFSCObj::queryAtomic(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::ExprTransform::simplifyWithCare(), and LFSCObj::what_is_proven().
|
inline |
TRUE Expr.
Definition at line 280 of file expr_manager.h.
Referenced by CVC3::TheoryCore::computeModelBasic(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryArithNew::computeTypePred(), CVC3::Theory::computeTypePred(), CVC3::TheoryBitvector::computeTypePred(), CVC3::TheoryArith3::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryCore::computeTypePred(), LFSCConvert::cvc3_to_lfsc(), LFSCObj::getY(), CVC3::CommonTheoremProducer::iffTrue(), CVC3::TheoryCore::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryCore::print(), LFSCObj::queryAtomic(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ExprTransform::simplifyWithCare(), CVC3::Theory::trueExpr(), CVC3::CommonTheoremProducer::trueTheorem(), CVC3::QuantTheoremProducer::universalInst(), and LFSCObj::what_is_proven().
|
inline |
References to empty objects (used in ExprValue)
Definition at line 282 of file expr_manager.h.
Referenced by CVC3::Expr::begin(), CVC3::Expr::end(), and CVC3::Expr::getKids().
|
inline |
References to empty objects (used in ExprValue)
Definition at line 284 of file expr_manager.h.
|
inline |
Return either an existing or a new Expr matching ev.
Definition at line 289 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(), and CVC3::ExprManager::newVarExpr().
|
inline |
Definition at line 454 of file expr_manager.h.
References APPLY, DebugAssert, CVC3::Expr::getEM(), CVC3::Op::getExpr(), CVC3::Op::getKind(), and CVC3::ExprManager::newExpr().
Referenced by CVC3::ExprStream::addLetHeader(), CVC3::Type::anyType(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::ExprManager::ExprManager(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::CommonTheoremProducer::substitutivityRule(), and CVC3::TheoremProducer::TheoremProducer().
|
inline |
Definition at line 468 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::Translator::finish(), LFSCObj::initialize(), and CVC3::TheoryQuant::TheoryQuant().
|
inline |
Definition at line 471 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::CommonTheoremProducer::andElim(), LFSCConvert::cvc3_to_lfsc(), CVC3::CompleteInstPreProcessor::inst(), CVC3::CompleteInstPreProcessor::minusOne(), CVC3::CompleteInstPreProcessor::plusOne(), CVC3::ArithTheoremProducer3::rat(), CVC3::ArithTheoremProducerOld::rat(), CVC3::ArithTheoremProducer::rat(), CVC3::TheoryArith::rat(), CVC3::TheoryBitvector::rat(), CVC3::BitvectorTheoremProducer::rat(), and LFSCObj::what_is_proven().
|
inline |
Definition at line 474 of file expr_manager.h.
References DebugAssert, CVC3::Expr::getEM(), and CVC3::ExprManager::newExpr().
Referenced by CVC3::Expr::skolemExpr().
|
inline |
Definition at line 478 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::ExprStream::addLetHeader(), CVC3::TheoryQuant::checkSat(), LFSCObj::initialize(), CVC3::Theory::lookupVar(), CVC3::TheoremProducer::newPf(), and CVC3::Theory::newVar().
|
inline |
Definition at line 481 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::TheoryDatatype::dataType(), CVC3::Theory::lookupFunction(), CVC3::Theory::newFunction(), CVC3::Theory::newVar(), and CVC3::Translator::printArrayExpr().
|
inline |
Definition at line 484 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::TheoryUF::computeModel(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::ExprManager::newBoundVarExpr(), CVC3::TheoremProducer::newLabel(), CVC3::Theory::newSubtypeExpr(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::TheoryQuant::TheoryQuant(), and CVC3::CommonTheoremProducer::varIntroRule().
|
inline |
Definition at line 488 of file expr_manager.h.
References ARROW, DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Type::isNull(), CVC3::Expr::lookupType(), CVC3::ExprManager::newBoundVarExpr(), and CVC3::Expr::setType().
|
inline |
Definition at line 499 of file expr_manager.h.
References CVC3::int2string(), and CVC3::ExprManager::newBoundVarExpr().
Definition at line 506 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::arrayLiteral(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoryUF::lambdaExpr(), CVC3::TheoremProducer::newPf(), CVC3::Theory::newSubtypeExpr(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::QuantTheoremProducer::packVar(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), and CVC3::CommonTheoremProducer::varIntroRule().
|
inline |
Definition at line 511 of file expr_manager.h.
References CVC3::ExprManager::newExpr().
|
inline |
Definition at line 530 of file expr_manager.h.
References CVC3::ExprManager::newExpr(), and CVC3::Expr::setTrigger().
|
inline |
Definition at line 516 of file expr_manager.h.
References CVC3::ExprManager::newExpr(), and CVC3::Expr::setTriggers().
|
inline |
Definition at line 523 of file expr_manager.h.
References CVC3::ExprManager::newExpr(), and CVC3::Expr::setTriggers().
|
inline |
Definition at line 312 of file expr_manager.h.
References AND.
|
inline |
Definition at line 314 of file expr_manager.h.
References OR.
|
inline |
Hash function for a single Expr.
Definition at line 542 of file expr_manager.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::hash(), and CVC3::Expr::isNull().
|
inline |
Fetch our ContextManager.
Definition at line 322 of file expr_manager.h.
|
inline |
Get the current context from our ContextManager.
Definition at line 324 of file expr_manager.h.
Referenced by CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), CVC3::Expr::setRep(), and CVC3::Expr::setSig().
|
inline |
Get current scope level.
Definition at line 326 of file expr_manager.h.
|
inline |
Set the TheoremManager.
Definition at line 329 of file expr_manager.h.
|
inline |
Fetch the TheoremManager.
Definition at line 331 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().
|
inline |
Return a MemoryManager for the given ExprValue type.
Definition at line 334 of file expr_manager.h.
References DebugAssert.
Referenced by CVC3::BVConstExpr::copy(), CVC3::ExprValue::copy(), CVC3::ExprNode::copy(), CVC3::ExprNodeTmp::copy(), CVC3::ExprApplyTmp::copy(), CVC3::ExprApply::copy(), CVC3::ExprString::copy(), CVC3::ExprSkolem::copy(), CVC3::ExprRational::copy(), CVC3::ExprVar::copy(), CVC3::ExprSymbol::copy(), CVC3::ExprBoundVar::copy(), CVC3::ExprClosure::copy(), and CVC3::ExprManager::rebuildRec().
|
inline |
Get the simplifier's cache tag.
Definition at line 339 of file expr_manager.h.
Referenced by CVC3::Expr::setSimpCache(), and CVC3::Expr::validSimpCache().
|
inline |
Invalidate the simplifier's cache tag.
Definition at line 341 of file expr_manager.h.
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::CoreNotifyObj::notify(), CVC3::ExprTransform::preprocess(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and CVC3::Theory::updateCC().
|
inline |
Register type computer.
Definition at line 344 of file expr_manager.h.
Referenced by CVC3::TheoryCore::TheoryCore().
|
inline |
Get printing depth.
Definition at line 348 of file expr_manager.h.
|
inline |
Whether to print with indentation.
Definition at line 350 of file expr_manager.h.
|
inline |
Suggested line width for printing with indentation.
Definition at line 352 of file expr_manager.h.
|
inline |
Get initial indentation.
Definition at line 354 of file expr_manager.h.
Referenced by CVC3::ExprStream::ExprStream(), and CVC3::Theorem::print().
int ExprManager::indent | ( | int | n, |
bool | permanent = false |
||
) |
Set initial indentation. Returns the previous permanent value.
Definition at line 334 of file expr_manager.cpp.
References CVC3::ExprManager::d_indent, and CVC3::ExprManager::d_indentTransient.
int ExprManager::incIndent | ( | int | n, |
bool | permanent = false |
||
) |
Increment the current transient indentation by n.
If the second argument is true, sets the result as permanent.
Definition at line 345 of file expr_manager.cpp.
References CVC3::ExprManager::d_indent, and CVC3::ExprManager::d_indentTransient.
Referenced by CVC3::Theorem::print().
|
inline |
Set transient indentation to permanent.
Definition at line 362 of file expr_manager.h.
Referenced by CVC3::operator<<().
InputLanguage ExprManager::getInputLang | ( | ) | const |
Get the input language for printing.
Definition at line 354 of file expr_manager.cpp.
References CVC3::ExprManager::d_inputLang, and CVC3::getLanguage().
Referenced by CVC3::VCCmd::evaluateCommand(), and main().
InputLanguage ExprManager::getOutputLang | ( | ) | const |
Get the output language for printing.
Definition at line 360 of file expr_manager.cpp.
References CVC3::ExprManager::d_inputLang, CVC3::ExprManager::d_outputLang, and CVC3::getLanguage().
Referenced by CVC3::Translator::dumpQueryResult(), CVC3::Translator::escapeSymbol(), CVC3::Translator::finish(), CVC3::Translator::fixConstName(), main(), CVC3::Translator::printArrayExpr(), CVC3::VCCmd::reportResult(), and CVC3::Translator::start().
|
inline |
Whether to print Expr's as DAGs.
Definition at line 368 of file expr_manager.h.
|
inline |
Return the pretty-printer if there is one; otherwise return NULL.
Definition at line 371 of file expr_manager.h.
Referenced by CVC3::operator<<().
void ExprManager::newKind | ( | int | kind, |
const std::string & | name, | ||
bool | isType = false |
||
) |
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 367 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, Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert(), and CVC3::int2string().
Referenced by registerKinds(), CVC3::TheoremManager::TheoremManager(), CVC3::TheoryArith3::TheoryArith3(), 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 | ) |
Register the pretty-printer (can only do it if none registered)
The pointer is NOT owned by ExprManager. Delete it yourself.
Definition at line 391 of file expr_manager.cpp.
References CVC3::ExprManager::d_prettyPrinter, and DebugAssert.
Referenced by CVC3::TheoryCore::TheoryCore().
void ExprManager::unregisterPrettyPrinter | ( | ) |
Tell ExprManager that the printer is no longer valid.
Definition at line 398 of file expr_manager.cpp.
References CVC3::ExprManager::d_prettyPrinter, and FatalAssert.
Referenced by CVC3::TheoryCore::~TheoryCore().
|
inline |
Returns true if kind is built into CVC or has been registered via newKind.
Definition at line 392 of file expr_manager.h.
Referenced by CVC3::ExprValue::ExprValue().
|
inline |
Check if a kind represents a type.
Definition at line 394 of file expr_manager.h.
Referenced by CVC3::Expr::isType().
const string & ExprManager::getKindName | ( | int | kind | ) |
Return the name associated with a kind. The kind must already be registered.
Definition at line 405 of file expr_manager.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), CVC3::ExprManager::d_kindMap, DebugAssert, and CVC3::int2string().
Referenced by CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::Theory::registerKinds(), and CVC3::Theory::theoryOf().
int ExprManager::getKind | ( | const std::string & | name | ) |
Return a kind associated with a name. Returns NULL_KIND if not found.
Definition at line 412 of file expr_manager.cpp.
References CVC3::ExprManager::d_kindMapByName, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), and NULL_KIND.
Referenced by CVC3::VCCmd::evaluateCommand(), CVC3::TheoryCore::parseExpr(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), and CVC3::TheoryQuant::parseExprOp().
size_t ExprManager::registerSubclass | ( | size_t | sizeOfSubclass | ) |
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 421 of file expr_manager.cpp.
References CVC3::ExprManager::d_mm, CVC3::ExprManager::d_mmFlag, and FatalAssert.
Referenced by CVC3::TheoryBitvector::TheoryBitvector().
unsigned long ExprManager::getMemory | ( | int | verbosity | ) |
Calculate memory usage.
Definition at line 433 of file expr_manager.cpp.
References CVC3::ExprManager::d_mmFlag, CVC3::ExprManager::ExprManager(), CVC3::MemoryTracker::getString(), and CVC3::MemoryTracker::print().
|
inline |
Constructor.
Definition at line 433 of file expr_manager.h.
Referenced by CVC3::ExprManagerNotifyObj::getMemory().
|
virtual |
Reimplemented from CVC3::ContextNotifyObj.
Definition at line 659 of file expr_manager.cpp.
|
virtual |
Reimplemented from CVC3::ContextNotifyObj.
Definition at line 664 of file expr_manager.cpp.
|
inlinevirtual |
Reimplemented from CVC3::ContextNotifyObj.
Definition at line 438 of file expr_manager.h.
References CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj().
|
inlineprivate |
Definition at line 449 of file expr_manager.h.
References DebugAssert, and CVC3::ExprValue::hash().
Referenced by CVC3::Expr::hash().
|
private |
Definition at line 77 of file expr_manager.h.
|
private |
Definition at line 117 of file expr_manager.h.
|
private |
Definition at line 430 of file expr_manager.h.