CVC3::ExprApply Class Reference

#include <expr_value.h>

Inheritance diagram for CVC3::ExprApply:

Inheritance graph
[legend]
Collaboration diagram for CVC3::ExprApply:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Member Functions

Private Attributes

Friends


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

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

Referenced by operator==().

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

Referenced by copy().


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:15:14 2009 for CVC3 by  doxygen 1.5.2