CVC3
Public Member Functions | Protected Member Functions | Private Attributes | Friends | List of all members
CVC3::ExprApply Class Reference

#include <expr_value.h>

Inherits CVC3::ExprNode.

Collaboration diagram for CVC3::ExprApply:
Collaboration graph

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 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 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 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

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.
 
ExprValuecopy (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
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.
 

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< Exprd_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: