#include <expr_value.h>

Collaboration diagram for CVC3::ExprSymbol:

Public Member Functions
	ExprSymbol (ExprManager *em, int kind, const std::string &name, ExprIndex idx=0)

virtual	~ExprSymbol ()

virtual bool	operator== (const ExprValue &ev2) const
	Equality between any two ExprValue objects (including subclasses)

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::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	isApply () const
	Application of another expression.

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

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

virtual const std::vector< Expr > &	getKids () const
	Get kids: by default, returns a ref to an empty vector.

virtual unsigned	arity () const
	Default arity = 0.

virtual CDO< Theorem > *	getSig () const
	Special attributes for uninterpreted functions.

virtual CDO< Theorem > *	getRep () const

virtual void	setSig (CDO< Theorem > *sig)

virtual void	setRep (CDO< Theorem > *rep)

virtual const std::string &	getUid () const

virtual const std::string &	getString () const

virtual const Rational &	getRational () const

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

virtual Op	getOp () const
	Get the Op from an Apply Expr.

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
virtual size_t	computeHash () const
	Non-caching hash function which actually computes the hash.

virtual ExprValue *	copy (ExprManager *em, ExprIndex idx=0) const
	Make a clean copy of itself using the given memory manager.

bool	isSymbol () const
	Special named symbol.

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.

virtual Unsigned	computeSize () const
	Non-caching size function which actually computes the size.

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

virtual size_t	getMMIndex () const
	Get unique memory manager ID.

Private Attributes
std::string	d_name

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::ExprValue
int	d_kind
	The kind of the expression. In particular, it determines which subclass of ExprValue is used to store the expression.

ExprManager *	d_em
	Our expr. manager.

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

Constructor & Destructor Documentation

CVC3::ExprSymbol::ExprSymbol	(	ExprManager *	em,
		int	kind,
		const std::string &	name,
		ExprIndex	idx = `0`
	)

inline

Definition at line 842 of file expr_value.h.

virtual CVC3::ExprSymbol::~ExprSymbol ( )

inlinevirtual

Definition at line 846 of file expr_value.h.

Member Function Documentation

virtual const std::string& CVC3::ExprSymbol::getName ( ) const

inlineprivatevirtual

Returns the string name of UCONST and BOUND_VAR expr's.

Reimplemented from CVC3::ExprValue.

Definition at line 827 of file expr_value.h.

References d_name.

virtual size_t CVC3::ExprSymbol::getMMIndex ( ) const

inlineprivatevirtual

Get unique memory manager ID.

Reimplemented from CVC3::ExprValue.

Definition at line 830 of file expr_value.h.

References CVC3::EXPR_SYMBOL.

virtual size_t CVC3::ExprSymbol::computeHash ( ) const

inlineprotectedvirtual

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

References CVC3::ExprValue::d_kind, d_name, PRIME, CVC3::ExprValue::s_charHash, and CVC3::ExprValue::s_intHash.

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

protectedvirtual

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

Reimplemented from CVC3::ExprValue.

Definition at line 205 of file expr_value.cpp.

References CVC3::ExprManager::getMM().

bool CVC3::ExprSymbol::isSymbol ( ) const

inlineprotectedvirtual

Special named symbol.

Reimplemented from CVC3::ExprValue.

Definition at line 838 of file expr_value.h.

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

virtual

Equality between any two ExprValue objects (including subclasses)

Reimplemented from CVC3::ExprValue.

Definition at line 198 of file expr_value.cpp.

References CVC3::ExprValue::getKind(), CVC3::ExprValue::getMMIndex(), and CVC3::ExprValue::getName().

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

inline

Definition at line 850 of file expr_value.h.

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

inline

Definition at line 853 of file expr_value.h.

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

inline

Definition at line 856 of file expr_value.h.

Friends And Related Function Documentation

friend class Expr

friend

Definition at line 822 of file expr_value.h.

friend class ExprManager

friend

Definition at line 823 of file expr_value.h.

Member Data Documentation

std::string CVC3::ExprSymbol::d_name

private

Definition at line 825 of file expr_value.h.

Referenced by computeHash(), and getName().

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

Public Member Functions

Protected Member Functions

Private Member Functions

Private Attributes

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation