5 files changed, 44 insertions, 1 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 4cbcba50e..c9661c0c7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -178,10 +178,23 @@ 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); 
+  }
+  
   /** 
    * Total division function that returns 0 when the denominator is 0.  
    */
   BitVector unsignedDivTotal (const BitVector& y) const {
+
     CheckArgument(d_size == y.d_size, y);
     if (y.d_value == 0) {
       return BitVector(d_size, 0u);
@@ -190,6 +203,7 @@ public:
     CheckArgument(y.d_value > 0, y);
     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
   }
+  
   /** 
    * Total division function that returns 0 when the denominator is 0.  
    */
diff --git a/src/util/index.h b/src/util/index.h
index 4c03af5b0..252f7066b 100644
--- a/src/util/index.h
+++ b/src/util/index.h
@@ -21,6 +21,7 @@
 
 #include <stdint.h>
 #include <boost/static_assert.hpp>
+#include <limits>
 
 namespace CVC4 {
 
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index b5452ae00..81c0428cb 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 176604268..85d49f921 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..089be478d 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -67,7 +67,6 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre
   return (match2 == last) ? match : last;
 }
 
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__UTILITY_H */