CVC3::ExprRational Class Reference

#include <expr_value.h>

Inherits CVC3::ExprValue.

Collaboration diagram for CVC3::ExprRational:

List of all members.

Public Member Functions

• ExprRational (ExprManager *em, const Rational &r, ExprIndex idx=0)
• virtual ~ExprRational ()
• 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 operator== (const ExprValue &ev2) const

  Equality between any two ExprValue objects (including subclasses)
  

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

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

• virtual bool isRational () const

  Rational number expression tester.
  

Private Member Functions

• virtual const Rational & getRational () const
• virtual size_t getMMIndex () const

  Get unique memory manager ID.
  

Static Private Member Functions

• static size_t hash (const Rational &r)

Private Attributes

• Rational d_r

Friends

• class Expr
• class ExprManager

---

Detailed Description

Definition at line 741 of file expr_value.h.

---

Constructor & Destructor Documentation

CVC3::ExprRational::ExprRational	(	ExprManager *	em,
		const Rational &	r,
		ExprIndex	idx = 0
	)		[inline]

Definition at line 767 of file expr_value.h.

virtual CVC3::ExprRational::~ExprRational

(

)

[inline, virtual]

Definition at line 770 of file expr_value.h.

---

Member Function Documentation

virtual const Rational& CVC3::ExprRational::getRational

(

)

const [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 747 of file expr_value.h.

References d_r.

static size_t CVC3::ExprRational::hash

(

const Rational &

r

)

[inline, static, private]

Definition at line 750 of file expr_value.h.

References CVC3::ExprValue::s_charHash, and CVC3::Rational::toString().

virtual size_t CVC3::ExprRational::getMMIndex

(

)

const [inline, private, virtual]

Get unique memory manager ID.

Reimplemented from CVC3::ExprValue.

Definition at line 755 of file expr_value.h.

References CVC3::EXPR_RATIONAL.

virtual size_t CVC3::ExprRational::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 759 of file expr_value.h.

References d_r, and CVC3::ExprValue::hash().

bool CVC3::ExprRational::operator==

(

const ExprValue &

ev2

)

const [protected, virtual]

Equality between any two ExprValue objects (including subclasses)

Reimplemented from CVC3::ExprValue.

Definition at line 174 of file expr_value.cpp.

References CVC3::ExprValue::getMMIndex(), and CVC3::ExprValue::getRational().

ExprValue * CVC3::ExprRational::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 181 of file expr_value.cpp.

References CVC3::ExprManager::getMM().

virtual bool CVC3::ExprRational::isRational

(

)

const [inline, protected, virtual]

Rational number expression tester.

Reimplemented from CVC3::ExprValue.

Definition at line 763 of file expr_value.h.

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

Overload operator new.

Reimplemented from CVC3::ExprValue.

Definition at line 772 of file expr_value.h.

References CVC3::MemoryManager::newData().

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

Reimplemented from CVC3::ExprValue.

Definition at line 775 of file expr_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::ExprRational::operator delete

(

void *

)

[inline]

Overload operator delete.

Reimplemented from CVC3::ExprValue.

Definition at line 778 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 742 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 743 of file expr_value.h.

---

Member Data Documentation

Rational CVC3::ExprRational::d_r [private]

Definition at line 745 of file expr_value.h.

Referenced by computeHash(), and getRational().

---

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

• expr_value.h
• expr_value.cpp