CVC3::ExprNode Class Reference

#include <expr_value.h>

Inheritance diagram for CVC3::ExprNode:

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

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Friends


Detailed Description

Definition at line 387 of file expr_value.h.


Constructor & Destructor Documentation

CVC3::ExprNode::ExprNode ( ExprManager em,
int  kind,
ExprIndex  idx = 0 
) [inline]

Constructor.

Definition at line 424 of file expr_value.h.

Referenced by copy().

CVC3::ExprNode::ExprNode ( ExprManager em,
int  kind,
const std::vector< Expr > &  kids,
ExprIndex  idx = 0 
) [inline]

Constructor.

Definition at line 427 of file expr_value.h.

CVC3::ExprNode::~ExprNode (  )  [virtual]

Destructor.

Definition at line 98 of file expr_value.cpp.

References d_rep, and d_sig.


Member Function Documentation

size_t CVC3::ExprNode::getMMIndex (  )  const [inline, private, virtual]

Tell ExprManager who we are.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 402 of file expr_value.h.

References CVC3::EXPR_NODE.

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

unsigned CVC3::ExprNode::arity (  )  const [inline, protected, virtual]

Return number of children.

Reimplemented from CVC3::ExprValue.

Definition at line 406 of file expr_value.h.

References d_children.

std::vector<Expr>& CVC3::ExprNode::getKids1 (  )  [inline, protected]

Return reference to children.

Definition at line 409 of file expr_value.h.

References d_children.

Referenced by CVC3::Expr::Expr().

const std::vector<Expr>& CVC3::ExprNode::getKids (  )  const [inline, protected, virtual]

Return reference to children.

Reimplemented from CVC3::ExprValue.

Definition at line 412 of file expr_value.h.

References d_children.

Referenced by CVC3::ExprApply::operator==(), and operator==().

size_t CVC3::ExprNode::computeHash (  )  const [inline, protected, virtual]

Use our static hash() for the member method.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 415 of file expr_value.h.

References d_children, CVC3::ExprValue::d_kind, and CVC3::ExprValue::hash().

Referenced by CVC3::ExprApply::computeHash().

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

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

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 125 of file expr_value.cpp.

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

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

Overload operator new.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 434 of file expr_value.h.

References CVC3::MemoryManager::newData().

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

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 436 of file expr_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::ExprNode::operator delete ( void *   )  [inline]

Overload operator delete.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 441 of file expr_value.h.

bool CVC3::ExprNode::operator== ( const ExprValue ev2  )  const [virtual]

Compare with another ExprValue.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 117 of file expr_value.cpp.

References CVC3::ExprValue::d_kind, CVC3::ExprValue::getKids(), getKids(), CVC3::ExprValue::getKind(), CVC3::ExprValue::getMMIndex(), and getMMIndex().

virtual CDO<Theorem>* CVC3::ExprNode::getSig (  )  const [inline, virtual]

Special attributes for uninterpreted functions.

Reimplemented from CVC3::ExprValue.

Definition at line 446 of file expr_value.h.

References d_sig.

virtual CDO<Theorem>* CVC3::ExprNode::getRep (  )  const [inline, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 447 of file expr_value.h.

References d_rep.

virtual void CVC3::ExprNode::setRep ( CDO< Theorem > *  rep  )  [inline, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 449 of file expr_value.h.

References d_rep.

virtual void CVC3::ExprNode::setSig ( CDO< Theorem > *  sig  )  [inline, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 450 of file expr_value.h.

References d_sig.


Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 388 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 389 of file expr_value.h.


Member Data Documentation

std::vector<Expr> CVC3::ExprNode::d_children [protected]

Vector of children.

Definition at line 393 of file expr_value.h.

Referenced by arity(), computeHash(), CVC3::ExprApply::copy(), copy(), getKids(), and getKids1().

CDO<Theorem>* CVC3::ExprNode::d_sig [protected]

Definition at line 396 of file expr_value.h.

Referenced by getSig(), setSig(), and ~ExprNode().

CDO<Theorem>* CVC3::ExprNode::d_rep [protected]

Definition at line 397 of file expr_value.h.

Referenced by getRep(), setRep(), and ~ExprNode().


The documentation for this class was generated from the following files:
Generated on Tue Jul 3 14:36:34 2007 for CVC3 by  doxygen 1.5.1