summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/util/bitvector.h170
1 files changed, 91 insertions, 79 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 770257f1a..acc31a8b5 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -67,6 +67,18 @@ public:
return *this;
}
+ BitVector concat (const BitVector& other) const {
+ return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
+ }
+
+ BitVector extract(unsigned high, unsigned low) const {
+ return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
+ }
+
+ /**
+ * Predicates
+ */
+
bool operator ==(const BitVector& y) const {
if (d_size != y.d_size) return false;
return d_value == y.d_value;
@@ -77,63 +89,96 @@ public:
return d_value != y.d_value;
}
- BitVector concat (const BitVector& other) const {
- return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
+ /**
+ * Unsigned predicates
+ */
+
+ bool operator <(const BitVector& y) const {
+ return d_value < y.d_value;
}
- BitVector extract(unsigned high, unsigned low) const {
- return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
+ bool unsignedLessThan(const BitVector& y) const {
+ CheckArgument(d_size == y.d_size, y);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value >= 0, y);
+ return d_value < y.d_value;
+ }
+
+ bool operator <=(const BitVector& y) const {
+ return d_value <= y.d_value;
+ }
+
+ bool unsignedLessThanEq(const BitVector& y) const {
+ CheckArgument(d_size == y.d_size, this);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value >= 0, y);
+ return d_value <= y.d_value;
+ }
+
+ bool operator >(const BitVector& y) const {
+ return d_value > y.d_value ;
+ }
+
+ bool operator >=(const BitVector& y) const {
+ return d_value >= y.d_value ;
+ }
+
+ /**
+ * Signed predicates
+ */
+
+ bool signedLessThan(const BitVector& y) const {
+ CheckArgument(d_size == y.d_size, y);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value >= 0, y);
+ Integer a = (*this).toSignedInt();
+ Integer b = y.toSignedInt();
+
+ return a < b;
+ }
+
+ bool signedLessThanEq(const BitVector& y) const {
+ CheckArgument(d_size == y.d_size, y);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value >= 0, y);
+ Integer a = (*this).toSignedInt();
+ Integer b = y.toSignedInt();
+
+ return a <= b;
}
/**
- * Bitwise operations on BitVectors
+ * Bitwise operations
*/
- // xor
+ /** xor */
BitVector operator ^(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
return BitVector(d_size, d_value.bitwiseXor(y.d_value));
}
- // or
+ /** or */
BitVector operator |(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
return BitVector(d_size, d_value.bitwiseOr(y.d_value));
}
- // and
+ /** and */
BitVector operator &(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
}
- // not
+ /** not */
BitVector operator ~() const {
return BitVector(d_size, d_value.bitwiseNot());
}
+
/**
- * Arithmetic operations on BitVectors
+ * Arithmetic operations
*/
-
- bool operator <(const BitVector& y) const {
- return d_value < y.d_value;
- }
-
- bool operator >(const BitVector& y) const {
- return d_value > y.d_value ;
- }
-
- bool operator <=(const BitVector& y) const {
- return d_value <= y.d_value;
- }
-
- bool operator >=(const BitVector& y) const {
- return d_value >= y.d_value ;
- }
-
-
BitVector operator +(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
Integer sum = d_value + y.d_value;
@@ -159,20 +204,10 @@ public:
return BitVector(d_size, prod);
}
- BitVector setBit(uint32_t i) const {
- CheckArgument(i < d_size, i);
- Integer res = d_value.setBit(i);
- return BitVector(d_size, res);
- }
-
- bool isBitSet(uint32_t i) const {
- CheckArgument(i < d_size, i);
- return d_value.isBitSet(i);
- }
-
/**
- * Total division function that returns 2^d_size-1 (signed: -1) when the
- * denominator is 0 (d_value / 0 = 2^d_size - 1)..
+ * Total division function.
+ * Returns 2^d_size-1 (signed: -1) when the denominator is zero
+ * (d_value / 0 = 2^d_size - 1).
*/
BitVector unsignedDivTotal (const BitVector& y) const {
@@ -187,8 +222,8 @@ public:
}
/**
- * Total remainder function that returns d_value when the denominator is 0
- * (d_value % 0 = d_value).
+ * Total remainder function.
+ * Returns d_value when the denominator is zero (d_value % 0 = d_value).
*/
BitVector unsignedRemTotal(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
@@ -201,44 +236,10 @@ public:
}
- bool signedLessThan(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value >= 0, y);
- Integer a = (*this).toSignedInt();
- Integer b = y.toSignedInt();
-
- return a < b;
- }
-
- bool unsignedLessThan(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value >= 0, y);
- return d_value < y.d_value;
- }
-
- bool signedLessThanEq(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, y);
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value >= 0, y);
- Integer a = (*this).toSignedInt();
- Integer b = y.toSignedInt();
-
- return a <= b;
- }
-
- bool unsignedLessThanEq(const BitVector& y) const {
- CheckArgument(d_size == y.d_size, this);
- CheckArgument(d_value >= 0, this);
- CheckArgument(y.d_value >= 0, y);
- return d_value <= y.d_value;
- }
-
-
/**
* Extend operations
*/
+
BitVector zeroExtend(unsigned amount) const {
return BitVector(d_size + amount, d_value);
}
@@ -254,7 +255,7 @@ public:
}
/**
- * Shifts on BitVectors
+ * Shifts
*/
BitVector leftShift(const BitVector& y) const {
if (y.d_value > Integer(d_size)) {
@@ -338,6 +339,17 @@ public:
return d_value;
}
+ BitVector setBit(uint32_t i) const {
+ CheckArgument(i < d_size, i);
+ Integer res = d_value.setBit(i);
+ return BitVector(d_size, res);
+ }
+
+ bool isBitSet(uint32_t i) const {
+ CheckArgument(i < d_size, i);
+ return d_value.isBitSet(i);
+ }
+
/**
* Return Integer corresponding to two's complement interpretation of bv.
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback