CVC3  2.4.1
Public Member Functions | Private Attributes | List of all members
CVC3::BVConstExpr Class Reference

An expression subclass for bitvector constants. More...

#include <bitvector_expr_value.h>

Inheritance diagram for CVC3::BVConstExpr:
CVC3::ExprValue

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

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

- 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...
 
virtual Unsigned computeSize () const
 Non-caching size function which actually computes the size. More...
 
- 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

An expression subclass for bitvector constants.

Definition at line 33 of file bitvector_expr_value.h.

Constructor & Destructor Documentation

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.

Member Function Documentation

ExprValue* CVC3::BVConstExpr::copy ( ExprManager em,
ExprIndex  idx = 0 
) const
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().

size_t BVConstExpr::computeHash ( ) const
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.

size_t CVC3::BVConstExpr::getMMIndex ( ) const
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().

const ExprValue* CVC3::BVConstExpr::getExprValue ( ) const
inlinevirtual

Test whether the expression is a generic subclass.

Returns
0 for the core classes, and getMMIndex() value for generic subclasses (those defined in DPs)

Reimplemented from CVC3::ExprValue.

Definition at line 54 of file bitvector_expr_value.h.

bool CVC3::BVConstExpr::operator== ( const ExprValue ev2) const
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().

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

Definition at line 62 of file bitvector_expr_value.h.

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

Definition at line 65 of file bitvector_expr_value.h.

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

Definition at line 69 of file bitvector_expr_value.h.

unsigned CVC3::BVConstExpr::size ( void  ) const
inline

Definition at line 71 of file bitvector_expr_value.h.

Referenced by getValue().

bool CVC3::BVConstExpr::getValue ( int  i) const
inline

Definition at line 72 of file bitvector_expr_value.h.

References DebugAssert, and size().

Member Data Documentation

std::vector<bool> CVC3::BVConstExpr::d_bvconst
private

value of bitvector constant

Definition at line 35 of file bitvector_expr_value.h.

Referenced by BVConstExpr(), and computeHash().

size_t CVC3::BVConstExpr::d_MMIndex
private

The registration index for ExprManager.

Definition at line 36 of file bitvector_expr_value.h.

Referenced by getMMIndex(), and operator==().


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