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

A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers. More...

#include <expr_value.h>

Inheritance diagram for CVC3::ExprClosure:
CVC3::ExprValue

Public Member Functions

 ExprClosure (ExprManager *em, int kind, const Expr &var, const Expr &body, ExprIndex idx=0)
 
 ExprClosure (ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, ExprIndex idx=0)
 
 ExprClosure (ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &trigs, ExprIndex idx=0)
 
virtual ~ExprClosure ()
 
bool operator== (const ExprValue &ev2) const
 Equality between any two ExprValue objects (including subclasses) More...
 
void * operator new (size_t size, MemoryManager *mm)
 
void operator delete (void *pMem, MemoryManager *mm)
 
void operator delete (void *)
 
virtual bool isClosure () const
 A LAMBDA-expression or a quantifier. More...
 
- Public Member Functions inherited from CVC3::ExprValue
 ExprValue (ExprManager *em, int kind, ExprIndex idx=0)
 Constructor. More...
 
virtual ~ExprValue ()
 Destructor. More...
 
int getKind () const
 Get the kind of the expression. More...
 
void * operator new (size_t size, MemoryManager *mm)
 Overload operator new. More...
 
void operator delete (void *pMem, MemoryManager *mm)
 
void operator delete (void *)
 Overload operator delete. More...
 
virtual const ExprValuegetExprValue () const
 Test whether the expression is a generic subclass. More...
 
virtual bool isString () const
 String expression tester. More...
 
virtual bool isRational () const
 Rational number expression tester. More...
 
virtual bool isVar () const
 Uninterpreted constants. More...
 
virtual bool isApply () const
 Application of another expression. More...
 
virtual bool isSymbol () const
 Special named symbol. More...
 
virtual bool isTheorem () const
 Special Expr holding a theorem. More...
 
virtual const std::vector< Expr > & getKids () const
 Get kids: by default, returns a ref to an empty vector. More...
 
virtual unsigned arity () const
 Default arity = 0. More...
 
virtual CDO< Theorem > * getSig () const
 Special attributes for uninterpreted functions. More...
 
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 RationalgetRational () const
 
virtual const std::string & getName () const
 Returns the string name of UCONST and BOUND_VAR expr's. More...
 
virtual const ExprgetVar () const
 Returns the original Boolean variable (for BoolVarExprValue) More...
 
virtual Op getOp () const
 Get the Op from an Apply Expr. More...
 
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 computeHash () const
 Non-caching hash function which actually computes the hash. More...
 
Unsigned computeSize () const
 Non-caching size function which actually computes the size. More...
 
ExprValuecopy (ExprManager *em, ExprIndex idx=0) const
 Make a clean copy of itself using the given memory manager. More...
 
- Protected Member Functions inherited from CVC3::ExprValue
MemoryManagergetMM (size_t MMIndex)
 Return the memory manager (for the benefit of subclasses) More...
 
ExprValuerebuild (ExprManager *em) const
 Make a clean copy of itself using the given ExprManager. More...
 
Expr rebuild (Expr e, ExprManager *em) const
 Make a clean copy of the expr using the given ExprManager. More...
 

Private Member Functions

virtual size_t getMMIndex () const
 Tell ExprManager who we are. More...
 
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
 

Private Attributes

std::vector< Exprd_vars
 Bound variables. More...
 
Expr d_body
 The body of the quantifier/lambda. More...
 
std::vector< std::vector< Expr > > d_manual_triggers
 Manual triggers. // added by yeting. More...
 

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. More...
 
ExprManagerd_em
 Our expr. manager. More...
 
- Static Protected Attributes inherited from CVC3::ExprValue
static std::hash< char * > s_charHash
 Return child with greatest height. More...
 
static std::hash< long int > s_intHash
 

Detailed Description

A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers.

Definition at line 901 of file expr_value.h.

Constructor & Destructor Documentation

CVC3::ExprClosure::ExprClosure ( ExprManager em,
int  kind,
const Expr var,
const Expr body,
ExprIndex  idx = 0 
)
inline

Definition at line 929 of file expr_value.h.

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

Definition at line 933 of file expr_value.h.

CVC3::ExprClosure::ExprClosure ( ExprManager em,
int  kind,
const std::vector< Expr > &  vars,
const Expr body,
const std::vector< std::vector< Expr > > &  trigs,
ExprIndex  idx = 0 
)
inline

Definition at line 937 of file expr_value.h.

virtual CVC3::ExprClosure::~ExprClosure ( )
inlinevirtual

Definition at line 942 of file expr_value.h.

Member Function Documentation

virtual size_t CVC3::ExprClosure::getMMIndex ( ) const
inlineprivatevirtual

Tell ExprManager who we are.

Reimplemented from CVC3::ExprValue.

Definition at line 913 of file expr_value.h.

References CVC3::EXPR_CLOSURE.

virtual const std::vector<Expr>& CVC3::ExprClosure::getVars ( ) const
inlineprivatevirtual

Reimplemented from CVC3::ExprValue.

Definition at line 915 of file expr_value.h.

References d_vars.

virtual const Expr& CVC3::ExprClosure::getBody ( ) const
inlineprivatevirtual

Reimplemented from CVC3::ExprValue.

Definition at line 916 of file expr_value.h.

References d_body.

virtual void CVC3::ExprClosure::setTriggers ( const std::vector< std::vector< Expr > > &  triggers)
inlineprivatevirtual

Reimplemented from CVC3::ExprValue.

Definition at line 917 of file expr_value.h.

virtual const std::vector<std::vector<Expr> >& CVC3::ExprClosure::getTriggers ( ) const
inlineprivatevirtual

Reimplemented from CVC3::ExprValue.

Definition at line 918 of file expr_value.h.

References d_manual_triggers.

size_t CVC3::ExprClosure::computeHash ( ) const
protectedvirtual

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 333 of file expr_value.cpp.

References CVC3::Unsigned::hash(), and PRIME.

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

Non-caching size function which actually computes the size.

This is the method that all subclasses should implement

Reimplemented from CVC3::ExprValue.

Definition at line 923 of file expr_value.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::getSize().

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

References CVC3::ExprManager::getMM().

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

Equality between any two ExprValue objects (including subclasses)

Reimplemented from CVC3::ExprValue.

Definition at line 269 of file expr_value.cpp.

References CVC3::ExprValue::getBody(), CVC3::ExprValue::getKind(), CVC3::ExprValue::getMMIndex(), and CVC3::ExprValue::getVars().

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

Definition at line 946 of file expr_value.h.

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

Definition at line 949 of file expr_value.h.

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

Definition at line 952 of file expr_value.h.

virtual bool CVC3::ExprClosure::isClosure ( ) const
inlinevirtual

A LAMBDA-expression or a quantifier.

Reimplemented from CVC3::ExprValue.

Definition at line 953 of file expr_value.h.

Friends And Related Function Documentation

friend class Expr
friend

Definition at line 902 of file expr_value.h.

friend class ExprManager
friend

Definition at line 903 of file expr_value.h.

Member Data Documentation

std::vector<Expr> CVC3::ExprClosure::d_vars
private

Bound variables.

Definition at line 906 of file expr_value.h.

Referenced by getVars().

Expr CVC3::ExprClosure::d_body
private

The body of the quantifier/lambda.

Definition at line 908 of file expr_value.h.

Referenced by getBody().

std::vector<std::vector<Expr> > CVC3::ExprClosure::d_manual_triggers
private

Manual triggers. // added by yeting.

Definition at line 911 of file expr_value.h.

Referenced by getTriggers().


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