CVC3::ExprApplyTmp Class Reference

#include <expr_value.h>

Inheritance diagram for CVC3::ExprApplyTmp:

[legend]Collaboration diagram for CVC3::ExprApplyTmp:

[legend]List of all members.

Public Member Functions

• ExprApplyTmp (ExprManager *em, const Op &op, const std::vector< Expr > &kids)
• virtual ~ExprApplyTmp ()
• bool operator== (const ExprValue &ev2) const

  Compare with another ExprValue.
  

Protected Member Functions

• size_t getMMIndex () const

  Tell ExprManager who we are.
  

• size_t computeHash () const

  Use our static hash() for the member method.
  

• Op getOp () const

  Get the Op from an Apply Expr.
  

• bool isApply () const

  Application of another expression.
  

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

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

Private Attributes

• Expr d_opExpr

Friends

• class Expr
• class ExprManager

---

Detailed Description

Definition at line 534 of file expr_value.h.

---

Constructor & Destructor Documentation

CVC3::ExprApplyTmp::ExprApplyTmp	(	ExprManager *	em,
		const Op &	op,
		const std::vector< Expr > &	kids
	)			[inline]

Definition at line 550 of file expr_value.h.

References CVC3::APPLY, CVC3::ExprValue::d_kind, DebugAssert, CVC3::Op::getExpr(), and CVC3::Expr::isNull().

virtual CVC3::ExprApplyTmp::~ExprApplyTmp

(

)

[inline, virtual]

Definition at line 555 of file expr_value.h.

---

Member Function Documentation

size_t CVC3::ExprApplyTmp::getMMIndex

(

)

const [inline, protected, virtual]

Tell ExprManager who we are.

Reimplemented from CVC3::ExprNodeTmp.

Definition at line 540 of file expr_value.h.

References CVC3::EXPR_APPLY.

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

size_t CVC3::ExprApplyTmp::computeHash

(

)

const [inline, protected, virtual]

Use our static hash() for the member method.

Reimplemented from CVC3::ExprNodeTmp.

Definition at line 541 of file expr_value.h.

References CVC3::ExprNodeTmp::computeHash(), d_opExpr, CVC3::Expr::hash(), and PRIME.

Op CVC3::ExprApplyTmp::getOp

(

)

const [inline, protected, virtual]

Get the Op from an Apply Expr.

Reimplemented from CVC3::ExprValue.

Definition at line 544 of file expr_value.h.

References d_opExpr.

Referenced by operator==().

bool CVC3::ExprApplyTmp::isApply

(

)

const [inline, protected, virtual]

Application of another expression.

Reimplemented from CVC3::ExprValue.

Definition at line 545 of file expr_value.h.

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

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

Reimplemented from CVC3::ExprNodeTmp.

Definition at line 254 of file expr_value.cpp.

References CVC3::ExprNodeTmp::d_children, CVC3::ExprValue::d_em, d_opExpr, CVC3::ExprValue::ExprApply, CVC3::ExprManager::getMM(), getMMIndex(), and CVC3::ExprValue::rebuild().

bool CVC3::ExprApplyTmp::operator==

(

const ExprValue &

ev2

)

const [virtual]

Compare with another ExprValue.

Reimplemented from CVC3::ExprNodeTmp.

Definition at line 246 of file expr_value.cpp.

References CVC3::ExprValue::getKids(), CVC3::ExprNodeTmp::getKids(), CVC3::ExprValue::getMMIndex(), getMMIndex(), CVC3::ExprValue::getOp(), and getOp().

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprNodeTmp.

Definition at line 535 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprNodeTmp.

Definition at line 536 of file expr_value.h.

---

Member Data Documentation

Expr CVC3::ExprApplyTmp::d_opExpr [private]

Definition at line 538 of file expr_value.h.

Referenced by computeHash(), copy(), and getOp().

---

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

• expr_value.h
• expr_value.cpp

---