diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/bitvector.h | 14 | ||||
-rw-r--r-- | src/util/index.h | 1 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 10 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 19 | ||||
-rw-r--r-- | src/util/utility.h | 1 |
5 files changed, 44 insertions, 1 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 4cbcba50e..c9661c0c7 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -178,10 +178,23 @@ public: Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } + + BitVector setBit(uint32_t i) const { + CheckArgument(i < d_size, i); + Integer res = d_value.setBit(i); + return BitVector(d_size, res); + } + + bool isBitSet(uint32_t i) const { + CheckArgument(i < d_size, i); + return d_value.isBitSet(i); + } + /** * Total division function that returns 0 when the denominator is 0. */ BitVector unsignedDivTotal (const BitVector& y) const { + CheckArgument(d_size == y.d_size, y); if (y.d_value == 0) { return BitVector(d_size, 0u); @@ -190,6 +203,7 @@ public: CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } + /** * Total division function that returns 0 when the denominator is 0. */ diff --git a/src/util/index.h b/src/util/index.h index 4c03af5b0..252f7066b 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -21,6 +21,7 @@ #include <stdint.h> #include <boost/static_assert.hpp> +#include <limits> namespace CVC4 { diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index b5452ae00..81c0428cb 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -218,6 +218,16 @@ public: return Integer( d_value << ipow); } + 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 oneExtend(uint32_t size, uint32_t amount) const { DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); cln::cl_byte range(amount, size); diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 176604268..85d49f921 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -137,6 +137,7 @@ public: return *this; } + Integer bitwiseOr(const Integer& y) const { mpz_class result; mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); @@ -170,6 +171,24 @@ public: return Integer( result ); } + /** + * Returns the Integer obtained by setting the ith bit of the + * current Integer to 1. + * + * @param bit + * + * @return + */ + Integer setBit(uint32_t i) const { + mpz_class res = d_value; + mpz_setbit(res.get_mpz_t(), i); + return Integer(res); + } + + bool isBitSet(uint32_t i) const { + return !extractBitRange(1, i).isZero(); + } + /** * Returns the integer with the binary representation of size bits * extended with amount 1's diff --git a/src/util/utility.h b/src/util/utility.h index 5ce185b5b..089be478d 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -67,7 +67,6 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre return (match2 == last) ? match : last; } - }/* CVC4 namespace */ #endif /* __CVC4__UTILITY_H */ |