CVC3::ExprApply Class Reference

#include <expr_value.h>

Inheritance diagram for CVC3::ExprApply:

[legend]Collaboration diagram for CVC3::ExprApply:

[legend]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 523 of file expr_value.h.

---

Constructor & Destructor Documentation

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

Definition at line 539 of file expr_value.h.

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

Referenced by copy().

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

Definition at line 543 of file expr_value.h.

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

virtual CVC3::ExprApply::~ExprApply

(

)

[inline, virtual]

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

References CVC3::EXPR_APPLY.

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

size_t CVC3::ExprApply::computeHash

(

)

const [inline, protected, virtual]

Use our static hash() for the member method.

Reimplemented from CVC3::ExprNode.

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

Referenced by operator==().

bool CVC3::ExprApply::isApply

(

)

const [inline, protected, virtual]

Application of another expression.

Reimplemented from CVC3::ExprValue.

Definition at line 534 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 225 of file expr_value.cpp.

References CVC3::ExprNode::d_children, CVC3::ExprValue::d_em, d_opExpr, ExprApply(), CVC3::ExprManager::getMM(), getMMIndex(), and CVC3::ExprValue::rebuild().

bool CVC3::ExprApply::operator==

(

const ExprValue &

ev2

)

const [virtual]

Compare with another ExprValue.

Reimplemented from CVC3::ExprNode.

Definition at line 217 of file expr_value.cpp.

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

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

Overload operator new.

Reimplemented from CVC3::ExprNode.

Definition at line 552 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 555 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 558 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprNode.

Definition at line 524 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprNode.

Definition at line 525 of file expr_value.h.

---

Member Data Documentation

Expr CVC3::ExprApply::d_opExpr [private]

Definition at line 527 of file expr_value.h.

Referenced by copy().

---

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

• expr_value.h
• expr_value.cpp

---