src/util/bitvector.cpp

   1 /*********************                                                        */
   2 /*! \file bitvector.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Liana Hadarean, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A fixed-size bit-vector.
  13  **
  14  ** A fixed-size bit-vector, implemented as a wrapper around Integer.
  15  **
  16  ** \todo document this file
  17  **/
  18
  19 #include "util/bitvector.h"
  20
  21 namespace CVC4 {
  22
  23 unsigned BitVector::getSize() const { return d_size; }
  24
  25 const Integer& BitVector::getValue() const { return d_value; }
  26
  27 Integer BitVector::toInteger() const { return d_value; }
  28
  29 Integer BitVector::toSignedInteger() const
  30 {
  31   unsigned size = d_size;
  32   Integer sign_bit = d_value.extractBitRange(1, size - 1);
  33   Integer val = d_value.extractBitRange(size - 1, 0);
  34   Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
  35   return res;
  36 }
  37
  38 std::string BitVector::toString(unsigned int base) const
  39 {
  40   std::string str = d_value.toString(base);
  41   if (base == 2 && d_size > str.size())
  42   {
  43     std::string zeroes;
  44     for (unsigned int i = 0; i < d_size - str.size(); ++i)
  45     {
  46       zeroes.append("0");
  47     }
  48     return zeroes + str;
  49   }
  50   else
  51   {
  52     return str;
  53   }
  54 }
  55
  56 size_t BitVector::hash() const
  57 {
  58   return d_value.hash() + d_size;
  59 }
  60
  61 BitVector BitVector::setBit(uint32_t i) const
  62 {
  63   CheckArgument(i < d_size, i);
  64   Integer res = d_value.setBit(i);
  65   return BitVector(d_size, res);
  66 }
  67
  68 bool BitVector::isBitSet(uint32_t i) const
  69 {
  70   CheckArgument(i < d_size, i);
  71   return d_value.isBitSet(i);
  72 }
  73
  74 unsigned BitVector::isPow2() const
  75 {
  76   return d_value.isPow2();
  77 }
  78
  79 /* -----------------------------------------------------------------------
  80  ** Operators
  81  * ----------------------------------------------------------------------- */
  82
  83 /* String Operations ----------------------------------------------------- */
  84
  85 BitVector BitVector::concat(const BitVector& other) const
  86 {
  87   return BitVector(d_size + other.d_size,
  88                    (d_value.multiplyByPow2(other.d_size)) + other.d_value);
  89 }
  90
  91 BitVector BitVector::extract(unsigned high, unsigned low) const
  92 {
  93   CheckArgument(high < d_size, high);
  94   CheckArgument(low <= high, low);
  95   return BitVector(high - low + 1,
  96                    d_value.extractBitRange(high - low + 1, low));
  97 }
  98
  99 /* (Dis)Equality --------------------------------------------------------- */
 100
 101 bool BitVector::operator==(const BitVector& y) const
 102 {
 103   if (d_size != y.d_size) return false;
 104   return d_value == y.d_value;
 105 }
 106
 107 bool BitVector::operator!=(const BitVector& y) const
 108 {
 109   if (d_size != y.d_size) return true;
 110   return d_value != y.d_value;
 111 }
 112
 113 /* Unsigned Inequality --------------------------------------------------- */
 114
 115 bool BitVector::operator<(const BitVector& y) const
 116 {
 117   return d_value < y.d_value;
 118 }
 119
 120 bool BitVector::operator<=(const BitVector& y) const
 121 {
 122   return d_value <= y.d_value;
 123 }
 124
 125 bool BitVector::operator>(const BitVector& y) const
 126 {
 127   return d_value > y.d_value;
 128 }
 129
 130 bool BitVector::operator>=(const BitVector& y) const
 131 {
 132   return d_value >= y.d_value;
 133 }
 134
 135 bool BitVector::unsignedLessThan(const BitVector& y) const
 136 {
 137   CheckArgument(d_size == y.d_size, y);
 138   CheckArgument(d_value >= 0, this);
 139   CheckArgument(y.d_value >= 0, y);
 140   return d_value < y.d_value;
 141 }
 142
 143 bool BitVector::unsignedLessThanEq(const BitVector& y) const
 144 {
 145   CheckArgument(d_size == y.d_size, this);
 146   CheckArgument(d_value >= 0, this);
 147   CheckArgument(y.d_value >= 0, y);
 148   return d_value <= y.d_value;
 149 }
 150
 151 /* Signed Inequality ----------------------------------------------------- */
 152
 153 bool BitVector::signedLessThan(const BitVector& y) const
 154 {
 155   CheckArgument(d_size == y.d_size, y);
 156   CheckArgument(d_value >= 0, this);
 157   CheckArgument(y.d_value >= 0, y);
 158   Integer a = (*this).toSignedInteger();
 159   Integer b = y.toSignedInteger();
 160
 161   return a < b;
 162 }
 163
 164 bool BitVector::signedLessThanEq(const BitVector& y) const
 165 {
 166   CheckArgument(d_size == y.d_size, y);
 167   CheckArgument(d_value >= 0, this);
 168   CheckArgument(y.d_value >= 0, y);
 169   Integer a = (*this).toSignedInteger();
 170   Integer b = y.toSignedInteger();
 171
 172   return a <= b;
 173 }
 174
 175 /* Bit-wise operations --------------------------------------------------- */
 176
 177 BitVector BitVector::operator^(const BitVector& y) const
 178 {
 179   CheckArgument(d_size == y.d_size, y);
 180   return BitVector(d_size, d_value.bitwiseXor(y.d_value));
 181 }
 182
 183 BitVector BitVector::operator|(const BitVector& y) const
 184 {
 185   CheckArgument(d_size == y.d_size, y);
 186   return BitVector(d_size, d_value.bitwiseOr(y.d_value));
 187 }
 188
 189 BitVector BitVector::operator&(const BitVector& y) const
 190 {
 191   CheckArgument(d_size == y.d_size, y);
 192   return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
 193 }
 194
 195 BitVector BitVector::operator~() const
 196 {
 197   return BitVector(d_size, d_value.bitwiseNot());
 198 }
 199
 200 /* Arithmetic operations ------------------------------------------------- */
 201
 202 BitVector BitVector::operator+(const BitVector& y) const
 203 {
 204   CheckArgument(d_size == y.d_size, y);
 205   Integer sum = d_value + y.d_value;
 206   return BitVector(d_size, sum);
 207 }
 208
 209 BitVector BitVector::operator-(const BitVector& y) const
 210 {
 211   CheckArgument(d_size == y.d_size, y);
 212   // to maintain the invariant that we are only adding BitVectors of the
 213   // same size
 214   BitVector one(d_size, Integer(1));
 215   return *this + ~y + one;
 216 }
 217
 218 BitVector BitVector::operator-() const
 219 {
 220   BitVector one(d_size, Integer(1));
 221   return ~(*this) + one;
 222 }
 223
 224 BitVector BitVector::operator*(const BitVector& y) const
 225 {
 226   CheckArgument(d_size == y.d_size, y);
 227   Integer prod = d_value * y.d_value;
 228   return BitVector(d_size, prod);
 229 }
 230
 231 BitVector BitVector::unsignedDivTotal(const BitVector& y) const
 232 {
 233   CheckArgument(d_size == y.d_size, y);
 234   /* d_value / 0 = -1 = 2^d_size - 1 */
 235   if (y.d_value == 0)
 236   {
 237     return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
 238   }
 239   CheckArgument(d_value >= 0, this);
 240   CheckArgument(y.d_value > 0, y);
 241   return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
 242 }
 243
 244 BitVector BitVector::unsignedRemTotal(const BitVector& y) const
 245 {
 246   CheckArgument(d_size == y.d_size, y);
 247   if (y.d_value == 0)
 248   {
 249     return BitVector(d_size, d_value);
 250   }
 251   CheckArgument(d_value >= 0, this);
 252   CheckArgument(y.d_value > 0, y);
 253   return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
 254 }
 255
 256 /* Extend operations ----------------------------------------------------- */
 257
 258 BitVector BitVector::zeroExtend(unsigned n) const
 259 {
 260   return BitVector(d_size + n, d_value);
 261 }
 262
 263 BitVector BitVector::signExtend(unsigned n) const
 264 {
 265   Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
 266   if (sign_bit == Integer(0))
 267   {
 268     return BitVector(d_size + n, d_value);
 269   }
 270   Integer val = d_value.oneExtend(d_size, n);
 271   return BitVector(d_size + n, val);
 272 }
 273
 274 /* Shift operations ------------------------------------------------------ */
 275
 276 BitVector BitVector::leftShift(const BitVector& y) const
 277 {
 278   if (y.d_value > Integer(d_size))
 279   {
 280     return BitVector(d_size, Integer(0));
 281   }
 282   if (y.d_value == 0)
 283   {
 284     return *this;
 285   }
 286   // making sure we don't lose information casting
 287   CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
 288   uint32_t amount = y.d_value.toUnsignedInt();
 289   Integer res = d_value.multiplyByPow2(amount);
 290   return BitVector(d_size, res);
 291 }
 292
 293 BitVector BitVector::logicalRightShift(const BitVector& y) const
 294 {
 295   if (y.d_value > Integer(d_size))
 296   {
 297     return BitVector(d_size, Integer(0));
 298   }
 299   // making sure we don't lose information casting
 300   CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
 301   uint32_t amount = y.d_value.toUnsignedInt();
 302   Integer res = d_value.divByPow2(amount);
 303   return BitVector(d_size, res);
 304 }
 305
 306 BitVector BitVector::arithRightShift(const BitVector& y) const
 307 {
 308   Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
 309   if (y.d_value > Integer(d_size))
 310   {
 311     if (sign_bit == Integer(0))
 312     {
 313       return BitVector(d_size, Integer(0));
 314     }
 315     else
 316     {
 317       return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
 318     }
 319   }
 320
 321   if (y.d_value == 0)
 322   {
 323     return *this;
 324   }
 325
 326   // making sure we don't lose information casting
 327   CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
 328
 329   uint32_t amount = y.d_value.toUnsignedInt();
 330   Integer rest = d_value.divByPow2(amount);
 331
 332   if (sign_bit == Integer(0))
 333   {
 334     return BitVector(d_size, rest);
 335   }
 336   Integer res = rest.oneExtend(d_size - amount, amount);
 337   return BitVector(d_size, res);
 338 }
 339
 340 /* -----------------------------------------------------------------------
 341  ** Static helpers.
 342  * ----------------------------------------------------------------------- */
 343
 344 BitVector BitVector::mkZero(unsigned size)
 345 {
 346   CheckArgument(size > 0, size);
 347   return BitVector(size);
 348 }
 349
 350 BitVector BitVector::mkOne(unsigned size)
 351 {
 352   CheckArgument(size > 0, size);
 353   return BitVector(size, 1u);
 354 }
 355
 356 BitVector BitVector::mkOnes(unsigned size)
 357 {
 358   CheckArgument(size > 0, size);
 359   return BitVector(1, Integer(1)).signExtend(size - 1);
 360 }
 361
 362 BitVector BitVector::mkMinSigned(unsigned size)
 363 {
 364   CheckArgument(size > 0, size);
 365   return BitVector(size).setBit(size - 1);
 366 }
 367
 368 BitVector BitVector::mkMaxSigned(unsigned size)
 369 {
 370   CheckArgument(size > 0, size);
 371   return ~BitVector::mkMinSigned(size);
 372 }
 373
 374 }  // namespace CVC4