CVCL::ExprNode Class Reference

#include <expr_value.h>

Inheritance diagram for CVCL::ExprNode:

[legend]Collaboration diagram for CVCL::ExprNode:

[legend]List of all members.

Public Member Functions

• ExprNode (ExprManager *em, int kind, const std::vector< Expr > &kids, unsigned idx=0)

  Constructor.
  

• virtual ~ExprNode ()

  Destructor.
  

• void * operator new (size_t size, MemoryManager *mm)

  Overload operator new.
  

• void operator delete (void *)

  Overload operator delete.
  

• virtual bool operator== (const ExprValue &ev2) const

  Compare with another ExprValue.
  

• virtual CDO< Theorem > * getSig () const

  Special attributes for uninterpreted functions.
  

• virtual CDO< Theorem > * getRep () const
• virtual void setRep (CDO< Theorem > *rep)
• virtual void setSig (CDO< Theorem > *sig)

Protected Member Functions

• unsigned arity () const

  Return number of children.
  

• const std::vector< Expr > & getKids () const

  Return reference to children.
  

• size_t computeHash () const

  Use our static hash() for the member method.
  

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

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

Protected Attributes

• std::vector< Expr > d_children

  Vector of children.
  

• CDO< Theorem > * d_sig
• CDO< Theorem > * d_rep

Private Member Functions

• size_t getMMIndex () const

  Tell ExprManager who we are.
  

Friends

• class Expr
• class ExprManager

---

Detailed Description

Definition at line 376 of file expr_value.h.

---

Constructor & Destructor Documentation

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

Constructor. Definition at line 410 of file expr_value.h. Referenced by copy().

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

Destructor. Definition at line 88 of file expr_value.cpp. References d_rep, and d_sig.

---

Member Function Documentation

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

Tell ExprManager who we are. Reimplemented from CVCL::ExprValue. Reimplemented in CVCL::ExprApply. Definition at line 391 of file expr_value.h. References CVCL::EXPR_NODE. Referenced by copy(), and operator==().

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

Return number of children. Reimplemented from CVCL::ExprValue. Definition at line 395 of file expr_value.h.

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

Return reference to children. Reimplemented from CVCL::ExprValue. Definition at line 398 of file expr_value.h. Referenced by CVCL::ExprApply::operator==(), and operator==().

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

Use our static hash() for the member method. Reimplemented from CVCL::ExprValue. Reimplemented in CVCL::ExprApply. Definition at line 401 of file expr_value.h. References CVCL::hash().

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

Make a clean copy of itself using the given memory manager. Reimplemented from CVCL::ExprValue. Reimplemented in CVCL::ExprApply. Definition at line 113 of file expr_value.cpp. References d_children, CVCL::ExprValue::d_em, CVCL::ExprValue::d_kind, ExprNode(), CVCL::ExprManager::getMM(), getMMIndex(), and CVCL::ExprValue::rebuild().

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

Overload operator new. Reimplemented from CVCL::ExprValue. Reimplemented in CVCL::ExprApply. Definition at line 417 of file expr_value.h. References CVCL::MemoryManager::newData().

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

Overload operator delete. Reimplemented from CVCL::ExprValue. Reimplemented in CVCL::ExprApply. Definition at line 421 of file expr_value.h.

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

Compare with another ExprValue. Reimplemented from CVCL::ExprValue. Reimplemented in CVCL::ExprApply. Definition at line 105 of file expr_value.cpp. References CVCL::ExprValue::d_kind, CVCL::ExprValue::getKids(), getKids(), CVCL::ExprValue::getKind(), CVCL::ExprValue::getMMIndex(), and getMMIndex().

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

Special attributes for uninterpreted functions. Reimplemented from CVCL::ExprValue. Definition at line 426 of file expr_value.h.

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

Reimplemented from CVCL::ExprValue. Definition at line 427 of file expr_value.h.

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

Reimplemented from CVCL::ExprValue. Definition at line 429 of file expr_value.h.

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

Reimplemented from CVCL::ExprValue. Definition at line 430 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVCL::ExprValue. Reimplemented in CVCL::ExprApply. Definition at line 377 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVCL::ExprValue. Reimplemented in CVCL::ExprApply. Definition at line 378 of file expr_value.h.

---

Member Data Documentation

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

Vector of children. Definition at line 382 of file expr_value.h. Referenced by CVCL::ExprApply::copy(), and copy().

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

Definition at line 385 of file expr_value.h. Referenced by ~ExprNode().

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

Definition at line 386 of file expr_value.h. Referenced by ~ExprNode().

---

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

• expr_value.h
• expr_value.cpp

---