CVC3  2.4.1
Functions | Variables
Private methods

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. More...
 
virtual void CVC3::ExprManager::TypeComputer::checkType (const Expr &e)=0
 Check that e is a valid Type expr. More...
 
virtual Cardinality CVC3::ExprManager::TypeComputer::finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)=0
 Get information related to finiteness of a type. More...
 
Expr CVC3::ExprManager::rebuildRec (const Expr &e)
 Cached recursive descent. Must be called only during rebuild() More...
 
ExprValueCVC3::ExprManager::newExprValue (ExprValue *ev)
 Return either an existing or a new ExprValue matching ev. More...
 
unsigned CVC3::ExprManager::getFlag ()
 Return the current Expr flag counter. More...
 
unsigned CVC3::ExprManager::nextFlag ()
 Increment and return the Expr flag counter (this clears all the flags) More...
 
void CVC3::ExprManager::computeType (const Expr &e)
 Compute the type of the Expr. More...
 
void CVC3::ExprManager::checkType (const Expr &e)
 Check well-formedness of a type Expr. More...
 
Cardinality CVC3::ExprManager::finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)
 Get information related to finiteness of a type. More...
 
 CVC3::ExprManager::ExprManager (ContextManager *cm, const CLFlags &flags)
 Constructor. More...
 
 CVC3::ExprManager::~ExprManager ()
 Destructor. More...
 
void CVC3::ExprManager::clear ()
 Free up all memory and delete all the expressions. More...
 
bool CVC3::ExprManager::isActive ()
 Check if the ExprManager is still active (clear() was not called) More...
 
void CVC3::ExprManager::gc (ExprValue *ev)
 Garbage collect the ExprValue pointer. More...
 
void CVC3::ExprManager::postponeGC ()
 Postpone deletion of garbage-collected expressions. More...
 
void CVC3::ExprManager::resumeGC ()
 Resume deletion of garbage-collected expressions. More...
 
Expr CVC3::ExprManager::rebuild (const Expr &e)
 Rebuild the Expr with this ExprManager if it belongs to another ExprManager. More...
 
ExprIndex CVC3::ExprManager::nextIndex ()
 Return the next Expr index. More...
 
ExprIndex CVC3::ExprManager::lastIndex ()
 
void CVC3::ExprManager::clearFlags ()
 Clears the generic Expr flag in all Exprs. More...
 
const Expr & CVC3::ExprManager::boolExpr ()
 BOOLEAN Expr. More...
 
const Expr & CVC3::ExprManager::falseExpr ()
 FALSE Expr. More...
 
const Expr & CVC3::ExprManager::trueExpr ()
 TRUE Expr. More...
 
const std::vector< Expr > & CVC3::ExprManager::getEmptyVector ()
 References to empty objects (used in ExprValue) More...
 
const Expr & CVC3::ExprManager::getNullExpr ()
 References to empty objects (used in ExprValue) More...
 
Expr CVC3::ExprManager::newExpr (ExprValue *ev)
 Return either an existing or a new Expr matching ev. More...
 
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. More...
 
ContextManager * CVC3::ExprManager::getCM () const
 Fetch our ContextManager. More...
 
Context * CVC3::ExprManager::getCurrentContext () const
 Get the current context from our ContextManager. More...
 
int CVC3::ExprManager::scopelevel ()
 Get current scope level. More...
 
void CVC3::ExprManager::setTM (TheoremManager *tm)
 Set the TheoremManager. More...
 
TheoremManager * CVC3::ExprManager::getTM () const
 Fetch the TheoremManager. More...
 
MemoryManager * CVC3::ExprManager::getMM (size_t MMIndex)
 Return a MemoryManager for the given ExprValue type. More...
 
unsigned CVC3::ExprManager::getSimpCacheTag () const
 Get the simplifier's cache tag. More...
 
void CVC3::ExprManager::invalidateSimpCache ()
 Invalidate the simplifier's cache tag. More...
 
void CVC3::ExprManager::registerTypeComputer (TypeComputer *typeComputer)
 Register type computer. More...
 
int CVC3::ExprManager::printDepth () const
 Get printing depth. More...
 
bool CVC3::ExprManager::withIndentation () const
 Whether to print with indentation. More...
 
int CVC3::ExprManager::lineWidth () const
 Suggested line width for printing with indentation. More...
 
int CVC3::ExprManager::indent () const
 Get initial indentation. More...
 
int CVC3::ExprManager::indent (int n, bool permanent=false)
 Set initial indentation. Returns the previous permanent value. More...
 
int CVC3::ExprManager::incIndent (int n, bool permanent=false)
 Increment the current transient indentation by n. More...
 
void CVC3::ExprManager::restoreIndent ()
 Set transient indentation to permanent. More...
 
InputLanguage CVC3::ExprManager::getInputLang () const
 Get the input language for printing. More...
 
InputLanguage CVC3::ExprManager::getOutputLang () const
 Get the output language for printing. More...
 
bool CVC3::ExprManager::dagPrinting () const
 Whether to print Expr's as DAGs. More...
 
PrettyPrinter * CVC3::ExprManager::getPrinter () const
 Return the pretty-printer if there is one; otherwise return NULL. More...
 
void CVC3::ExprManager::newKind (int kind, const std::string &name, bool isType=false)
 Register a new kind. More...
 
void CVC3::ExprManager::registerPrettyPrinter (PrettyPrinter &printer)
 Register the pretty-printer (can only do it if none registered) More...
 
void CVC3::ExprManager::unregisterPrettyPrinter ()
 Tell ExprManager that the printer is no longer valid. More...
 
bool CVC3::ExprManager::isKindRegistered (int kind)
 Returns true if kind is built into CVC or has been registered via newKind. More...
 
bool CVC3::ExprManager::isTypeKind (int kind)
 Check if a kind represents a type. More...
 
const std::string & CVC3::ExprManager::getKindName (int kind)
 Return the name associated with a kind. The kind must already be registered. More...
 
int CVC3::ExprManager::getKind (const std::string &name)
 Return a kind associated with a name. Returns NULL_KIND if not found. More...
 
size_t CVC3::ExprManager::registerSubclass (size_t sizeOfSubclass)
 Register a new subclass of ExprValue. More...
 
unsigned long CVC3::ExprManager::getMemory (int verbosity)
 Calculate memory usage. More...
 
 CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj (ExprManager *em, Context *cxt)
 Constructor. More...
 
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
 

Detailed Description

Function Documentation

size_t CVC3::ExprManager::HashString::operator() ( const std::string &  s) const
inline

Definition at line 79 of file expr_manager.h.

CVC3::ExprManager::HashEV::HashEV ( ExprManager em)
inline

Definition at line 119 of file expr_manager.h.

size_t CVC3::ExprManager::HashEV::operator() ( ExprValue ev) const
inline

Definition at line 120 of file expr_manager.h.

bool CVC3::ExprManager::EqEV::operator() ( const ExprValue ev1,
const ExprValue ev2 
) const
inline

Definition at line 537 of file expr_manager.h.

CVC3::ExprManager::TypeComputer::TypeComputer ( )
inline

Definition at line 185 of file expr_manager.h.

virtual CVC3::ExprManager::TypeComputer::~TypeComputer ( )
inlinevirtual

Definition at line 186 of file expr_manager.h.

virtual void CVC3::ExprManager::TypeComputer::computeType ( const Expr e)
pure virtual

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

Check that e is a valid Type expr.

Implemented in CVC3::TypeComputerCore.

Referenced by CVC3::ExprManager::checkType().

virtual Cardinality CVC3::ExprManager::TypeComputer::finiteTypeInfo ( Expr e,
Unsigned n,
bool  enumerate,
bool  computeSize 
)
pure virtual

Get information related to finiteness of a type.

Implemented in CVC3::TypeComputerCore.

Referenced by CVC3::ExprManager::finiteTypeInfo().

Expr ExprManager::rebuildRec ( const Expr e)
private
ExprValue * ExprManager::newExprValue ( ExprValue ev)
private
unsigned CVC3::ExprManager::getFlag ( )
inlineprivate

Return the current Expr flag counter.

Definition at line 213 of file expr_manager.h.

Referenced by CVC3::Expr::setFlag().

unsigned CVC3::ExprManager::nextFlag ( )
inlineprivate

Increment and return the Expr flag counter (this clears all the flags)

Definition at line 215 of file expr_manager.h.

References FatalAssert.

void ExprManager::computeType ( const Expr e)
private
void ExprManager::checkType ( const Expr e)
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().

Cardinality ExprManager::finiteTypeInfo ( Expr e,
Unsigned n,
bool  enumerate,
bool  computeSize 
)
private
ExprManager::ExprManager ( ContextManager cm,
const CLFlags flags 
)
ExprManager::~ExprManager ( )
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)
void CVC3::ExprManager::postponeGC ( )
inline

Postpone deletion of garbage-collected expressions.

See Also
resumeGC()

Definition at line 257 of file expr_manager.h.

void ExprManager::resumeGC ( )

Resume deletion of garbage-collected expressions.

See Also
postponeGC()

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().

Expr ExprManager::rebuild ( const Expr e)
ExprIndex CVC3::ExprManager::nextIndex ( )
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().

ExprIndex CVC3::ExprManager::lastIndex ( )
inline

Definition at line 269 of file expr_manager.h.

Referenced by CVC3::Expr::hasLastIndex().

void CVC3::ExprManager::clearFlags ( )
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().

const Expr& CVC3::ExprManager::boolExpr ( )
inline

BOOLEAN Expr.

Definition at line 276 of file expr_manager.h.

Referenced by CVC3::TheoryCore::parseExprOp(), and CVC3::Type::typeBool().

const Expr& CVC3::ExprManager::falseExpr ( )
inline
const Expr& CVC3::ExprManager::trueExpr ( )
inline
const std::vector<Expr>& CVC3::ExprManager::getEmptyVector ( )
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().

const Expr& CVC3::ExprManager::getNullExpr ( )
inline

References to empty objects (used in ExprValue)

Definition at line 284 of file expr_manager.h.

Expr CVC3::ExprManager::newExpr ( ExprValue ev)
inline
Expr CVC3::ExprManager::newLeafExpr ( const Op op)
inline
Expr CVC3::ExprManager::newStringExpr ( const std::string &  s)
inline
Expr CVC3::ExprManager::newRatExpr ( const Rational r)
inline
Expr CVC3::ExprManager::newSkolemExpr ( const Expr e,
int  i 
)
inline

Definition at line 474 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
Expr CVC3::ExprManager::newSymbolExpr ( const std::string &  s,
int  kind 
)
inline
Expr CVC3::ExprManager::newBoundVarExpr ( const std::string &  name,
const std::string &  uid 
)
inline
Expr CVC3::ExprManager::newBoundVarExpr ( const std::string &  name,
const std::string &  uid,
const Type type 
)
inline
Expr CVC3::ExprManager::newBoundVarExpr ( const Type type)
inline

Definition at line 499 of file expr_manager.h.

References CVC3::int2string(), and CVC3::ExprManager::newBoundVarExpr().

Expr CVC3::ExprManager::newClosureExpr ( int  kind,
const Expr var,
const Expr body 
)
inline
Expr CVC3::ExprManager::newClosureExpr ( int  kind,
const std::vector< Expr > &  vars,
const Expr body 
)
inline

Definition at line 511 of file expr_manager.h.

References CVC3::ExprManager::newExpr().

Expr CVC3::ExprManager::newClosureExpr ( int  kind,
const std::vector< Expr > &  vars,
const Expr body,
const Expr trigger 
)
inline

Definition at line 530 of file expr_manager.h.

References CVC3::ExprManager::newExpr(), and CVC3::Expr::setTrigger().

Expr CVC3::ExprManager::newClosureExpr ( int  kind,
const std::vector< Expr > &  vars,
const Expr body,
const std::vector< Expr > &  triggers 
)
inline

Definition at line 516 of file expr_manager.h.

References CVC3::ExprManager::newExpr(), and CVC3::Expr::setTriggers().

Expr CVC3::ExprManager::newClosureExpr ( int  kind,
const std::vector< Expr > &  vars,
const Expr body,
const std::vector< std::vector< Expr > > &  triggers 
)
inline

Definition at line 523 of file expr_manager.h.

References CVC3::ExprManager::newExpr(), and CVC3::Expr::setTriggers().

Expr CVC3::ExprManager::andExpr ( const std::vector< Expr > &  children)
inline

Definition at line 312 of file expr_manager.h.

References AND.

Expr CVC3::ExprManager::orExpr ( const std::vector< Expr > &  children)
inline

Definition at line 314 of file expr_manager.h.

References OR.

size_t CVC3::ExprManager::hash ( const Expr e) const
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().

ContextManager* CVC3::ExprManager::getCM ( ) const
inline

Fetch our ContextManager.

Definition at line 322 of file expr_manager.h.

Context* CVC3::ExprManager::getCurrentContext ( ) const
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().

int CVC3::ExprManager::scopelevel ( )
inline

Get current scope level.

Definition at line 326 of file expr_manager.h.

void CVC3::ExprManager::setTM ( TheoremManager tm)
inline

Set the TheoremManager.

Definition at line 329 of file expr_manager.h.

TheoremManager* CVC3::ExprManager::getTM ( ) const
inline
MemoryManager* CVC3::ExprManager::getMM ( size_t  MMIndex)
inline
unsigned CVC3::ExprManager::getSimpCacheTag ( ) const
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().

void CVC3::ExprManager::invalidateSimpCache ( )
inline
void CVC3::ExprManager::registerTypeComputer ( TypeComputer typeComputer)
inline

Register type computer.

Definition at line 344 of file expr_manager.h.

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

int CVC3::ExprManager::printDepth ( ) const
inline

Get printing depth.

Definition at line 348 of file expr_manager.h.

bool CVC3::ExprManager::withIndentation ( ) const
inline

Whether to print with indentation.

Definition at line 350 of file expr_manager.h.

int CVC3::ExprManager::lineWidth ( ) const
inline

Suggested line width for printing with indentation.

Definition at line 352 of file expr_manager.h.

int CVC3::ExprManager::indent ( ) const
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.

Returns
previous permanent value.

Definition at line 345 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

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
bool CVC3::ExprManager::dagPrinting ( ) const
inline

Whether to print Expr's as DAGs.

Definition at line 368 of file expr_manager.h.

PrettyPrinter* CVC3::ExprManager::getPrinter ( ) const
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 
)
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().

bool CVC3::ExprManager::isKindRegistered ( int  kind)
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().

bool CVC3::ExprManager::isTypeKind ( int  kind)
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)
int ExprManager::getKind ( const std::string &  name)
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)
CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj ( ExprManager em,
Context cxt 
)
inline

Constructor.

Definition at line 433 of file expr_manager.h.

Referenced by CVC3::ExprManagerNotifyObj::getMemory().

void ExprManagerNotifyObj::notifyPre ( void  )
virtual

Reimplemented from CVC3::ContextNotifyObj.

Definition at line 659 of file expr_manager.cpp.

void ExprManagerNotifyObj::notify ( void  )
virtual

Reimplemented from CVC3::ContextNotifyObj.

Definition at line 664 of file expr_manager.cpp.

unsigned long CVC3::ExprManagerNotifyObj::getMemory ( int  verbosity)
inlinevirtual

Reimplemented from CVC3::ContextNotifyObj.

Definition at line 438 of file expr_manager.h.

References CVC3::ExprManagerNotifyObj::ExprManagerNotifyObj().

size_t CVC3::ExprManager::hash ( const ExprValue ev) const
inlineprivate

Definition at line 449 of file expr_manager.h.

References DebugAssert, and CVC3::ExprValue::hash().

Referenced by CVC3::Expr::hash().

Variable Documentation

std::hash<char*> CVC3::ExprManager::HashString::h
private

Definition at line 77 of file expr_manager.h.

ExprManager* CVC3::ExprManager::HashEV::d_em
private

Definition at line 117 of file expr_manager.h.

ExprManager* CVC3::ExprManagerNotifyObj::d_em
private

Definition at line 430 of file expr_manager.h.