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

#include <expr_value.h>

Inherited by CVC3::BVConstExpr, CVC3::ExprBoundVar, CVC3::ExprClosure, CVC3::ExprNode, CVC3::ExprNodeTmp, CVC3::ExprRational, CVC3::ExprSkolem, CVC3::ExprString, CVC3::ExprSymbol, and CVC3::ExprVar.

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 void setTriggers (const std::vector< std::vector< Expr > > &triggers)
virtual const std::vector
< std::vector< Expr > > & getTriggers () 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 Unsigned computeSize () const
Non-caching size function which actually computes the size.
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)
static Unsigned sizeWithChildren (const std::vector< Expr > &kids)

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
Return child with greatest height.
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.
Unsigned getSize () const
Return DAG-size of Expr.

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)
CDO< Theorem > * d_eqNext
Equality between this term and next term in ring of all terms in the equivalence class.
Type d_type
The cached type of the expression (may be Null)
NotifyList * d_notifyList
The cached TCC of the expression (may be Null)
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_size
Size of dag rooted at this expression.
unsigned d_flag
Which child has the largest height.

Friends

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

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

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

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

Destructor.

Definition at line 41 of file expr_value.cpp.

Member Function Documentation

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

Set the ExprIndex.

Definition at line 139 of file expr_value.h.

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

Increment reference counter.

Definition at line 142 of file expr_value.h.

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

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

Decrement reference counter.

Definition at line 145 of file expr_value.h.

References FatalAssert, and IF_DEBUG.

Referenced by CVC3::Expr::operator=().

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

Caching hash function.

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

Definition at line 155 of file expr_value.h.

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

Unsigned CVC3::ExprValue::getSize ( ) const [inline, private]

Return DAG-size of Expr.

Definition at line 162 of file expr_value.h.

Referenced by CVC3::ExprClosure::computeSize(), and CVC3::Expr::getSize().

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

Definition at line 185 of file expr_value.h.

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

Definition at line 310 of file expr_value.cpp.

References PRIME.

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

Definition at line 189 of file expr_value.h.

Unsigned CVC3::ExprValue::sizeWithChildren ( const std::vector< Expr > & kids ) [static, protected]

Definition at line 322 of file expr_value.cpp.

Referenced by CVC3::ExprNodeTmp::computeSize(), and CVC3::ExprNode::computeSize().

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

Return the memory manager (for the benefit of subclasses)

Definition at line 195 of file expr_value.h.

References DebugAssert.

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

Make a clean copy of itself using the given ExprManager.

Definition at line 201 of file expr_value.h.

Referenced by 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 205 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, and CVC3::BVConstExpr.

Definition at line 212 of file expr_value.h.

virtual Unsigned CVC3::ExprValue::computeSize ( ) const [inline, protected, virtual]

Non-caching size function which actually computes the size.

This is the method that all subclasses should implement

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

Definition at line 216 of file expr_value.h.

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

Make a clean copy of itself using the given ExprManager.

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

Definition at line 78 of file expr_value.cpp.

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

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

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

Get the kind of the expression.

Definition at line 250 of file expr_value.h.

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, and CVC3::BVConstExpr.

Definition at line 253 of file expr_value.h.

References CVC3::MemoryManager::newData().

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

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

Definition at line 255 of file expr_value.h.

References CVC3::MemoryManager::deleteData().

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

Overload operator delete.

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

Definition at line 260 of file expr_value.h.

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

Get unique memory manager ID.

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

Definition at line 263 of file expr_value.h.

References CVC3::EXPR_VALUE.

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

Equality between any two ExprValue objects (including subclasses)

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

Definition at line 68 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 275 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 278 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 280 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 282 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 284 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 286 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 288 of file expr_value.h.

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

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

Special Expr holding a theorem.

Definition at line 290 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 293 of file expr_value.h.

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 299 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 302 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 307 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 312 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 316 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 320 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 326 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 332 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 339 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 346 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 353 of file expr_value.h.

References DebugAssert, and 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 358 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 364 of file expr_value.h.

References DebugAssert.

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

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

Reimplemented in CVC3::ExprClosure.

Definition at line 370 of file expr_value.h.

References DebugAssert.

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

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

Reimplemented in CVC3::ExprClosure.

Definition at line 374 of file expr_value.h.

References DebugAssert.

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

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

Reimplemented in CVC3::ExprSkolem.

Definition at line 381 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 386 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 391 of file expr_value.h.

References DebugAssert.

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

Definition at line 396 of file expr_value.h.

References DebugAssert.

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

Definition at line 401 of file expr_value.h.

References DebugAssert.

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

Definition at line 405 of file expr_value.h.

References DebugAssert.

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

Friends And Related Function Documentation

friend class Expr [friend]

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

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]

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

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.

friend class Theorem [friend]

Definition at line 75 of file expr_value.h.

friend class ExprClosure [friend]

Definition at line 76 of file expr_value.h.

Member Data Documentation

ExprIndex CVC3::ExprValue::d_index [private]

Unique expression id.

Definition at line 79 of file expr_value.h.

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

unsigned CVC3::ExprValue::d_refcount [private]

Reference counter for garbage collection.

Definition at line 82 of file expr_value.h.

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

size_t CVC3::ExprValue::d_hash [private]

Cached hash value (initially 0)

Definition at line 85 of file expr_value.h.

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

The find attribute (may be NULL)

Definition at line 88 of file expr_value.h.

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

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

Equality between this term and next term in ring of all terms in the equivalence class.

Definition at line 91 of file expr_value.h.

Referenced by CVC3::Expr::getEqNext(), and CVC3::Expr::setEqNext().

Type CVC3::ExprValue::d_type [private]

The cached type of the expression (may be Null)

Definition at line 94 of file expr_value.h.

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

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

The cached TCC of the expression (may be Null)

Subtyping predicate for the expression and all subexpressions Notify list may be NULL (== no such attribute)

Definition at line 103 of file expr_value.h.

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

Theorem CVC3::ExprValue::d_simpCache [private]

For caching calls to Simplify.

Definition at line 106 of file expr_value.h.

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

unsigned CVC3::ExprValue::d_simpCacheTag [private]

For checking whether simplify cache is valid.

Definition at line 109 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 112 of file expr_value.h.

Referenced by CVC3::Expr::clearRewriteNormal(), CVC3::Expr::computeTransClosure(), CVC3::Expr::containsBoundVar(), CVC3::Expr::getIsAtomicFlag(), CVC3::Expr::getTerminalsConstFlag(), 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::notArrayNormalized(), 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::setNotArrayNormalized(), CVC3::Expr::setRegisteredAtom(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTerminalsConstFlag(), CVC3::Expr::setTranslated(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setUsesCC(), CVC3::Expr::setValidType(), CVC3::Expr::setWellFounded(), CVC3::Expr::usesCC(), CVC3::Expr::validIsAtomicFlag(), and CVC3::Expr::validTerminalsConstFlag().

Unsigned CVC3::ExprValue::d_size [private]

Size of dag rooted at this expression.

Definition at line 115 of file expr_value.h.

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

unsigned CVC3::ExprValue::d_flag [private]

Which child has the largest height.

Most distant expression we were simplified *from* Generic flag for marking expressions (e.g. in DAG traversal)

Definition at line 124 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 129 of file expr_value.h.

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

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

Our expr. manager.

Definition at line 132 of file expr_value.h.

Referenced by CVC3::Expr::getEM(), CVC3::Expr::hasLastIndex(), and CVC3::Expr::~Expr().

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

Return child with greatest height.

Get Expr simplified to obtain this expr Set Expr simplified to obtain this expr

Definition at line 182 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 183 of file expr_value.h.

Referenced by CVC3::ExprSymbol::computeHash().

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

CVC3::ExprValue Class Reference

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Static Protected Attributes

Private Member Functions

Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation