#include <expr_value.h>

Collaboration diagram for CVC3::ExprString:

Public Member Functions
	ExprString (ExprManager *em, const std::string &s, ExprIndex idx=0)

virtual	~ExprString ()

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	isRational () const
	Rational number expression tester.

virtual bool	isVar () const
	Uninterpreted constants.

virtual bool	isApply () const
	Application of another expression.

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::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 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 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 bool	isString () const
	String expression tester.

virtual const std::string &	getString () const

virtual 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::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 size_t	getMMIndex () const
	Get unique memory manager ID.

Static Private Member Functions
static size_t	hash (const std::string &str)

Private Attributes
std::string	d_str

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

Constructor & Destructor Documentation

CVC3::ExprString::ExprString	(	ExprManager *	em,
		const std::string &	s,
		ExprIndex	idx = `0`
	)

inline

Definition at line 684 of file expr_value.h.

virtual CVC3::ExprString::~ExprString ( )

inlinevirtual

Definition at line 687 of file expr_value.h.

Member Function Documentation

static size_t CVC3::ExprString::hash ( const std::string & str )

inlinestaticprivate

Definition at line 666 of file expr_value.h.

References CVC3::ExprValue::s_charHash.

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

inlineprivatevirtual

Get unique memory manager ID.

Reimplemented from CVC3::ExprValue.

Definition at line 671 of file expr_value.h.

References CVC3::EXPR_STRING.

virtual size_t CVC3::ExprString::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 675 of file expr_value.h.

References d_str, and CVC3::ExprValue::hash().

virtual bool CVC3::ExprString::isString ( ) const

inlineprotectedvirtual

String expression tester.

Reimplemented from CVC3::ExprValue.

Definition at line 677 of file expr_value.h.

virtual const std::string& CVC3::ExprString::getString ( ) const

inlineprotectedvirtual

Reimplemented from CVC3::ExprValue.

Definition at line 678 of file expr_value.h.

References d_str.

ExprValue * CVC3::ExprString::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 151 of file expr_value.cpp.

References CVC3::ExprManager::getMM().

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

virtual

Equality between any two ExprValue objects (including subclasses)

Reimplemented from CVC3::ExprValue.

Definition at line 144 of file expr_value.cpp.

References CVC3::ExprValue::getMMIndex(), and CVC3::ExprValue::getString().

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

inline

Definition at line 691 of file expr_value.h.

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

inline

Definition at line 694 of file expr_value.h.

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

inline

Definition at line 697 of file expr_value.h.

Friends And Related Function Documentation

friend class Expr

friend

Definition at line 660 of file expr_value.h.

friend class ExprManager

friend

Definition at line 661 of file expr_value.h.

Member Data Documentation

std::string CVC3::ExprString::d_str

private

Definition at line 663 of file expr_value.h.

Referenced by computeHash(), and getString().

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

Public Member Functions

Protected Member Functions

Private Member Functions

Static 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