CVC3
|
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers. More...
#include <expr_value.h>
Inherits 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) | |
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. | |
![]() | |
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 | 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 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 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 | |
size_t | computeHash () const |
Non-caching hash function which actually computes the hash. | |
Unsigned | computeSize () const |
Non-caching size function which actually computes the size. | |
ExprValue * | copy (ExprManager *em, ExprIndex idx=0) const |
Make a clean copy of itself using the given memory manager. | |
![]() | |
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. | |
Private Member Functions | |
virtual size_t | getMMIndex () const |
Tell ExprManager who we are. | |
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 |
Private Attributes | |
std::vector< Expr > | d_vars |
Bound variables. | |
Expr | d_body |
The body of the quantifier/lambda. | |
std::vector< std::vector< Expr > > | d_manual_triggers |
Manual triggers. // added by yeting. | |
Friends | |
class | Expr |
class | ExprManager |
Additional Inherited Members | |
![]() | |
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) |
![]() | |
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 std::hash< char * > | s_charHash |
Return child with greatest height. | |
static std::hash< long int > | s_intHash |
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers.
Definition at line 901 of file expr_value.h.
|
inline |
Definition at line 929 of file expr_value.h.
References d_vars.
|
inline |
Definition at line 933 of file expr_value.h.
|
inline |
Definition at line 937 of file expr_value.h.
|
inlinevirtual |
Definition at line 942 of file expr_value.h.
|
inlineprivatevirtual |
Tell ExprManager who we are.
Reimplemented from CVC3::ExprValue.
Definition at line 913 of file expr_value.h.
References CVC3::EXPR_CLOSURE.
|
inlineprivatevirtual |
|
inlineprivatevirtual |
|
inlineprivatevirtual |
Reimplemented from CVC3::ExprValue.
Definition at line 917 of file expr_value.h.
References d_manual_triggers.
|
inlineprivatevirtual |
Reimplemented from CVC3::ExprValue.
Definition at line 918 of file expr_value.h.
References d_manual_triggers.
|
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.
|
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 d_body, CVC3::Expr::d_expr, and CVC3::ExprValue::getSize().
|
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().
|
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().
|
inline |
Definition at line 946 of file expr_value.h.
|
inline |
Definition at line 949 of file expr_value.h.
|
inline |
Definition at line 952 of file expr_value.h.
|
inlinevirtual |
A LAMBDA-expression or a quantifier.
Reimplemented from CVC3::ExprValue.
Definition at line 953 of file expr_value.h.
|
friend |
Definition at line 902 of file expr_value.h.
|
friend |
Definition at line 903 of file expr_value.h.
|
private |
Bound variables.
Definition at line 906 of file expr_value.h.
Referenced by ExprClosure(), and getVars().
|
private |
The body of the quantifier/lambda.
Definition at line 908 of file expr_value.h.
Referenced by computeSize(), and getBody().
|
private |
Manual triggers. // added by yeting.
Definition at line 911 of file expr_value.h.
Referenced by getTriggers(), and setTriggers().