CVCL::ExprValue Class Reference

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

#include <expr_value.h>

Inheritance diagram for CVCL::ExprValue:

[legend]Collaboration diagram for CVCL::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 *)
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 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 & ExprValue::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

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

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

Static Protected Attributes

static std::hash< char * > s_charHash
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.
int getHeight () const
Return height of Expr.
int getHighestKid () const
Return child with greatest height.
const Expr & getSimpFrom () const
Get Expr simplified to obtain this expr.
void setSimpFrom (const Expr &simpFrom)
Set Expr simplified to obtain this expr.

Private Attributes

ExprIndex d_index
Unique expression id.
int d_refcount
Reference counter for garbage collection.
unsigned d_flag
Generic flag for marking expressions (e.g. in DAG traversal).
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).
Expr d_tcc
The cached TCC of the expression (may be Null).
Theorem d_subtypePred
Subtyping predicate for the expression and all subexpressions.
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-dependend
int d_height
Height of this expression.
int d_highestKid
Which child has the largest height.
Expr d_simpFrom
Most distant expression we were simplified *from*.

Friends

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

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 77 of file expr_value.h.

Constructor & Destructor Documentation

CVCL::ExprValue::ExprValue ( ExprManager * em,

int kind,

ExprIndex idx = 0

) [inline]

Constructor.

Definition at line 215 of file expr_value.h.
References CVCL::APPLY, CVCL::int2string(), and CVCL::ExprManager::isKindRegistered().
Referenced by copy().

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

Destructor.

Definition at line 49 of file expr_value.cpp.
References d_find, d_notifyList, d_simpCache, d_simpFrom, d_subtypePred, d_tcc, d_type, and Expr.

Member Function Documentation

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

Set the ExprIndex.

Definition at line 142 of file expr_value.h.
References d_index.

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

Increment reference counter.

Definition at line 145 of file expr_value.h.
References d_refcount.
Referenced by CVCL::Expr::Expr(), and CVCL::Expr::operator=().

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

Decrement reference counter.

Definition at line 148 of file expr_value.h.
References d_em, d_refcount, and CVCL::ExprManager::gc().
Referenced by CVCL::Expr::operator=(), and CVCL::Expr::~Expr().

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

Caching hash function.
Do NOT implement it in subclasses! Implement computeHash() instead.
Definition at line 158 of file expr_value.h.
References computeHash(), and d_hash.
Referenced by computeHash(), and CVCL::ExprManager::hash().

int CVCL::ExprValue::getHeight ( ) const [inline, private]

Return height of Expr.

Definition at line 165 of file expr_value.h.
References d_height.
Referenced by CVCL::Expr::getHeight().

int CVCL::ExprValue::getHighestKid ( ) const [inline, private]

Return child with greatest height.

Definition at line 168 of file expr_value.h.
References d_highestKid.
Referenced by CVCL::Expr::getHighestKid().

const Expr& CVCL::ExprValue::getSimpFrom ( ) const [inline, private]

Get Expr simplified to obtain this expr.

Definition at line 171 of file expr_value.h.
References d_simpFrom.
Referenced by CVCL::Expr::getSimpFrom(), and CVCL::Expr::hasSimpFrom().

void CVCL::ExprValue::setSimpFrom ( const Expr & simpFrom ) [inline, private]

Set Expr simplified to obtain this expr.

Definition at line 174 of file expr_value.h.
References d_simpFrom.
Referenced by CVCL::Expr::setSimpFrom().

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

Definition at line 184 of file expr_value.h.
References s_intHash.
Referenced by hash().

size_t CVCL::ExprValue::hash ( const int kind,

const std::vector< Expr > & kids

) [static, protected]

Definition at line 254 of file expr_value.cpp.
References pointerHash(), and s_intHash.

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

Definition at line 188 of file expr_value.h.
References s_intHash.

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

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

Definition at line 191 of file expr_value.h.
References d_em, and CVCL::ExprManager::getMM().

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

Make a clean copy of itself using the given ExprManager.

Definition at line 197 of file expr_value.h.
References copy().
Referenced by CVCL::ExprClosure::copy(), CVCL::ExprApply::copy(), CVCL::ExprSkolem::copy(), CVCL::ExprNode::copy(), and CVCL::ExprManager::rebuildRec().

Expr CVCL::ExprValue::rebuild ( Expr e,

ExprManager * em

) const [inline, protected]

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

Definition at line 201 of file expr_value.h.
References CVCL::ExprManager::rebuildRec().

virtual size_t CVCL::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 CVCL::ExprNode, CVCL::ExprApply, CVCL::ExprString, CVCL::ExprSkolem, CVCL::ExprRational, CVCL::ExprVar, CVCL::ExprSymbol, CVCL::ExprBoundVar, CVCL::ExprClosure, and CVCL::BVConstExpr.
Definition at line 208 of file expr_value.h.
References d_kind, and hash().
Referenced by hash().

ExprValue * CVCL::ExprValue::copy ( ExprManager * em,

ExprIndex idx

) const [protected, virtual]

Make a clean copy of itself using the given ExprManager.

Reimplemented in CVCL::ExprNode, CVCL::ExprApply, CVCL::ExprString, CVCL::ExprSkolem, CVCL::ExprRational, CVCL::ExprVar, CVCL::ExprSymbol, CVCL::ExprBoundVar, CVCL::ExprClosure, and CVCL::BVConstExpr.
Definition at line 81 of file expr_value.cpp.
References d_kind, CVCL::EXPR_VALUE, ExprValue(), CVCL::ExprManager::getMM(), and getMMIndex().
Referenced by CVCL::ExprManager::newExprValue(), and rebuild().

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

Get the kind of the expression.

Definition at line 233 of file expr_value.h.
References d_kind.
Referenced by CVCL::ExprClosure::operator==(), CVCL::ExprBoundVar::operator==(), CVCL::ExprSymbol::operator==(), CVCL::ExprVar::operator==(), and CVCL::ExprNode::operator==().

void* CVCL::ExprValue::operator new ( size_t size,

MemoryManager * mm

) [inline]

Overload operator new.

Reimplemented in CVCL::ExprNode, CVCL::ExprApply, CVCL::ExprString, CVCL::ExprSkolem, CVCL::ExprRational, CVCL::ExprVar, CVCL::ExprSymbol, CVCL::ExprBoundVar, CVCL::ExprClosure, and CVCL::BVConstExpr.
Definition at line 236 of file expr_value.h.
References CVCL::MemoryManager::newData().

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

Overload operator delete.

Reimplemented in CVCL::ExprNode, CVCL::ExprApply, CVCL::ExprString, CVCL::ExprSkolem, CVCL::ExprRational, CVCL::ExprVar, CVCL::ExprSymbol, CVCL::ExprBoundVar, CVCL::ExprClosure, and CVCL::BVConstExpr.
Definition at line 240 of file expr_value.h.

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

Equality between any two ExprValue objects (including subclasses).

Reimplemented in CVCL::ExprNode, CVCL::ExprApply, CVCL::ExprString, CVCL::ExprSkolem, CVCL::ExprRational, CVCL::ExprVar, CVCL::ExprSymbol, CVCL::ExprBoundVar, CVCL::ExprClosure, and CVCL::BVConstExpr.
Definition at line 71 of file expr_value.cpp.
References d_kind, CVCL::EXPR_VALUE, and getMMIndex().

virtual const ExprValue* CVCL::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 CVCL::BVConstExpr.
Definition at line 255 of file expr_value.h.
Referenced by CVCL::Expr::getExprValue().

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

String expression tester.

Reimplemented in CVCL::ExprString.
Definition at line 258 of file expr_value.h.
Referenced by CVCL::Expr::isString().

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

Rational number expression tester.

Reimplemented in CVCL::ExprRational.
Definition at line 260 of file expr_value.h.

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

Uninterpreted constants.

Reimplemented in CVCL::ExprSkolem, CVCL::ExprVar, and CVCL::ExprBoundVar.
Definition at line 262 of file expr_value.h.
Referenced by CVCL::Expr::isVar().

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

Application of another expression.

Reimplemented in CVCL::ExprApply.
Definition at line 264 of file expr_value.h.
Referenced by CVCL::Expr::isApply().

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

Special named symbol.

Reimplemented in CVCL::ExprSymbol.
Definition at line 266 of file expr_value.h.
Referenced by CVCL::Expr::isSymbol().

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

A LAMBDA-expression or a quantifier.

Reimplemented in CVCL::ExprClosure.
Definition at line 268 of file expr_value.h.
Referenced by CVCL::Expr::isClosure().

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

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

Reimplemented in CVCL::ExprNode.
Definition at line 271 of file expr_value.h.
References d_em, and CVCL::ExprManager::getEmptyVector().
Referenced by CVCL::Expr::getKids(), CVCL::ExprManager::installExprValue(), CVCL::ExprApply::operator==(), CVCL::ExprNode::operator==(), and CVCL::Expr::operator[]().

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

Default arity = 0.

Reimplemented in CVCL::ExprNode.
Definition at line 277 of file expr_value.h.
Referenced by CVCL::Expr::arity(), and CVCL::ExprManager::installExprValue().

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

Special attributes for uninterpreted functions.

Reimplemented in CVCL::ExprNode.
Definition at line 280 of file expr_value.h.
Referenced by CVCL::Expr::getSig(), CVCL::Expr::hasSig(), and CVCL::Expr::setSig().

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

Reimplemented in CVCL::ExprNode.
Definition at line 285 of file expr_value.h.
Referenced by CVCL::Expr::getRep(), CVCL::Expr::hasRep(), and CVCL::Expr::setRep().

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

Reimplemented in CVCL::ExprNode.
Definition at line 290 of file expr_value.h.
Referenced by CVCL::Expr::setSig().

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

Reimplemented in CVCL::ExprNode.
Definition at line 294 of file expr_value.h.
Referenced by CVCL::Expr::setRep().

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

Reimplemented in CVCL::ExprBoundVar.
Definition at line 298 of file expr_value.h.
Referenced by CVCL::Expr::getUid(), and CVCL::ExprBoundVar::operator==().

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

Reimplemented in CVCL::ExprString.
Definition at line 304 of file expr_value.h.
Referenced by CVCL::Expr::getString(), and CVCL::ExprString::operator==().

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

Reimplemented in CVCL::ExprRational.
Definition at line 310 of file expr_value.h.
Referenced by CVCL::Expr::getRational(), and CVCL::ExprRational::operator==().

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

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

Definition at line 317 of file expr_value.h.
References ExprValue::getName().
Referenced by ExprValue::getName().

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

Returns the original Boolean variable (for BoolVarExprValue).

Definition at line 324 of file expr_value.h.

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

Get the Op from an Apply Expr.

Reimplemented in CVCL::ExprApply.
Definition at line 331 of file expr_value.h.
References CVCL::NULL_KIND.
Referenced by CVCL::Expr::getOp(), and CVCL::ExprApply::operator==().

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

Reimplemented in CVCL::ExprClosure.
Definition at line 336 of file expr_value.h.
Referenced by CVCL::Expr::getVars(), and CVCL::ExprClosure::operator==().

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

Reimplemented in CVCL::ExprClosure.
Definition at line 342 of file expr_value.h.
Referenced by CVCL::Expr::getBody(), and CVCL::ExprClosure::operator==().

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

Reimplemented in CVCL::ExprSkolem.
Definition at line 348 of file expr_value.h.
Referenced by CVCL::Expr::getExistential(), and CVCL::ExprSkolem::operator==().

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

Reimplemented in CVCL::ExprSkolem.
Definition at line 353 of file expr_value.h.
Referenced by CVCL::Expr::getBoundIndex(), and CVCL::ExprSkolem::operator==().

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

Definition at line 358 of file expr_value.h.

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

Definition at line 363 of file expr_value.h.

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

Definition at line 368 of file expr_value.h.

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented in CVCL::ExprNode, CVCL::ExprApply, CVCL::ExprString, CVCL::ExprSkolem, CVCL::ExprRational, CVCL::ExprVar, CVCL::ExprSymbol, CVCL::ExprBoundVar, and CVCL::ExprClosure.
Definition at line 78 of file expr_value.h.
Referenced by ~ExprValue().

friend class Expr::iterator [friend]

Definition at line 79 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented in CVCL::ExprNode, CVCL::ExprApply, CVCL::ExprString, CVCL::ExprSkolem, CVCL::ExprRational, CVCL::ExprVar, CVCL::ExprSymbol, CVCL::ExprBoundVar, and CVCL::ExprClosure.
Definition at line 80 of file expr_value.h.

friend class ::CInterface [friend]

Definition at line 81 of file expr_value.h.

friend class ExprApply [friend]

Definition at line 82 of file expr_value.h.

Member Data Documentation

ExprIndex CVCL::ExprValue::d_index [private]

Unique expression id.

Definition at line 85 of file expr_value.h.
Referenced by CVCL::Expr::getIndex(), and setIndex().

int CVCL::ExprValue::d_refcount [private]

Reference counter for garbage collection.

Definition at line 88 of file expr_value.h.
Referenced by decRefcount(), and incRefcount().

unsigned CVCL::ExprValue::d_flag [private]

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

Definition at line 91 of file expr_value.h.
Referenced by CVCL::Expr::getFlag(), and CVCL::Expr::setFlag().

size_t CVCL::ExprValue::d_hash [private]

Cached hash value (initially 0).

Definition at line 94 of file expr_value.h.
Referenced by hash().

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

The find attribute (may be NULL).

Definition at line 97 of file expr_value.h.
Referenced by CVCL::Expr::getFind(), CVCL::Expr::hasFind(), CVCL::Expr::setFind(), and ~ExprValue().

Type CVCL::ExprValue::d_type [private]

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

Definition at line 100 of file expr_value.h.
Referenced by CVCL::Expr::getType(), CVCL::Expr::lookupType(), CVCL::ExprManager::rebuildRec(), CVCL::Expr::setType(), and ~ExprValue().

Expr CVCL::ExprValue::d_tcc [private]

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

Definition at line 103 of file expr_value.h.
Referenced by CVCL::Expr::lookupTCC(), CVCL::Expr::setTCC(), and ~ExprValue().

Theorem CVCL::ExprValue::d_subtypePred [private]

Subtyping predicate for the expression and all subexpressions.

Definition at line 106 of file expr_value.h.
Referenced by CVCL::Expr::lookupSubtypePred(), CVCL::Expr::setSubtypePred(), and ~ExprValue().

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

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

Definition at line 109 of file expr_value.h.
Referenced by CVCL::Expr::addToNotify(), CVCL::Expr::getNotify(), and ~ExprValue().

Theorem CVCL::ExprValue::d_simpCache [private]

For caching calls to Simplify.

Definition at line 112 of file expr_value.h.
Referenced by CVCL::Expr::getSimpCache(), CVCL::Expr::setSimpCache(), and ~ExprValue().

unsigned CVCL::ExprValue::d_simpCacheTag [private]

For checking whether simplify cache is valid.

Definition at line 115 of file expr_value.h.
Referenced by CVCL::Expr::setSimpCache(), and CVCL::Expr::validSimpCache().

CDFlags CVCL::ExprValue::d_dynamicFlags [private]

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

Definition at line 118 of file expr_value.h.
Referenced by CVCL::Expr::clearRewriteNormal(), CVCL::Expr::computeTransClosure(), CVCL::Expr::getIsAtomicFlag(), CVCL::Expr::isFinite(), CVCL::Expr::isImpliedLiteral(), CVCL::Expr::isIntAssumption(), CVCL::Expr::isJustified(), CVCL::Expr::isRewriteNormal(), CVCL::Expr::isSelected(), CVCL::Expr::isTranslated(), CVCL::Expr::isUserAssumption(), CVCL::Expr::isUserRegisteredAtom(), CVCL::Expr::isValidType(), CVCL::Expr::isWellFounded(), CVCL::Expr::setComputeTransClosure(), CVCL::Expr::setFinite(), CVCL::Expr::setImpliedLiteral(), CVCL::Expr::setIntAssumption(), CVCL::Expr::setIsAtomicFlag(), CVCL::Expr::setJustified(), CVCL::Expr::setRewriteNormal(), CVCL::Expr::setSelected(), CVCL::Expr::setTranslated(), CVCL::Expr::setUserAssumption(), CVCL::Expr::setUserRegisteredAtom(), CVCL::Expr::setValidType(), CVCL::Expr::setWellFounded(), and CVCL::Expr::validIsAtomicFlag().

int CVCL::ExprValue::d_height [private]

Height of this expression.

Definition at line 121 of file expr_value.h.
Referenced by getHeight(), and CVCL::ExprManager::installExprValue().

int CVCL::ExprValue::d_highestKid [private]

Which child has the largest height.

Definition at line 124 of file expr_value.h.
Referenced by getHighestKid(), and CVCL::ExprManager::installExprValue().

Expr CVCL::ExprValue::d_simpFrom [private]

Most distant expression we were simplified *from*.

Definition at line 127 of file expr_value.h.
Referenced by getSimpFrom(), setSimpFrom(), and ~ExprValue().

ExprManager* CVCL::ExprValue::d_em [protected]

Our expr. manager.

Definition at line 131 of file expr_value.h.
Referenced by CVCL::ExprClosure::copy(), CVCL::ExprApply::copy(), CVCL::ExprSkolem::copy(), CVCL::ExprNode::copy(), decRefcount(), CVCL::Expr::getEM(), getKids(), getMM(), CVCL::Expr::hasLastIndex(), and CVCL::Expr::~Expr().

int CVCL::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 135 of file expr_value.h.
Referenced by computeHash(), CVCL::ExprClosure::computeHash(), CVCL::ExprClosure::copy(), CVCL::ExprSymbol::copy(), CVCL::ExprNode::copy(), copy(), getKind(), CVCL::Expr::getKind(), CVCL::ExprManager::installExprValue(), CVCL::Expr::isNull(), CVCL::ExprNode::operator==(), and operator==().

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

Definition at line 181 of file expr_value.h.

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

Definition at line 182 of file expr_value.h.
Referenced by hash(), and pointerHash().

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

Generated on Thu Apr 13 16:57:43 2006 for CVC Lite by

1.4.4