20 #ifndef __CVC4__BITVECTOR_H 21 #define __CVC4__BITVECTOR_H 25 #include "util/integer.h" 43 unsigned size = d_size;
55 d_value(val.modByPow2(size))
59 : d_size(size), d_value(0) {}
62 : d_size(size), d_value(z) {
67 : d_size(size), d_value(z) {
72 : d_size(size), d_value(q.d_value) {}
74 BitVector(
const std::string& num,
unsigned base = 2);
91 if (d_size != y.d_size)
return false;
92 return d_value == y.d_value;
96 if (d_size != y.d_size)
return true;
97 return d_value != y.d_value;
141 return d_value < y.d_value;
145 return d_value > y.d_value ;
149 return d_value <= y.d_value;
153 return d_value >= y.d_value ;
159 Integer sum = d_value + y.d_value;
168 return *
this + ~y + one;
173 return ~(*this) + one;
178 Integer prod = d_value * y.d_value;
199 if (y.d_value == 0) {
213 if (y.d_value == 0) {
226 Integer a = (*this).toSignedInt();
236 return d_value < y.d_value;
243 Integer a = (*this).toSignedInt();
253 return d_value <= y.d_value;
262 return BitVector(d_size + amount, d_value);
268 return BitVector(d_size + amount, d_value);
280 if (y.d_value >
Integer(d_size)) {
283 if (y.d_value == 0) {
295 if(y.d_value >
Integer(d_size)) {
308 if(y.d_value >
Integer(d_size)) {
316 if (y.d_value == 0) {
339 return d_value.
hash() + d_size;
342 std::string
toString(
unsigned int base = 2)
const {
343 std::string str = d_value.
toString(base);
344 if( base == 2 && d_size > str.size() ) {
346 for(
unsigned int i=0; i < d_size - str.size(); ++i ) {
382 d_size = num.size() * 4;
410 : high(high), low(low) {}
413 return high == extract.
high && low == extract.
low;
422 size_t hash = extract.
low;
423 hash ^= extract.
high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
458 operator unsigned ()
const {
return size; }
464 : repeatAmount(repeatAmount) {}
465 operator unsigned ()
const {
return repeatAmount; }
471 : zeroExtendAmount(zeroExtendAmount) {}
472 operator unsigned ()
const {
return zeroExtendAmount; }
478 : signExtendAmount(signExtendAmount) {}
479 operator unsigned ()
const {
return signExtendAmount; }
485 : rotateLeftAmount(rotateLeftAmount) {}
486 operator unsigned ()
const {
return rotateLeftAmount; }
492 : rotateRightAmount(rotateRightAmount) {}
493 operator unsigned ()
const {
return rotateRightAmount; }
500 operator unsigned ()
const {
return size; }
503 template <
typename T>
517 return os <<
"[" << bv.
high <<
":" << bv.
low <<
"]";
522 return os <<
"[" << bv.
bitIndex <<
"]";
527 return os <<
"[" << bv.
size <<
"]";
Hash function for the BitVectorBitOf objects.
Integer bitwiseXor(const Integer &y) const
Integer oneExtend(uint32_t size, uint32_t amount) const
Hash function for the BitVector constants.
Integer setBit(uint32_t i) const
BitVectorSize(unsigned size)
std::string toString(unsigned int base=2) const
BitVectorBitOf(unsigned i)
size_t hash() const
Computes the hash of the node from the first word of the numerator, the denominator.
bool unsignedLessThan(const BitVector &y) const
bool unsignedLessThanEq(const BitVector &y) const
BitVector(unsigned size, const Integer &val)
Integer floorDivideQuotient(const Integer &y) const
Returns the floor(this / y)
bool isBitSet(uint32_t i) const
The structure representing the extraction of one Boolean bit.
BitVector(unsigned size, unsigned long int z)
BitVectorZeroExtend(unsigned zeroExtendAmount)
std::ostream & operator<<(std::ostream &out, const UninterpretedConstant &uc)
BitVector unsignedDivTotal(const BitVector &y) const
Total division function that returns 0 when the denominator is 0.
uint32_t toUnsignedInt() const
const Integer & getValue() const
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
std::string toString(int base=10) const
BitVector arithRightShift(const BitVector &y) const
Integer extractBitRange(uint32_t bitCount, uint32_t low) const
See CLN Documentation.
unsigned rotateLeftAmount
BitVector leftShift(const BitVector &y) const
CVC4's exception base class and some associated utilities.
BitVectorRotateLeft(unsigned rotateLeftAmount)
size_t operator()(const BitVectorBitOf &b) const
unsigned isPow2()
Returns k is the integer is equal to 2^{k-1} and zero otherwise.
bool signedLessThanEq(const BitVector &y) const
size_t operator()(const T &x) const
BitVector setBit(uint32_t i) const
BitVectorRotateRight(unsigned rotateRightAmount)
BitVector extract(unsigned high, unsigned low) const
BitVectorSignExtend(unsigned signExtendAmount)
BitVector(unsigned size=0)
Integer modByPow2(uint32_t exp) const
BitVector zeroExtend(unsigned amount) const
unsigned zeroExtendAmount
Macros that should be defined everywhere during the building of the libraries and driver binary...
IntToBitVector(unsigned size)
Integer bitwiseNot() const
BitVector(unsigned size, unsigned int z)
Integer divByPow2(uint32_t exp) const
Integer multiplyByPow2(uint32_t pow) const
Return this*(2^pow).
BitVector unsignedRemTotal(const BitVector &y) const
Total division function that returns 0 when the denominator is 0.
size_t operator()(const BitVector &bv) const
Integer floorDivideRemainder(const Integer &y) const
Returns r == this - floor(this/y)*y.
BitVectorRepeat(unsigned repeatAmount)
unsigned rotateRightAmount
BitVector(unsigned size, const BitVector &q)
BitVector signExtend(unsigned amount) const
unsigned isPow2() const
Returns k if the integer is equal to 2^(k-1)
BitVector logicalRightShift(const BitVector &y) const
unsigned signExtendAmount
Integer toInteger() const
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)
BitVector concat(const BitVector &other) const
unsigned bitIndex
The index of the bit.
bool isBitSet(uint32_t i) const
Integer bitwiseAnd(const Integer &y) const
bool signedLessThan(const BitVector &y) const
Integer bitwiseOr(const Integer &y) const