From: Aina Niemetz Date: Fri, 19 Mar 2021 17:28:14 +0000 (-0700) Subject: BitVector: Change setBit to set the bit in place. (#6176) X-Git-Tag: cvc5-1.0.0~2053 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=58e219362b2e9a7d7b9b9b526760c392cd50e878;p=cvc5.git 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 6d0413cb7..bbf7c62e7 100644 --- 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::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::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 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; diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp index c544913a7..3de70cfec 100644 --- 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));