CVC3::ExprBoundVar Class Reference

#include <expr_value.h>

Inheritance diagram for CVC3::ExprBoundVar:

[legend]Collaboration diagram for CVC3::ExprBoundVar:

[legend]List of all members.

Public Member Functions

• ExprBoundVar (ExprManager *em, const std::string &name, const std::string &uid, ExprIndex idx=0)
• virtual ~ExprBoundVar ()
• virtual bool operator== (const ExprValue &ev2) const

  Equality between any two ExprValue objects (including subclasses).
  

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

Protected Member Functions

• virtual size_t computeHash () const

  Non-caching hash function which actually computes the hash.
  

• virtual bool isVar () const

  Uninterpreted constants.
  

• virtual ExprValue * copy (ExprManager *em, ExprIndex idx=0) const

  Make a clean copy of itself using the given memory manager.
  

Private Member Functions

• virtual const std::string & getName () const

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

• virtual const std::string & getUid () const
• virtual size_t getMMIndex () const

  Get unique memory manager ID.
  

Private Attributes

• std::string d_name
• std::string d_uid

Friends

• class Expr
• class ExprManager

---

Detailed Description

Definition at line 822 of file expr_value.h.

---

Constructor & Destructor Documentation

CVC3::ExprBoundVar::ExprBoundVar	(	ExprManager *	em,
		const std::string &	name,
		const std::string &	uid,
		ExprIndex	idx = 0
	)			[inline]

Definition at line 845 of file expr_value.h.

Referenced by copy().

virtual CVC3::ExprBoundVar::~ExprBoundVar

(

)

[inline, virtual]

Definition at line 849 of file expr_value.h.

---

Member Function Documentation

virtual const std::string& CVC3::ExprBoundVar::getName

(

)

const [inline, private, virtual]

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

Reimplemented from CVC3::ExprValue.

Definition at line 829 of file expr_value.h.

References d_name.

Referenced by operator==().

virtual const std::string& CVC3::ExprBoundVar::getUid

(

)

const [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 830 of file expr_value.h.

References d_uid.

Referenced by operator==().

virtual size_t CVC3::ExprBoundVar::getMMIndex

(

)

const [inline, private, virtual]

Get unique memory manager ID.

Reimplemented from CVC3::ExprValue.

Definition at line 833 of file expr_value.h.

References CVC3::EXPR_BOUND_VAR.

Referenced by copy(), and operator==().

virtual size_t CVC3::ExprBoundVar::computeHash

(

)

const [inline, protected, virtual]

Non-caching hash function which actually computes the hash.

This is the method that all subclasses should implement

Reimplemented from CVC3::ExprValue.

Definition at line 836 of file expr_value.h.

References d_name, d_uid, PRIME, and CVC3::ExprValue::s_charHash.

virtual bool CVC3::ExprBoundVar::isVar

(

)

const [inline, protected, virtual]

Uninterpreted constants.

Reimplemented from CVC3::ExprValue.

Definition at line 839 of file expr_value.h.

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

Make a clean copy of itself using the given memory manager.

Reimplemented from CVC3::ExprValue.

Definition at line 212 of file expr_value.cpp.

References d_name, d_uid, ExprBoundVar(), CVC3::ExprManager::getMM(), and getMMIndex().

bool CVC3::ExprBoundVar::operator==

(

const ExprValue &

ev2

)

const [virtual]

Equality between any two ExprValue objects (including subclasses).

Reimplemented from CVC3::ExprValue.

Definition at line 204 of file expr_value.cpp.

References CVC3::ExprValue::getKind(), CVC3::ExprValue::getMMIndex(), getMMIndex(), CVC3::ExprValue::getName(), getName(), CVC3::ExprValue::getUid(), and getUid().

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

Overload operator new.

Reimplemented from CVC3::ExprValue.

Definition at line 853 of file expr_value.h.

References CVC3::MemoryManager::newData().

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

Reimplemented from CVC3::ExprValue.

Definition at line 856 of file expr_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::ExprBoundVar::operator delete

(

void *

)

[inline]

Overload operator delete.

Reimplemented from CVC3::ExprValue.

Definition at line 859 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 823 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 824 of file expr_value.h.

---

Member Data Documentation

std::string CVC3::ExprBoundVar::d_name [private]

Definition at line 826 of file expr_value.h.

Referenced by computeHash(), copy(), and getName().

std::string CVC3::ExprBoundVar::d_uid [private]

Definition at line 827 of file expr_value.h.

Referenced by computeHash(), copy(), and getUid().

---

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

• expr_value.h
• expr_value.cpp

---