CVC3
2.4.1
|
An expression subclass for bitvector constants. More...
#include <bitvector_expr_value.h>
Public Member Functions | |
BVConstExpr (ExprManager *em, std::string bvconst, size_t mmIndex, ExprIndex idx=0) | |
Constructor. More... | |
BVConstExpr (ExprManager *em, std::vector< bool > bvconst, size_t mmIndex, ExprIndex idx=0) | |
Constructor. More... | |
ExprValue * | copy (ExprManager *em, ExprIndex idx=0) const |
Make a clean copy of itself using the given ExprManager. More... | |
size_t | computeHash () const |
Non-caching hash function which actually computes the hash. More... | |
size_t | getMMIndex () const |
Get unique memory manager ID. More... | |
const ExprValue * | getExprValue () const |
Test whether the expression is a generic subclass. More... | |
bool | operator== (const ExprValue &ev2) const |
Only compare the bitvector constant, not the integer attribute. More... | |
void * | operator new (size_t size, MemoryManager *mm) |
void | operator delete (void *pMem, MemoryManager *mm) |
void | operator delete (void *) |
unsigned | size () const |
bool | getValue (int i) const |
![]() | |
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 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 | isClosure () const |
A LAMBDA-expression or a quantifier. 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 Rational & | getRational () const |
virtual const std::string & | getName () const |
Returns the string name of UCONST and BOUND_VAR expr's. More... | |
virtual const Expr & | getVar () const |
Returns the original Boolean variable (for BoolVarExprValue) More... | |
virtual Op | getOp () const |
Get the Op from an Apply Expr. More... | |
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 |
Private Attributes | |
std::vector< bool > | d_bvconst |
value of bitvector constant More... | |
size_t | d_MMIndex |
The registration index for ExprManager. More... | |
Additional Inherited Members | |
![]() | |
MemoryManager * | getMM (size_t MMIndex) |
Return the memory manager (for the benefit of subclasses) More... | |
ExprValue * | rebuild (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... | |
virtual Unsigned | computeSize () const |
Non-caching size function which actually computes the size. More... | |
![]() | |
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. More... | |
ExprManager * | d_em |
Our expr. manager. More... | |
![]() | |
static std::hash< char * > | s_charHash |
Return child with greatest height. More... | |
static std::hash< long int > | s_intHash |
An expression subclass for bitvector constants.
Definition at line 33 of file bitvector_expr_value.h.
BVConstExpr::BVConstExpr | ( | ExprManager * | em, |
std::string | bvconst, | ||
size_t | mmIndex, | ||
ExprIndex | idx = 0 |
||
) |
Constructor.
Definition at line 5521 of file theory_bitvector.cpp.
References d_bvconst, DebugAssert, and TRACE.
Referenced by copy().
BVConstExpr::BVConstExpr | ( | ExprManager * | em, |
std::vector< bool > | bvconst, | ||
size_t | mmIndex, | ||
ExprIndex | idx = 0 |
||
) |
Constructor.
Definition at line 5547 of file theory_bitvector.cpp.
References d_bvconst, CVC3::int2string(), and TRACE.
|
inlinevirtual |
Make a clean copy of itself using the given ExprManager.
Reimplemented from CVC3::ExprValue.
Definition at line 46 of file bitvector_expr_value.h.
References BVConstExpr(), CVC3::ExprManager::getMM(), and getMMIndex().
|
virtual |
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 5556 of file theory_bitvector.cpp.
References CVC3::BVCONST, d_bvconst, CVC3::ExprValue::hash(), HASH_VALUE_ONE, HASH_VALUE_ZERO, and PRIME.
|
inlinevirtual |
Get unique memory manager ID.
Reimplemented from CVC3::ExprValue.
Definition at line 52 of file bitvector_expr_value.h.
References d_MMIndex.
Referenced by copy().
|
inlinevirtual |
Test whether the expression is a generic subclass.
Reimplemented from CVC3::ExprValue.
Definition at line 54 of file bitvector_expr_value.h.
|
inlinevirtual |
Only compare the bitvector constant, not the integer attribute.
Reimplemented from CVC3::ExprValue.
Definition at line 57 of file bitvector_expr_value.h.
References d_MMIndex, and CVC3::ExprValue::getMMIndex().
|
inline |
Definition at line 62 of file bitvector_expr_value.h.
|
inline |
Definition at line 65 of file bitvector_expr_value.h.
|
inline |
Definition at line 69 of file bitvector_expr_value.h.
|
inline |
Definition at line 71 of file bitvector_expr_value.h.
Referenced by getValue().
|
inline |
Definition at line 72 of file bitvector_expr_value.h.
References DebugAssert, and size().
|
private |
value of bitvector constant
Definition at line 35 of file bitvector_expr_value.h.
Referenced by BVConstExpr(), and computeHash().
|
private |
The registration index for ExprManager.
Definition at line 36 of file bitvector_expr_value.h.
Referenced by getMMIndex(), and operator==().