#include <expr_value.h>
Inheritance diagram for CVC3::ExprNode:
Definition at line 387 of file expr_value.h.
CVC3::ExprNode::ExprNode | ( | ExprManager * | em, | |
int | kind, | |||
ExprIndex | idx = 0 | |||
) | [inline] |
CVC3::ExprNode::ExprNode | ( | ExprManager * | em, | |
int | kind, | |||
const std::vector< Expr > & | kids, | |||
ExprIndex | idx = 0 | |||
) | [inline] |
CVC3::ExprNode::~ExprNode | ( | ) | [virtual] |
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().
Special attributes for uninterpreted functions.
Reimplemented from CVC3::ExprValue.
Definition at line 446 of file expr_value.h.
References d_sig.
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.
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] |
CDO<Theorem>* CVC3::ExprNode::d_rep [protected] |