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.

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 6d0413cb73b57d85e56717d893a5f8772749aa83..bbf7c62e7b1f513e96ff2042e78da67baa9fac0b 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1891,7 +1891,8 @@ 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, true);
+    BitVector bv_msb_x(size_c);
+    bv_msb_x.setBit(msb_x_pos, true);
     // (~0 << (n - 1))
     BitVector bv_upper_bits =
         (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
@@ -1927,7 +1928,8 @@ 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, true);
+  BitVector bv_msb_x(size_c);
+  bv_msb_x.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 ac56488a9d6bc9301392d143bcaac3daa940da6a..3d907150d929c45681e77b1ea6f4c36c46bccda7 100644 (file)
--- 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 ab6d8b0302a020d32ca27ccba7a3295f9d8e028a..c5a690c0372da11c1eb3a6068fb4cf2619b3073b 100644 (file)
--- 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 42f411ab266c807e494cc02aec3a9445038c77cf..cebdbbb296b361b25f4529959eee17a4097ba7d2 100644 (file)
--- 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 b4233425695039eef778a712709c607adc0b6d8b..a4035165ee2a30f8b3a13aedb61aed3f2d5a0e52 100644 (file)
--- 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 1687bc77652b614f499997f26d3da8c86d5cabaa..db1e5068f268f544b720038c690375cb9f327a2b 100644 (file)
--- 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 517f149551feb655389a7402ac2105b5998957bf..89f6dc30841f5b7a1ec8b5b2463372970e84c13b 100644 (file)
--- 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 9cd230d3568667824db5a07f3e2b9823826ec597..616408b428428b47a306ddfd72d098c2b74d89c5 100644 (file)
--- 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;

diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp
index c544913a757ab2ced166bae615aabceddab4d60f..3de70cfecc7cad202e0ffde0b919882af8e81be0 100644 (file)
--- a/test/unit/util/bitvector_black.cpp
+++ b/test/unit/util/bitvector_black.cpp
@@ -28,7 +28,7 @@ class TestUtilBlackBitVector : public TestInternal
   void SetUp() override
   {
     d_zero = BitVector(4);
-    d_one = d_zero.setBit(0, true);
+    d_one = BitVector::mkOne(4);
     d_two = BitVector("0010", 2);
     d_neg_one = BitVector(4, Integer(-1));
     d_ones = BitVector::mkOnes(4);
@@ -83,12 +83,19 @@ TEST_F(TestUtilBlackBitVector, conversions)
 
 TEST_F(TestUtilBlackBitVector, setBit_getBit)
 {
-  ASSERT_EQ(d_one.setBit(1, true).setBit(2, true).setBit(3, true), d_ones);
-  ASSERT_EQ(d_ones.setBit(0, false).setBit(1, false).setBit(2, false).setBit(
-                3, false),
-            d_zero);
-  ASSERT_EQ(d_ones.setBit(0, false).setBit(0, true), d_ones);
-  ASSERT_EQ(d_ones.setBit(0, false), ~BitVector::mkOne(d_one.getSize()));
+  BitVector ones(d_one);
+  ASSERT_EQ(ones.setBit(1, true).setBit(2, true).setBit(3, true), d_ones);
+
+  BitVector zero(d_ones);
+  ASSERT_EQ(
+      zero.setBit(0, false).setBit(1, false).setBit(2, false).setBit(3, false),
+      d_zero);
+
+  ones = d_ones;
+  ASSERT_EQ(ones.setBit(0, false).setBit(0, true), d_ones);
+
+  BitVector not_one(d_ones);
+  ASSERT_EQ(not_one.setBit(0, false), ~BitVector::mkOne(d_one.getSize()));
 
   ASSERT_TRUE(d_ones.isBitSet(3));
   ASSERT_FALSE(d_two.isBitSet(3));