src/util/bitvector.h

   1 /*
   2  * bitvector.h
   3  *
   4  *  Created on: Mar 31, 2010
   5  *      Author: dejan
   6  */
   7
   8 #ifndef __CVC4__BITVECTOR_H_
   9 #define __CVC4__BITVECTOR_H_
  10
  11 #include <string>
  12 #include <iostream>
  13 #include "util/gmp_util.h"
  14
  15 namespace CVC4 {
  16
  17 class BitVector {
  18
  19 private:
  20
  21   unsigned d_size;
  22   mpz_class d_value;
  23
  24   BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {}
  25
  26 public:
  27
  28   BitVector(unsigned size = 0)
  29   : d_size(size), d_value(0) {}
  30
  31   BitVector(unsigned size, unsigned int z)
  32   : d_size(size), d_value(z) {}
  33
  34   BitVector(unsigned size, unsigned long int z)
  35   : d_size(size), d_value(z) {}
  36
  37   BitVector(unsigned size, const BitVector& q)
  38   : d_size(size), d_value(q.d_value) {}
  39
  40   ~BitVector() {}
  41
  42   BitVector& operator =(const BitVector& x) {
  43     if(this == &x)
  44       return *this;
  45     d_value = x.d_value;
  46     return *this;
  47   }
  48
  49   bool operator ==(const BitVector& y) const {
  50     if (d_size != y.d_size) return false;
  51     return d_value == y.d_value;
  52   }
  53
  54   bool operator !=(const BitVector& y) const {
  55     if (d_size == y.d_size) return false;
  56     return d_value != y.d_value;
  57   }
  58
  59   BitVector operator +(const BitVector& y) const {
  60     return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
  61   }
  62
  63   BitVector operator -(const BitVector& y) const {
  64     return *this + ~y + 1;
  65   }
  66
  67   BitVector operator -() const {
  68     return ~(*this) + 1;
  69   }
  70
  71   BitVector operator *(const BitVector& y) const {
  72     return BitVector(d_size, d_value * y.d_value);
  73   }
  74
  75   BitVector operator ~() const {
  76     return BitVector(d_size, d_value);
  77   }
  78
  79   size_t hash() const {
  80     return gmpz_hash(d_value.get_mpz_t());
  81   }
  82
  83   std::string toString(unsigned int base = 2) const {
  84     return d_value.get_str(base);
  85   }
  86 };
  87
  88 /**
  89  * Hash function for the BitVector constants.
  90  */
  91 struct BitVectorHashStrategy {
  92   static inline size_t hash(const BitVector& bv) {
  93     return bv.hash();
  94   }
  95 };
  96
  97 /**
  98  * The structure representing the extraction operation for bit-vectors. The
  99  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 100  * by taking the bits at indices <code>high ... low</code>
 101  */
 102 struct BitVectorExtract  {
 103   /** The high bit of the range for this extract */
 104   unsigned high;
 105   /** The low bit of the range for this extract */
 106   unsigned low;
 107
 108   bool operator == (const BitVectorExtract& extract) const {
 109     return high == extract.high && low == extract.low;
 110   }
 111 };
 112
 113 /**
 114  * Hash function for the BitVectorExtract objects.
 115  */
 116 class BitVectorExtractHashStrategy {
 117 public:
 118   static size_t hash(const BitVectorExtract& extract) {
 119     size_t hash = extract.low;
 120     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 121     return hash;
 122   }
 123 };
 124
 125 /**
 126  * Hash function for the unsigned integers.
 127  */
 128 struct UnsignedHashStrategy {
 129   static inline size_t hash(unsigned x) {
 130     return (size_t)x;
 131   }
 132 };
 133
 134 std::ostream& operator <<(std::ostream& os, const BitVector& bv);
 135 std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv);
 136 }
 137
 138
 139 #endif /* __CVC4__BITVECTOR_H_ */