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.

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index dd0d47078dc2ddf5f65ef26515d2d0d13cff1475..20dac35cd9d3450ead505d6c2348be8b2a6459ff 100644 (file)
--- 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 f5e8c9b1687ed93e15ba564127a02260760a299f..9233bde530219acc38a1e62f9a8881dfeaa12f74 100644 (file)
--- 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 9d4f778cdcb861983c82484ff69f7d37f1a66074..3ca410f72e11334bab8e76c44009cab70824fa53 100644 (file)
--- 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 3ec2f90fd13099ebf0724df25e59e1b2c0acfeba..6293544ffc5afb90a73ce1e9d3ad11bbb7182e2c 100644 (file)
--- 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 c4f5182bf5f7867b065c5ccbcf2e121dce38cc9b..2c62aa02ed33392fdaa38bdb2134d02d70df7a35 100644 (file)
--- 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 a714999b38bd22b1ec95fa009f406dd22f90837d..b435c6ca78e151e56d2f7b3c1c80876ce143a70f 100644 (file)
--- 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 33e0d5ebd18152776ebba9e61b82405ad635ec31..e7c0ee3a4992c178c39e7ef72c084fac715910a3 100644 (file)
--- 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(); }
 

diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
index 7fba53adc1a29131022def3a341aefa07e62a05d..5b6eecc5f6cf45d264db4f79421a5ba122475baa 100644 (file)
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -29,9 +29,10 @@ public:
  void setUp() override
  {
    zero = BitVector(4);
-   one = zero.setBit(0);
+   one = zero.setBit(0, true);
    two = BitVector("0010", 2);
    negOne = BitVector(4, Integer(-1));
+   ones = BitVector::mkOnes(4);
  }
 
  void testStringConstructor()
@@ -76,16 +77,22 @@ public:
 
   void testSetGetBit()
   {
-    TS_ASSERT_EQUALS(one.setBit(1).setBit(2).setBit(3), negOne);
-
-    TS_ASSERT(negOne.isBitSet(3));
+    TS_ASSERT_EQUALS(one.setBit(1, true).setBit(2, true).setBit(3, true), ones);
+    TS_ASSERT_EQUALS(
+        ones.setBit(0, false).setBit(1, false).setBit(2, false).setBit(3,
+                                                                       false),
+        zero);
+    TS_ASSERT_EQUALS(ones.setBit(0, false).setBit(0, true), ones);
+    TS_ASSERT_EQUALS(ones.setBit(0, false), ~BitVector::mkOne(one.getSize()));
+
+    TS_ASSERT(ones.isBitSet(3));
     TS_ASSERT(!two.isBitSet(3));
 
     TS_ASSERT_EQUALS(one.getValue(), Integer(1));
     TS_ASSERT_EQUALS(zero.isPow2(), 0);
     TS_ASSERT_EQUALS(one.isPow2(), 1);
     TS_ASSERT_EQUALS(two.isPow2(), 2);
-    TS_ASSERT_EQUALS(negOne.isPow2(), 0);
+    TS_ASSERT_EQUALS(ones.isPow2(), 0);
   }
 
   void testConcatExtract()
@@ -177,6 +184,8 @@ public:
 
   void testStaticHelpers()
   {
+    TS_ASSERT_EQUALS(BitVector::mkZero(4), zero);
+    TS_ASSERT_EQUALS(BitVector::mkOne(4), one);
     TS_ASSERT_EQUALS(BitVector::mkOnes(4), negOne);
     TS_ASSERT_EQUALS(BitVector::mkMinSigned(4).toSignedInteger(), Integer(-8));
     TS_ASSERT_EQUALS(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7));
@@ -187,4 +196,5 @@ public:
   BitVector one;
   BitVector two;
   BitVector negOne;
+  BitVector ones;
 };