src/util/bitvector.h

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