CVC3::ExprValue Class Reference

The base class for holding the actual data in expressions. More...

#include <expr_value.h>

Inheritance diagram for CVC3::ExprValue:

[legend]Collaboration diagram for CVC3::ExprValue:

[legend]List of all members.

Public Member Functions

ExprValue (ExprManager *em, int kind, ExprIndex idx=0)
Constructor.
virtual ~ExprValue ()
Destructor.
int getKind () const
Get the kind of the expression.
void * operator new (size_t size, MemoryManager *mm)
Overload operator new.
void operator delete (void *pMem, MemoryManager *mm)
void operator delete (void *)
Overload operator delete.
virtual size_t getMMIndex () const
Get unique memory manager ID.
virtual bool operator== (const ExprValue &ev2) const
Equality between any two ExprValue objects (including subclasses).
virtual const ExprValue * getExprValue () const
Test whether the expression is a generic subclass.
virtual bool isString () const
String expression tester.
virtual bool isRational () const
Rational number expression tester.
virtual bool isVar () const
Uninterpreted constants.
virtual bool isApply () const
Application of another expression.
virtual bool isSymbol () const
Special named symbol.
virtual bool isClosure () const
A LAMBDA-expression or a quantifier.
virtual bool isTheorem () const
Special Expr holding a theorem.
virtual const std::vector<
Expr > & getKids () const
Get kids: by default, returns a ref to an empty vector.
virtual unsigned arity () const
Default arity = 0.
virtual CDO< Theorem > * getSig () const
Special attributes for uninterpreted functions.
virtual CDO< Theorem > * getRep () const
virtual void setSig (CDO< Theorem > *sig)
virtual void setRep (CDO< Theorem > *rep)
virtual const std::string & getUid () const
virtual const std::string & getString () const
virtual const Rational & getRational () const
virtual const std::string & getName () const
Returns the string name of UCONST and BOUND_VAR expr's.
virtual const Expr & getVar () const
Returns the original Boolean variable (for BoolVarExprValue).
virtual Op getOp () const
Get the Op from an Apply Expr.
virtual const std::vector<
Expr > & getVars () const
virtual const Expr & getBody () const
virtual const Expr & getExistential () const
virtual int getBoundIndex () const
virtual const std::vector<
std::string > & getFields () const
virtual const std::string & getField () const
virtual int getTupleIndex () const
virtual const Theorem & getTheorem () const

Protected Member Functions

MemoryManager * getMM (size_t MMIndex)
Return the memory manager (for the benefit of subclasses).
ExprValue * rebuild (ExprManager *em) const
Make a clean copy of itself using the given ExprManager.
Expr rebuild (Expr e, ExprManager *em) const
Make a clean copy of the expr using the given ExprManager.
virtual size_t computeHash () const
Non-caching hash function which actually computes the hash.
virtual ExprValue * copy (ExprManager *em, ExprIndex idx) const
Make a clean copy of itself using the given ExprManager.

Static Protected Member Functions

static size_t pointerHash (void *p)
static size_t hash (const int kind, const std::vector< Expr > &kids)
static size_t hash (const int n)

Protected Attributes

int d_kind
The kind of the expression. In particular, it determines which subclass of ExprValue is used to store the expression.
ExprManager * d_em
Our expr. manager.

Static Protected Attributes

static std::hash< char * > s_charHash
Set Expr simplified to obtain this expr.
static std::hash< long int > s_intHash

Private Member Functions

void setIndex (ExprIndex idx)
Set the ExprIndex.
void incRefcount ()
Increment reference counter.
void decRefcount ()
Decrement reference counter.
size_t hash () const
Caching hash function.

Private Attributes

ExprIndex d_index
Unique expression id.
unsigned d_refcount
Reference counter for garbage collection.
size_t d_hash
Cached hash value (initially 0).
CDO< Theorem > * d_find
The find attribute (may be NULL).
Type d_type
The cached type of the expression (may be Null).
NotifyList * d_notifyList
Notify list may be NULL (== no such attribute).
Theorem d_simpCache
For caching calls to Simplify.
unsigned d_simpCacheTag
For checking whether simplify cache is valid.
CDFlags d_dynamicFlags
context-dependent bit-vector for flags that are context-dependent
unsigned d_flag
Generic flag for marking expressions (e.g. in DAG traversal).

Friends

class Expr
class Expr::iterator
class ExprManager
class ::CInterface
class ExprApply
class Theorem

Detailed Description

The base class for holding the actual data in expressions.

Author: Sergey Berezin

Created: long time ago

The base class just holds the operator. All the additional data resides in subclasses.

Definition at line 69 of file expr_value.h.

Constructor & Destructor Documentation

CVC3::ExprValue::ExprValue	(	ExprManager *	em,
		int	kind,
		ExprIndex	idx = `0`
	)			`[inline]`

Constructor.

Definition at line 208 of file expr_value.h.

References CVC3::APPLY, DebugAssert, and CVC3::ExprManager::isKindRegistered().

Referenced by copy().

CVC3::ExprValue::~ExprValue ( ) [virtual]

Destructor.

Definition at line 41 of file expr_value.cpp.

References d_find, d_notifyList, d_simpCache, d_type, and Theorem.

Member Function Documentation

void CVC3::ExprValue::setIndex ( ExprIndex idx ) [inline, private]

Set the ExprIndex.

Definition at line 135 of file expr_value.h.

References d_index.

void CVC3::ExprValue::incRefcount ( ) [inline, private]

Increment reference counter.

Definition at line 138 of file expr_value.h.

References d_refcount.

Referenced by CVC3::Expr::Expr(), CVC3::Theorem::operator=(), CVC3::Expr::operator=(), and CVC3::Theorem::Theorem().

void CVC3::ExprValue::decRefcount ( ) [inline, private]

Decrement reference counter.

Definition at line 141 of file expr_value.h.

References d_em, d_refcount, FatalAssert, and CVC3::ExprManager::gc().

Referenced by CVC3::Theorem::operator=(), CVC3::Expr::operator=(), CVC3::Expr::~Expr(), and CVC3::Theorem::~Theorem().

size_t CVC3::ExprValue::hash ( ) const [inline, private]

Caching hash function.

Do NOT implement it in subclasses! Implement computeHash() instead.

Definition at line 151 of file expr_value.h.

References computeHash(), and d_hash.

Referenced by CVC3::BVConstExpr::computeHash(), CVC3::ExprRational::computeHash(), CVC3::ExprString::computeHash(), CVC3::ExprNodeTmp::computeHash(), CVC3::ExprNode::computeHash(), computeHash(), CVC3::ExprClosure::computeHash(), and CVC3::ExprManager::hash().

static size_t CVC3::ExprValue::pointerHash ( void * p ) [inline, static, protected]

Definition at line 177 of file expr_value.h.

References s_intHash.

Referenced by hash().

size_t CVC3::ExprValue::hash	(	const int	kind,
		const std::vector< Expr > &	kids
	)			`[static, protected]`

Definition at line 304 of file expr_value.cpp.

References pointerHash(), PRIME, and s_intHash.

static size_t CVC3::ExprValue::hash ( const int n ) [inline, static, protected]

Definition at line 181 of file expr_value.h.

References s_intHash.

MemoryManager* CVC3::ExprValue::getMM ( size_t MMIndex ) [inline, protected]

Return the memory manager (for the benefit of subclasses).

Definition at line 184 of file expr_value.h.

References d_em, DebugAssert, and CVC3::ExprManager::getMM().

ExprValue* CVC3::ExprValue::rebuild ( ExprManager * em ) const [inline, protected]

Make a clean copy of itself using the given ExprManager.

Definition at line 190 of file expr_value.h.

References copy().

Referenced by CVC3::ExprClosure::copy(), CVC3::ExprApplyTmp::copy(), CVC3::ExprApply::copy(), CVC3::ExprSkolem::copy(), CVC3::ExprNode::copy(), CVC3::ExprNodeTmp::copy(), and CVC3::ExprManager::rebuildRec().

Expr CVC3::ExprValue::rebuild	(	Expr	e,
		ExprManager *	em
	)			const `[inline, protected]`

Make a clean copy of the expr using the given ExprManager.

Definition at line 194 of file expr_value.h.

References CVC3::ExprManager::rebuildRec().

virtual size_t CVC3::ExprValue::computeHash ( ) const [inline, protected, virtual]

Non-caching hash function which actually computes the hash.

This is the method that all subclasses should implement

Reimplemented in CVC3::ExprNode, CVC3::ExprNodeTmp, CVC3::ExprApplyTmp, CVC3::ExprApply, CVC3::ExprString, CVC3::ExprSkolem, CVC3::ExprRational, CVC3::ExprVar, CVC3::ExprSymbol, CVC3::ExprBoundVar, CVC3::ExprClosure, CVC3::ExprTheorem, and CVC3::BVConstExpr.

Definition at line 201 of file expr_value.h.

References d_kind, and hash().

Referenced by hash().

ExprValue * CVC3::ExprValue::copy	(	ExprManager *	em,
		ExprIndex	idx
	)			const `[protected, virtual]`

Make a clean copy of itself using the given ExprManager.

Definition at line 72 of file expr_value.cpp.

References d_kind, DebugAssert, CVC3::EXPR_VALUE, ExprValue(), CVC3::ExprManager::getMM(), and getMMIndex().

Referenced by CVC3::ExprManager::newExprValue(), and rebuild().

int CVC3::ExprValue::getKind ( ) const [inline]

Get the kind of the expression.

Definition at line 234 of file expr_value.h.

References d_kind.

Referenced by CVC3::ExprClosure::operator==(), CVC3::ExprBoundVar::operator==(), CVC3::ExprSymbol::operator==(), CVC3::ExprVar::operator==(), CVC3::ExprNode::operator==(), and CVC3::ExprNodeTmp::operator==().

void* CVC3::ExprValue::operator new	(	size_t	size,
		MemoryManager *	mm
	)			`[inline]`

Overload operator new.

Reimplemented in CVC3::ExprNode, CVC3::ExprApply, CVC3::ExprString, CVC3::ExprSkolem, CVC3::ExprRational, CVC3::ExprVar, CVC3::ExprSymbol, CVC3::ExprBoundVar, CVC3::ExprClosure, CVC3::ExprTheorem, and CVC3::BVConstExpr.

Definition at line 237 of file expr_value.h.

References CVC3::MemoryManager::newData().

void CVC3::ExprValue::operator delete	(	void *	pMem,
		MemoryManager *	mm
	)			`[inline]`

Definition at line 239 of file expr_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::ExprValue::operator delete ( void * ) [inline]

Overload operator delete.

Definition at line 244 of file expr_value.h.

virtual size_t CVC3::ExprValue::getMMIndex ( ) const [inline, virtual]

Get unique memory manager ID.

Definition at line 247 of file expr_value.h.

References CVC3::EXPR_VALUE.

Referenced by copy(), CVC3::Expr::getMMIndex(), CVC3::ExprTheorem::operator==(), CVC3::ExprClosure::operator==(), CVC3::ExprApplyTmp::operator==(), CVC3::ExprApply::operator==(), CVC3::ExprBoundVar::operator==(), CVC3::ExprSymbol::operator==(), CVC3::ExprVar::operator==(), CVC3::ExprRational::operator==(), CVC3::ExprSkolem::operator==(), CVC3::ExprString::operator==(), CVC3::ExprNode::operator==(), CVC3::ExprNodeTmp::operator==(), operator==(), and CVC3::BVConstExpr::operator==().

bool CVC3::ExprValue::operator== ( const ExprValue & ev2 ) const [virtual]

Equality between any two ExprValue objects (including subclasses).

Definition at line 62 of file expr_value.cpp.

References d_kind, DebugAssert, CVC3::EXPR_VALUE, and getMMIndex().

virtual const ExprValue* CVC3::ExprValue::getExprValue ( ) const [inline, virtual]

Test whether the expression is a generic subclass.

Returns:: 0 for the core classes, and getMMIndex() value for generic subclasses (those defined in DPs)

Reimplemented in CVC3::BVConstExpr.

Definition at line 259 of file expr_value.h.

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

virtual bool CVC3::ExprValue::isString ( ) const [inline, virtual]

String expression tester.

Reimplemented in CVC3::ExprString.

Definition at line 262 of file expr_value.h.

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

virtual bool CVC3::ExprValue::isRational ( ) const [inline, virtual]

Rational number expression tester.

Reimplemented in CVC3::ExprRational.

Definition at line 264 of file expr_value.h.

virtual bool CVC3::ExprValue::isVar ( ) const [inline, virtual]

Uninterpreted constants.

Reimplemented in CVC3::ExprSkolem, CVC3::ExprVar, and CVC3::ExprBoundVar.

Definition at line 266 of file expr_value.h.

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

virtual bool CVC3::ExprValue::isApply ( ) const [inline, virtual]

Application of another expression.

Reimplemented in CVC3::ExprApplyTmp, and CVC3::ExprApply.

Definition at line 268 of file expr_value.h.

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

virtual bool CVC3::ExprValue::isSymbol ( ) const [inline, virtual]

Special named symbol.

Reimplemented in CVC3::ExprSymbol.

Definition at line 270 of file expr_value.h.

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

virtual bool CVC3::ExprValue::isClosure ( ) const [inline, virtual]

A LAMBDA-expression or a quantifier.

Reimplemented in CVC3::ExprClosure.

Definition at line 272 of file expr_value.h.

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

virtual bool CVC3::ExprValue::isTheorem ( ) const [inline, virtual]

Special Expr holding a theorem.

Reimplemented in CVC3::ExprTheorem.

Definition at line 274 of file expr_value.h.

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

virtual const std::vector<Expr>& CVC3::ExprValue::getKids ( ) const [inline, virtual]

Get kids: by default, returns a ref to an empty vector.

Reimplemented in CVC3::ExprNode, and CVC3::ExprNodeTmp.

Definition at line 277 of file expr_value.h.

References d_em, and CVC3::ExprManager::getEmptyVector().

Referenced by CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::getKids(), CVC3::ExprApplyTmp::operator==(), CVC3::ExprApply::operator==(), CVC3::ExprNode::operator==(), CVC3::ExprNodeTmp::operator==(), and CVC3::Expr::operator[]().

virtual unsigned CVC3::ExprValue::arity ( ) const [inline, virtual]

Default arity = 0.

Reimplemented in CVC3::ExprNode, and CVC3::ExprNodeTmp.

Definition at line 283 of file expr_value.h.

Referenced by CVC3::Expr::arity(), CVC3::Expr::begin(), and CVC3::Expr::end().

virtual CDO<Theorem>* CVC3::ExprValue::getSig ( ) const [inline, virtual]

Special attributes for uninterpreted functions.

Reimplemented in CVC3::ExprNode.

Definition at line 286 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getSig(), CVC3::Expr::hasSig(), and CVC3::Expr::setSig().

virtual CDO<Theorem>* CVC3::ExprValue::getRep ( ) const [inline, virtual]

Reimplemented in CVC3::ExprNode.

Definition at line 291 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getRep(), CVC3::Expr::hasRep(), and CVC3::Expr::setRep().

virtual void CVC3::ExprValue::setSig ( CDO< Theorem > * sig ) [inline, virtual]

Reimplemented in CVC3::ExprNode.

Definition at line 296 of file expr_value.h.

References DebugAssert.

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

virtual void CVC3::ExprValue::setRep ( CDO< Theorem > * rep ) [inline, virtual]

Reimplemented in CVC3::ExprNode.

Definition at line 300 of file expr_value.h.

References DebugAssert.

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

virtual const std::string& CVC3::ExprValue::getUid ( ) const [inline, virtual]

Reimplemented in CVC3::ExprBoundVar.

Definition at line 304 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getUid(), and CVC3::ExprBoundVar::operator==().

virtual const std::string& CVC3::ExprValue::getString ( ) const [inline, virtual]

Reimplemented in CVC3::ExprString.

Definition at line 310 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getString(), and CVC3::ExprString::operator==().

virtual const Rational& CVC3::ExprValue::getRational ( ) const [inline, virtual]

Reimplemented in CVC3::ExprRational.

Definition at line 316 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getRational(), and CVC3::ExprRational::operator==().

virtual const std::string& CVC3::ExprValue::getName ( ) const [inline, virtual]

Returns the string name of UCONST and BOUND_VAR expr's.

Reimplemented in CVC3::ExprVar, CVC3::ExprSymbol, and CVC3::ExprBoundVar.

Definition at line 323 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getName(), CVC3::ExprBoundVar::operator==(), CVC3::ExprSymbol::operator==(), and CVC3::ExprVar::operator==().

virtual const Expr& CVC3::ExprValue::getVar ( ) const [inline, virtual]

Returns the original Boolean variable (for BoolVarExprValue).

Definition at line 330 of file expr_value.h.

References DebugAssert.

virtual Op CVC3::ExprValue::getOp ( ) const [inline, virtual]

Get the Op from an Apply Expr.

Reimplemented in CVC3::ExprApplyTmp, and CVC3::ExprApply.

Definition at line 337 of file expr_value.h.

References DebugAssert, and CVC3::NULL_KIND.

Referenced by CVC3::Expr::getOp(), CVC3::ExprApplyTmp::operator==(), and CVC3::ExprApply::operator==().

virtual const std::vector<Expr>& CVC3::ExprValue::getVars ( ) const [inline, virtual]

Reimplemented in CVC3::ExprClosure.

Definition at line 342 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getVars(), and CVC3::ExprClosure::operator==().

virtual const Expr& CVC3::ExprValue::getBody ( ) const [inline, virtual]

Reimplemented in CVC3::ExprClosure.

Definition at line 348 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getBody(), and CVC3::ExprClosure::operator==().

virtual const Expr& CVC3::ExprValue::getExistential ( ) const [inline, virtual]

Reimplemented in CVC3::ExprSkolem.

Definition at line 354 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getExistential(), and CVC3::ExprSkolem::operator==().

virtual int CVC3::ExprValue::getBoundIndex ( ) const [inline, virtual]

Reimplemented in CVC3::ExprSkolem.

Definition at line 359 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getBoundIndex(), and CVC3::ExprSkolem::operator==().

virtual const std::vector<std::string>& CVC3::ExprValue::getFields ( ) const [inline, virtual]

Definition at line 364 of file expr_value.h.

References DebugAssert.

virtual const std::string& CVC3::ExprValue::getField ( ) const [inline, virtual]

Definition at line 369 of file expr_value.h.

References DebugAssert.

virtual int CVC3::ExprValue::getTupleIndex ( ) const [inline, virtual]

Definition at line 374 of file expr_value.h.

References DebugAssert.

virtual const Theorem& CVC3::ExprValue::getTheorem ( ) const [inline, virtual]

Reimplemented in CVC3::ExprTheorem.

Definition at line 378 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getTheorem(), and CVC3::ExprTheorem::operator==().

Friends And Related Function Documentation

friend class Expr [friend]

Definition at line 70 of file expr_value.h.

friend class Expr::iterator [friend]

Definition at line 71 of file expr_value.h.

friend class ExprManager [friend]

Definition at line 72 of file expr_value.h.

friend class ::CInterface [friend]

Definition at line 73 of file expr_value.h.

friend class ExprApply [friend]

Definition at line 74 of file expr_value.h.

Referenced by CVC3::ExprApplyTmp::copy().

friend class Theorem [friend]

Definition at line 75 of file expr_value.h.

Referenced by ~ExprValue().

Member Data Documentation

ExprIndex CVC3::ExprValue::d_index [private]

Unique expression id.

Definition at line 78 of file expr_value.h.

Referenced by CVC3::Expr::getIndex(), and setIndex().

unsigned CVC3::ExprValue::d_refcount [private]

Reference counter for garbage collection.

Definition at line 81 of file expr_value.h.

Referenced by decRefcount(), and incRefcount().

size_t CVC3::ExprValue::d_hash [private]

Cached hash value (initially 0).

Definition at line 84 of file expr_value.h.

Referenced by hash().

CDO<Theorem>* CVC3::ExprValue::d_find [private]

The find attribute (may be NULL).

Definition at line 87 of file expr_value.h.

Referenced by CVC3::Expr::getFind(), CVC3::Expr::getFindLevel(), CVC3::Expr::hasFind(), CVC3::Expr::setFind(), and ~ExprValue().

Type CVC3::ExprValue::d_type [private]

The cached type of the expression (may be Null).

Definition at line 90 of file expr_value.h.

Referenced by CVC3::Expr::getType(), CVC3::Expr::lookupType(), CVC3::ExprManager::rebuildRec(), CVC3::Expr::setType(), and ~ExprValue().

NotifyList* CVC3::ExprValue::d_notifyList [private]

Notify list may be NULL (== no such attribute).

Definition at line 99 of file expr_value.h.

Referenced by CVC3::Expr::addToNotify(), CVC3::Expr::getNotify(), and ~ExprValue().

Theorem CVC3::ExprValue::d_simpCache [private]

For caching calls to Simplify.

Definition at line 102 of file expr_value.h.

Referenced by CVC3::Expr::getSimpCache(), CVC3::Expr::setSimpCache(), and ~ExprValue().

unsigned CVC3::ExprValue::d_simpCacheTag [private]

For checking whether simplify cache is valid.

Definition at line 105 of file expr_value.h.

Referenced by CVC3::Expr::setSimpCache(), and CVC3::Expr::validSimpCache().

CDFlags CVC3::ExprValue::d_dynamicFlags [private]

context-dependent bit-vector for flags that are context-dependent

Definition at line 108 of file expr_value.h.

Referenced by CVC3::Expr::clearRewriteNormal(), CVC3::Expr::computeTransClosure(), CVC3::Expr::containsBoundVar(), CVC3::Expr::getIsAtomicFlag(), CVC3::Expr::inUserAssumption(), CVC3::Expr::isFinite(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isIntAssumption(), CVC3::Expr::isJustified(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isRewriteNormal(), CVC3::Expr::isSelected(), CVC3::Expr::isStoredPredicate(), CVC3::Expr::isTranslated(), CVC3::Expr::isUserAssumption(), CVC3::Expr::isUserRegisteredAtom(), CVC3::Expr::isValidType(), CVC3::Expr::isWellFounded(), CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::setFinite(), CVC3::Expr::setImpliedLiteral(), CVC3::Expr::setIntAssumption(), CVC3::Expr::setInUserAssumption(), CVC3::Expr::setIsAtomicFlag(), CVC3::Expr::setJustified(), CVC3::Expr::setRegisteredAtom(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTranslated(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setValidType(), CVC3::Expr::setWellFounded(), and CVC3::Expr::validIsAtomicFlag().

unsigned CVC3::ExprValue::d_flag [private]

Generic flag for marking expressions (e.g. in DAG traversal).

Definition at line 120 of file expr_value.h.

Referenced by CVC3::Expr::getFlag(), and CVC3::Expr::setFlag().

int CVC3::ExprValue::d_kind [protected]

The kind of the expression. In particular, it determines which subclass of ExprValue is used to store the expression.

Definition at line 125 of file expr_value.h.

Referenced by CVC3::ExprSymbol::computeHash(), CVC3::ExprNodeTmp::computeHash(), CVC3::ExprNode::computeHash(), computeHash(), CVC3::ExprClosure::computeHash(), CVC3::ExprClosure::copy(), CVC3::ExprSymbol::copy(), CVC3::ExprNode::copy(), CVC3::ExprNodeTmp::copy(), copy(), CVC3::ExprApplyTmp::ExprApplyTmp(), getKind(), CVC3::Expr::getKind(), CVC3::Expr::isNull(), CVC3::ExprNode::operator==(), CVC3::ExprNodeTmp::operator==(), and operator==().

std::hash< char * > CVC3::ExprValue::s_charHash [static, protected]

Set Expr simplified to obtain this expr.

Definition at line 174 of file expr_value.h.

Referenced by CVC3::ExprBoundVar::computeHash(), CVC3::ExprSymbol::computeHash(), CVC3::ExprVar::computeHash(), CVC3::ExprRational::hash(), and CVC3::ExprString::hash().

std::hash< long int > CVC3::ExprValue::s_intHash [static, protected]

Definition at line 175 of file expr_value.h.

Referenced by CVC3::ExprSymbol::computeHash(), hash(), and pointerHash().

The documentation for this class was generated from the following files:

Generated on Tue Jul 3 14:36:32 2007 for CVC3 by

1.5.1