#include <bitvector_expr_value.h>

Inherits CVC3::ExprValue.

Collaboration diagram for CVC3::BVConstExpr:

[legend]

List of all members.

Public Member Functions

BVConstExpr (ExprManager *em, std::string bvconst, size_t mmIndex, ExprIndex idx=0)
Constructor.
BVConstExpr (ExprManager *em, std::vector< bool > 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.
size_t getMMIndex () const
Get unique memory manager ID.
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.
void * operator new (size_t size, MemoryManager *mm)
Overload operator new.
void operator delete (void *pMem, MemoryManager *mm)
void operator delete (void *)
Overload operator delete.
unsigned size () const
bool getValue (int i) const

Private Attributes

std::vector< bool > d_bvconst
value of bitvector constant
size_t d_MMIndex
The registration index for ExprManager.

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:

CVC3::BVConstExpr Class Reference

Public Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation