BitVector: Extend interface of setBit to set it to a specific value. (#5173)

Previously, BitVector::setBit only allowed to set the bit at the given
index to 1. This changes its behavior to be also able to set it to 0.

7 files changed, 39 insertions, 23 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index dd0d47078..20dac35cd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1893,7 +1893,7 @@ inline bool RewriteRule<SignExtendUltConst>::applies(TNode node)
     unsigned size_c = utils::getSize(c);
     unsigned msb_x_pos = utils::getSize(x) - 1;
     // (1 << (n - 1)))
-    BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos);
+    BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos, true);
     // (~0 << (n - 1))
     BitVector bv_upper_bits =
         (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
@@ -1929,7 +1929,7 @@ inline Node RewriteRule<SignExtendUltConst>::apply(TNode node)
   unsigned msb_x_pos = utils::getSize(x) - 1;
   Node c_lo = utils::mkConst(bv_c.extract(msb_x_pos, 0));
   // (1 << (n - 1)))
-  BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos);
+  BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos, true);
   // (~0 << (n - 1))
   BitVector bv_upper_bits =
       (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index f5e8c9b16..9233bde53 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -58,10 +58,10 @@ size_t BitVector::hash() const
   return d_value.hash() + d_size;
 }
 
-BitVector BitVector::setBit(uint32_t i) const
+BitVector BitVector::setBit(uint32_t i, bool value) const
 {
   CheckArgument(i < d_size, i);
-  Integer res = d_value.setBit(i);
+  Integer res = d_value.setBit(i, value);
   return BitVector(d_size, res);
 }
 
@@ -362,7 +362,7 @@ BitVector BitVector::mkOnes(unsigned size)
 BitVector BitVector::mkMinSigned(unsigned size)
 {
   CheckArgument(size > 0, size);
-  return BitVector(size).setBit(size - 1);
+  return BitVector(size).setBit(size - 1, true);
 }
 
 BitVector BitVector::mkMaxSigned(unsigned size)
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 9d4f778cd..3ca410f72 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -116,9 +116,15 @@ class CVC4_PUBLIC BitVector
   /* Return hash value. */
   size_t hash() const;
 
-  /* Set bit at index 'i'. */
-  BitVector setBit(uint32_t i) const;
-  /* Return true if bit at index 'i' is set. */
+  /**
+   * Set bit at index 'i' to given value.
+   * value: True to set bit to 1, and false to set it to 0.
+   *
+   * Note: Least significant bit is at index 0.
+   */
+  BitVector setBit(uint32_t i, bool value) const;
+
+  /** Return true if bit at index 'i' is 1, and false otherwise. */
   bool isBitSet(uint32_t i) const;
 
   /* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 3ec2f90fd..6293544ff 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -44,6 +44,15 @@ unsigned long Integer::s_signedLongMin = std::numeric_limits<signed long>::min()
 unsigned long Integer::s_signedLongMax = std::numeric_limits<signed long>::max();
 unsigned long Integer::s_unsignedLongMax = std::numeric_limits<unsigned long>::max();
 
+Integer Integer::setBit(uint32_t i, bool value) const
+{
+  cln::cl_I mask(1);
+  mask = mask << i;
+  if (value) return Integer(cln::logior(d_value, mask));
+  mask = cln::lognot(mask);
+  return Integer(cln::logand(d_value, mask));
+}
+
 Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
   DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
   cln::cl_byte range(amount, size);
@@ -53,7 +62,6 @@ Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
   return Integer(cln::deposit_field(allones, d_value, range));
 }
 
-
 Integer Integer::exactQuotient(const Integer& y) const {
   DebugCheckArgument(y.divides(*this), y);
   return Integer( cln::exquo(d_value, y.d_value) );
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index c4f5182bf..2c62aa02e 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -162,12 +162,7 @@ class CVC4_PUBLIC Integer
 
   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 setBit(uint32_t i, bool value) const;
 
   Integer oneExtend(uint32_t size, uint32_t amount) const;
 
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index a714999b3..b435c6ca7 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -27,8 +27,7 @@
 
 #ifndef CVC4_GMP_IMP
 #  error "This source should only ever be built if CVC4_GMP_IMP is on !"
-#endif /* CVC4_GMP_IMP */
-
+#endif
 
 using namespace std;
 
@@ -42,6 +41,19 @@ Integer::Integer(const std::string& s, unsigned base)
   : d_value(s, base)
 {}
 
+Integer Integer::setBit(uint32_t i, bool value) const
+{
+  mpz_class res = d_value;
+  if (value)
+  {
+    mpz_setbit(res.get_mpz_t(), i);
+  }
+  else
+  {
+    mpz_clrbit(res.get_mpz_t(), i);
+  }
+  return Integer(res);
+}
 
 bool Integer::fitsSignedInt() const {
   return d_value.fits_sint_p();
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 33e0d5ebd..e7c0ee3a4 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -165,12 +165,7 @@ class CVC4_PUBLIC Integer
    * Returns the Integer obtained by setting the ith bit of the
    * current Integer to 1.
    */
-  Integer setBit(uint32_t i) const
-  {
-    mpz_class res = d_value;
-    mpz_setbit(res.get_mpz_t(), i);
-    return Integer(res);
-  }
+  Integer setBit(uint32_t i, bool value) const;
 
   bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); }