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 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

  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.
  

• 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

  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_size

  Size of dag rooted at this expression.
  

• 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
• 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 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_eqNext, 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 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::Theorem::operator=(), 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::Theorem::operator=(), CVC3::Expr::operator=(), 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 155 of file expr_value.h.

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

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.

Referenced by hash().

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 pointerHash(), PRIME, and s_intHash.

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::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 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 d_kind, DebugAssert, CVC3::EXPR_VALUE, ExprValue(), CVC3::ExprManager::getMM(), and getMMIndex().

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.

Referenced by copy(), CVC3::Expr::getMMIndex(), 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).

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

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

friend class Theorem [friend]

Definition at line 75 of file expr_value.h.

Referenced by ~ExprValue().

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(), CVC3::Expr::setFind(), and ~ExprValue().

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(), CVC3::Expr::setEqNext(), and ~ExprValue().

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(), CVC3::Expr::setType(), and ~ExprValue().

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

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

Definition at line 103 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 106 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 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]

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::ExprClosure::computeHash(), CVC3::ExprClosure::copy(), CVC3::ExprSymbol::copy(), CVC3::ExprNode::copy(), CVC3::ExprNodeTmp::copy(), copy(), CVC3::ExprApplyTmp::ExprApplyTmp(), CVC3::Expr::getKind(), CVC3::Expr::isNull(), CVC3::ExprNode::operator==(), CVC3::ExprNodeTmp::operator==(), and operator==().

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

Our expr. manager.

Definition at line 132 of file expr_value.h.

Referenced by CVC3::Theorem::clearAllFlags(), CVC3::ExprClosure::copy(), CVC3::ExprApplyTmp::copy(), CVC3::ExprApply::copy(), CVC3::ExprSkolem::copy(), CVC3::ExprNode::copy(), CVC3::ExprNodeTmp::copy(), CVC3::Theorem::getCachedValue(), CVC3::Expr::getEM(), CVC3::Theorem::getExpandFlag(), CVC3::Theorem::getLitFlag(), CVC3::Expr::hasLastIndex(), CVC3::Theorem::isFlagged(), CVC3::Theorem::setCachedValue(), CVC3::Theorem::setExpandFlag(), CVC3::Theorem::setFlag(), CVC3::Theorem::setLitFlag(), CVC3::Theorem::withAssumptions(), CVC3::Theorem::withProof(), and CVC3::Expr::~Expr().

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

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(), and hash().

---

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

• expr_value.h
• expr_value.cpp

---