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.
std::ostream & operator<<(std::ostream &out, const Predicate &p)
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::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)