Reorganized bitvector.h

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 770257f1a0869db6a0905bdbfb3a2a4e18473841..acc31a8b50633e40f6a1fbfc50ef905746183eb8 100644 (file)
--- 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.
    */