CVCL::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 CVCL::ExprClosure:

[legend]Collaboration diagram for CVCL::ExprClosure:

[legend]List of all members.

Public Member Functions

• ExprClosure (ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, unsigned 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 *)

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

---

Constructor & Destructor Documentation

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

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

virtual CVCL::ExprClosure::~ExprClosure (   )  [inline, virtual]

Definition at line 783 of file expr_value.h.

---

Member Function Documentation

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

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

virtual const std::vector<Expr>& CVCL::ExprClosure::getVars (   )  const [inline, private, virtual]

Reimplemented from CVCL::ExprValue. Definition at line 767 of file expr_value.h. References d_vars(). Referenced by operator==().

virtual const Expr& CVCL::ExprClosure::getBody (   )  const [inline, private, virtual]

Reimplemented from CVCL::ExprValue. Definition at line 768 of file expr_value.h. Referenced by operator==().

size_t CVCL::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 CVCL::ExprValue. Definition at line 264 of file expr_value.cpp. References d_body, CVCL::ExprValue::d_kind, d_vars, CVCL::hash(), and CVCL::Expr::hash().

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

Make a clean copy of itself using the given memory manager. Reimplemented from CVCL::ExprValue. Definition at line 236 of file expr_value.cpp. References d_body, CVCL::ExprValue::d_em, CVCL::ExprValue::d_kind, d_vars, ExprClosure(), CVCL::ExprManager::getMM(), getMMIndex(), and CVCL::ExprValue::rebuild().

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

Equality between any two ExprValue objects (including subclasses). Reimplemented from CVCL::ExprValue. Definition at line 227 of file expr_value.cpp. References CVCL::ExprValue::getBody(), getBody(), CVCL::ExprValue::getKind(), CVCL::ExprValue::getMMIndex(), getMMIndex(), CVCL::ExprValue::getVars(), and getVars().

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

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

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

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

virtual bool CVCL::ExprClosure::isClosure (   )  const [inline, virtual]

A LAMBDA-expression or a quantifier. Reimplemented from CVCL::ExprValue. Definition at line 791 of file expr_value.h.

---

Friends And Related Function Documentation

friend class Expr [friend]

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

friend class ExprManager [friend]

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

---

Member Data Documentation

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

Bound variables. Definition at line 760 of file expr_value.h. Referenced by computeHash(), and copy().

Expr CVCL::ExprClosure::d_body [private]

The body of the quantifier/lambda. Definition at line 762 of file expr_value.h. Referenced by computeHash(), and copy().

---

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

• expr_value.h
• expr_value.cpp

---