CVC3::BVConstExpr Class Reference

#include <bitvector_expr_value.h>

Inheritance diagram for CVC3::BVConstExpr:

Inheritance graph
[legend]
Collaboration diagram for CVC3::BVConstExpr:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Attributes


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.

Constructor

Definition at line 4361 of file theory_bitvector.cpp.

References d_bvconst, DebugAssert, and CVC3::TRACE.

Referenced by copy().

BVConstExpr::BVConstExpr ( ExprManager em,
std::vector< bool >  bvconst,
size_t  mmIndex,
ExprIndex  idx = 0 
)

Constructor.

Definition at line 4385 of file theory_bitvector.cpp.

References d_bvconst, and CVC3::TRACE.


Member Function Documentation

ExprValue* CVC3::BVConstExpr::copy ( ExprManager em,
ExprIndex  idx = 0 
) const [inline, virtual]

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(), d_bvconst, d_MMIndex, 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 4392 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 [inline, virtual]

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 [inline, virtual]

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 [inline, virtual]

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_bvconst, d_MMIndex, and CVC3::ExprValue::getMMIndex().

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

Overload operator new.

Reimplemented from CVC3::ExprValue.

Definition at line 62 of file bitvector_expr_value.h.

References CVC3::MemoryManager::newData().

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

Reimplemented from CVC3::ExprValue.

Definition at line 65 of file bitvector_expr_value.h.

References CVC3::MemoryManager::deleteData().

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

Overload operator delete.

Reimplemented from CVC3::ExprValue.

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.

References d_bvconst.

Referenced by CVC3::computeBVConst(), and getValue().

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

Definition at line 72 of file bitvector_expr_value.h.

References d_bvconst, DebugAssert, and size().

Referenced by CVC3::computeBVConst().


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(), computeHash(), copy(), getValue(), operator==(), and size().

size_t CVC3::BVConstExpr::d_MMIndex [private]

The registration index for ExprManager.

Definition at line 36 of file bitvector_expr_value.h.

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


The documentation for this class was generated from the following files:
Generated on Tue Jul 3 14:41:37 2007 for CVC3 by  doxygen 1.5.1