CVC3
Public Member Functions | Private Attributes

CVC3::BVConstExpr Class Reference

#include <bitvector_expr_value.h>

Inherits CVC3::ExprValue.

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.

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 [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 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 [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 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().


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: