summaryrefslogtreecommitdiff
path: root/src/util/bitvector.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/bitvector.cpp')
-rw-r--r--src/util/bitvector.cpp360
1 files changed, 360 insertions, 0 deletions
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
new file mode 100644
index 000000000..2d94be875
--- /dev/null
+++ b/src/util/bitvector.cpp
@@ -0,0 +1,360 @@
+/********************* */
+/*! \file bitvector.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Liana Hadarean, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A fixed-size bit-vector.
+ **
+ ** A fixed-size bit-vector, implemented as a wrapper around Integer.
+ **
+ ** \todo document this file
+ **/
+
+#include "util/bitvector.h"
+
+namespace CVC4 {
+
+unsigned BitVector::getSize() const { return d_size; }
+
+const Integer& BitVector::getValue() const { return d_value; }
+
+Integer BitVector::toInteger() const { return d_value; }
+
+Integer BitVector::toSignedInteger() const
+{
+ unsigned size = d_size;
+ Integer sign_bit = d_value.extractBitRange(1, size - 1);
+ Integer val = d_value.extractBitRange(size - 1, 0);
+ Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
+ return res;
+}
+
+std::string BitVector::toString(unsigned int base) const
+{
+ std::string str = d_value.toString(base);
+ if (base == 2 && d_size > str.size())
+ {
+ std::string zeroes;
+ for (unsigned int i = 0; i < d_size - str.size(); ++i)
+ {
+ zeroes.append("0");
+ }
+ return zeroes + str;
+ }
+ else
+ {
+ return str;
+ }
+}
+
+size_t BitVector::hash() const
+{
+ return d_value.hash() + d_size;
+}
+
+BitVector BitVector::setBit(uint32_t i) const
+{
+ CheckArgument(i < d_size, i);
+ Integer res = d_value.setBit(i);
+ return BitVector(d_size, res);
+}
+
+bool BitVector::isBitSet(uint32_t i) const
+{
+ CheckArgument(i < d_size, i);
+ return d_value.isBitSet(i);
+}
+
+unsigned BitVector::isPow2() const
+{
+ return d_value.isPow2();
+}
+
+/* -----------------------------------------------------------------------
+ ** Operators
+ * ----------------------------------------------------------------------- */
+
+/* String Operations ----------------------------------------------------- */
+
+BitVector BitVector::concat(const BitVector& other) const
+{
+ return BitVector(d_size + other.d_size,
+ (d_value.multiplyByPow2(other.d_size)) + other.d_value);
+}
+
+BitVector BitVector::extract(unsigned high, unsigned low) const
+{
+ return BitVector(high - low + 1,
+ d_value.extractBitRange(high - low + 1, low));
+}
+
+/* (Dis)Equality --------------------------------------------------------- */
+
+bool BitVector::operator==(const BitVector& y) const
+{
+ if (d_size != y.d_size) return false;
+ return d_value == y.d_value;
+}
+
+bool BitVector::operator!=(const BitVector& y) const
+{
+ if (d_size != y.d_size) return true;
+ return d_value != y.d_value;
+}
+
+/* Unsigned Inequality --------------------------------------------------- */
+
+bool BitVector::operator<(const BitVector& y) const
+{
+ return d_value < y.d_value;
+}
+
+bool BitVector::operator<=(const BitVector& y) const
+{
+ return d_value <= y.d_value;
+}
+
+bool BitVector::operator>(const BitVector& y) const
+{
+ return d_value > y.d_value;
+}
+
+bool BitVector::operator>=(const BitVector& y) const
+{
+ return d_value >= y.d_value;
+}
+
+bool BitVector::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 BitVector::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;
+}
+
+/* Signed Inequality ----------------------------------------------------- */
+
+bool BitVector::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).toSignedInteger();
+ Integer b = y.toSignedInteger();
+
+ return a < b;
+}
+
+bool BitVector::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).toSignedInteger();
+ Integer b = y.toSignedInteger();
+
+ return a <= b;
+}
+
+/* Bit-wise operations --------------------------------------------------- */
+
+BitVector BitVector::operator^(const BitVector& y) const
+{
+ CheckArgument(d_size == y.d_size, y);
+ return BitVector(d_size, d_value.bitwiseXor(y.d_value));
+}
+
+BitVector BitVector::operator|(const BitVector& y) const
+{
+ CheckArgument(d_size == y.d_size, y);
+ return BitVector(d_size, d_value.bitwiseOr(y.d_value));
+}
+
+BitVector BitVector::operator&(const BitVector& y) const
+{
+ CheckArgument(d_size == y.d_size, y);
+ return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
+}
+
+BitVector BitVector::operator~() const
+{
+ return BitVector(d_size, d_value.bitwiseNot());
+}
+
+/* Arithmetic operations ------------------------------------------------- */
+
+BitVector BitVector::operator+(const BitVector& y) const
+{
+ CheckArgument(d_size == y.d_size, y);
+ Integer sum = d_value + y.d_value;
+ return BitVector(d_size, sum);
+}
+
+BitVector BitVector::operator-(const BitVector& y) const
+{
+ CheckArgument(d_size == y.d_size, y);
+ // to maintain the invariant that we are only adding BitVectors of the
+ // same size
+ BitVector one(d_size, Integer(1));
+ return *this + ~y + one;
+}
+
+BitVector BitVector::operator-() const
+{
+ BitVector one(d_size, Integer(1));
+ return ~(*this) + one;
+}
+
+BitVector BitVector::operator*(const BitVector& y) const
+{
+ CheckArgument(d_size == y.d_size, y);
+ Integer prod = d_value * y.d_value;
+ return BitVector(d_size, prod);
+}
+
+BitVector BitVector::unsignedDivTotal(const BitVector& y) const
+{
+ CheckArgument(d_size == y.d_size, y);
+ /* d_value / 0 = -1 = 2^d_size - 1 */
+ if (y.d_value == 0)
+ {
+ return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
+ }
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value > 0, y);
+ return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
+}
+
+BitVector BitVector::unsignedRemTotal(const BitVector& y) const
+{
+ CheckArgument(d_size == y.d_size, y);
+ if (y.d_value == 0)
+ {
+ return BitVector(d_size, d_value);
+ }
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value > 0, y);
+ return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
+}
+
+/* Extend operations ----------------------------------------------------- */
+
+BitVector BitVector::zeroExtend(unsigned n) const
+{
+ return BitVector(d_size + n, d_value);
+}
+
+BitVector BitVector::signExtend(unsigned n) const
+{
+ Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
+ if (sign_bit == Integer(0))
+ {
+ return BitVector(d_size + n, d_value);
+ }
+ Integer val = d_value.oneExtend(d_size, n);
+ return BitVector(d_size + n, val);
+}
+
+/* Shift operations ------------------------------------------------------ */
+
+BitVector BitVector::leftShift(const BitVector& y) const
+{
+ if (y.d_value > Integer(d_size))
+ {
+ return BitVector(d_size, Integer(0));
+ }
+ if (y.d_value == 0)
+ {
+ return *this;
+ }
+ // making sure we don't lose information casting
+ CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
+ uint32_t amount = y.d_value.toUnsignedInt();
+ Integer res = d_value.multiplyByPow2(amount);
+ return BitVector(d_size, res);
+}
+
+BitVector BitVector::logicalRightShift(const BitVector& y) const
+{
+ if (y.d_value > Integer(d_size))
+ {
+ return BitVector(d_size, Integer(0));
+ }
+ // making sure we don't lose information casting
+ CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
+ uint32_t amount = y.d_value.toUnsignedInt();
+ Integer res = d_value.divByPow2(amount);
+ return BitVector(d_size, res);
+}
+
+BitVector BitVector::arithRightShift(const BitVector& y) const
+{
+ Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
+ if (y.d_value > Integer(d_size))
+ {
+ if (sign_bit == Integer(0))
+ {
+ return BitVector(d_size, Integer(0));
+ }
+ else
+ {
+ return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
+ }
+ }
+
+ if (y.d_value == 0)
+ {
+ return *this;
+ }
+
+ // making sure we don't lose information casting
+ CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
+
+ uint32_t amount = y.d_value.toUnsignedInt();
+ Integer rest = d_value.divByPow2(amount);
+
+ if (sign_bit == Integer(0))
+ {
+ return BitVector(d_size, rest);
+ }
+ Integer res = rest.oneExtend(d_size - amount, amount);
+ return BitVector(d_size, res);
+}
+
+/* -----------------------------------------------------------------------
+ ** Static helpers.
+ * ----------------------------------------------------------------------- */
+
+BitVector BitVector::mkOnes(unsigned size)
+{
+ CheckArgument(size > 0, size);
+ return BitVector(1, Integer(1)).signExtend(size - 1);
+}
+
+BitVector BitVector::mkMinSigned(unsigned size)
+{
+ CheckArgument(size > 0, size);
+ return BitVector(size).setBit(size - 1);
+}
+
+BitVector BitVector::mkMaxSigned(unsigned size)
+{
+ CheckArgument(size > 0, size);
+ return ~BitVector::mkMinSigned(size);
+}
+
+} // namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback