22 #ifndef _cvc3__theory_bitvector__bitvector_expr_value_h_
23 #define _cvc3__theory_bitvector__bitvector_expr_value_h_
63 return mm->newData(
size);
69 void operator delete(
void*) { }
virtual size_t getMMIndex() const
Get unique memory manager ID.
size_t getMMIndex() const
Get unique memory manager ID.
bool getValue(int i) const
long unsigned ExprIndex
Expression index type.
#define DebugAssert(cond, str)
std::vector< bool > d_bvconst
value of bitvector constant
MemoryManager * getMM(size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
size_t d_MMIndex
The registration index for ExprManager.
An expression subclass for bitvector constants.
const ExprValue * getExprValue() const
Test whether the expression is a generic subclass.
bool operator==(const ExprValue &ev2) const
Only compare the bitvector constant, not the integer attribute.
BVConstExpr(ExprManager *em, std::string bvconst, size_t mmIndex, ExprIndex idx=0)
Constructor.
ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given ExprManager.
size_t computeHash() const
Non-caching hash function which actually computes the hash.
The base class for holding the actual data in expressions.