CVC3::ExprApply Class Reference

#include <expr_value.h>

Inherits CVC3::ExprNode.

Collaboration diagram for CVC3::ExprApply:

List of all members.

Public Member Functions

• ExprApply (ExprManager *em, const Op &op, ExprIndex idx=0)
• ExprApply (ExprManager *em, const Op &op, const std::vector< Expr > &kids, ExprIndex idx=0)
• virtual ~ExprApply ()
• bool operator== (const ExprValue &ev2) const

  Compare with another ExprValue.
  

• 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

• size_t getMMIndex () const

  Tell ExprManager who we are.
  

• size_t computeHash () const

  Use our static hash() for the member method.
  

• Op getOp () const

  Get the Op from an Apply Expr.
  

• bool isApply () const

  Application of another expression.
  

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

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

Private Attributes

• Expr d_opExpr

Friends

• class Expr
• class ExprManager

---

Detailed Description

Definition at line 560 of file expr_value.h.

---

Constructor & Destructor Documentation

CVC3::ExprApply::ExprApply	(	ExprManager *	em,
		const Op &	op,
		ExprIndex	idx = 0
	)		[inline]

Definition at line 576 of file expr_value.h.

References APPLY, DebugAssert, CVC3::Op::getExpr(), and CVC3::Expr::isNull().

CVC3::ExprApply::ExprApply	(	ExprManager *	em,
		const Op &	op,
		const std::vector< Expr > &	kids,
		ExprIndex	idx = 0
	)		[inline]

Definition at line 580 of file expr_value.h.

References APPLY, DebugAssert, CVC3::Op::getExpr(), and CVC3::Expr::isNull().

virtual CVC3::ExprApply::~ExprApply

(

)

[inline, virtual]

Definition at line 585 of file expr_value.h.

---

Member Function Documentation

size_t CVC3::ExprApply::getMMIndex

(

)

const [inline, protected, virtual]

Tell ExprManager who we are.

Reimplemented from CVC3::ExprNode.

Definition at line 566 of file expr_value.h.

References CVC3::EXPR_APPLY.

size_t CVC3::ExprApply::computeHash

(

)

const [inline, protected, virtual]

Use our static hash() for the member method.

Reimplemented from CVC3::ExprNode.

Definition at line 567 of file expr_value.h.

References CVC3::ExprNode::computeHash(), and PRIME.

Op CVC3::ExprApply::getOp

(

)

const [inline, protected, virtual]

Get the Op from an Apply Expr.

Reimplemented from CVC3::ExprValue.

Definition at line 570 of file expr_value.h.

bool CVC3::ExprApply::isApply

(

)

const [inline, protected, virtual]

Application of another expression.

Reimplemented from CVC3::ExprValue.

Definition at line 571 of file expr_value.h.

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

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

Reimplemented from CVC3::ExprNode.

Definition at line 231 of file expr_value.cpp.

References CVC3::ExprManager::getMM().

bool CVC3::ExprApply::operator==

(

const ExprValue &

ev2

)

const [virtual]

Compare with another ExprValue.

Reimplemented from CVC3::ExprNode.

Definition at line 223 of file expr_value.cpp.

References CVC3::ExprValue::getKids(), CVC3::ExprValue::getMMIndex(), and CVC3::ExprValue::getOp().

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

Overload operator new.

Reimplemented from CVC3::ExprNode.

Definition at line 589 of file expr_value.h.

References CVC3::MemoryManager::newData().

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

Reimplemented from CVC3::ExprNode.

Definition at line 592 of file expr_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::ExprApply::operator delete

(

void *

)

[inline]

Overload operator delete.

Reimplemented from CVC3::ExprNode.

Definition at line 595 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprNode.

Definition at line 561 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprNode.

Definition at line 562 of file expr_value.h.

---

Member Data Documentation

Expr CVC3::ExprApply::d_opExpr [private]

Definition at line 564 of file expr_value.h.

---

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

• expr_value.h
• expr_value.cpp