cvc4-1.4
CVC4::BitVector Class Reference

#include <bitvector.h>

Public Member Functions

 BitVector (unsigned size, const Integer &val)
 
 BitVector (unsigned size=0)
 
 BitVector (unsigned size, unsigned int z)
 
 BitVector (unsigned size, unsigned long int z)
 
 BitVector (unsigned size, const BitVector &q)
 
 BitVector (const std::string &num, unsigned base=2)
 
 ~BitVector ()
 
Integer toInteger () const
 
BitVectoroperator= (const BitVector &x)
 
bool operator== (const BitVector &y) const
 
bool operator!= (const BitVector &y) const
 
BitVector concat (const BitVector &other) const
 
BitVector extract (unsigned high, unsigned low) const
 
BitVector operator^ (const BitVector &y) const
 
BitVector operator| (const BitVector &y) const
 
BitVector operator& (const BitVector &y) const
 
BitVector operator~ () const
 
bool operator< (const BitVector &y) const
 
bool operator> (const BitVector &y) const
 
bool operator<= (const BitVector &y) const
 
bool operator>= (const BitVector &y) const
 
BitVector operator+ (const BitVector &y) const
 
BitVector operator- (const BitVector &y) const
 
BitVector operator- () const
 
BitVector operator* (const BitVector &y) const
 
BitVector setBit (uint32_t i) const
 
bool isBitSet (uint32_t i) const
 
BitVector unsignedDivTotal (const BitVector &y) const
 Total division function that returns 0 when the denominator is 0. More...
 
BitVector unsignedRemTotal (const BitVector &y) const
 Total division function that returns 0 when the denominator is 0. More...
 
bool signedLessThan (const BitVector &y) const
 
bool unsignedLessThan (const BitVector &y) const
 
bool signedLessThanEq (const BitVector &y) const
 
bool unsignedLessThanEq (const BitVector &y) const
 
BitVector zeroExtend (unsigned amount) const
 
BitVector signExtend (unsigned amount) const
 
BitVector leftShift (const BitVector &y) const
 
BitVector logicalRightShift (const BitVector &y) const
 
BitVector arithRightShift (const BitVector &y) const
 
size_t hash () const
 
std::string toString (unsigned int base=2) const
 
unsigned getSize () const
 
const IntegergetValue () const
 
unsigned isPow2 ()
 Returns k is the integer is equal to 2^{k-1} and zero otherwise. More...
 

Detailed Description

Definition at line 29 of file bitvector.h.

Constructor & Destructor Documentation

◆ BitVector() [1/6]

CVC4::BitVector::BitVector ( unsigned  size,
const Integer val 
)
inline

Definition at line 53 of file bitvector.h.

◆ BitVector() [2/6]

CVC4::BitVector::BitVector ( unsigned  size = 0)
inline

Definition at line 58 of file bitvector.h.

◆ BitVector() [3/6]

CVC4::BitVector::BitVector ( unsigned  size,
unsigned int  z 
)
inline

Definition at line 61 of file bitvector.h.

References CVC4::Integer::modByPow2().

◆ BitVector() [4/6]

CVC4::BitVector::BitVector ( unsigned  size,
unsigned long int  z 
)
inline

Definition at line 66 of file bitvector.h.

References CVC4::Integer::modByPow2().

◆ BitVector() [5/6]

CVC4::BitVector::BitVector ( unsigned  size,
const BitVector q 
)
inline

Definition at line 71 of file bitvector.h.

◆ BitVector() [6/6]

CVC4::BitVector::BitVector ( const std::string &  num,
unsigned  base = 2 
)
inline

Definition at line 376 of file bitvector.h.

References CVC4::CheckArgument().

◆ ~BitVector()

CVC4::BitVector::~BitVector ( )
inline

Definition at line 76 of file bitvector.h.

Member Function Documentation

◆ arithRightShift()

BitVector CVC4::BitVector::arithRightShift ( const BitVector y) const
inline

◆ concat()

BitVector CVC4::BitVector::concat ( const BitVector other) const
inline

Definition at line 100 of file bitvector.h.

References CVC4::Integer::multiplyByPow2().

◆ extract()

BitVector CVC4::BitVector::extract ( unsigned  high,
unsigned  low 
) const
inline

Definition at line 104 of file bitvector.h.

References CVC4::Integer::extractBitRange().

◆ getSize()

unsigned CVC4::BitVector::getSize ( ) const
inline

Definition at line 355 of file bitvector.h.

◆ getValue()

const Integer& CVC4::BitVector::getValue ( ) const
inline

Definition at line 359 of file bitvector.h.

◆ hash()

size_t CVC4::BitVector::hash ( ) const
inline

Definition at line 338 of file bitvector.h.

References CVC4::Integer::hash().

Referenced by CVC4::BitVectorHashFunction::operator()().

◆ isBitSet()

bool CVC4::BitVector::isBitSet ( uint32_t  i) const
inline

Definition at line 188 of file bitvector.h.

References CVC4::CheckArgument(), and CVC4::Integer::isBitSet().

◆ isPow2()

unsigned CVC4::BitVector::isPow2 ( )
inline

Returns k is the integer is equal to 2^{k-1} and zero otherwise.

Returns
k if the integer is equal to 2^{k-1} and zero otherwise

Definition at line 368 of file bitvector.h.

References CVC4::Integer::isPow2().

◆ leftShift()

BitVector CVC4::BitVector::leftShift ( const BitVector y) const
inline

◆ logicalRightShift()

BitVector CVC4::BitVector::logicalRightShift ( const BitVector y) const
inline

◆ operator!=()

bool CVC4::BitVector::operator!= ( const BitVector y) const
inline

Definition at line 95 of file bitvector.h.

◆ operator&()

BitVector CVC4::BitVector::operator & ( const BitVector y) const
inline

Definition at line 125 of file bitvector.h.

References CVC4::Integer::bitwiseAnd(), and CVC4::CheckArgument().

◆ operator*()

BitVector CVC4::BitVector::operator* ( const BitVector y) const
inline

Definition at line 176 of file bitvector.h.

References CVC4::CheckArgument().

◆ operator+()

BitVector CVC4::BitVector::operator+ ( const BitVector y) const
inline

Definition at line 157 of file bitvector.h.

References CVC4::CheckArgument().

◆ operator-() [1/2]

BitVector CVC4::BitVector::operator- ( const BitVector y) const
inline

Definition at line 163 of file bitvector.h.

References CVC4::CheckArgument().

◆ operator-() [2/2]

BitVector CVC4::BitVector::operator- ( ) const
inline

Definition at line 171 of file bitvector.h.

◆ operator<()

bool CVC4::BitVector::operator< ( const BitVector y) const
inline

Definition at line 140 of file bitvector.h.

◆ operator<=()

bool CVC4::BitVector::operator<= ( const BitVector y) const
inline

Definition at line 148 of file bitvector.h.

◆ operator=()

BitVector& CVC4::BitVector::operator= ( const BitVector x)
inline

Definition at line 82 of file bitvector.h.

◆ operator==()

bool CVC4::BitVector::operator== ( const BitVector y) const
inline

Definition at line 90 of file bitvector.h.

◆ operator>()

bool CVC4::BitVector::operator> ( const BitVector y) const
inline

Definition at line 144 of file bitvector.h.

◆ operator>=()

bool CVC4::BitVector::operator>= ( const BitVector y) const
inline

Definition at line 152 of file bitvector.h.

◆ operator^()

BitVector CVC4::BitVector::operator^ ( const BitVector y) const
inline

Definition at line 113 of file bitvector.h.

References CVC4::Integer::bitwiseXor(), and CVC4::CheckArgument().

◆ operator|()

BitVector CVC4::BitVector::operator| ( const BitVector y) const
inline

Definition at line 119 of file bitvector.h.

References CVC4::Integer::bitwiseOr(), and CVC4::CheckArgument().

◆ operator~()

BitVector CVC4::BitVector::operator~ ( ) const
inline

Definition at line 131 of file bitvector.h.

References CVC4::Integer::bitwiseNot().

◆ setBit()

BitVector CVC4::BitVector::setBit ( uint32_t  i) const
inline

Definition at line 182 of file bitvector.h.

References CVC4::CheckArgument(), and CVC4::Integer::setBit().

◆ signedLessThan()

bool CVC4::BitVector::signedLessThan ( const BitVector y) const
inline

Definition at line 222 of file bitvector.h.

References CVC4::CheckArgument().

◆ signedLessThanEq()

bool CVC4::BitVector::signedLessThanEq ( const BitVector y) const
inline

Definition at line 239 of file bitvector.h.

References CVC4::CheckArgument().

◆ signExtend()

BitVector CVC4::BitVector::signExtend ( unsigned  amount) const
inline

Definition at line 265 of file bitvector.h.

References CVC4::Integer::extractBitRange(), and CVC4::Integer::oneExtend().

◆ toInteger()

Integer CVC4::BitVector::toInteger ( ) const
inline

Definition at line 78 of file bitvector.h.

◆ toString()

std::string CVC4::BitVector::toString ( unsigned int  base = 2) const
inline

Definition at line 342 of file bitvector.h.

References CVC4::Integer::toString().

Referenced by CVC4::operator<<().

◆ unsignedDivTotal()

BitVector CVC4::BitVector::unsignedDivTotal ( const BitVector y) const
inline

Total division function that returns 0 when the denominator is 0.

Definition at line 196 of file bitvector.h.

References CVC4::CheckArgument(), and CVC4::Integer::floorDivideQuotient().

◆ unsignedLessThan()

bool CVC4::BitVector::unsignedLessThan ( const BitVector y) const
inline

Definition at line 232 of file bitvector.h.

References CVC4::CheckArgument().

◆ unsignedLessThanEq()

bool CVC4::BitVector::unsignedLessThanEq ( const BitVector y) const
inline

Definition at line 249 of file bitvector.h.

References CVC4::CheckArgument().

◆ unsignedRemTotal()

BitVector CVC4::BitVector::unsignedRemTotal ( const BitVector y) const
inline

Total division function that returns 0 when the denominator is 0.

Definition at line 211 of file bitvector.h.

References CVC4::CheckArgument(), and CVC4::Integer::floorDivideRemainder().

◆ zeroExtend()

BitVector CVC4::BitVector::zeroExtend ( unsigned  amount) const
inline

Definition at line 261 of file bitvector.h.


The documentation for this class was generated from the following file: