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 <<
"]";
BitVector leftShift(const BitVector &y) const
Hash function for the BitVectorBitOf objects.
Integer setBit(uint32_t i) const
bool isBitSet(uint32_t i) const
std::string toString(int base=10) const
Hash function for the BitVector constants.
size_t operator()(const BitVector &bv) const
bool signedLessThanEq(const BitVector &y) const
Integer toInteger() const
uint32_t toUnsignedInt() const
Integer floorDivideQuotient(const Integer &y) const
Returns the floor(this / y)
BitVectorSize(unsigned size)
Integer divByPow2(uint32_t exp) const
BitVectorBitOf(unsigned i)
BitVector setBit(uint32_t i) const
BitVector(unsigned size, const Integer &val)
bool isBitSet(uint32_t i) const
Integer multiplyByPow2(uint32_t pow) const
Return this*(2^pow).
size_t hash() const
Computes the hash of the node from the first word of the numerator, the denominator.
The structure representing the extraction of one Boolean bit.
BitVector(unsigned size, unsigned long int z)
BitVectorZeroExtend(unsigned zeroExtendAmount)
BitVector unsignedRemTotal(const BitVector &y) const
Total division function that returns 0 when the denominator is 0.
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
unsigned rotateLeftAmount
CVC4's exception base class and some associated utilities.
const Integer & getValue() const
BitVector concat(const BitVector &other) const
BitVectorRotateLeft(unsigned rotateLeftAmount)
BitVector unsignedDivTotal(const BitVector &y) const
Total division function that returns 0 when the denominator is 0.
unsigned isPow2()
Returns k is the integer is equal to 2^{k-1} and zero otherwise.
BitVectorRotateRight(unsigned rotateRightAmount)
BitVectorSignExtend(unsigned signExtendAmount)
BitVector(unsigned size=0)
Integer floorDivideRemainder(const Integer &y) const
Returns r == this - floor(this/y)*y.
BitVector zeroExtend(unsigned amount) const
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
std::string toString(unsigned int base=2) const
Integer bitwiseNot() const
unsigned zeroExtendAmount
BitVector signExtend(unsigned amount) const
Macros that should be defined everywhere during the building of the libraries and driver binary...
IntToBitVector(unsigned size)
Integer bitwiseXor(const Integer &y) const
Integer modByPow2(uint32_t exp) const
BitVector(unsigned size, unsigned int z)
size_t operator()(const T &x) const
BitVector arithRightShift(const BitVector &y) const
Integer bitwiseOr(const Integer &y) const
BitVector logicalRightShift(const BitVector &y) const
BitVectorRepeat(unsigned repeatAmount)
unsigned rotateRightAmount
BitVector(unsigned size, const BitVector &q)
bool unsignedLessThan(const BitVector &y) const
BitVector extract(unsigned high, unsigned low) const
Integer extractBitRange(uint32_t bitCount, uint32_t low) const
See CLN Documentation.
unsigned signExtendAmount
bool signedLessThan(const BitVector &y) const
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)
unsigned bitIndex
The index of the bit.
bool unsignedLessThanEq(const BitVector &y) const
Integer oneExtend(uint32_t size, uint32_t amount) const
size_t operator()(const BitVectorBitOf &b) const
Integer bitwiseAnd(const Integer &y) const
unsigned isPow2() const
Returns k if the integer is equal to 2^(k-1)