From d7f92f70bb8ff221dc3d7cb086e5e2e237dadc67 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 30 Sep 2020 17:26:46 -0700 Subject: [PATCH] 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. --- .../theory_bv_rewrite_rules_simplification.h | 4 ++-- src/util/bitvector.cpp | 6 +++--- src/util/bitvector.h | 12 ++++++++--- src/util/integer_cln_imp.cpp | 10 +++++++++- src/util/integer_cln_imp.h | 7 +------ src/util/integer_gmp_imp.cpp | 16 +++++++++++++-- src/util/integer_gmp_imp.h | 7 +------ test/unit/util/bitvector_black.h | 20 ++++++++++++++----- 8 files changed, 54 insertions(+), 28 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::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::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::min() unsigned long Integer::s_signedLongMax = std::numeric_limits::max(); unsigned long Integer::s_unsignedLongMax = std::numeric_limits::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(); } diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index 7fba53adc..5b6eecc5f 100644 --- 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; }; -- 2.30.2