CVCL::BVConstExpr Class Reference

#include <bitvector_expr_value.h>

Inheritance diagram for CVCL::BVConstExpr:

[legend]Collaboration diagram for CVCL::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 *)

  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 41 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 4133 of file theory_bitvector.cpp. References d_bvconst, and CVCL::TRACE. Referenced by copy().

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

Constructor. Definition at line 4157 of file theory_bitvector.cpp. References d_bvconst, CVCL::int2string(), and CVCL::TRACE.

---

Member Function Documentation

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

Make a clean copy of itself using the given ExprManager. Reimplemented from CVCL::ExprValue. Definition at line 54 of file bitvector_expr_value.h. References BVConstExpr(), d_bvconst, d_MMIndex, CVCL::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 CVCL::ExprValue. Definition at line 4164 of file theory_bitvector.cpp. References CVCL::BVCONST, d_bvconst, and CVCL::hash().

size_t CVCL::BVConstExpr::getMMIndex (   )  const [inline, virtual]

Get unique memory manager ID. Reimplemented from CVCL::ExprValue. Definition at line 60 of file bitvector_expr_value.h. References d_MMIndex. Referenced by copy().

const ExprValue* CVCL::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 CVCL::ExprValue. Definition at line 62 of file bitvector_expr_value.h.

bool CVCL::BVConstExpr::operator== (  const ExprValue &  ev2  )  const [inline, virtual]

Only compare the bitvector constant, not the integer attribute. Reimplemented from CVCL::ExprValue. Definition at line 65 of file bitvector_expr_value.h. References d_bvconst, d_MMIndex, and CVCL::ExprValue::getMMIndex().

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

Overload operator new. Reimplemented from CVCL::ExprValue. Definition at line 70 of file bitvector_expr_value.h. References CVCL::MemoryManager::newData().

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

Overload operator delete. Reimplemented from CVCL::ExprValue. Definition at line 74 of file bitvector_expr_value.h.

unsigned CVCL::BVConstExpr::size (   )  const [inline]

Definition at line 76 of file bitvector_expr_value.h. References d_bvconst. Referenced by CVCL::computeBVConst(), CVCL::TheoryBitvector::getBVConstSize(), and getValue().

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

Definition at line 77 of file bitvector_expr_value.h. References d_bvconst, and size(). Referenced by CVCL::computeBVConst(), and CVCL::TheoryBitvector::getBVConstValue().

---

Member Data Documentation

std::vector<bool> CVCL::BVConstExpr::d_bvconst [private]

value of bitvector constant Definition at line 43 of file bitvector_expr_value.h. Referenced by BVConstExpr(), computeHash(), copy(), getValue(), operator==(), and size().

size_t CVCL::BVConstExpr::d_MMIndex [private]

The registration index for ExprManager. Definition at line 44 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

---