#include <expr_value.h>

Collaboration diagram for CVC3::ExprNodeTmp:

Public Member Functions
	ExprNodeTmp (ExprManager *em, int kind, const std::vector< Expr > &kids)
	Constructor.

virtual	~ExprNodeTmp ()
	Destructor.

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

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	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 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 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
unsigned	arity () const
	Return number of children.

const std::vector< Expr > &	getKids () const
	Return reference to children.

size_t	computeHash () const
	Use our static hash() for the member method.

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

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.

Protected Attributes
const std::vector< Expr > &	d_children
	Vector of children.

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.

Private Member Functions
size_t	getMMIndex () const
	Tell ExprManager who we are.

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)

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

Constructor & Destructor Documentation

CVC3::ExprNodeTmp::ExprNodeTmp	(	ExprManager *	em,
		int	kind,
		const std::vector< Expr > &	kids
	)

inline

Constructor.

Definition at line 522 of file expr_value.h.

virtual CVC3::ExprNodeTmp::~ExprNodeTmp ( )

inlinevirtual

Destructor.

Definition at line 526 of file expr_value.h.

Member Function Documentation

size_t CVC3::ExprNodeTmp::getMMIndex ( ) const

inlineprivatevirtual

Tell ExprManager who we are.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApplyTmp.

Definition at line 498 of file expr_value.h.

References CVC3::EXPR_NODE.

unsigned CVC3::ExprNodeTmp::arity ( ) const

inlineprotectedvirtual

Return number of children.

Reimplemented from CVC3::ExprValue.

Definition at line 502 of file expr_value.h.

References d_children.

const std::vector<Expr>& CVC3::ExprNodeTmp::getKids ( ) const

inlineprotectedvirtual

Return reference to children.

Reimplemented from CVC3::ExprValue.

Definition at line 505 of file expr_value.h.

References d_children.

size_t CVC3::ExprNodeTmp::computeHash ( ) const

inlineprotectedvirtual

Use our static hash() for the member method.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApplyTmp.

Definition at line 508 of file expr_value.h.

References d_children, CVC3::ExprValue::d_kind, and CVC3::ExprValue::hash().

Referenced by CVC3::ExprApplyTmp::computeHash().

Unsigned CVC3::ExprNodeTmp::computeSize ( ) const

inlineprotectedvirtual

Use our static sizeWithChildren() for the member method.

Reimplemented from CVC3::ExprValue.

Definition at line 513 of file expr_value.h.

References d_children, and CVC3::ExprValue::sizeWithChildren().

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

protectedvirtual

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

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApplyTmp.

Definition at line 91 of file expr_value.cpp.

References CVC3::ExprManager::getMM().

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

virtual

Compare with another ExprValue.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApplyTmp.

Definition at line 85 of file expr_value.cpp.

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

Friends And Related Function Documentation

friend class Expr

friend

Definition at line 488 of file expr_value.h.

friend class ExprManager

friend

Definition at line 489 of file expr_value.h.

Member Data Documentation

const std::vector<Expr>& CVC3::ExprNodeTmp::d_children

protected

Vector of children.

Definition at line 493 of file expr_value.h.

Referenced by arity(), computeHash(), computeSize(), and getKids().

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

Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation