BitVector: Change setBit to set the bit in place. (#6176)

Creating BitVectors (and deleting them) is in general expensive because
of the underlying multi-precision Integer. If possible, unnecessary
constructions and desctructions of BitVectors should be avoided.
The most common use case for `setBit` is that for an existing BitVector,
a given bit should be set to a certain value. Not doing this in place
generates unnecessary constructions and destructions of BitVectors.

7 files changed, 28 insertions, 26 deletions

diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index ac56488a9..3d907150d 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -60,11 +60,11 @@ size_t BitVector::hash() const
   return d_value.hash() + d_size;
 }
 
-BitVector BitVector::setBit(uint32_t i, bool value) const
+BitVector& BitVector::setBit(uint32_t i, bool value)
 {
   CheckArgument(i < d_size, i);
-  Integer res = d_value.setBit(i, value);
-  return BitVector(d_size, res);
+  d_value.setBit(i, value);
+  return *this;
 }
 
 bool BitVector::isBitSet(uint32_t i) const
@@ -364,7 +364,9 @@ BitVector BitVector::mkOnes(unsigned size)
 BitVector BitVector::mkMinSigned(unsigned size)
 {
   CheckArgument(size > 0, size);
-  return BitVector(size).setBit(size - 1, true);
+  BitVector res(size);
+  res.setBit(size - 1, true);
+  return res;
 }
 
 BitVector BitVector::mkMaxSigned(unsigned size)
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index ab6d8b030..c5a690c03 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -118,11 +118,13 @@ class BitVector
 
   /**
    * Set bit at index 'i' to given value.
+   * Returns a reference to this bit-vector to allow for chaining.
+   *
    * 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;
+  BitVector& setBit(uint32_t i, bool value);
 
   /** Return true if bit at index 'i' is 1, and false otherwise. */
   bool isBitSet(uint32_t i) const;
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 42f411ab2..cebdbbb29 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -361,8 +361,8 @@ FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size,
                                            bool sign)
 {
   BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
-  BitVector bvexp =
-      BitVector::mkOnes(size.packedExponentWidth()).setBit(0, false);
+  BitVector bvexp = BitVector::mkOnes(size.packedExponentWidth());
+  bvexp.setBit(0, false);
   BitVector bvsig = BitVector::mkOnes(size.packedSignificandWidth());
   return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
 }
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index b42334256..a4035165e 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -142,13 +142,19 @@ bool Integer::isBitSet(uint32_t i) const
   return !extractBitRange(1, i).isZero();
 }
 
-Integer Integer::setBit(uint32_t i, bool value) const
+void Integer::setBit(uint32_t i, bool value)
 {
   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));
+  if (value)
+  {
+    d_value = cln::logior(d_value, mask);
+  }
+  else
+  {
+    mask = cln::lognot(mask);
+    d_value = cln::logand(d_value, mask);
+  }
 }
 
 Integer Integer::oneExtend(uint32_t size, uint32_t amount) const
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 1687bc776..db1e5068f 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -132,11 +132,8 @@ class CVC4_EXPORT Integer
   /** Return true if bit at index 'i' is 1, and false otherwise. */
   bool isBitSet(uint32_t i) const;
 
-  /**
-   * Returns the Integer obtained by setting the ith bit of the
-   * current Integer to 1.
-   */
-  Integer setBit(uint32_t i, bool value) const;
+  /** Set the ith bit of the current Integer to 'value'.  */
+  void setBit(uint32_t i, bool value);
 
   /**
    * Returns the integer with the binary representation of 'size' bits
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 517f14955..89f6dc308 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -142,18 +142,16 @@ Integer Integer::multiplyByPow2(uint32_t pow) const
   return Integer(result);
 }
 
-Integer Integer::setBit(uint32_t i, bool value) const
+void Integer::setBit(uint32_t i, bool value)
 {
-  mpz_class res = d_value;
   if (value)
   {
-    mpz_setbit(res.get_mpz_t(), i);
+    mpz_setbit(d_value.get_mpz_t(), i);
   }
   else
   {
-    mpz_clrbit(res.get_mpz_t(), i);
+    mpz_clrbit(d_value.get_mpz_t(), i);
   }
-  return Integer(res);
 }
 
 bool Integer::isBitSet(uint32_t i) const
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 9cd230d35..616408b42 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -114,11 +114,8 @@ class CVC4_EXPORT Integer
   /** Return this*(2^pow). */
   Integer multiplyByPow2(uint32_t pow) const;
 
-  /**
-   * Returns the Integer obtained by setting the ith bit of the
-   * current Integer to 1.
-   */
-  Integer setBit(uint32_t i, bool value) const;
+  /** Set the ith bit of the current Integer to 'value'.  */
+  void setBit(uint32_t i, bool value);
 
   /** Return true if bit at index 'i' is 1, and false otherwise. */
   bool isBitSet(uint32_t i) const;