src/util/bitvector.h

   1 /*********************                                                        */
   2 /*! \file bitvector.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: cconway, mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief [[ Add one-line brief description here ]]
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20 #include "cvc4_public.h"
  21
  22 #ifndef __CVC4__BITVECTOR_H
  23 #define __CVC4__BITVECTOR_H
  24
  25 #include <iostream>
  26 #include "util/Assert.h"
  27 #include "util/integer.h"
  28
  29 namespace CVC4 {
  30
  31 class CVC4_PUBLIC BitVector {
  32
  33 private:
  34
  35   /*
  36     Class invariants:
  37     * no overflows: 2^d_size < d_value
  38     * no negative numbers: d_value >= 0
  39    */
  40   unsigned d_size;
  41   Integer d_value;
  42
  43   Integer toSignedInt() const {
  44     // returns Integer corresponding to two's complement interpretation of bv
  45     unsigned size = d_size;
  46     Integer sign_bit = d_value.extractBitRange(1,size-1);
  47     Integer val = d_value.extractBitRange(size-1, 0);
  48     Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
  49     return res;
  50   }
  51
  52
  53 public:
  54
  55   BitVector(unsigned size, const Integer& val):
  56     d_size(size),
  57     d_value(val.modByPow2(size))
  58       {}
  59
  60   BitVector(unsigned size = 0)
  61     : d_size(size), d_value(0) {}
  62
  63   BitVector(unsigned size, unsigned int z)
  64     : d_size(size), d_value(z) {
  65     d_value = d_value.modByPow2(size);
  66   }
  67
  68   BitVector(unsigned size, unsigned long int z)
  69     : d_size(size), d_value(z) {
  70     d_value = d_value.modByPow2(size);
  71   }
  72
  73   BitVector(unsigned size, const BitVector& q)
  74     : d_size(size), d_value(q.d_value) {}
  75
  76   BitVector(const std::string& num, unsigned base = 2);
  77
  78   ~BitVector() {}
  79
  80   Integer toInteger() const {
  81     return d_value;
  82   }
  83
  84   BitVector& operator =(const BitVector& x) {
  85     if(this == &x)
  86       return *this;
  87     d_size = x.d_size;
  88     d_value = x.d_value;
  89     return *this;
  90   }
  91
  92   bool operator ==(const BitVector& y) const {
  93     if (d_size != y.d_size) return false;
  94     return d_value == y.d_value;
  95   }
  96
  97   bool operator !=(const BitVector& y) const {
  98     if (d_size != y.d_size) return true;
  99     return d_value != y.d_value;
 100   }
 101
 102   BitVector equals(const BitVector&  y) const {
 103     Assert(d_size == y.d_size);
 104     return d_value == y.d_value;
 105   }
 106
 107   BitVector concat (const BitVector& other) const {
 108     return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
 109   }
 110
 111   BitVector extract(unsigned high, unsigned low) const {
 112     return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
 113   }
 114
 115   /*
 116     Bitwise operations on BitVectors
 117    */
 118
 119   // xor
 120   BitVector operator ^(const BitVector& y) const {
 121     Assert (d_size == y.d_size);
 122     return BitVector(d_size, d_value.bitwiseXor(y.d_value));
 123   }
 124
 125   // or
 126   BitVector operator |(const BitVector& y) const {
 127     Assert (d_size == y.d_size);
 128     return BitVector(d_size, d_value.bitwiseOr(y.d_value));
 129   }
 130
 131   // and
 132   BitVector operator &(const BitVector& y) const {
 133     Assert (d_size == y.d_size);
 134     return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
 135   }
 136
 137   // not
 138   BitVector operator ~() const {
 139     return BitVector(d_size, d_value.bitwiseNot());
 140   }
 141
 142   /*
 143     Arithmetic operations on BitVectors
 144    */
 145
 146
 147   bool operator <(const BitVector& y) const {
 148     return d_value < y.d_value;
 149   }
 150
 151   bool operator >(const BitVector& y) const {
 152     return d_value > y.d_value ;
 153   }
 154
 155   bool operator <=(const BitVector& y) const {
 156     return d_value <= y.d_value;
 157   }
 158
 159   bool operator >=(const BitVector& y) const {
 160     return d_value >= y.d_value ;
 161   }
 162
 163
 164   BitVector operator +(const BitVector& y) const {
 165     Assert (d_size == y.d_size);
 166     Integer sum = d_value +  y.d_value;
 167     return BitVector(d_size, sum);
 168   }
 169
 170   BitVector operator -(const BitVector& y) const {
 171     Assert (d_size == y.d_size);
 172     // to maintain the invariant that we are only adding BitVectors of the
 173     // same size
 174     BitVector one(d_size, Integer(1));
 175     return *this + ~y + one;
 176   }
 177
 178   BitVector operator -() const {
 179     BitVector one(d_size, Integer(1));
 180     return ~(*this) + one;
 181   }
 182
 183   BitVector operator *(const BitVector& y) const {
 184     Assert (d_size == y.d_size);
 185     Integer prod = d_value * y.d_value;
 186     return BitVector(d_size, prod);
 187   }
 188
 189   BitVector unsignedDiv (const BitVector& y) const {
 190     Assert (d_size == y.d_size);
 191     // TODO: decide whether we really want these semantics
 192     if (y.d_value == 0) {
 193       return BitVector(d_size, Integer(0));
 194     }
 195     Assert (d_value >= 0 && y.d_value > 0);
 196     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
 197   }
 198
 199   BitVector unsignedRem(const BitVector& y) const {
 200     Assert (d_size == y.d_size);
 201     // TODO: decide whether we really want these semantics
 202     if (y.d_value == 0) {
 203       return BitVector(d_size, Integer(0));
 204     }
 205     Assert (d_value >= 0 && y.d_value > 0);
 206     return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
 207   }
 208
 209
 210   bool signedLessThan(const BitVector& y) const {
 211     Assert(d_size == y.d_size);
 212     Assert(d_value >= 0 && y.d_value >= 0);
 213     Integer a = (*this).toSignedInt();
 214     Integer b = y.toSignedInt();
 215
 216     return a < b;
 217   }
 218
 219   bool unsignedLessThan(const BitVector& y) const {
 220     Assert(d_size == y.d_size);
 221     Assert(d_value >= 0 && y.d_value >= 0);
 222     return d_value < y.d_value;
 223   }
 224
 225   bool signedLessThanEq(const BitVector& y) const {
 226     Assert(d_size == y.d_size);
 227     Assert(d_value >= 0 && y.d_value >= 0);
 228     Integer a = (*this).toSignedInt();
 229     Integer b = y.toSignedInt();
 230
 231     return a <= b;
 232   }
 233
 234   bool unsignedLessThanEq(const BitVector& y) const {
 235     Assert(d_size == y.d_size);
 236     Assert(d_value >= 0 && y.d_value >= 0);
 237     return d_value <= y.d_value;
 238   }
 239
 240
 241   /*
 242     Extend operations
 243    */
 244
 245   BitVector zeroExtend(unsigned amount) const {
 246     return BitVector(d_size + amount, d_value);
 247   }
 248
 249   BitVector signExtend(unsigned amount) const {
 250     Integer sign_bit = d_value.extractBitRange(1, d_size -1);
 251     if(sign_bit == Integer(0)) {
 252       return BitVector(d_size + amount, d_value);
 253     } else {
 254       Integer val = d_value.oneExtend(d_size, amount);
 255       return BitVector(d_size+ amount, val);
 256     }
 257   }
 258
 259   /*
 260     Shifts on BitVectors
 261    */
 262
 263   BitVector leftShift(const BitVector& y) const {
 264     if (y.d_value > Integer(d_size)) {
 265       return BitVector(d_size, Integer(0));
 266     }
 267     if (y.d_value == 0) {
 268       return *this;
 269     }
 270
 271     // making sure we don't lose information casting
 272     Assert(y.d_value < Integer(1).multiplyByPow2(32));
 273     uint32_t amount = y.d_value.toUnsignedInt();
 274     Integer res = d_value.multiplyByPow2(amount);
 275     return BitVector(d_size, res);
 276   }
 277
 278   BitVector logicalRightShift(const BitVector& y) const {
 279     if(y.d_value > Integer(d_size)) {
 280       return BitVector(d_size, Integer(0));
 281     }
 282
 283     // making sure we don't lose information casting
 284     Assert(y.d_value < Integer(1).multiplyByPow2(32));
 285     uint32_t amount = y.d_value.toUnsignedInt();
 286     Integer res = d_value.divByPow2(amount);
 287     return BitVector(d_size, res);
 288   }
 289
 290   BitVector arithRightShift(const BitVector& y) const {
 291     Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
 292     if(y.d_value > Integer(d_size)) {
 293       if(sign_bit == Integer(0)) {
 294         return BitVector(d_size, Integer(0));
 295       } else {
 296         return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
 297       }
 298     }
 299
 300     if (y.d_value == 0) {
 301       return *this;
 302     }
 303
 304     // making sure we don't lose information casting
 305     Assert(y.d_value < Integer(1).multiplyByPow2(32));
 306
 307     uint32_t amount  = y.d_value.toUnsignedInt();
 308     Integer rest = d_value.divByPow2(amount);
 309
 310     if(sign_bit == Integer(0)) {
 311       return BitVector(d_size, rest);
 312     }
 313     Integer res = rest.oneExtend(d_size - amount, amount);
 314     return BitVector(d_size, res);
 315   }
 316
 317
 318   /*
 319     Convenience functions
 320    */
 321
 322   size_t hash() const {
 323     return d_value.hash() + d_size;
 324   }
 325
 326   std::string toString(unsigned int base = 2) const {
 327     std::string str = d_value.toString(base);
 328     if( base == 2 && d_size > str.size() ) {
 329       std::string zeroes;
 330       for( unsigned int i=0; i < d_size - str.size(); ++i ) {
 331         zeroes.append("0");
 332       }
 333       return zeroes + str;
 334     } else {
 335       return str;
 336     }
 337   }
 338
 339   unsigned getSize() const {
 340     return d_size;
 341   }
 342
 343   const Integer& getValue() const {
 344     return d_value;
 345   }
 346
 347   /**
 348    Returns k is the integer is equal to 2^{k-1} and zero
 349    otherwise
 350    @return k if the integer is equal to 2^{k-1} and zero otherwise
 351    */
 352   unsigned isPow2() {
 353     return d_value.isPow2();
 354   }
 355
 356 };/* class BitVector */
 357
 358
 359
 360 inline BitVector::BitVector(const std::string& num, unsigned base) {
 361   AlwaysAssert( base == 2 || base == 16 );
 362
 363   if( base == 2 ) {
 364     d_size = num.size();
 365   } else if( base == 16 ) {
 366     d_size = num.size() * 4;
 367   } else {
 368     Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
 369   }
 370
 371   d_value = Integer(num,base);
 372 }/* BitVector::BitVector() */
 373
 374
 375 /**
 376  * Hash function for the BitVector constants.
 377  */
 378 struct CVC4_PUBLIC BitVectorHashFunction {
 379   inline size_t operator()(const BitVector& bv) const {
 380     return bv.hash();
 381   }
 382 };/* struct BitVectorHashFunction */
 383
 384 /**
 385  * The structure representing the extraction operation for bit-vectors. The
 386  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 387  * by taking the bits at indices <code>high ... low</code>
 388  */
 389 struct CVC4_PUBLIC BitVectorExtract {
 390   /** The high bit of the range for this extract */
 391   unsigned high;
 392   /** The low bit of the range for this extract */
 393   unsigned low;
 394
 395   BitVectorExtract(unsigned high, unsigned low)
 396   : high(high), low(low) {}
 397
 398   bool operator == (const BitVectorExtract& extract) const {
 399     return high == extract.high && low == extract.low;
 400   }
 401 };/* struct BitVectorExtract */
 402
 403 /**
 404  * Hash function for the BitVectorExtract objects.
 405  */
 406 struct CVC4_PUBLIC BitVectorExtractHashFunction {
 407   size_t operator()(const BitVectorExtract& extract) const {
 408     size_t hash = extract.low;
 409     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 410     return hash;
 411   }
 412 };/* struct BitVectorExtractHashFunction */
 413
 414
 415 /**
 416  * The structure representing the extraction of one Boolean bit.
 417  */
 418 struct CVC4_PUBLIC BitVectorBitOf {
 419   /** The index of the bit */
 420   unsigned bitIndex;
 421   BitVectorBitOf(unsigned i)
 422     : bitIndex(i) {}
 423
 424   bool operator == (const BitVectorBitOf& other) const {
 425     return bitIndex == other.bitIndex;
 426   }
 427 };/* struct BitVectorBitOf */
 428
 429 /**
 430  * Hash function for the BitVectorBitOf objects.
 431  */
 432 struct CVC4_PUBLIC BitVectorBitOfHashFunction {
 433   size_t operator()(const BitVectorBitOf& b) const {
 434     return b.bitIndex;
 435   }
 436 };/* struct BitVectorBitOfHashFunction */
 437
 438
 439
 440 struct CVC4_PUBLIC BitVectorSize {
 441   unsigned size;
 442   BitVectorSize(unsigned size)
 443   : size(size) {}
 444   operator unsigned () const { return size; }
 445 };/* struct BitVectorSize */
 446
 447 struct CVC4_PUBLIC BitVectorRepeat {
 448   unsigned repeatAmount;
 449   BitVectorRepeat(unsigned repeatAmount)
 450   : repeatAmount(repeatAmount) {}
 451   operator unsigned () const { return repeatAmount; }
 452 };/* struct BitVectorRepeat */
 453
 454 struct CVC4_PUBLIC BitVectorZeroExtend {
 455   unsigned zeroExtendAmount;
 456   BitVectorZeroExtend(unsigned zeroExtendAmount)
 457   : zeroExtendAmount(zeroExtendAmount) {}
 458   operator unsigned () const { return zeroExtendAmount; }
 459 };/* struct BitVectorZeroExtend */
 460
 461 struct CVC4_PUBLIC BitVectorSignExtend {
 462   unsigned signExtendAmount;
 463   BitVectorSignExtend(unsigned signExtendAmount)
 464   : signExtendAmount(signExtendAmount) {}
 465   operator unsigned () const { return signExtendAmount; }
 466 };/* struct BitVectorSignExtend */
 467
 468 struct CVC4_PUBLIC BitVectorRotateLeft {
 469   unsigned rotateLeftAmount;
 470   BitVectorRotateLeft(unsigned rotateLeftAmount)
 471   : rotateLeftAmount(rotateLeftAmount) {}
 472   operator unsigned () const { return rotateLeftAmount; }
 473 };/* struct BitVectorRotateLeft */
 474
 475 struct CVC4_PUBLIC BitVectorRotateRight {
 476   unsigned rotateRightAmount;
 477   BitVectorRotateRight(unsigned rotateRightAmount)
 478   : rotateRightAmount(rotateRightAmount) {}
 479   operator unsigned () const { return rotateRightAmount; }
 480 };/* struct BitVectorRotateRight */
 481
 482 template <typename T>
 483 struct CVC4_PUBLIC UnsignedHashFunction {
 484   inline size_t operator()(const T& x) const {
 485     return (size_t)x;
 486   }
 487 };/* struct UnsignedHashFunction */
 488
 489 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
 490 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
 491   return os << bv.toString();
 492 }
 493
 494 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
 495 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
 496   return os << "[" << bv.high << ":" << bv.low << "]";
 497 }
 498
 499 inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) CVC4_PUBLIC;
 500 inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
 501   return os << "[" << bv.bitIndex << "]";
 502 }
 503
 504 }/* CVC4 namespace */
 505
 506 #endif /* __CVC4__BITVECTOR_H */