summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h6
-rw-r--r--src/util/bitvector.cpp10
-rw-r--r--src/util/bitvector.h4
-rw-r--r--src/util/floatingpoint.cpp4
-rw-r--r--src/util/integer_cln_imp.cpp14
-rw-r--r--src/util/integer_cln_imp.h7
-rw-r--r--src/util/integer_gmp_imp.cpp8
-rw-r--r--src/util/integer_gmp_imp.h7
-rw-r--r--test/unit/util/bitvector_black.cpp21
9 files changed, 46 insertions, 35 deletions
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<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 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));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback