Split and document bitvector.h. (#1615)

3 files changed, 547 insertions, 355 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index ddee2e72b..4867b775b 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -20,6 +20,7 @@ libutil_la_SOURCES = \
 	abstract_value.h \
 	bin_heap.h \
 	bitvector.h \
+	bitvector.cpp \
 	bool.h \
 	cache.h \
 	cardinality.cpp \
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
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 114b111cb..5beaa20f4 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -12,8 +12,6 @@
  ** \brief A fixed-size bit-vector.
  **
  ** A fixed-size bit-vector, implemented as a wrapper around Integer.
- **
- ** \todo document this file
  **/
 
 #include "cvc4_public.h"
@@ -28,34 +26,35 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC BitVector {
-public:
-
-  BitVector(unsigned size, const Integer& val):
-    d_size(size),
-    d_value(val.modByPow2(size))
-      {}
+class CVC4_PUBLIC BitVector
+{
+ public:
+  BitVector(unsigned size, const Integer& val)
+      : d_size(size), d_value(val.modByPow2(size))
+  {
+  }
 
-  BitVector(unsigned size = 0)
-    : d_size(size), d_value(0) {}
+  BitVector(unsigned size = 0) : d_size(size), d_value(0) {}
 
-  BitVector(unsigned size, unsigned int z)
-    : d_size(size), d_value(z) {
+  BitVector(unsigned size, unsigned int z) : d_size(size), d_value(z)
+  {
     d_value = d_value.modByPow2(size);
   }
 
-  BitVector(unsigned size, unsigned long int z)
-    : d_size(size), d_value(z) {
+  BitVector(unsigned size, unsigned long int z) : d_size(size), d_value(z)
+  {
     d_value = d_value.modByPow2(size);
   }
 
   BitVector(unsigned size, const BitVector& q)
-    : d_size(size), d_value(q.d_value) {}
+      : d_size(size), d_value(q.d_value)
+  {
+  }
 
   BitVector(const std::string& num, unsigned base = 2)
   {
     CheckArgument(base == 2 || base == 16, base);
-    d_size = base == 2 ?  num.size() : num.size() * 4;
+    d_size = base == 2 ? num.size() : num.size() * 4;
     d_value = Integer(num, base);
   }
 
@@ -69,76 +68,28 @@ public:
     return *this;
   }
 
-  unsigned getSize() const
-  {
-    return d_size;
-  }
-
-  const Integer& getValue() const
-  {
-    return d_value;
-  }
-
-  Integer toInteger() const
-  {
-    return d_value;
-  }
+  /* Get size (bit-width). */
+  unsigned getSize() const;
+  /* Get value. */
+  const Integer& getValue() const;
 
-  /**
-   * Return Integer corresponding to two's complement interpretation of bv.
-   */
-  Integer 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;
-  }
+  /* Return value. */
+  Integer toInteger() const;
+  /* Return Integer corresponding to two's complement interpretation of this. */
+  Integer toSignedInteger() const;
+  /* Return (binary) string representation. */
+  std::string toString(unsigned int base = 2) const;
 
-  size_t hash() const
-  {
-    return d_value.hash() + d_size;
-  }
+  /* Return hash value. */
+  size_t hash() const;
 
-  std::string toString(unsigned int base = 2) 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;
-    }
-  }
+  /* Set bit at index 'i'. */
+  BitVector setBit(uint32_t i) const;
+  /* Return true if bit at index 'i' is set. */
+  bool isBitSet(uint32_t i) const;
 
-  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 k if the integer is equal to 2^{k-1} and zero otherwise.
-   */
-  unsigned isPow2() {
-    return d_value.isPow2();
-  }
+  /* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
+  unsigned isPow2() const;
 
   /* -----------------------------------------------------------------------
    ** Operators
@@ -146,262 +97,126 @@ public:
 
   /* String Operations ----------------------------------------------------- */
 
-  BitVector concat (const BitVector& other) const {
-    return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
-  }
+  /* Return the concatenation of this and bit-vector 'other'. */
+  BitVector concat(const BitVector& other) const;
 
-  BitVector extract(unsigned high, unsigned low) const {
-    return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
-  }
+  /* Return the bit range from index 'high' to index 'low'. */
+  BitVector extract(unsigned high, unsigned low) const;
 
   /* (Dis)Equality --------------------------------------------------------- */
 
-  bool operator ==(const BitVector& y) const {
-    if (d_size != y.d_size) return false;
-    return d_value == y.d_value;
-  }
+  /* Return true if this is equal to 'y'. */
+  bool operator==(const BitVector& y) const;
 
-  bool operator !=(const BitVector& y) const {
-    if (d_size != y.d_size) return true;
-    return d_value != y.d_value;
-  }
+  /* Return true if this is not equal to 'y'. */
+  bool operator!=(const BitVector& y) const;
 
   /* Unsigned Inequality --------------------------------------------------- */
 
-  bool operator <(const BitVector& y) const {
-    return d_value < y.d_value;
-  }
+  /* Return true if this is unsigned less than bit-vector 'y'. */
+  bool operator<(const BitVector& y) const;
 
-  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;
-  }
+  /* Return true if this is unsigned less than or equal to bit-vector 'y'. */
+  bool operator<=(const BitVector& y) const;
 
-  bool operator <=(const BitVector& y) const {
-    return d_value <= y.d_value;
-  }
+  /* Return true if this is unsigned greater than bit-vector 'y'. */
+  bool operator>(const BitVector& y) const;
 
-  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;
-  }
+  /* Return true if this is unsigned greater than or equal to bit-vector 'y'. */
+  bool operator>=(const BitVector& y) const;
 
-  bool operator >(const BitVector& y) const {
-    return d_value > y.d_value ;
-  }
+  /* Return true if this is unsigned less than bit-vector 'y'.
+   * This function is a synonym for operator < but performs additional
+   * argument checks.*/
+  bool unsignedLessThan(const BitVector& y) const;
 
-  bool operator >=(const BitVector& y) const {
-    return d_value >= y.d_value ;
-  }
+  /* Return true if this is unsigned less than or equal to bit-vector 'y'.
+   * This function is a synonym for operator >= but performs additional
+   * argument checks.*/
+  bool unsignedLessThanEq(const BitVector& y) const;
 
   /* Signed Inequality ----------------------------------------------------- */
 
-  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).toSignedInteger();
-    Integer b = y.toSignedInteger();
+  /* Return true if this is signed less than bit-vector 'y'. */
+  bool signedLessThan(const BitVector& y) const;
 
-    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).toSignedInteger();
-    Integer b = y.toSignedInteger();
-
-    return a <= b;
-  }
+  /* Return true if this is signed less than or equal to bit-vector 'y'. */
+  bool signedLessThanEq(const BitVector& y) const;
 
   /* Bit-wise operations --------------------------------------------------- */
 
-  /** 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 */
-  BitVector operator |(const BitVector& y) const {
-    CheckArgument(d_size == y.d_size, y);
-    return BitVector(d_size, d_value.bitwiseOr(y.d_value));
-  }
+  /* Return a bit-vector representing the bit-wise xor (this ^ y). */
+  BitVector operator^(const BitVector& y) const;
 
-  /** and */
-  BitVector operator &(const BitVector& y) const {
-    CheckArgument(d_size == y.d_size, y);
-    return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
-  }
+  /* Return a bit-vector representing the bit-wise or (this | y). */
+  BitVector operator|(const BitVector& y) const;
 
-  /** not */
-  BitVector operator ~() const {
-    return BitVector(d_size, d_value.bitwiseNot());
-  }
+  /* Return a bit-vector representing the bit-wise and (this & y). */
+  BitVector operator&(const BitVector& y) const;
 
+  /* Return a bit-vector representing the bit-wise not of this. */
+  BitVector operator~() const;
 
   /* Arithmetic operations ------------------------------------------------- */
 
-  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 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;
-  }
+  /* Return a bit-vector representing the addition (this + y). */
+  BitVector operator+(const BitVector& y) const;
 
-  BitVector operator -() const {
-    BitVector one(d_size, Integer(1));
-    return ~(*this) + one;
-  }
+  /* Return a bit-vector representing the subtraction (this - y). */
+  BitVector operator-(const BitVector& y) const;
 
-  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);
-  }
+  /* Return a bit-vector representing the negation of this. */
+  BitVector operator-() const;
 
-  /**
-   * 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 {
-
-    CheckArgument(d_size == y.d_size, y);
-    if (y.d_value == 0) {
-      // under division by zero return -1
-      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));
-  }
+  /* Return a bit-vector representing the multiplication (this * y). */
+  BitVector operator*(const BitVector& y) const;
 
-  /**
-   * 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);
-    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));
-  }
+  /* Total division function.
+   * Returns a bit-vector representing 2^d_size-1 (signed: -1) when the
+   * denominator is zero, and a bit-vector representing the unsigned division
+   * (this / y), otherwise.  */
+  BitVector unsignedDivTotal(const BitVector& y) const;
 
+  /* Total remainder function.
+   * Returns this when the denominator is zero, and the unsigned remainder
+   * (this % y), otherwise.  */
+  BitVector unsignedRemTotal(const BitVector& y) const;
 
   /* Extend operations ----------------------------------------------------- */
 
-  BitVector zeroExtend(unsigned amount) const {
-    return BitVector(d_size + amount, d_value);
-  }
+  /* Return a bit-vector representing this extended by 'n' zero bits. */
+  BitVector zeroExtend(unsigned n) const;
 
-  BitVector signExtend(unsigned amount) const {
-    Integer sign_bit = d_value.extractBitRange(1, d_size -1);
-    if(sign_bit == Integer(0)) {
-      return BitVector(d_size + amount, d_value);
-    } else {
-      Integer val = d_value.oneExtend(d_size, amount);
-      return BitVector(d_size+ amount, val);
-    }
-  }
+  /* Return a bit-vector representing this extended by 'n' bits of the value
+   * of the signed bit. */
+  BitVector signExtend(unsigned n) const;
 
   /* Shift operations ------------------------------------------------------ */
 
-  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);
-  }
+  /* Return a bit-vector representing a left shift of this by 'y'. */
+  BitVector leftShift(const BitVector& y) const;
 
-  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);
-  }
+  /* Return a bit-vector representing a logical right shift of this by 'y'. */
+  BitVector logicalRightShift(const BitVector& y) const;
 
-  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);
-  }
+  /* Return a bit-vector representing an arithmetic right shift of this
+   * by 'y'.*/
+  BitVector arithRightShift(const BitVector& y) const;
 
   /* -----------------------------------------------------------------------
    ** Static helpers.
    * ----------------------------------------------------------------------- */
 
   /* Create bit-vector of ones of given size. */
-  static BitVector mkOnes(unsigned size)
-  {
-    CheckArgument(size > 0, size);
-    return BitVector(1, Integer(1)).signExtend(size - 1);
-  }
+  static BitVector mkOnes(unsigned size);
 
   /* Create bit-vector representing the minimum signed value of given size. */
-  static BitVector mkMinSigned(unsigned size)
-  {
-    CheckArgument(size > 0, size);
-    return BitVector(size).setBit(size - 1);
-  }
+  static BitVector mkMinSigned(unsigned size);
 
   /* Create bit-vector representing the maximum signed value of given size. */
-  static BitVector mkMaxSigned(unsigned size)
-  {
-    CheckArgument(size > 0, size);
-    return ~BitVector::mkMinSigned(size);
-  }
+  static BitVector mkMaxSigned(unsigned size);
 
  private:
-
   /**
    * Class invariants:
    *  - no overflows: 2^d_size < d_value
@@ -411,9 +226,7 @@ public:
   unsigned d_size;
   Integer d_value;
 
-};/* class BitVector */
-
-
+}; /* class BitVector */
 
 /* -----------------------------------------------------------------------
  ** BitVector structs
@@ -442,66 +255,78 @@ struct CVC4_PUBLIC BitVectorExtract
 /**
  * The structure representing the extraction of one Boolean bit.
  */
-struct CVC4_PUBLIC BitVectorBitOf {
+struct CVC4_PUBLIC BitVectorBitOf
+{
   /** The index of the bit */
   unsigned bitIndex;
-  BitVectorBitOf(unsigned i)
-    : bitIndex(i) {}
+  BitVectorBitOf(unsigned i) : bitIndex(i) {}
 
-  bool operator == (const BitVectorBitOf& other) const {
+  bool operator==(const BitVectorBitOf& other) const
+  {
     return bitIndex == other.bitIndex;
   }
-};/* struct BitVectorBitOf */
+}; /* struct BitVectorBitOf */
 
-struct CVC4_PUBLIC BitVectorSize {
+struct CVC4_PUBLIC BitVectorSize
+{
   unsigned size;
-  BitVectorSize(unsigned size)
-  : size(size) {}
-  operator unsigned () const { return size; }
-};/* struct BitVectorSize */
+  BitVectorSize(unsigned size) : size(size) {}
+  operator unsigned() const { return size; }
+}; /* struct BitVectorSize */
 
-struct CVC4_PUBLIC BitVectorRepeat {
+struct CVC4_PUBLIC BitVectorRepeat
+{
   unsigned repeatAmount;
-  BitVectorRepeat(unsigned repeatAmount)
-  : repeatAmount(repeatAmount) {}
-  operator unsigned () const { return repeatAmount; }
-};/* struct BitVectorRepeat */
+  BitVectorRepeat(unsigned repeatAmount) : repeatAmount(repeatAmount) {}
+  operator unsigned() const { return repeatAmount; }
+}; /* struct BitVectorRepeat */
 
-struct CVC4_PUBLIC BitVectorZeroExtend {
+struct CVC4_PUBLIC BitVectorZeroExtend
+{
   unsigned zeroExtendAmount;
   BitVectorZeroExtend(unsigned zeroExtendAmount)
-  : zeroExtendAmount(zeroExtendAmount) {}
-  operator unsigned () const { return zeroExtendAmount; }
-};/* struct BitVectorZeroExtend */
+      : zeroExtendAmount(zeroExtendAmount)
+  {
+  }
+  operator unsigned() const { return zeroExtendAmount; }
+}; /* struct BitVectorZeroExtend */
 
-struct CVC4_PUBLIC BitVectorSignExtend {
+struct CVC4_PUBLIC BitVectorSignExtend
+{
   unsigned signExtendAmount;
   BitVectorSignExtend(unsigned signExtendAmount)
-  : signExtendAmount(signExtendAmount) {}
-  operator unsigned () const { return signExtendAmount; }
-};/* struct BitVectorSignExtend */
+      : signExtendAmount(signExtendAmount)
+  {
+  }
+  operator unsigned() const { return signExtendAmount; }
+}; /* struct BitVectorSignExtend */
 
-struct CVC4_PUBLIC BitVectorRotateLeft {
+struct CVC4_PUBLIC BitVectorRotateLeft
+{
   unsigned rotateLeftAmount;
   BitVectorRotateLeft(unsigned rotateLeftAmount)
-  : rotateLeftAmount(rotateLeftAmount) {}
-  operator unsigned () const { return rotateLeftAmount; }
-};/* struct BitVectorRotateLeft */
+      : rotateLeftAmount(rotateLeftAmount)
+  {
+  }
+  operator unsigned() const { return rotateLeftAmount; }
+}; /* struct BitVectorRotateLeft */
 
-struct CVC4_PUBLIC BitVectorRotateRight {
+struct CVC4_PUBLIC BitVectorRotateRight
+{
   unsigned rotateRightAmount;
   BitVectorRotateRight(unsigned rotateRightAmount)
-  : rotateRightAmount(rotateRightAmount) {}
-  operator unsigned () const { return rotateRightAmount; }
-};/* struct BitVectorRotateRight */
+      : rotateRightAmount(rotateRightAmount)
+  {
+  }
+  operator unsigned() const { return rotateRightAmount; }
+}; /* struct BitVectorRotateRight */
 
-struct CVC4_PUBLIC IntToBitVector {
+struct CVC4_PUBLIC IntToBitVector
+{
   unsigned size;
-  IntToBitVector(unsigned size)
-  : size(size) {}
-  operator unsigned () const { return size; }
-};/* struct IntToBitVector */
-
+  IntToBitVector(unsigned size) : size(size) {}
+  operator unsigned() const { return size; }
+}; /* struct IntToBitVector */
 
 /* -----------------------------------------------------------------------
  ** Hash Function structs
@@ -510,64 +335,70 @@ struct CVC4_PUBLIC IntToBitVector {
 /*
  * Hash function for the BitVector constants.
  */
-struct CVC4_PUBLIC BitVectorHashFunction {
-  inline size_t operator()(const BitVector& bv) const {
-    return bv.hash();
-  }
-};/* struct BitVectorHashFunction */
+struct CVC4_PUBLIC BitVectorHashFunction
+{
+  inline size_t operator()(const BitVector& bv) const { return bv.hash(); }
+}; /* struct BitVectorHashFunction */
 
 /**
  * Hash function for the BitVectorExtract objects.
  */
-struct CVC4_PUBLIC BitVectorExtractHashFunction {
-  size_t operator()(const BitVectorExtract& extract) const {
+struct CVC4_PUBLIC BitVectorExtractHashFunction
+{
+  size_t operator()(const BitVectorExtract& extract) const
+  {
     size_t hash = extract.low;
     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
     return hash;
   }
-};/* struct BitVectorExtractHashFunction */
+}; /* struct BitVectorExtractHashFunction */
 
 /**
  * Hash function for the BitVectorBitOf objects.
  */
-struct CVC4_PUBLIC BitVectorBitOfHashFunction {
-  size_t operator()(const BitVectorBitOf& b) const {
-    return b.bitIndex;
-  }
-};/* struct BitVectorBitOfHashFunction */
+struct CVC4_PUBLIC BitVectorBitOfHashFunction
+{
+  size_t operator()(const BitVectorBitOf& b) const { return b.bitIndex; }
+}; /* struct BitVectorBitOfHashFunction */
 
 template <typename T>
-struct CVC4_PUBLIC UnsignedHashFunction {
-  inline size_t operator()(const T& x) const {
-    return (size_t)x;
-  }
-};/* struct UnsignedHashFunction */
-
+struct CVC4_PUBLIC UnsignedHashFunction
+{
+  inline size_t operator()(const T& x) const { return (size_t)x; }
+}; /* struct UnsignedHashFunction */
 
 /* -----------------------------------------------------------------------
  ** Output stream
  * ----------------------------------------------------------------------- */
 
-inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
+inline std::ostream& operator<<(std::ostream& os,
+                                const BitVector& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVector& bv)
+{
   return os << bv.toString();
 }
 
-inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
+inline std::ostream& operator<<(std::ostream& os,
+                                const BitVectorExtract& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv)
+{
   return os << "[" << bv.high << ":" << bv.low << "]";
 }
 
-inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
+inline std::ostream& operator<<(std::ostream& os,
+                                const BitVectorBitOf& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv)
+{
   return os << "[" << bv.bitIndex << "]";
 }
 
-inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) CVC4_PUBLIC;
-inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) {
+inline std::ostream& operator<<(std::ostream& os,
+                                const IntToBitVector& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
+{
   return os << "[" << bv.size << "]";
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC4
 
 #endif /* __CVC4__BITVECTOR_H */