#include <expr_value.h>

Collaboration diagram for CVC3::ExprApply:

Public Member Functions
	ExprApply (ExprManager *em, const Op &op, ExprIndex idx=0)

	ExprApply (ExprManager *em, const Op &op, const std::vector< Expr > &kids, ExprIndex idx=0)

virtual	~ExprApply ()

bool	operator== (const ExprValue &ev2) const
	Compare with another ExprValue.

void *	operator new (size_t size, MemoryManager *mm)

void	operator delete (void pMem, MemoryManager mm)

void	operator delete (void *)

Public Member Functions inherited from CVC3::ExprNode
	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 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)

Public Member Functions inherited from CVC3::ExprValue
	ExprValue (ExprManager *em, int kind, ExprIndex idx=0)
	Constructor.

virtual	~ExprValue ()
	Destructor.

int	getKind () const
	Get the kind of the expression.

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 const ExprValue *	getExprValue () const
	Test whether the expression is a generic subclass.

virtual bool	isString () const
	String expression tester.

virtual bool	isRational () const
	Rational number expression tester.

virtual bool	isVar () const
	Uninterpreted constants.

virtual bool	isSymbol () const
	Special named symbol.

virtual bool	isClosure () const
	A LAMBDA-expression or a quantifier.

virtual bool	isTheorem () const
	Special Expr holding a theorem.

virtual const std::string &	getUid () const

virtual const std::string &	getString () const

virtual const Rational &	getRational () const

virtual const std::string &	getName () const
	Returns the string name of UCONST and BOUND_VAR expr's.

virtual const Expr &	getVar () const
	Returns the original Boolean variable (for BoolVarExprValue)

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 > > &	getTriggers () const

virtual const Expr &	getExistential () const

virtual int	getBoundIndex () const

virtual const std::vector < std::string > &	getFields () const

virtual const std::string &	getField () const

virtual int	getTupleIndex () const

virtual const Theorem &	getTheorem () const

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.

Protected Member Functions inherited from CVC3::ExprNode
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.

Unsigned	computeSize () const
	Use our static sizeWithChildren() for the member method.

Protected Member Functions inherited from CVC3::ExprValue
MemoryManager *	getMM (size_t MMIndex)
	Return the memory manager (for the benefit of subclasses)

ExprValue *	rebuild (ExprManager *em) const
	Make a clean copy of itself using the given ExprManager.

Expr	rebuild (Expr e, ExprManager *em) const
	Make a clean copy of the expr using the given ExprManager.

Private Attributes
Expr	d_opExpr

Friends
class	Expr

class	ExprManager

Additional Inherited Members
Static Protected Member Functions inherited from CVC3::ExprValue
static size_t	pointerHash (void *p)

static size_t	hash (const int kind, const std::vector< Expr > &kids)

static size_t	hash (const int n)

static Unsigned	sizeWithChildren (const std::vector< Expr > &kids)

Protected Attributes inherited from CVC3::ExprNode
std::vector< Expr >	d_children
	Vector of children.

CDO< Theorem > *	d_sig

CDO< Theorem > *	d_rep

Static Protected Attributes inherited from CVC3::ExprValue
static std::hash< char * >	s_charHash
	Return child with greatest height.

static std::hash< long int >	s_intHash

Detailed Description

Definition at line 560 of file expr_value.h.

Constructor & Destructor Documentation

CVC3::ExprApply::ExprApply	(	ExprManager *	em,
		const Op &	op,
		ExprIndex	idx = `0`
	)

inline

Definition at line 576 of file expr_value.h.

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

CVC3::ExprApply::ExprApply	(	ExprManager *	em,
		const Op &	op,
		const std::vector< Expr > &	kids,
		ExprIndex	idx = `0`
	)

inline

Definition at line 580 of file expr_value.h.

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

virtual CVC3::ExprApply::~ExprApply ( )

inlinevirtual

Definition at line 585 of file expr_value.h.

Member Function Documentation

size_t CVC3::ExprApply::getMMIndex ( ) const

inlineprotectedvirtual

Tell ExprManager who we are.

Reimplemented from CVC3::ExprNode.

Definition at line 566 of file expr_value.h.

References CVC3::EXPR_APPLY.

size_t CVC3::ExprApply::computeHash ( ) const

inlineprotectedvirtual

Use our static hash() for the member method.

Reimplemented from CVC3::ExprNode.

Definition at line 567 of file expr_value.h.

References CVC3::ExprNode::computeHash(), and PRIME.

Op CVC3::ExprApply::getOp ( ) const

inlineprotectedvirtual

Get the Op from an Apply Expr.

Reimplemented from CVC3::ExprValue.

Definition at line 570 of file expr_value.h.

bool CVC3::ExprApply::isApply ( ) const

inlineprotectedvirtual

Application of another expression.

Reimplemented from CVC3::ExprValue.

Definition at line 571 of file expr_value.h.

ExprValue * CVC3::ExprApply::copy	(	ExprManager *	em,
		ExprIndex	idx = `0`
	)		const

protectedvirtual

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

Reimplemented from CVC3::ExprNode.

Definition at line 231 of file expr_value.cpp.

References CVC3::ExprManager::getMM().

bool CVC3::ExprApply::operator== ( const ExprValue & ev2 ) const

virtual

Compare with another ExprValue.

Reimplemented from CVC3::ExprNode.

Definition at line 223 of file expr_value.cpp.

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

void* CVC3::ExprApply::operator new	(	size_t	size,
		MemoryManager *	mm
	)

inline

Definition at line 589 of file expr_value.h.

void CVC3::ExprApply::operator delete	(	void *	pMem,
		MemoryManager *	mm
	)

inline

Definition at line 592 of file expr_value.h.

void CVC3::ExprApply::operator delete ( void * )

inline

Definition at line 595 of file expr_value.h.

Friends And Related Function Documentation

friend class Expr

friend

Definition at line 561 of file expr_value.h.

friend class ExprManager

friend

Definition at line 562 of file expr_value.h.

Member Data Documentation

Expr CVC3::ExprApply::d_opExpr

private

Definition at line 564 of file expr_value.h.

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

Public Member Functions

Protected Member Functions

Private Attributes

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation