CVC3::ExprNode Class Reference

#include <expr_value.h>

Inheritance diagram for CVC3::ExprNode:

[legend]Collaboration diagram for CVC3::ExprNode:

[legend]List of all members.

Public Member Functions

• ExprNode (ExprManager *em, int kind, ExprIndex idx=0)

  Constructor.
  

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

  Constructor.
  

• virtual ~ExprNode ()

  Destructor.
  

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

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

• std::vector< Expr > & getKids1 ()

  Return reference to children.
  

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

  Return reference to children.
  

• size_t computeHash () const

  Use our static hash() for the member method.
  

• Unsigned computeSize () const

  Use our static sizeWithChildren() 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 414 of file expr_value.h.

---

Constructor & Destructor Documentation

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

Constructor.

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

CVC3::ExprNode::~ExprNode

(

)

[virtual]

Destructor.

Definition at line 104 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 429 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 433 of file expr_value.h.

std::vector<Expr>& CVC3::ExprNode::getKids1

(

)

[inline, protected]

Return reference to children.

Definition at line 436 of file expr_value.h.

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 439 of file expr_value.h.

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 442 of file expr_value.h.

References CVC3::ExprValue::hash().

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

Unsigned CVC3::ExprNode::computeSize

(

)

const [inline, protected, virtual]

Use our static sizeWithChildren() for the member method.

Reimplemented from CVC3::ExprValue.

Definition at line 447 of file expr_value.h.

References CVC3::ExprValue::sizeWithChildren().

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 131 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 466 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 468 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 473 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 123 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 478 of file expr_value.h.

virtual CDO<Theorem>* CVC3::ExprNode::getRep

(

)

const [inline, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 479 of file expr_value.h.

virtual void CVC3::ExprNode::setRep

(

CDO< Theorem > *

rep

)

[inline, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 481 of file expr_value.h.

virtual void CVC3::ExprNode::setSig

(

CDO< Theorem > *

sig

)

[inline, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 482 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 415 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 416 of file expr_value.h.

---

Member Data Documentation

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

Vector of children.

Definition at line 420 of file expr_value.h.

Referenced by CVC3::ExprApply::copy(), and copy().

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

Definition at line 423 of file expr_value.h.

Referenced by ~ExprNode().

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

Definition at line 424 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

---