CVC3::ExprClosure Class Reference

A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers. More...

#include <expr_value.h>

Inheritance diagram for CVC3::ExprClosure:

[legend]Collaboration diagram for CVC3::ExprClosure:

[legend]List of all members.

Public Member Functions

• ExprClosure (ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, ExprIndex idx=0)
• virtual ~ExprClosure ()
• bool operator== (const ExprValue &ev2) const

  Equality between any two ExprValue objects (including subclasses).
  

• 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 isClosure () const

  A LAMBDA-expression or a quantifier.
  

Protected Member Functions

• size_t computeHash () const

  Non-caching hash function which actually computes the hash.
  

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

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

Private Member Functions

• virtual size_t getMMIndex () const

  Tell ExprManager who we are.
  

• virtual const std::vector<
  Expr > & getVars () const
• virtual const Expr & getBody () const

Private Attributes

• std::vector< Expr > d_vars

  Bound variables.
  

• Expr d_body

  The body of the quantifier/lambda.
  

Friends

• class Expr
• class ExprManager

---

Detailed Description

A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers.

Definition at line 864 of file expr_value.h.

---

Constructor & Destructor Documentation

CVC3::ExprClosure::ExprClosure	(	ExprManager *	em,
		int	kind,
		const std::vector< Expr > &	vars,
		const Expr &	body,
		ExprIndex	idx = 0
	)			[inline]

Definition at line 888 of file expr_value.h.

Referenced by copy().

virtual CVC3::ExprClosure::~ExprClosure

(

)

[inline, virtual]

Definition at line 892 of file expr_value.h.

---

Member Function Documentation

virtual size_t CVC3::ExprClosure::getMMIndex

(

)

const [inline, private, virtual]

Tell ExprManager who we are.

Reimplemented from CVC3::ExprValue.

Definition at line 874 of file expr_value.h.

References CVC3::EXPR_CLOSURE.

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

virtual const std::vector<Expr>& CVC3::ExprClosure::getVars

(

)

const [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 876 of file expr_value.h.

References d_vars.

Referenced by operator==().

virtual const Expr& CVC3::ExprClosure::getBody

(

)

const [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 877 of file expr_value.h.

References d_body.

Referenced by operator==().

size_t CVC3::ExprClosure::computeHash

(

)

const [protected, virtual]

Non-caching hash function which actually computes the hash.

This is the method that all subclasses should implement

Reimplemented from CVC3::ExprValue.

Definition at line 314 of file expr_value.cpp.

References d_body, CVC3::ExprValue::d_kind, d_vars, CVC3::ExprValue::hash(), CVC3::Expr::hash(), and PRIME.

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

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

Reimplemented from CVC3::ExprValue.

Definition at line 272 of file expr_value.cpp.

References d_body, CVC3::ExprValue::d_em, CVC3::ExprValue::d_kind, d_vars, ExprClosure(), CVC3::ExprManager::getMM(), getMMIndex(), and CVC3::ExprValue::rebuild().

bool CVC3::ExprClosure::operator==

(

const ExprValue &

ev2

)

const [virtual]

Equality between any two ExprValue objects (including subclasses).

Reimplemented from CVC3::ExprValue.

Definition at line 263 of file expr_value.cpp.

References CVC3::ExprValue::getBody(), getBody(), CVC3::ExprValue::getKind(), CVC3::ExprValue::getMMIndex(), getMMIndex(), CVC3::ExprValue::getVars(), and getVars().

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

Overload operator new.

Reimplemented from CVC3::ExprValue.

Definition at line 896 of file expr_value.h.

References CVC3::MemoryManager::newData().

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

Reimplemented from CVC3::ExprValue.

Definition at line 899 of file expr_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::ExprClosure::operator delete

(

void *

)

[inline]

Overload operator delete.

Reimplemented from CVC3::ExprValue.

Definition at line 902 of file expr_value.h.

virtual bool CVC3::ExprClosure::isClosure

(

)

const [inline, virtual]

A LAMBDA-expression or a quantifier.

Reimplemented from CVC3::ExprValue.

Definition at line 903 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 865 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 866 of file expr_value.h.

---

Member Data Documentation

std::vector<Expr> CVC3::ExprClosure::d_vars [private]

Bound variables.

Definition at line 869 of file expr_value.h.

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

Expr CVC3::ExprClosure::d_body [private]

The body of the quantifier/lambda.

Definition at line 871 of file expr_value.h.

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

---

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

• expr_value.h
• expr_value.cpp

---