CVC3  2.4.1
Public Member Functions | Protected Member Functions | Protected Attributes | Private Member Functions | Friends
CVC3::ExprNode Class Reference

#include <expr_value.h>

Inheritance diagram for CVC3::ExprNode:
CVC3::ExprValue CVC3::ExprApply

List of all members.

Public Member Functions

 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 bool operator== (const ExprValue &ev2) const
 Compare with another ExprValue.
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.
virtual const ExprValuegetExprValue () 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 const std::string & getUid () const
virtual const std::string & getString () const
virtual const RationalgetRational () const
virtual const std::string & getName () const
 Returns the string name of UCONST and BOUND_VAR expr's.
virtual const ExprgetVar () 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 ExprgetBody () const
virtual void setTriggers (const std::vector< std::vector< Expr > > &triggers)
virtual const std::vector
< std::vector< Expr > > & 
getTriggers () const
virtual const ExprgetExistential () 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 TheoremgetTheorem () const

Protected Member Functions

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.
size_t computeHash () const
 Use our static hash() for the member method.
Unsigned computeSize () const
 Use our static sizeWithChildren() for the member method.
virtual ExprValuecopy (ExprManager *em, ExprIndex idx=0) const
 Make a clean copy of itself using the given memory manager.
- Protected Member Functions inherited from CVC3::ExprValue
MemoryManagergetMM (size_t MMIndex)
 Return the memory manager (for the benefit of subclasses)
ExprValuerebuild (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

std::vector< Exprd_children
 Vector of children.
CDO< Theorem > * d_sig
CDO< Theorem > * d_rep
- 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.
ExprManagerd_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 414 of file expr_value.h.


Constructor & Destructor Documentation

CVC3::ExprNode::ExprNode ( ExprManager em,
int  kind,
ExprIndex  idx = 0 
)
inline

Constructor.

Definition at line 456 of file expr_value.h.

CVC3::ExprNode::ExprNode ( ExprManager em,
int  kind,
const std::vector< Expr > &  kids,
ExprIndex  idx = 0 
)
inline

Constructor.

Definition at line 459 of file expr_value.h.

CVC3::ExprNode::~ExprNode ( )
virtual

Destructor.

Definition at line 104 of file expr_value.cpp.


Member Function Documentation

size_t CVC3::ExprNode::getMMIndex ( ) const
inlineprivatevirtual

Tell ExprManager who we are.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 429 of file expr_value.h.

References CVC3::EXPR_NODE.

unsigned CVC3::ExprNode::arity ( ) const
inlineprotectedvirtual

Return number of children.

Reimplemented from CVC3::ExprValue.

Definition at line 433 of file expr_value.h.

std::vector<Expr>& CVC3::ExprNode::getKids1 ( )
inlineprotected

Return reference to children.

Definition at line 436 of file expr_value.h.

Referenced by CVC3::Expr::Expr().

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

Return reference to children.

Reimplemented from CVC3::ExprValue.

Definition at line 439 of file expr_value.h.

size_t CVC3::ExprNode::computeHash ( ) const
inlineprotectedvirtual

Use our static hash() for the member method.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 442 of file expr_value.h.

References CVC3::ExprValue::hash().

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

Unsigned CVC3::ExprNode::computeSize ( ) const
inlineprotectedvirtual

Use our static sizeWithChildren() for the member method.

Reimplemented from CVC3::ExprValue.

Definition at line 447 of file expr_value.h.

References CVC3::ExprValue::sizeWithChildren().

ExprValue * CVC3::ExprNode::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::ExprApply.

Definition at line 131 of file expr_value.cpp.

References CVC3::ExprManager::getMM().

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

Overload operator new.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 466 of file expr_value.h.

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

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 468 of file expr_value.h.

void CVC3::ExprNode::operator delete ( void *  )
inline

Overload operator delete.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 473 of file expr_value.h.

bool CVC3::ExprNode::operator== ( const ExprValue ev2) const
virtual

Compare with another ExprValue.

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 123 of file expr_value.cpp.

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

virtual CDO<Theorem>* CVC3::ExprNode::getSig ( ) const
inlinevirtual

Special attributes for uninterpreted functions.

Reimplemented from CVC3::ExprValue.

Definition at line 478 of file expr_value.h.

virtual CDO<Theorem>* CVC3::ExprNode::getRep ( ) const
inlinevirtual

Reimplemented from CVC3::ExprValue.

Definition at line 479 of file expr_value.h.

virtual void CVC3::ExprNode::setRep ( CDO< Theorem > *  rep)
inlinevirtual

Reimplemented from CVC3::ExprValue.

Definition at line 481 of file expr_value.h.

virtual void CVC3::ExprNode::setSig ( CDO< Theorem > *  sig)
inlinevirtual

Reimplemented from CVC3::ExprValue.

Definition at line 482 of file expr_value.h.


Friends And Related Function Documentation

friend class Expr
friend

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 415 of file expr_value.h.

friend class ExprManager
friend

Reimplemented from CVC3::ExprValue.

Reimplemented in CVC3::ExprApply.

Definition at line 416 of file expr_value.h.


Member Data Documentation

std::vector<Expr> CVC3::ExprNode::d_children
protected

Vector of children.

Definition at line 420 of file expr_value.h.

CDO<Theorem>* CVC3::ExprNode::d_sig
protected

Definition at line 423 of file expr_value.h.

CDO<Theorem>* CVC3::ExprNode::d_rep
protected

Definition at line 424 of file expr_value.h.


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