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) {
63 d_value = d_value.modByPow2(size);
67 : d_size(size), d_value(z) {
68 d_value = d_value.modByPow2(size);
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;
101 return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
105 return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
115 return BitVector(d_size, d_value.bitwiseXor(y.d_value));
121 return BitVector(d_size, d_value.bitwiseOr(y.d_value));
127 return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
132 return BitVector(d_size, d_value.bitwiseNot());
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;
190 return d_value.isBitSet(i);
199 if (y.d_value == 0) {
204 return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
212 if (y.d_value == 0) {
217 return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
225 Integer a = (*this).toSignedInt();
235 return d_value < y.d_value;
242 Integer a = (*this).toSignedInt();
252 return d_value <= y.d_value;
261 return BitVector(d_size + amount, d_value);
267 return BitVector(d_size + amount, d_value);
279 if (y.d_value >
Integer(d_size)) {
282 if (y.d_value == 0) {
294 if(y.d_value >
Integer(d_size)) {
307 if(y.d_value >
Integer(d_size)) {
315 if (y.d_value == 0) {
338 return d_value.hash() + d_size;
341 std::string
toString(
unsigned int base = 2)
const {
342 std::string str = d_value.toString(base);
343 if( base == 2 && d_size > str.size() ) {
345 for(
unsigned int i=0; i < d_size - str.size(); ++i ) {
368 return d_value.isPow2();
381 d_size = num.size() * 4;
409 : high(high), low(low) {}
412 return high == extract.
high && low == extract.
low;
421 size_t hash = extract.
low;
422 hash ^= extract.
high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
457 operator unsigned ()
const {
return size; }
463 : repeatAmount(repeatAmount) {}
464 operator unsigned ()
const {
return repeatAmount; }
470 : zeroExtendAmount(zeroExtendAmount) {}
471 operator unsigned ()
const {
return zeroExtendAmount; }
477 : signExtendAmount(signExtendAmount) {}
478 operator unsigned ()
const {
return signExtendAmount; }
484 : rotateLeftAmount(rotateLeftAmount) {}
485 operator unsigned ()
const {
return rotateLeftAmount; }
491 : rotateRightAmount(rotateRightAmount) {}
492 operator unsigned ()
const {
return rotateRightAmount; }
499 operator unsigned ()
const {
return size; }
502 template <
typename T>
516 return os <<
"[" << bv.
high <<
":" << bv.
low <<
"]";
521 return os <<
"[" << bv.
bitIndex <<
"]";
526 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
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
BitVectorSize(unsigned size)
Integer divByPow2(uint32_t exp) const
BitVectorBitOf(unsigned i)
BitVector setBit(uint32_t i) const
BitVector(unsigned size, const Integer &val)
Integer multiplyByPow2(uint32_t pow) const
Return this*(2^pow).
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.
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
BitVectorRotateRight(unsigned rotateRightAmount)
BitVectorSignExtend(unsigned signExtendAmount)
BitVector(unsigned size=0)
BitVector zeroExtend(unsigned amount) const
std::string toString(unsigned int base=2) 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)
BitVector(unsigned size, unsigned int z)
size_t operator()(const T &x) const
BitVector arithRightShift(const BitVector &y) const
BitVector logicalRightShift(const BitVector &y) const
std::ostream & operator<<(std::ostream &out, ModelFormatMode mode)
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