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:

Inheritance graph

Collaboration diagram for CVC3::ExprClosure:

Collaboration graph

List of all members.

Public Member Functions

ExprClosure (ExprManager *em, int kind, const Expr &var, const Expr &body, ExprIndex idx=0)
ExprClosure (ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, ExprIndex idx=0)
ExprClosure (ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &trigs, 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.
Unsigned computeSize () const
Non-caching size function which actually computes the size.
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
virtual void setTriggers (const std::vector< std::vector< Expr > > &triggers)
virtual const std::vector
< std::vector< Expr > > & getTrigs () const

Private Attributes

std::vector< Expr > d_vars
Bound variables.
Expr d_body
The body of the quantifier/lambda.
std::vector< std::vector< Expr > > d_manual_triggers
Manual triggers. // added by yeting.

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

Constructor & Destructor Documentation

CVC3::ExprClosure::ExprClosure	(	ExprManager *	em,
		int	kind,
		const Expr &	var,
		const Expr &	body,
		ExprIndex	idx = `0`
	)			`[inline]`

Definition at line 929 of file expr_value.h.

References d_vars.

Referenced by copy().

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

Definition at line 933 of file expr_value.h.

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

Definition at line 937 of file expr_value.h.

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

Definition at line 942 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 913 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 915 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 916 of file expr_value.h.

References d_body.

Referenced by operator==().

virtual void CVC3::ExprClosure::setTriggers ( const std::vector< std::vector< Expr > > & triggers ) [inline, private, virtual]

Reimplemented from CVC3::ExprValue.

Definition at line 917 of file expr_value.h.

References d_manual_triggers.

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

Reimplemented from CVC3::ExprValue.

Definition at line 918 of file expr_value.h.

References d_manual_triggers.

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 333 of file expr_value.cpp.

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

Unsigned CVC3::ExprClosure::computeSize ( ) const [inline, protected, virtual]

Non-caching size function which actually computes the size.

This is the method that all subclasses should implement

Reimplemented from CVC3::ExprValue.

Definition at line 923 of file expr_value.h.

References d_body, CVC3::Expr::d_expr, and CVC3::ExprValue::getSize().

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 278 of file expr_value.cpp.

References d_body, CVC3::ExprValue::d_em, CVC3::ExprValue::d_kind, d_manual_triggers, 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 269 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 946 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 949 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 952 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 953 of file expr_value.h.

Friends And Related Function Documentation

friend class Expr [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 902 of file expr_value.h.

friend class ExprManager [friend]

Reimplemented from CVC3::ExprValue.

Definition at line 903 of file expr_value.h.

Member Data Documentation

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

Bound variables.

Definition at line 906 of file expr_value.h.

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

Expr CVC3::ExprClosure::d_body [private]

The body of the quantifier/lambda.

Definition at line 908 of file expr_value.h.

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

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

Manual triggers. // added by yeting.

Definition at line 911 of file expr_value.h.

Referenced by copy(), getTrigs(), and setTriggers().

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

Generated on Thu Oct 15 22:19:37 2009 for CVC3 by

doxygen

1.5.8