CVC3::BVConstExpr Class Reference

#include <bitvector_expr_value.h>

Inheritance diagram for CVC3::BVConstExpr:

[legend]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.

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:

• bitvector_expr_value.h
• theory_bitvector.cpp

---