diff --git a/makefile b/makefile index 3204a6e06..7fdd171fa 100644 --- a/makefile +++ b/makefile @@ -67,6 +67,9 @@ tests/adiar/bool_op: tests/adiar/builder: $(MAKE) $(MAKE_FLAGS) tests TEST_SUBFOLDER=adiar/ TEST_NAME=builder +tests/adiar/bvec: + $(MAKE) $(MAKE_FLAGS) tests TEST_SUBFOLDER=adiar/ TEST_NAME=bvec + tests/adiar/domain: $(MAKE) $(MAKE_FLAGS) tests TEST_SUBFOLDER=adiar/ TEST_NAME=domain diff --git a/src/adiar/CMakeLists.txt b/src/adiar/CMakeLists.txt index a761b3163..aeacd924d 100644 --- a/src/adiar/CMakeLists.txt +++ b/src/adiar/CMakeLists.txt @@ -10,6 +10,7 @@ set(HEADERS adiar.h bool_op.h builder.h + bvec.h deprecated.h domain.h exception.h @@ -106,6 +107,7 @@ set(HEADERS set(SOURCES # adiar/ adiar.cpp + bvec.cpp domain.cpp statistics.cpp diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index b97f7665a..c65216258 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -21,12 +21,12 @@ #include #include -#include #include #include #include #include +#include #include #include diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp new file mode 100644 index 000000000..edb451e8e --- /dev/null +++ b/src/adiar/bvec.cpp @@ -0,0 +1,324 @@ +#include +#include +#include +#include + +#include +#include + +namespace adiar +{ + /// \brief Find the most significant bit for an integer. + size_t + msb(size_t value) + { + // TODO: optimize based on operations available from the compiler. + return value > 0 ? std::floor(std::log2(value)) + 1 : 0; + } + + /// \brief Derive the `bitlen` to be used when combining two `bvec`s. + size_t + join_bitlen(const bvec& x, const bvec& y) + { + const size_t upcasted = std::max(x.bitlen(), y.bitlen()); + + const size_t size = std::max(x.size(), y.size()); + const bool variadic_x = x.bitlen() == bvec::variadic_bitlen; + const bool variadic_y = y.bitlen() == bvec::variadic_bitlen; + + if ((variadic_x || variadic_y) && upcasted < size) { return bvec::variadic_bitlen; } + return upcasted; + } + + ////////////////////////////////////////////////////////////////////////////////////////////////// + // `bvec` class + + bvec::bvec() + : _bits(0) + , _bitlen(bvec::variadic_bitlen) + {} + + bvec::bvec(const bvec& fs) + : _bits(fs._bits) + , _bitlen(fs._bitlen) + {} + + bvec::bvec(bvec&& fs) + : _bits(std::move(fs._bits)) + , _bitlen(fs._bitlen) + {} + + bvec::bvec(size_t value) + : bvec(bvec_const(bvec::variadic_bitlen, value)) + {} + + bvec::bvec(size_t bitlen, size_t value) + : bvec(bvec_const(bitlen, value)) + {} + + bvec::bvec(const std::vector& bits) + : bvec(bvec::variadic_bitlen, bits) + {} + + bvec::bvec(size_t bitlen, const std::vector& bits) + : _bits(bits) + , _bitlen(bitlen) + { + this->truncate(bitlen); + } + + bvec::bvec(std::vector&& bits) + : bvec(bvec::variadic_bitlen, std::move(bits)) + {} + + bvec::bvec(size_t bitlen, std::vector&& bits) + : _bits(std::move(bits)) + , _bitlen(bitlen) + { + this->truncate(bitlen); + } + + const bdd& + bvec::at(size_t index) const + { + if (_bits.size() <= index) { return this->_default_value; } + return _bits.at(index); + } + + std::vector::const_iterator + bvec::begin() const + { + return _bits.cbegin(); + } + + std::vector::const_iterator + bvec::end() const + { + return _bits.cend(); + } + + std::vector::const_reverse_iterator + bvec::rbegin() const + { + return _bits.crbegin(); + } + + std::vector::const_reverse_iterator + bvec::rend() const + { + return _bits.crend(); + } + + std::string + bvec::to_string() const + { + std::stringstream out; + + out << "0x"; + for (auto i = this->rbegin(); i != this->rend(); i++) { + if (bdd_isfalse(*i)) { + out << "0"; + } else if (bdd_istrue(*i)) { + out << "1"; + } else { + out << "_"; + } + } + + return out.str(); + } + + void + bvec::truncate(size_t bitlen) + { + this->_bitlen = bitlen; + + if (bitlen != bvec::variadic_bitlen) { + // Truncate to bitlen + while (bitlen < this->_bits.size()) { this->_bits.pop_back(); } + } + + // Truncate only-false suffix + while (this->_bits.size() > 0 && !this->_bits.back()) { this->_bits.pop_back(); } + } + + ////////////////////////////////////////////////////////////////////////////////////////////////// + // Comparators + + std::ostream& + operator<<(std::ostream& os, const bvec& a) + { + return os << a.to_string(); + } + + bool + operator==(const bvec& x, const bvec& y) + { + return bvec_equal(x, y); + } + + bool + bvec_equal(const bvec& x, const bvec& y) + { + if (x.size() != y.size()) { return false; } + + for (size_t i = 0; i < x.size(); i++) { + if (!bdd_equal(x.at(i), y.at(i))) { return false; } + } + return true; + } + + ////////////////////////////////////////////////////////////////////////////////////////////////// + // Constructors + + bvec + bvec_false(size_t bitlen) + { + return bvec(bitlen, std::vector(0, bdd_false())); + } + + bvec + bvec_true(size_t bits) + { + return bvec_true(bvec::variadic_bitlen, bits); + } + + bvec + bvec_true(size_t bitlen, size_t bits) + { + return bvec(bitlen, + std::vector(bitlen == bvec::variadic_bitlen ? bits : std::min(bitlen, bits), + bdd_true())); + } + + bvec + bvec_const(size_t bitlen, size_t value) + { + std::vector res; + res.reserve(msb(value)); + + for (; value != 0; value >>= 1) { res.push_back(value & 1 ? bdd_true() : bdd_false()); } + + return bvec(bitlen, res); + } + + bvec + bvec_const(size_t value) + { + return bvec_const(bvec::variadic_bitlen, value); + } + + ////////////////////////////////////////////////////////////////////////////////////////////////// + // Bitwise operations + + // Helper function for bitwise operations + template + bvec + _bvec_bitwise_op(size_t size, size_t bitlen, const BDD_OP& op) + { + std::vector res; + res.reserve(size); + + for (size_t i = 0; i < size; i++) { + const bdd bit = op(i); + if (bit) { + while (res.size() < i) { res.push_back(bdd_false()); } + res.push_back(bit); + } + } + + return bvec(bitlen, res); + } + + template + bvec + _bvec_bitwise_op(const bvec& x, const bvec& y, const BDD_OP& op) + { + const size_t size = std::max(x.size(), y.size()); + const size_t bitlen = join_bitlen(x, y); + + return _bvec_bitwise_op(size, bitlen, op); + } + + bvec + bvec_and(const bvec& x, const bvec& y) + { + return _bvec_bitwise_op(x, y, [&](size_t i) { return bdd_and(x.at(i), y.at(i)); }); + } + + bvec + bvec_or(const bvec& x, const bvec& y) + { + return _bvec_bitwise_op(x, y, [&](size_t i) { return bdd_or(x.at(i), y.at(i)); }); + } + + bvec + bvec_xor(const bvec& x, const bvec& y) + { + return _bvec_bitwise_op(x, y, [&](size_t i) { return bdd_xor(x.at(i), y.at(i)); }); + } + + bvec + bvec_not(const bvec& x) + { + return _bvec_bitwise_op( + std::max(x.bitlen(), x.size()), x.bitlen(), [&](size_t i) { return ~x.at(i); }); + } + + ////////////////////////////////////////////////////////////////////////////////////////////////// + // Arithmetic operations + + template + bvec + __bvec_add(const bvec& x, const bvec& y) + { + const size_t bitlen = join_bitlen(x, y); + const size_t size = Subtract && bitlen != bvec::variadic_bitlen + ? bitlen + : std::max(x.size(), y.size()) + !Subtract; + + bdd carry = bdd_const(Subtract); + + std::vector res; + res.reserve(size); + + for (size_t i = 0; i < size; ++i) { + const bdd x_bit = x.at(i); + const bdd y_bit = Subtract ? ~y.at(i) : y.at(i); + + const bdd res_bit = x_bit ^ y_bit ^ carry; + res.push_back(res_bit); + + carry = (carry & (x_bit | y_bit)) | (x_bit & y_bit); + } + + if constexpr (!Subtract) { + // This assumes that the vector constructor truncates size above bitlen and any false suffix + // to fix the possibly erronous highest bits. + res.push_back(carry); + } + + return bvec(bitlen, res); + } + + bvec + bvec_add(const bvec& x, const bvec& y) + { + return __bvec_add(x, y); + } + + bvec + bvec_sub(const bvec& x, const bvec& y) + { + return __bvec_add(x, y); + } + + // Helper + bvec + bvec_truncate(size_t bitlen, const bvec& x) + { + bvec y = x; + y.truncate(bitlen); + return y; + } +} diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h new file mode 100644 index 000000000..774fa22b4 --- /dev/null +++ b/src/adiar/bvec.h @@ -0,0 +1,395 @@ +#ifndef ADIAR_BVEC_H +#define ADIAR_BVEC_H + +//////////////////////////////////////////////////////////////////////////////////////////////////// +/// \defgroup module__bvec Symbolic Bitvectors +/// +/// \brief A symbolic bitvector (`bvec`) combines several \ref module__bdd together to simulate an +/// unsigned integer of a certain bitlength. As part of this, we support various logic +/// operations and arithmetic operations. +/// +/// \hidegroupgraph +//////////////////////////////////////////////////////////////////////////////////////////////////// + +#include +#include +#include +#include + +#include +#include + +namespace adiar +{ + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Symbolic Bitvector + ////////////////////////////////////////////////////////////////////////////////////////////////// + class bvec + { + public: + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Default width of a `bvec` if nothing else is provided. + /// + /// \details Most functions include an optional `bitlen` as their first argument. If nothing is + /// or otherwise stated, then this value is used instead. + /// + /// \details To change it, either set the variable at runtime or set it at compile time with the + /// `ADIAR_BVEC_BITLEN` preprocessor variable. + //////////////////////////////////////////////////////////////////////////////////////////////// + static constexpr size_t variadic_bitlen = 0; + + private: + /// \brief Vector to hold the BDDs representing the actual bits, starting from the least + /// significant bit. This only contains up to the most significant non-false bit. + std::vector _bits; + + /// \brief The total number of bits, including the only-false suffix. + size_t _bitlen; + + /// \brief The default BDD to be returned if asking out of bounds. + const bdd _default_value = bdd(); + + public: + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief The variable-sized zero-valued bitvector. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(); + + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(const bvec& fs); + + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(bvec&& fs); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct a variable-sized bitvector with initial `value`. + /// + /// \see bvec_const + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(size_t value); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct a fixed-size bitvector with initial value with `bitlen` number of bits. + /// + /// \see bvec_const + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(size_t bitlen, size_t value); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct a variable-size from a raw vector (least to most significant bit) and with + /// a variadic number of bits. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(const std::vector& bits); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct a fixed-size bitvector from a raw vector (least to most significant bit) + /// and a certain bit length. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(size_t bitlen, const std::vector& bits); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct variable-size bitvector from a movable raw vector (least to most + /// significant bit) and with a variadic number of bits. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(std::vector&& bits); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct a fixed-size bitvector from a movable raw vector (least to most significant + /// bit) and a certain bit length. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(size_t bitlen, std::vector&& bits); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct variable-sized bitvector from a pair of iterators from least to most + /// significant bit. + //////////////////////////////////////////////////////////////////////////////////////////////// + template >> + bvec(ForwardIt begin, ForwardIt end) + : bvec(std::vector(begin, end)) + {} + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct a fixed-size bitvector with a certain bit length and an iterator pair from + /// least to most significant bit. + //////////////////////////////////////////////////////////////////////////////////////////////// + template >> + bvec(size_t bitlen, ForwardIt begin, ForwardIt end) + : bvec(bitlen, std::vector(begin, end)) + {} + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Width of the symbolic bit vector. + //////////////////////////////////////////////////////////////////////////////////////////////// + inline size_t + bitlen() const + { + return _bitlen; + } + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief The actual number of bits represented, i.e. the position of the most significant bit. + //////////////////////////////////////////////////////////////////////////////////////////////// + inline size_t + size() const + { + return _bits.size(); + } + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief The BDD at a certain bit position. + //////////////////////////////////////////////////////////////////////////////////////////////// + const bdd& + at(size_t index) const; + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Iterator of bits from least to most significant bit. + //////////////////////////////////////////////////////////////////////////////////////////////// + std::vector::const_iterator + begin() const; + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief End of `begin()` iteration. + //////////////////////////////////////////////////////////////////////////////////////////////// + std::vector::const_iterator + end() const; + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Iterator of bits from most to least significant bit. + //////////////////////////////////////////////////////////////////////////////////////////////// + std::vector::const_reverse_iterator + rbegin() const; + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief End of `rbegin()` iteration. + //////////////////////////////////////////////////////////////////////////////////////////////// + std::vector::const_reverse_iterator + rend() const; + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Provides a human-readable string representation of the bitvector. + //////////////////////////////////////////////////////////////////////////////////////////////// + std::string + to_string() const; + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Changes the width of the vector, discarding bits if decreasing in size. + //////////////////////////////////////////////////////////////////////////////////////////////// + void + truncate(size_t bitlen = bvec::variadic_bitlen); + }; + + /// \cond + std::ostream& + operator<<(std::ostream& os, const bvec& a); + /// \endcond + + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__constructors Constructors + /// + /// \hidegroupgraph + /// + /// \{ + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief The all-zero bitvector. + /// + /// \param bitlen The width of the bit-vector, i.e. the number of 0 bits. By default, this is + /// a variable size. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_false(size_t bitlen = bvec::variadic_bitlen); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief The variable-sized bitvector with the first `bits` set to 1. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_true(size_t bits); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief The fixed-size bitvector with the first `bits` set to 1. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_true(size_t bitlen, size_t bits); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Create a variable-size bitvector which contains the given (non-negative) integer. + /// + /// \param value The integer to be represented. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_const(size_t value); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Create a fixed-size bitvector which contains the given (non-negative) integer. + /// + /// \param bitlen The width of the bit-vector, possibly truncating `value` if there is not enough + /// space for it. By default, this is `bvec::variadic_bitlen`. + /// + /// \param value The integer to be represented. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_const(size_t bitlen, size_t value); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct variable-sized bitvector from a pair of iterators from least to most + /// significant bit. + //////////////////////////////////////////////////////////////////////////////////////////////// + template >> + bvec + bvec_vars(ForwardIt begin, ForwardIt end) + { + return bvec(std::vector(begin, end)); + } + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct fixed-size bitvector with a certain bit length and an iterator pair from + /// least to most significant bit. + //////////////////////////////////////////////////////////////////////////////////////////////// + template >> + bvec + bvec_vars(size_t bitlen, ForwardIt begin, ForwardIt end) + { + return bvec(bitlen, std::vector(begin, end)); + } + + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__comparators Comparators + /// + /// \hidegroupgraph + /// + /// \{ + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Equality comparison of BDDs + //////////////////////////////////////////////////////////////////////////////////////////////// + bool + bvec_equal(const bvec& x, const bvec& y); + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bvec_equal + ////////////////////////////////////////////////////////////////////////////////////////////////// + bool + operator==(const bvec& x, const bvec& y); + + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__logical Logical Operations + /// + /// \hidegroupgraph + /// + /// \{ + + // TODO: Add optional `bitlen` as a first argument. + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Bitwise conjunction of two bitvectors, upcasting the `bitlen` if needed. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_and(const bvec& x, const bvec& y); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Bitwise disjunction of two bitvectors, upcasting the `bitlen` if needed. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_or(const bvec& x, const bvec& y); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Bitwise exclusive disjunction of two bitvectors, upcasting the `bitlen` if needed. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_xor(const bvec& x, const bvec& y); + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Bitwise negation of a bitvectors. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_not(const bvec& x); + + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__arithmetic Arithmetic Operations + /// + /// \hidegroupgraph + /// + /// \{ + + // TODO: Add optional `bitlen` as a first argument. + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Arithmetic addition of two symbolic bit-vectors. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_add(const bvec& x, const bvec& y); + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bvec_add + ////////////////////////////////////////////////////////////////////////////////////////////////// + inline bvec + operator+(const bvec& x, const bvec& y) + { + return bvec_add(x, y); + } + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Arithmetic subtraction of two symbolic bit-vectors. + /// + /// \details If `x < y`, then this will result in an underflow with `y.size()` bits. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec + bvec_sub(const bvec& x, const bvec& y); + + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__utility Utility + /// + /// \hidegroupgraph + /// + /// \{ + + bvec + bvec_truncate(size_t bitlen, const bvec& x); + + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// +} + +// TODO: Implement arithmetic operations +// TODO: Add variables, bvec_var(ITER begin, ITER end, bitlen) + +#endif // ADIAR_BVEC_H diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index bde706986..e77056859 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -26,6 +26,7 @@ #include #include #include +#include #include namespace adiar diff --git a/tests/adiar/CMakeLists.txt b/tests/adiar/CMakeLists.txt index c55d6d003..823657911 100644 --- a/tests/adiar/CMakeLists.txt +++ b/tests/adiar/CMakeLists.txt @@ -1,5 +1,6 @@ add_test(adiar-bool_op bool_op.test.cpp) add_test(adiar-builder builder.test.cpp) +add_test(adiar-bvec bvec.test.cpp) add_test(adiar-domain domain.test.cpp) add_test(adiar-exec_policy exec_policy.test.cpp) add_test(adiar-functional functional.test.cpp) diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp new file mode 100644 index 000000000..996e702f8 --- /dev/null +++ b/tests/adiar/bvec.test.cpp @@ -0,0 +1,891 @@ +#include "../test.h" + +#include + +go_bandit([]() { + describe("adiar/bvec.h", []() { + describe("bvec_false()", []() { + it("has variable bitlen by default", [&]() { + const bvec x = bvec_false(); + + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(x.size(), Is().EqualTo(0u)); + }); + + it("has 16 bits when asked", [&]() { + const bvec x = bvec_false(16); + + AssertThat(x.bitlen(), Is().EqualTo(16u)); + AssertThat(x.size(), Is().EqualTo(0u)); + }); + + it("has all its bits set to false", [&]() { + const bvec x = bvec_false(8); + + for (size_t i = 0; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_false())); } + }); + }); + + describe("bvec_true()", []() { + it("has no bits set when set so without a bitlen", [&]() { + const bvec x = bvec_true(8); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(x.size(), Is().EqualTo(8u)); + + // Check that all bits are one + for (size_t i = 0; i < x.size(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_true())); } + }); + + it("has 32 bits set when set so without a bitlen", [&]() { + const bvec x = bvec_true(32); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(x.size(), Is().EqualTo(32u)); + + // Check that all bits are one + for (size_t i = 0; i < x.size(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_true())); } + }); + + it("has 4 bits set when set so with a fixed bitlen of 8", [&]() { + const bvec x = bvec_true(8, 4); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + AssertThat(x.size(), Is().EqualTo(4u)); + + // Check that the bits are set as expected + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_true())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_false())); + AssertThat(x.at(6), Is().EqualTo(bdd_false())); + AssertThat(x.at(7), Is().EqualTo(bdd_false())); + }); + + it("truncates when more bits are set to one than the bit length", [&]() { + const bvec x = bvec_true(8, 12); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + AssertThat(x.size(), Is().EqualTo(8u)); + + // Check that the bits are set as expected + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_true())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_true())); + AssertThat(x.at(5), Is().EqualTo(bdd_true())); + AssertThat(x.at(6), Is().EqualTo(bdd_true())); + AssertThat(x.at(7), Is().EqualTo(bdd_true())); + }); + }); + + describe("bvec_const", []() { + it("0 has by default variadic bitlen", [&]() { + const bvec x = bvec_const(0); + AssertThat(x.size(), Is().EqualTo(0u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + }); + + it("0 can have a custom bitlen", [&]() { + const bvec x = bvec_const(7, 0); + AssertThat(x.size(), Is().EqualTo(0u)); + AssertThat(x.bitlen(), Is().EqualTo(7u)); + }); + + it("0 is derived to be ()", [&]() { + const bvec x = bvec_const(0); + + // Check that all bits are zero + for (size_t i = 0; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_false())); } + }); + + it("1 has by default variadic bitlen", [&]() { + const bvec x = bvec_const(1); + AssertThat(x.size(), Is().EqualTo(1u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + }); + + it("1 can have a custom bitlen", [&]() { + const bvec x = bvec_const(16, 1); + AssertThat(x.size(), Is().EqualTo(1u)); + AssertThat(x.bitlen(), Is().EqualTo(16u)); + }); + + it("1 is derived to be (1)", [&]() { + const bvec x = bvec_const(1); + + // Check that the first bit is set + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + + // Check that all bits are zero + for (size_t i = 1; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_false())); } + }); + + it("2 is derived to be (01)", [&]() { + const bvec x = bvec_const(2); + + // Check that the first bit is set + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + + // Check that all bits are zero + for (size_t i = 2; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_false())); } + }); + + it("42 has default size as bitlen", [&]() { + const bvec x = bvec_const(42); + AssertThat(x.size(), Is().EqualTo(6u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + }); + + it("42 can have a custom bitlen", [&]() { + const bvec x = bvec_const(24, 42); + AssertThat(x.size(), Is().EqualTo(6u)); + AssertThat(x.bitlen(), Is().EqualTo(24u)); + }); + + it("42 is derived to be (101010)", [&]() { + const bvec x = bvec_const(42); + + // Check that encoding is 101010 + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_true())); + }); + + it("(int) -1 is derived to be (111...1) with 32 bits", [&]() { + const bvec x = bvec_const(32, -1); + + AssertThat(x.bitlen(), Is().EqualTo(32u)); + for (size_t i = 0; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_true())); } + }); + + it("-2^32 is derived to be (000..01) with 32 bits", [&]() { + const bvec x = bvec_const(32, INT32_MIN); + + AssertThat(x.bitlen(), Is().EqualTo(32u)); + for (size_t i = 0; i < x.bitlen() - 1; i++) { + AssertThat(x.at(i), Is().EqualTo(bdd_false())); + } + + AssertThat(x.at(x.bitlen() - 1), Is().EqualTo(bdd_true())); + }); + }); + + describe("bvec::bvec(...)", []() { + describe("bvec::bvec(value)", []() { + it("derives 0 to be () with 0 bits required", [&]() { + const bvec x(0); + + AssertThat(x.size(), Is().EqualTo(0u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + }); + + it("derives 1 to be (1) with 1 bit required", [&]() { + const bvec x(1); + + AssertThat(x.size(), Is().EqualTo(1u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + + // Check that encoding is 1 + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + }); + + it("derives 2 to be (01) with 2 bits required", [&]() { + const bvec x(2); + + AssertThat(x.size(), Is().EqualTo(2u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + + // Check that encoding is 01 + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + }); + + it("derives 3 to be (01) with 2 bits required", [&]() { + const bvec x(3); + + AssertThat(x.size(), Is().EqualTo(2u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + + // Check that encoding is 11 + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + }); + + it("derives 42 to be (010101) with 6 bits required", [&]() { + const bvec x(42); + + AssertThat(x.size(), Is().EqualTo(6u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + + // Check that encoding is 101010 + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_true())); + }); + }); + + describe("bvec::bvec(bitlen, value)", []() { + it("derives 0 to be () with 7 number of bits", [&]() { + const bvec x(7, 0); + + AssertThat(x.size(), Is().EqualTo(0u)); + AssertThat(x.bitlen(), Is().EqualTo(7u)); + + // Check that all bits are false + for (size_t i = 0; i < x.bitlen(); i++) { + AssertThat(x.at(i), Is().EqualTo(bdd_false())); + } + }); + + it("derives 1 to be (1) with 9 number of bits", [&]() { + const bvec x(9, 1); + + AssertThat(x.size(), Is().EqualTo(1u)); + AssertThat(x.bitlen(), Is().EqualTo(9u)); + + // Check that encoding is 1 + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + + // Check that the rest of the bits are zero + for (size_t i = 1; i < x.bitlen(); i++) { + AssertThat(x.at(i), Is().EqualTo(bdd_false())); + } + }); + + it("derives 42 to be (010101) with 11 number of bits", [&]() { + const bvec x(11, 42); + + AssertThat(x.size(), Is().EqualTo(6u)); + AssertThat(x.bitlen(), Is().EqualTo(11u)); + + // Check that encoding is 101010 + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_true())); + + // Check that the rest of the bits are zero + for (size_t i = 6; i < x.bitlen(); i++) { + AssertThat(x.at(i), Is().EqualTo(bdd_false())); + } + }); + + it("truncates 42 to be (0101) with 4 number of bits", [&]() { + const bvec x(4, 42); + + AssertThat(x.size(), Is().EqualTo(4u)); + AssertThat(x.bitlen(), Is().EqualTo(4u)); + + // Check that encoding is 101010 + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + }); + }); + + describe("bvec::bvec(bits)", []() { + it("copies over bits (001)", [&]() { + const bvec x({ bdd_false(), bdd_false(), bdd_true() }); + + AssertThat(x.size(), Is().EqualTo(3u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_false())); + AssertThat(x.at(2), Is().EqualTo(bdd_true())); + }); + + it("copies over bits (1011)", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true(), bdd_true() }); + + AssertThat(x.size(), Is().EqualTo(4u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.at(1), Is().EqualTo(bdd_false())); + AssertThat(x.at(2), Is().EqualTo(bdd_true())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + }); + + it("ignores false bits at the end of (1010)", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true(), bdd_false() }); + + AssertThat(x.size(), Is().EqualTo(3u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.at(1), Is().EqualTo(bdd_false())); + AssertThat(x.at(2), Is().EqualTo(bdd_true())); + AssertThat(x.at(3), Is().EqualTo(bdd_false())); + }); + }); + + describe("bvec::bvec(bitlen, bits)", []() { + it("copies over bits (1001) with a bit length of 8", [&]() { + const bvec x(8, { bdd_true(), bdd_false(), bdd_false(), bdd_true() }); + + AssertThat(x.size(), Is().EqualTo(4u)); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.at(1), Is().EqualTo(bdd_false())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_false())); + AssertThat(x.at(6), Is().EqualTo(bdd_false())); + AssertThat(x.at(7), Is().EqualTo(bdd_false())); + }); + + it("ignores false bits at the end of (1000)", [&]() { + const bvec x(8, { bdd_true(), bdd_false(), bdd_false(), bdd_false() }); + + AssertThat(x.size(), Is().EqualTo(1u)); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.at(1), Is().EqualTo(bdd_false())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_false())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_false())); + AssertThat(x.at(6), Is().EqualTo(bdd_false())); + AssertThat(x.at(7), Is().EqualTo(bdd_false())); + }); + + it("truncates non-false bits at the end of (1011) down to 2 bits", [&]() { + const bvec x(2, { bdd_true(), bdd_false(), bdd_false(), bdd_false() }); + + AssertThat(x.size(), Is().EqualTo(1u)); + AssertThat(x.bitlen(), Is().EqualTo(2u)); + + AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.at(1), Is().EqualTo(bdd_false())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_false())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_false())); + AssertThat(x.at(6), Is().EqualTo(bdd_false())); + AssertThat(x.at(7), Is().EqualTo(bdd_false())); + }); + }); + + describe("bvec::bvec(begin, end)", []() { + it("copies over bits from iterator of (010101)", [&]() { + const std::vector vec( + { bdd_false(), bdd_true(), bdd_false(), bdd_true(), bdd_false(), bdd_true() }); + const bvec x(vec.begin(), vec.end()); + + AssertThat(x.size(), Is().EqualTo(6u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_true())); + }); + }); + + describe("bvec::bvec(bitlen, begin, end)", []() { + it("copies over bits from iterator of (010101) with 8 bits", [&]() { + const std::vector vec( + { bdd_false(), bdd_true(), bdd_false(), bdd_true(), bdd_false(), bdd_true() }); + const bvec x(8, vec.begin(), vec.end()); + + AssertThat(x.size(), Is().EqualTo(6u)); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + AssertThat(x.at(5), Is().EqualTo(bdd_true())); + AssertThat(x.at(6), Is().EqualTo(bdd_false())); + AssertThat(x.at(7), Is().EqualTo(bdd_false())); + }); + + it("truncates bits from iterator of (010101) with 5 bits", [&]() { + const std::vector vec( + { bdd_false(), bdd_true(), bdd_false(), bdd_true(), bdd_false(), bdd_true() }); + const bvec x(5, vec.begin(), vec.end()); + + AssertThat(x.size(), Is().EqualTo(4u)); + AssertThat(x.bitlen(), Is().EqualTo(5u)); + + AssertThat(x.at(0), Is().EqualTo(bdd_false())); + AssertThat(x.at(1), Is().EqualTo(bdd_true())); + AssertThat(x.at(2), Is().EqualTo(bdd_false())); + AssertThat(x.at(3), Is().EqualTo(bdd_true())); + AssertThat(x.at(4), Is().EqualTo(bdd_false())); + }); + }); + }); + + describe("bvec_equal", []() { + it("compares 101 == 101", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true() }); + + AssertThat(bvec_equal(x, y), Is().True()); + }); + + it("compares 0101 == 101", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true(), bdd_false() }); + + AssertThat(bvec_equal(x, y), Is().True()); + }); + + it("compares 101 == 0101", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true(), bdd_false() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true() }); + + AssertThat(bvec_equal(x, y), Is().True()); + }); + + it("compares 101 != 1101", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true(), bdd_true() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true() }); + + AssertThat(bvec_equal(x, y), Is().False()); + }); + + it("compares 1101 != 101", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true(), bdd_true() }); + + AssertThat(bvec_equal(x, y), Is().False()); + }); + + it("compares 1101 != 1110", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true(), bdd_true() }); + const bvec y({ bdd_false(), bdd_true(), bdd_true(), bdd_true() }); + + AssertThat(bvec_equal(x, y), Is().False()); + }); + + it("compares 1100 != 1110", [&]() { + const bvec x({ bdd_false(), bdd_false(), bdd_true(), bdd_true() }); + const bvec y({ bdd_false(), bdd_true(), bdd_true(), bdd_true() }); + + AssertThat(bvec_equal(x, y), Is().False()); + }); + + it("compares 1x0 == 1x0", [&]() { + const bvec x({ bdd_false(), bdd_ithvar(42), bdd_true() }); + const bvec y({ bdd_false(), bdd_ithvar(42), bdd_true() }); + + AssertThat(bvec_equal(x, y), Is().True()); + }); + + it("compares 1x0 != 1y0", [&]() { + const bvec x({ bdd_false(), bdd_ithvar(42), bdd_true() }); + const bvec y({ bdd_false(), bdd_ithvar(11), bdd_true() }); + + AssertThat(bvec_equal(x, y), Is().False()); + }); + }); + + describe("bvec_and", []() { + describe("constants", []() { + it("computes 5 & 3 == 1 (101 & 011 == 001)", [&]() { + const bvec x = bvec_const(8, 5); + const bvec y = bvec_const(8, 3); + const bvec expected = bvec_const(8, 1); + + const bvec res = bvec_and(x, y); + + AssertThat(res, Is().EqualTo(expected)); + }); + + it("computes 0 & 3 == 0 (000 & 011 == 000)", [&]() { + const bvec x = bvec_const(8, 0); + const bvec y = bvec_const(8, 3); + const bvec expected = bvec_const(8, 0); + + const bvec res = bvec_and(x, y); + + AssertThat(res, Is().EqualTo(expected)); + }); + }); + }); + + describe("bvec_or", []() { + describe("constants", []() { + it("computes 5 | 3 == 7 (101 | 011 == 111)", [&]() { + const bvec x = bvec_const(8, 5); + const bvec y = bvec_const(8, 3); + const bvec expected = bvec_const(8, 7); + + const bvec res = bvec_or(x, y); + + AssertThat(res, Is().EqualTo(expected)); + }); + + it("computes 0 | 3 == 3 (000 | 011 == 011)", [&]() { + const bvec x = bvec_const(8, 0); + const bvec y = bvec_const(8, 3); + const bvec expected = bvec_const(8, 3); + + const bvec res = bvec_or(x, y); + + AssertThat(res, Is().EqualTo(expected)); + }); + }); + }); + + describe("bvec_xor", []() { + describe("constants", []() { + it("computes 5 ^ 3 == 6 (101 ^ 011 == 110)", [&]() { + const bvec x = bvec_const(8, 5); + const bvec y = bvec_const(8, 3); + const bvec expected = bvec_const(8, 6); + + const bvec res = bvec_xor(x, y); + + AssertThat(res, Is().EqualTo(expected)); + }); + + it("computes 0 ^ 3 == 3 (000 ^ 011 == 011)", [&]() { + const bvec x = bvec_const(8, 0); + const bvec y = bvec_const(8, 3); + const bvec expected = bvec_const(8, 3); + + const bvec res = bvec_xor(x, y); + + AssertThat(res, Is().EqualTo(expected)); + }); + + it("computes 255 ^ 3 == 252 (11111111 ^ 00000011 == 11111100)", [&]() { + const bvec x = bvec_const(8, 255); + const bvec y = bvec_const(8, 3); + const bvec expected = bvec_const(8, 252); + + const bvec res = bvec_xor(x, y); + + AssertThat(res, Is().EqualTo(expected)); + }); + }); + }); + + describe("bvec_not", []() { + describe("constants", []() { + it("computes ~3 == 252 for bitlength 8 (~00000011 == 11111100)", [&]() { + const bvec x = bvec_const(8, 3); + const bvec expected = bvec_const(8, 252); + + const bvec res = bvec_not(x); + + AssertThat(res, Is().EqualTo(expected)); + }); + + it("computes ~3 == (65535 - 3) for bitlength 16 (~0000000000000011 == 1111111111111100)", + [&]() { + const bvec x = bvec_const(16, 3); + const bvec expected = bvec_const(16, (USHRT_MAX - 3)); + + const bvec res = bvec_not(x); + + AssertThat(res, Is().EqualTo(expected)); + }); + + it("computes ~2 == 1 for variadic bitlength", [&]() { + const bvec x = bvec_const(2); + const bvec res = bvec_not(x); + + const bvec expected = bvec_const(1); + AssertThat(res, Is().EqualTo(expected)); + }); + + it("computes ~3 == 0 for variadic bitlength", [&]() { + const bvec x = bvec_const(3); + const bvec res = bvec_not(x); + + const bvec expected = bvec_const(0); + AssertThat(res, Is().EqualTo(expected)); + }); + }); + }); + + describe("bvec_add", []() { + it("computes bvec[8](5) + bvec[8](3)", [&]() { + const bvec a = bvec_const(8, 5); + const bvec b = bvec_const(8, 3); + + const bvec expected = bvec_const(8, 8); + const bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(4u)); + }); + + it("computes bvec[8](42) + bvec[8](3)", [&]() { + const bvec a = bvec_const(8, 42); + const bvec b = bvec_const(8, 3); + + const bvec expected = bvec_const(8, 45); + const bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(6u)); + }); + + it("overflows bvec[8](255) + bvec[8](1)", [&]() { + const bvec a = bvec_const(8, 255); + const bvec b = bvec_const(8, 1); + + const bvec expected = bvec_const(8, 0); + const bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(0u)); + }); + + it("upcasts bvec[32](5) + bvec[8](3)", [&]() { + const bvec a = bvec_const(32, 5); + const bvec b = bvec_const(8, 3); + + const bvec expected = bvec_const(32, 8); + const bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(4u)); + }); + + it("upcasts bvec[32](0) + bvec[8](3)", [&]() { + const bvec a = bvec_const(32, 0); + const bvec b = bvec_const(8, 3); + + const bvec expected = bvec_const(32, 3); + const bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(2u)); + }); + + it("upcasts bvec[8](0) + bvec[32](3)", [&]() { + const bvec a = bvec_const(8, 0); + const bvec b = bvec_const(32, 3); + + const bvec expected = bvec_const(32, 3); + const bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(2u)); + }); + + it("upcasts bvec[32](17) + bvec[8](42)", [&]() { + const bvec a = bvec_const(32, 17); + const bvec b = bvec_const(8, 42); + + const bvec expected = bvec_const(32, 59); + const bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(6u)); + }); + + it("fixes size of bvec[_](9) + bvec[8](21)", [&]() { + const bvec a = bvec_const(9); + const bvec b = bvec_const(8, 21); + + const bvec expected = bvec_const(8, 30); + const bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(5u)); + }); + + it("fixes size of bvec[16](2) + bvec[_](4)", [&]() { + const bvec a = bvec_const(16, 2); + const bvec b = bvec_const(4); + + const bvec expected = bvec_const(16, 6); + const bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(16u)); + AssertThat(res.size(), Is().EqualTo(3u)); + }); + + it("makes bvec[8](42) + bvec[_](512) variadic bit length", [&]() { + const bvec a = bvec_const(8, 42); + const bvec b = bvec_const(512); + + const bvec expected = bvec_const(554); + const bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(res.size(), Is().EqualTo(10u)); + }); + + it("makes bvec[_](320) + bvec[8](5) variadic bit length", [&]() { + const bvec a = bvec_const(320); + const bvec b = bvec_const(8, 5); + + const bvec expected = bvec_const(325); + const bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(res.size(), Is().EqualTo(9u)); + }); + }); + + describe("bvec_sub", []() { + it("compute bvec[8](42) - bvec[8](3)", [&]() { + const bvec x = bvec_const(8, 42); + const bvec y = bvec_const(8, 3); + + const bvec expected = bvec_const(32, 39); + const bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(6u)); + }); + + it("compute bvec[8](140) - bvec[8](4)", [&]() { + const bvec x = bvec_const(8, 140); + const bvec y = bvec_const(8, 4); + + const bvec expected = bvec_const(8, 136); + const bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(8u)); + }); + + it("underflows bvec[8](0) - bvec[8](1)", [&]() { + const bvec x = bvec_const(8, 0); + const bvec y = bvec_const(8, 1); + + const bvec expected = bvec_const(8, -1); + const bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(8u)); + }); + + it("underflows bvec[8](4) - bvec[8](7)", [&]() { + const bvec x = bvec_const(8, 4); + const bvec y = bvec_const(8, 7); + + const bvec expected = bvec_const(8, -3); + const bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(8u)); + }); + + it("underflows bvec[16](21) - bvec[8](42)", [&]() { + const bvec x = bvec_const(16, 21); + const bvec y = bvec_const(8, 42); + + const bvec expected = bvec_const(16, -21); + const bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(16u)); + AssertThat(res.size(), Is().EqualTo(16u)); + }); + + it("underflows bvec[8](4) - bvec[16](7)", [&]() { + const bvec x = bvec_const(8, 3); + const bvec y = bvec_const(16, 9); + + const bvec expected = bvec_const(16, -6); + const bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(16u)); + AssertThat(res.size(), Is().EqualTo(16u)); + }); + + it("compute bvec[_](6) - bvec[_](4)", [&]() { + const bvec x = bvec_const(6); + const bvec y = bvec_const(4); + + const bvec expected = bvec_const(2); + const bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(res.size(), Is().EqualTo(2u)); + }); + + it("compute bvec[_](4) - bvec[_](6)", [&]() { + const bvec x = bvec_const(4); + const bvec y = bvec_const(6); + + const bvec expected = bvec_const(3, -2); + const bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(res.size(), Is().EqualTo(3u)); + }); + + it("makes bvec[_](511) - bvec[8](42) variadic bit length", [&]() { + const bvec a = bvec_const(511); + const bvec b = bvec_const(8, 42); + + const bvec expected = bvec_const(469); + const bvec res = bvec_sub(a, b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(res.size(), Is().EqualTo(9u)); + }); + + it("makes bvec[4](5) - bvec[_](320) variadic bit length", [&]() { + const bvec a = bvec_const(4, 5); + const bvec b = bvec_const(320); + + const bvec expected = bvec_const(8, -315); + const bvec res = bvec_sub(a, b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(res.size(), Is().EqualTo(8u)); + }); + }); + + describe("bvec_truncate", []() { + it("truncates to bitlen", [&]() { + const bvec x = bvec_true(32, 32); + + const bvec expected = bvec_true(8, 8); + const bvec res = bvec_truncate(8, x); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(8u)); + }); + + it("extends to bitlen", [&]() { + const bvec x = bvec_true(4, 4); + AssertThat(x.bitlen(), Is().EqualTo(4u)); + + const bvec expected = bvec_true(8, 4); + const bvec res = bvec_truncate(8, x); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(4u)); + }); + + it("truncates false prefix", [&]() { + const bvec x = bvec_const(18); + + const bvec expected = bvec_const(2); + const bvec res = bvec_truncate(4, x); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(4u)); + AssertThat(res.size(), Is().EqualTo(2u)); + }); + }); + }); +}); diff --git a/tests/all.cpp b/tests/all.cpp index 6d74de63e..c2760701e 100644 --- a/tests/all.cpp +++ b/tests/all.cpp @@ -105,6 +105,10 @@ go_bandit([]() { #include "adiar/zdd/subset.test.cpp" #include "adiar/zdd/zdd.test.cpp" +//////////////////////////////////////////////////////////////////////////////// +// Adiar BDD Bit Vector unit tests +#include "adiar/bvec.test.cpp" + //////////////////////////////////////////////////////////////////////////////// // Adiar Deinitialization unit tests go_bandit([]() {