ported my bv-core branch from svn to git

4 files changed, 49 insertions, 0 deletions

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 2c178ec2e..5df632ff4 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -178,6 +178,17 @@ public:
     Integer prod = d_value * y.d_value;
     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); 
+  }
   
   BitVector unsignedDiv (const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 211c40741..e2a8f4a62 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -218,6 +218,16 @@ public:
     return Integer( d_value << ipow);
   }
 
+  bool isBitSet(uint32_t i) const {
+    return !extractBitRange(1, i).isZero(); 
+  }
+  
+  Integer setBit(uint32_t i) const {
+    cln::cl_I mask(1);
+    mask = mask << i; 
+    return Integer(cln::logior(d_value, mask)); 
+  }
+  
   Integer oneExtend(uint32_t size, uint32_t amount) const {
     DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
     cln::cl_byte range(amount, size);
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index bebd0e1e2..d6882b6ac 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -137,6 +137,7 @@ public:
     return *this;
   }
 
+
   Integer bitwiseOr(const Integer& y) const {
     mpz_class result;
     mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
@@ -170,6 +171,24 @@ public:
     return Integer( result );
   }
 
+  /** 
+   * Returns the Integer obtained by setting the ith bit of the
+   * current Integer to 1. 
+   * 
+   * @param bit 
+   * 
+   * @return 
+   */
+  Integer setBit(uint32_t i) const {
+    mpz_class res = d_value;
+    mpz_setbit(res.get_mpz_t(), i);
+    return Integer(res); 
+  }
+
+  bool isBitSet(uint32_t i) const {
+    return !extractBitRange(1, i).isZero(); 
+  }
+  
   /**
    * Returns the integer with the binary representation of size bits
    * extended with amount 1's
diff --git a/src/util/utility.h b/src/util/utility.h
index 5ce185b5b..72213764f 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -67,6 +67,15 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre
   return (match2 == last) ? match : last;
 }
 
+template <class T>
+inline T gcd(T a, T b) {
+  while (b != 0) {
+    a = b;
+    b = a % b; 
+  }
+  return a;
+}
+
 
 }/* CVC4 namespace */