From cb9401699cea355975a16fb5be7aa771dba857af Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 19 Mar 2026 16:56:44 +0100 Subject: [PATCH 01/35] Initial setup of bvec class with tests --- makefile | 3 ++ src/adiar/CMakeLists.txt | 1 + src/adiar/bvec.h | 99 ++++++++++++++++++++++++++++++++++++++ tests/adiar/CMakeLists.txt | 1 + tests/adiar/bvec.test.cpp | 49 +++++++++++++++++++ 5 files changed, 153 insertions(+) create mode 100644 src/adiar/bvec.h create mode 100644 tests/adiar/bvec.test.cpp 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..890f64b35 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 diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h new file mode 100644 index 000000000..aecec7cc7 --- /dev/null +++ b/src/adiar/bvec.h @@ -0,0 +1,99 @@ +#ifndef ADIAR_BVEC_H +#define ADIAR_BVEC_H + +#include +#include + +namespace adiar { + class bvec + { + private: + const std::vector _bits; + + public: + ///////////////////////////////////////////////////////////////////////// + /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" + ///////////////////////////////////////////////////////////////////////// + bvec() + : _bits(0) + {} + ///////////////////////////////////////////////////////////////////////// + /// \brief Copy constructor + ///////////////////////////////////////////////////////////////////////// + bvec(const bvec& fs) + : _bits(fs._bits) + {} + ///////////////////////////////////////////////////////////////////////// + /// \brief Move constructor for right-hand values + ///////////////////////////////////////////////////////////////////////// + bvec(bvec&& fs) + : _bits(std::move(fs._bits)) + {} + + ///////////////////////////////////////////////////////////////////////// + /// \brief Conversion constructor from a raw bit-vector + ///////////////////////////////////////////////////////////////////////// + bvec(const std::vector& bits) + : _bits(bits) + {} + ///////////////////////////////////////////////////////////////////////// + /// \brief Conversion constructor from a raw bit-vector for right-hand values + ///////////////////////////////////////////////////////////////////////// + bvec(std::vector&& bits) + : _bits(std::move(bits)) + {} + + ///////////////////////////////////////////////////////////////////////// + /// \brief Parameterized constructor with length `bitlen` and given initial value `f` (default value is `bdd()`) + ///////////////////////////////////////////////////////////////////////// + bvec(const size_t bitlen, const bdd& f = bdd()) + : _bits(bitlen,f) + {} + + public: + size_t bitlen() const { return _bits.size(); } + + const bdd& // return type + at(size_t index) const //name(...) context + { + return _bits.at(index); + } + + std::vector::const_iterator + begin() const + { + return _bits.cbegin(); + } + + std::vector::const_iterator + end() const + { + return _bits.cend(); + } + + + }; + + bvec bvec_false(size_t bitlen) { + return bvec(bitlen,bdd_false()); + } + + bvec bvec_true(size_t bitlen) { + return bvec(bitlen,bdd_true()); + } + + bvec bvec_const(size_t bitlen, size_t i) { + std::vector res(bitlen); + //TODO: Implement actual integer value initialization + return res; + } + + template + bvec bvec_const(Integer i) { + return bvec_const(8 * sizeof(Integer), i); + } +} + + + +#endif // ADIAR_BVEC_H 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..d086c0c07 --- /dev/null +++ b/tests/adiar/bvec.test.cpp @@ -0,0 +1,49 @@ +#include "../test.h" +#include +go_bandit([]() { + describe("adiar/bvec.h", []() { + describe("bdd_false()", []() { + it("has 16 bits when asked", [&]() { + AssertThat(bvec_false(16).bitlen(), Is().EqualTo(16u)); + }); + }); + describe("bdd_true()", []() { + it("has 32 bits when asked", [&]() { + AssertThat(bvec_true(32).bitlen(), Is().EqualTo(32u)); + }); + }); + describe("bdd_const", []() { + describe("bitlength inference", []() { + it("has 8 bitlen when constructed with char", [&]() { + const bvec x = bvec_const((char)3); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + }); + it("has 16 bitlen when constructed with short", [&]() { + const bvec x = bvec_const((short)3); + AssertThat(x.bitlen(), Is().EqualTo(16u)); + }); + it("has 32 bitlen when constructed with int", [&]() { + const bvec x = bvec_const(3); + AssertThat(x.bitlen(), Is().EqualTo(32u)); + }); + it("has 64 bitlen when constructed with long", [&]() { + const bvec x = bvec_const(3l); + AssertThat(x.bitlen(), Is().EqualTo(64u)); + }); + }); + + describe("int encoding", []() { + it("is the binary encoding of 42", [&]() { + // 42_10 == 101010_2 (010101 litte-endian) + const bvec x = bvec_const(42); + 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())); + }); + }); + }); + }); +}); \ No newline at end of file From ee7f4099ae6db5f8a1714027a8269cfe47729969 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 19 Mar 2026 17:04:24 +0100 Subject: [PATCH 02/35] Implement bdd_const initialization from integer value --- src/adiar/bvec.h | 7 +++++-- tests/adiar/bvec.test.cpp | 2 +- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index aecec7cc7..2a9f96691 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -82,9 +82,12 @@ namespace adiar { return bvec(bitlen,bdd_true()); } - bvec bvec_const(size_t bitlen, size_t i) { + bvec bvec_const(size_t bitlen, size_t value) { std::vector res(bitlen); - //TODO: Implement actual integer value initialization + for (size_t i = 0; i< bitlen; i++) { + res.at(i) = value & 1 ? bdd_true() : bdd_false(); + value >>= 1; + } return res; } diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index d086c0c07..ab1bf2b13 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -34,7 +34,7 @@ go_bandit([]() { describe("int encoding", []() { it("is the binary encoding of 42", [&]() { - // 42_10 == 101010_2 (010101 litte-endian) + // 42_10 == 101010_2 const bvec x = bvec_const(42); AssertThat(x.at(0), Is().EqualTo(bdd_false())); AssertThat(x.at(1), Is().EqualTo(bdd_true())); From 14f68d0927ced6ad9870a4e840eb698c09dcb2f7 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 19 Mar 2026 19:18:48 +0100 Subject: [PATCH 03/35] Add and, or, xor operations --- src/adiar/bvec.h | 52 +++++++++++++++- tests/adiar/bvec.test.cpp | 128 +++++++++++++++++++++++++++++++++++++- 2 files changed, 177 insertions(+), 3 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 2a9f96691..616718ebc 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -71,9 +71,10 @@ namespace adiar { return _bits.cend(); } - }; + // Constructors + bvec bvec_false(size_t bitlen) { return bvec(bitlen,bdd_false()); } @@ -95,6 +96,55 @@ namespace adiar { bvec bvec_const(Integer i) { return bvec_const(8 * sizeof(Integer), i); } + + + //Helper function for bitwise operations + //TODO: Figure out how to do higher order function templating with constrains on function signature + template> + bvec _bvec_bitwise_op(bvec x, bvec y, BDD_OP op) { + std::vector res(x.bitlen()); + + for(size_t i = 0; i < x.bitlen(); i++) { + res.at(i) = op(x.at(i),y.at(i)); + } + + return bvec(res); + } + + + // Boolean operations + bvec bvec_and(bvec x, bvec y) { + //TODO: Do we require same bitlength? If yes, do we do it at compile-time or run-time? + std::vector res(x.bitlen()); + + for(size_t i = 0; i < x.bitlen(); i++) { + res.at(i) = bdd_and(x.at(i),y.at(i)); + } + + return bvec(res); + } + + bvec bvec_or(bvec x, bvec y) { + //TODO: Do we require same bitlength? If yes, do we do it at compile-time or run-time? + std::vector res(x.bitlen()); + + for(size_t i = 0; i < x.bitlen(); i++) { + res.at(i) = bdd_or(x.at(i),y.at(i)); + } + + return bvec(res); + } + + bvec bvec_xor(bvec x, bvec y) { + //TODO: Do we require same bitlength? If yes, do we do it at compile-time or run-time? + std::vector res(x.bitlen()); + + for(size_t i = 0; i < x.bitlen(); i++) { + res.at(i) = bdd_xor(x.at(i),y.at(i)); + } + + return bvec(res); + } } diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index ab1bf2b13..884609bfe 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -33,15 +33,139 @@ go_bandit([]() { }); describe("int encoding", []() { - it("is the binary encoding of 42", [&]() { - // 42_10 == 101010_2 + it("is the binary encoding of 42 (101010)", [&]() { + // const bvec x = bvec_const(42); + // Should initialize to bitlength 32 + AssertThat(x.bitlen(), Is().EqualTo(32u)); + + // 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("is the binary encoding of -1 ", [&]() { + // + const bvec x = bvec_const(-1); + // Should initialize to bitlength 32 + AssertThat(x.bitlen(), Is().EqualTo(32u)); + + for( size_t i = 0; i < x.bitlen(); i++) { + AssertThat(x.at(i), Is().EqualTo(bdd_true())); + } + + }); + + it("is the binary encoding of -2^32", [&]() { + // + const bvec x = bvec_const(INT32_MIN); + // Should initialize to bitlength 32 + 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_and", []() { + describe("constants", []() { + it("computes 5 & 3 == 1 (101 & 011 == 001)", [&]() { + const bvec x = bvec_const((char)5); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)1); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_and(x,y); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } + }); + it("computes 0 & 3 == 0 (000 & 011 == 000)", [&]() { + const bvec x = bvec_const((char)0); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)0); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_and(x,y); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } + }); + }); + }); + describe("bvec_or", []() { + describe("constants", []() { + it("computes 5 | 3 == 7 (101 | 011 == 111)", [&]() { + const bvec x = bvec_const((char)5); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)7); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_or(x,y); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } + }); + it("computes 0 | 3 == 3 (000 | 011 == 011)", [&]() { + const bvec x = bvec_const((char)0); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)3); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_or(x,y); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } + }); + }); + }); + describe("bvec_xor", []() { + describe("constants", []() { + it("computes 5 ^ 3 == 6 (101 ^ 011 == 110)", [&]() { + const bvec x = bvec_const((char)5); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)6); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_xor(x,y); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } + }); + it("computes 0 ^ 3 == 3 (000 ^ 011 == 011)", [&]() { + const bvec x = bvec_const((char)0); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)3); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_xor(x,y); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } + }); + it("computes 255 ^ 3 == 252 (11111111 ^ 00000011 == 11111100)", [&]() { + const bvec x = bvec_const((char)255); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)252); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_xor(x,y); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } }); }); }); From 2153130e363b2d8eed646db6efc58f74e728f4c2 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 19 Mar 2026 19:37:54 +0100 Subject: [PATCH 04/35] Add bvec_not --- src/adiar/bvec.h | 11 +++++++++++ tests/adiar/bvec.test.cpp | 27 +++++++++++++++++++++++++++ 2 files changed, 38 insertions(+) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 616718ebc..a90c5fbbe 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -145,6 +145,17 @@ namespace adiar { return bvec(res); } + + bvec bvec_not(bvec x) { + //TODO: Do we require same bitlength? If yes, do we do it at compile-time or run-time? + std::vector res(x.bitlen()); + + for(size_t i = 0; i < x.bitlen(); i++) { + res.at(i) = bdd_not(x.at(i)); + } + + return bvec(res); + } } diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index 884609bfe..fbe85b9b1 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -106,6 +106,7 @@ go_bandit([]() { }); }); }); + describe("bvec_or", []() { describe("constants", []() { it("computes 5 | 3 == 7 (101 | 011 == 111)", [&]() { @@ -132,6 +133,7 @@ go_bandit([]() { }); }); }); + describe("bvec_xor", []() { describe("constants", []() { it("computes 5 ^ 3 == 6 (101 ^ 011 == 110)", [&]() { @@ -169,5 +171,30 @@ go_bandit([]() { }); }); }); + + describe("bvec_not", []() { + describe("constants", []() { + it("computes ~3 == 252 for bitlength 8 (~00000011 == 11111100)", [&]() { + const bvec x = bvec_const((char)3); + const bvec expected = bvec_const((char)252); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_not(x); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } + }); + it("computes ~3 == (65535 - 3) for bitlength 16 (~0000000000000011 == 1111111111111100)", [&]() { + const bvec x = bvec_const((short)3); + const bvec expected = bvec_const((short)(USHRT_MAX-3)); //Is this expected, or should we check bdd structure? + + const bvec res = bvec_not(x); + + for(size_t i = 0; i < x.bitlen(); i++) { + AssertThat(res.at(i), Is().EqualTo(expected.at(i))); + } + }); + }); + }); }); }); \ No newline at end of file From 8b8387b60567af905209406fe557c66408c85e66 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 26 Mar 2026 15:53:50 +0100 Subject: [PATCH 05/35] Add to_string to bvec --- src/adiar/bvec.h | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index a90c5fbbe..5971060cd 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -3,6 +3,7 @@ #include #include +#include namespace adiar { class bvec @@ -71,8 +72,44 @@ namespace adiar { return _bits.cend(); } + std::vector::const_reverse_iterator + rbegin() const + { + return _bits.crbegin(); + } + + std::vector::const_reverse_iterator + rend() const + { + return _bits.crend(); + } + + std::string + 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(); + } }; + inline std::ostream& + operator<<(std::ostream& os, const bvec& a) + { + return os << a.to_string(); + } + // Constructors bvec bvec_false(size_t bitlen) { From 1e689fa46adda89740889f81a490f12e88d41b3c Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 26 Mar 2026 15:56:53 +0100 Subject: [PATCH 06/35] Variable length bvec --- src/adiar/bvec.h | 75 ++++++++++++++++++++++++--------------- tests/adiar/bvec.test.cpp | 31 +++++++--------- 2 files changed, 58 insertions(+), 48 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 5971060cd..9763c03ba 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -3,61 +3,67 @@ #include #include +#include +#include #include namespace adiar { class bvec { private: - const std::vector _bits; + std::vector _bits; + size_t _max_length; + const bdd default_value = bdd(); public: ///////////////////////////////////////////////////////////////////////// /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" ///////////////////////////////////////////////////////////////////////// - bvec() - : _bits(0) + bvec(size_t max_length = SIZE_T_MAX) + : _bits(0), _max_length(max_length) {} ///////////////////////////////////////////////////////////////////////// /// \brief Copy constructor ///////////////////////////////////////////////////////////////////////// bvec(const bvec& fs) - : _bits(fs._bits) + : _bits(fs._bits), _max_length(fs._max_length) {} ///////////////////////////////////////////////////////////////////////// /// \brief Move constructor for right-hand values ///////////////////////////////////////////////////////////////////////// bvec(bvec&& fs) - : _bits(std::move(fs._bits)) + : _bits(std::move(fs._bits)), _max_length(fs._max_length) {} ///////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector ///////////////////////////////////////////////////////////////////////// - bvec(const std::vector& bits) - : _bits(bits) + bvec(const std::vector& bits, size_t max_length = SIZE_T_MAX) + : _bits(bits), _max_length(max_length) {} ///////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector for right-hand values ///////////////////////////////////////////////////////////////////////// - bvec(std::vector&& bits) - : _bits(std::move(bits)) + bvec(std::vector&& bits, size_t max_length = SIZE_T_MAX) + : _bits(std::move(bits)), _max_length(max_length) {} ///////////////////////////////////////////////////////////////////////// - /// \brief Parameterized constructor with length `bitlen` and given initial value `f` (default value is `bdd()`) + /// \brief Parameterized constructor with length `bitlen` and given initial value `f` ///////////////////////////////////////////////////////////////////////// - bvec(const size_t bitlen, const bdd& f = bdd()) - : _bits(bitlen,f) + bvec(const size_t bitlen, const bdd& f) + : _bits(bitlen,f), _max_length(bitlen) {} public: - size_t bitlen() const { return _bits.size(); } + size_t bitlen() const { return _max_length; } + size_t size() const { return _bits.size(); } const bdd& // return type at(size_t index) const //name(...) context { - return _bits.at(index); + if (_bits.size() <= index) { return default_value; } //TODO: This warns that we are returning a local temp. Can we move it? + return _bits.at(index); } std::vector::const_iterator @@ -112,26 +118,31 @@ namespace adiar { // Constructors - bvec bvec_false(size_t bitlen) { - return bvec(bitlen,bdd_false()); + bvec bvec_false(size_t bitlen = SIZE_T_MAX) { + return bvec(std::vector(0,bdd_false()),bitlen); } - bvec bvec_true(size_t bitlen) { - return bvec(bitlen,bdd_true()); + bvec bvec_true(size_t bitlen = SIZE_T_MAX) { + return bvec(std::vector(bitlen,bdd_true()),bitlen); } - bvec bvec_const(size_t bitlen, size_t value) { - std::vector res(bitlen); - for (size_t i = 0; i< bitlen; i++) { - res.at(i) = value & 1 ? bdd_true() : bdd_false(); + bvec bvec_const(size_t value, size_t bitlen) { + size_t msb = value != 0 ? std::max(std::ceil(std::log2(value)),1.0) : 0; + std::vector res; + res.reserve(msb); + // Should be able to compute the most significant bit position and stop after that + for (size_t i = 0; i < msb; i++) { + res.push_back(value & 1 ? bdd_true() : bdd_false()); + value >>= 1; } - return res; + + return bvec(res,bitlen); } template bvec bvec_const(Integer i) { - return bvec_const(8 * sizeof(Integer), i); + return bvec_const(i,8 * sizeof(Integer)); } @@ -151,14 +162,20 @@ namespace adiar { // Boolean operations bvec bvec_and(bvec x, bvec y) { - //TODO: Do we require same bitlength? If yes, do we do it at compile-time or run-time? - std::vector res(x.bitlen()); + const size_t size = std::max(x.size(),y.size()); + std::vector res; - for(size_t i = 0; i < x.bitlen(); i++) { - res.at(i) = bdd_and(x.at(i),y.at(i)); + for(size_t i = 0; i < size; i++) { + const bdd bit = bdd_and(x.at(i),y.at(i)); + if (!bdd_isfalse(bit)) { + while(res.size()+1 < i) { + res.push_back(bdd_false()); + } + res.push_back(bit); + } } - return bvec(res); + return bvec(res, std::max(x.bitlen(),y.bitlen())); } bvec bvec_or(bvec x, bvec y) { diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index fbe85b9b1..b8166d67b 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -14,21 +14,20 @@ go_bandit([]() { }); describe("bdd_const", []() { describe("bitlength inference", []() { - it("has 8 bitlen when constructed with char", [&]() { - const bvec x = bvec_const((char)3); - AssertThat(x.bitlen(), Is().EqualTo(8u)); - }); - it("has 16 bitlen when constructed with short", [&]() { - const bvec x = bvec_const((short)3); - AssertThat(x.bitlen(), Is().EqualTo(16u)); - }); - it("has 32 bitlen when constructed with int", [&]() { - const bvec x = bvec_const(3); + it("has 0 bitlen when constructed with 0", [&]() { + const bvec x = bvec_const(0); + AssertThat(x.size(), Is().EqualTo(0u)); AssertThat(x.bitlen(), Is().EqualTo(32u)); }); - it("has 64 bitlen when constructed with long", [&]() { - const bvec x = bvec_const(3l); - AssertThat(x.bitlen(), Is().EqualTo(64u)); + it("has 8 bitlen when constructed with max char", [&]() { + const bvec x = bvec_const((unsigned char)255); + AssertThat(x.size(), Is().EqualTo(8u)); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + }); + it("has 8 bitlen when constructed with max char", [&]() { + const bvec x = bvec_const((char)127); + AssertThat(x.size(), Is().EqualTo(7u)); + AssertThat(x.bitlen(), Is().EqualTo(8u)); }); }); @@ -36,8 +35,6 @@ go_bandit([]() { it("is the binary encoding of 42 (101010)", [&]() { // const bvec x = bvec_const(42); - // Should initialize to bitlength 32 - AssertThat(x.bitlen(), Is().EqualTo(32u)); // Check that encoding is 101010 AssertThat(x.at(0), Is().EqualTo(bdd_false())); @@ -56,8 +53,6 @@ go_bandit([]() { it("is the binary encoding of -1 ", [&]() { // const bvec x = bvec_const(-1); - // Should initialize to bitlength 32 - AssertThat(x.bitlen(), Is().EqualTo(32u)); for( size_t i = 0; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_true())); @@ -68,8 +63,6 @@ go_bandit([]() { it("is the binary encoding of -2^32", [&]() { // const bvec x = bvec_const(INT32_MIN); - // Should initialize to bitlength 32 - AssertThat(x.bitlen(), Is().EqualTo(32u)); for( size_t i = 0; i < x.bitlen()-1; i++) { AssertThat(x.at(i), Is().EqualTo(bdd_false())); From 879c8ce350f7af14281f1160dda6bb6fb2ba45f9 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 26 Mar 2026 15:57:18 +0100 Subject: [PATCH 07/35] Add bvec_equal --- src/adiar/bvec.h | 16 ++++++++++++++++ tests/adiar/bvec.test.cpp | 5 ++--- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 9763c03ba..26819f83f 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -159,6 +159,22 @@ namespace adiar { return bvec(res); } + //Comparators + + 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; + } + + bool + operator==(const bvec& x, const bvec& y) { + return bvec_equal(x,y); + } // Boolean operations bvec bvec_and(bvec x, bvec y) { diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index b8166d67b..1659e42d5 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -82,9 +82,8 @@ go_bandit([]() { const bvec res = bvec_and(x,y); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + AssertThat(res, Is().EqualTo(expected)); + }); it("computes 0 & 3 == 0 (000 & 011 == 000)", [&]() { const bvec x = bvec_const((char)0); From e73e95e541c7cd8fcd120323082c13ca71e9e656 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 26 Mar 2026 16:14:20 +0100 Subject: [PATCH 08/35] Use bitwise_op for binary operations in bvec --- src/adiar/bvec.h | 52 ++++++++++++--------------------------- tests/adiar/bvec.test.cpp | 5 ++-- 2 files changed, 18 insertions(+), 39 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 26819f83f..34dfda66e 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -148,15 +148,22 @@ namespace adiar { //Helper function for bitwise operations //TODO: Figure out how to do higher order function templating with constrains on function signature - template> + template bvec _bvec_bitwise_op(bvec x, bvec y, BDD_OP op) { - std::vector res(x.bitlen()); + const size_t size = std::max(x.size(),y.size()); + std::vector res; - for(size_t i = 0; i < x.bitlen(); i++) { - res.at(i) = op(x.at(i),y.at(i)); + for(size_t i = 0; i < size; i++) { + const bdd bit = op(x.at(i),y.at(i)); + if (!bdd_isfalse(bit)) { + while(res.size() < i) { + res.push_back(bdd_false()); + } + res.push_back(bit); + } } - - return bvec(res); + + return bvec(res, std::max(x.bitlen(),y.bitlen())); } //Comparators @@ -178,42 +185,15 @@ namespace adiar { // Boolean operations bvec bvec_and(bvec x, bvec y) { - const size_t size = std::max(x.size(),y.size()); - std::vector res; - - for(size_t i = 0; i < size; i++) { - const bdd bit = bdd_and(x.at(i),y.at(i)); - if (!bdd_isfalse(bit)) { - while(res.size()+1 < i) { - res.push_back(bdd_false()); - } - res.push_back(bit); - } - } - - return bvec(res, std::max(x.bitlen(),y.bitlen())); + return _bvec_bitwise_op(x,y,[](const bdd& f, const bdd& g){ return bdd_and(f,g); }); } bvec bvec_or(bvec x, bvec y) { - //TODO: Do we require same bitlength? If yes, do we do it at compile-time or run-time? - std::vector res(x.bitlen()); - - for(size_t i = 0; i < x.bitlen(); i++) { - res.at(i) = bdd_or(x.at(i),y.at(i)); - } - - return bvec(res); + return _bvec_bitwise_op(x,y,[](const bdd& f, const bdd& g){ return bdd_or(f,g); }); } bvec bvec_xor(bvec x, bvec y) { - //TODO: Do we require same bitlength? If yes, do we do it at compile-time or run-time? - std::vector res(x.bitlen()); - - for(size_t i = 0; i < x.bitlen(); i++) { - res.at(i) = bdd_xor(x.at(i),y.at(i)); - } - - return bvec(res); + return _bvec_bitwise_op(x,y,[](const bdd& f, const bdd& g){ return bdd_xor(f,g); }); } bvec bvec_not(bvec x) { diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index 1659e42d5..403f86f63 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -135,9 +135,8 @@ go_bandit([]() { const bvec res = bvec_xor(x,y); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + AssertThat(res, Is().EqualTo(expected)); + }); it("computes 0 ^ 3 == 3 (000 ^ 011 == 011)", [&]() { const bvec x = bvec_const((char)0); From d4b0a3ad537d85060f7c3f186fef5787a8b39cc2 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 26 Mar 2026 16:33:49 +0100 Subject: [PATCH 09/35] Remake _bvec_bitwise_op to allow n-ary ops --- src/adiar/bvec.h | 33 +++++++++++++++++---------------- tests/adiar/bvec.test.cpp | 20 ++++++++++++++------ 2 files changed, 31 insertions(+), 22 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 34dfda66e..694b9d54e 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -127,7 +127,8 @@ namespace adiar { } bvec bvec_const(size_t value, size_t bitlen) { - size_t msb = value != 0 ? std::max(std::ceil(std::log2(value)),1.0) : 0; + size_t max = std::max(std::ceil(std::log2(value)),1.0); + size_t msb = std::min( value != 0 ? max : 0,bitlen); std::vector res; res.reserve(msb); // Should be able to compute the most significant bit position and stop after that @@ -149,12 +150,11 @@ namespace adiar { //Helper function for bitwise operations //TODO: Figure out how to do higher order function templating with constrains on function signature template - bvec _bvec_bitwise_op(bvec x, bvec y, BDD_OP op) { - const size_t size = std::max(x.size(),y.size()); + bvec _bvec_bitwise_op(size_t size, size_t bitlen, const BDD_OP& op) { std::vector res; for(size_t i = 0; i < size; i++) { - const bdd bit = op(x.at(i),y.at(i)); + const bdd bit = op(i); if (!bdd_isfalse(bit)) { while(res.size() < i) { res.push_back(bdd_false()); @@ -163,7 +163,15 @@ namespace adiar { } } - return bvec(res, std::max(x.bitlen(),y.bitlen())); + return bvec(res, bitlen); + } + + template + bvec _bvec_bitwise_op(bvec x, bvec y, const BDD_OP& op) { + const size_t size = std::max(x.size(),y.size()); + const size_t bitlen = std::max(x.bitlen(),y.bitlen()); + + return _bvec_bitwise_op(size,bitlen,op); } //Comparators @@ -185,26 +193,19 @@ namespace adiar { // Boolean operations bvec bvec_and(bvec x, bvec y) { - return _bvec_bitwise_op(x,y,[](const bdd& f, const bdd& g){ return bdd_and(f,g); }); + return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_and(x.at(i),y.at(i)); }); } bvec bvec_or(bvec x, bvec y) { - return _bvec_bitwise_op(x,y,[](const bdd& f, const bdd& g){ return bdd_or(f,g); }); + return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_or(x.at(i),y.at(i)); }); } bvec bvec_xor(bvec x, bvec y) { - return _bvec_bitwise_op(x,y,[](const bdd& f, const bdd& g){ return bdd_xor(f,g); }); + return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_xor(x.at(i),y.at(i)); }); } bvec bvec_not(bvec x) { - //TODO: Do we require same bitlength? If yes, do we do it at compile-time or run-time? - std::vector res(x.bitlen()); - - for(size_t i = 0; i < x.bitlen(); i++) { - res.at(i) = bdd_not(x.at(i)); - } - - return bvec(res); + return _bvec_bitwise_op(x.bitlen(),x.bitlen(),[&](size_t i){ return bdd_not(x.at(i)); }); } } diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index 403f86f63..234ff7687 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -19,12 +19,22 @@ go_bandit([]() { AssertThat(x.size(), Is().EqualTo(0u)); AssertThat(x.bitlen(), Is().EqualTo(32u)); }); - it("has 8 bitlen when constructed with max char", [&]() { + it("has 8 bitlen when constructed with max unsigned char", [&]() { const bvec x = bvec_const((unsigned char)255); AssertThat(x.size(), Is().EqualTo(8u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); }); - it("has 8 bitlen when constructed with max char", [&]() { + it("has 8 bitlen when constructed with overflowing char", [&]() { + const bvec x = bvec_const((char)253); + AssertThat(x.size(), Is().EqualTo(8u)); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + }); + it("has 8 bitlen when constructed with negative char", [&]() { + const bvec x = bvec_const((char)-52); + AssertThat(x.size(), Is().EqualTo(8u)); + AssertThat(x.bitlen(), Is().EqualTo(8u)); + }); + it("has 8 bitlen when constructed with max signed char", [&]() { const bvec x = bvec_const((char)127); AssertThat(x.size(), Is().EqualTo(7u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); @@ -167,13 +177,11 @@ go_bandit([]() { describe("constants", []() { it("computes ~3 == 252 for bitlength 8 (~00000011 == 11111100)", [&]() { const bvec x = bvec_const((char)3); - const bvec expected = bvec_const((char)252); //Is this expected, or should we check bdd structure? + const bvec expected = bvec_const((u_char)252); //Is this expected, or should we check bdd structure? const bvec res = bvec_not(x); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + AssertThat(res, Is().EqualTo(expected)); }); it("computes ~3 == (65535 - 3) for bitlength 16 (~0000000000000011 == 1111111111111100)", [&]() { const bvec x = bvec_const((short)3); From d105608ea6288db1f4e2e3bba0e77c9efc6700bd Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 26 Mar 2026 17:25:53 +0100 Subject: [PATCH 10/35] cleanup and todos --- src/adiar/bvec.h | 85 ++++++++++++++++++++++++++++-------------------- 1 file changed, 50 insertions(+), 35 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 694b9d54e..56d23ac99 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -10,53 +10,54 @@ namespace adiar { class bvec { - private: + public: static constexpr size_t MAX_BITLEN = 128; + private: std::vector _bits; - size_t _max_length; + size_t _bitlen; const bdd default_value = bdd(); - public: + public: ///////////////////////////////////////////////////////////////////////// /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" ///////////////////////////////////////////////////////////////////////// - bvec(size_t max_length = SIZE_T_MAX) - : _bits(0), _max_length(max_length) + bvec(size_t bitlen = MAX_BITLEN) + : _bits(0), _bitlen(bitlen) {} ///////////////////////////////////////////////////////////////////////// /// \brief Copy constructor ///////////////////////////////////////////////////////////////////////// bvec(const bvec& fs) - : _bits(fs._bits), _max_length(fs._max_length) + : _bits(fs._bits), _bitlen(fs._bitlen) {} ///////////////////////////////////////////////////////////////////////// /// \brief Move constructor for right-hand values ///////////////////////////////////////////////////////////////////////// bvec(bvec&& fs) - : _bits(std::move(fs._bits)), _max_length(fs._max_length) + : _bits(std::move(fs._bits)), _bitlen(fs._bitlen) {} ///////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector ///////////////////////////////////////////////////////////////////////// - bvec(const std::vector& bits, size_t max_length = SIZE_T_MAX) - : _bits(bits), _max_length(max_length) + bvec(const std::vector& bits, size_t bitlen = MAX_BITLEN) + : _bits(bits), _bitlen(bitlen) {} ///////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector for right-hand values ///////////////////////////////////////////////////////////////////////// - bvec(std::vector&& bits, size_t max_length = SIZE_T_MAX) - : _bits(std::move(bits)), _max_length(max_length) + bvec(std::vector&& bits, size_t bitlen = MAX_BITLEN) + : _bits(std::move(bits)), _bitlen(bitlen) {} ///////////////////////////////////////////////////////////////////////// /// \brief Parameterized constructor with length `bitlen` and given initial value `f` ///////////////////////////////////////////////////////////////////////// bvec(const size_t bitlen, const bdd& f) - : _bits(bitlen,f), _max_length(bitlen) + : _bits(bitlen,f), _bitlen(bitlen) {} public: - size_t bitlen() const { return _max_length; } + size_t bitlen() const { return _bitlen; } size_t size() const { return _bits.size(); } const bdd& // return type @@ -118,11 +119,11 @@ namespace adiar { // Constructors - bvec bvec_false(size_t bitlen = SIZE_T_MAX) { + bvec bvec_false(size_t bitlen = bvec::MAX_BITLEN) { return bvec(std::vector(0,bdd_false()),bitlen); } - bvec bvec_true(size_t bitlen = SIZE_T_MAX) { + bvec bvec_true(size_t bitlen = bvec::MAX_BITLEN) { return bvec(std::vector(bitlen,bdd_true()),bitlen); } @@ -147,8 +148,29 @@ namespace adiar { } + + //Comparators + + 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; + } + + bool + operator==(const bvec& x, const bvec& y) { + return bvec_equal(x,y); + } + + + + // Bitwise operations + //Helper function for bitwise operations - //TODO: Figure out how to do higher order function templating with constrains on function signature template bvec _bvec_bitwise_op(size_t size, size_t bitlen, const BDD_OP& op) { std::vector res; @@ -174,24 +196,6 @@ namespace adiar { return _bvec_bitwise_op(size,bitlen,op); } - //Comparators - - 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; - } - - bool - operator==(const bvec& x, const bvec& y) { - return bvec_equal(x,y); - } - - // Boolean operations bvec bvec_and(bvec x, bvec y) { return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_and(x.at(i),y.at(i)); }); } @@ -207,8 +211,19 @@ namespace adiar { bvec bvec_not(bvec x) { return _bvec_bitwise_op(x.bitlen(),x.bitlen(),[&](size_t i){ return bdd_not(x.at(i)); }); } -} + //Arithmetic operations + bvec + bvec_plus(bvec x, bvec y) {} + +} +//TODO: Move implementation to bvec.cpp +//TODO: Use "const bvec&" instead of "bvec" (call-by-reference instead of call-by-value) +//TODO: Rebase from main, then use (if(f) instead of if(!bdd_isfalse(f))) +//TODO: Test overview both existing and missing, test bvec_equal, use bvec_equal instead of bitwise assertions +//TODO: bvec_truncate(new_bitlen); use _bvec_bitwise_op(...new_bitlen...) to truncate +//TODO: Implement arithmetic operations +//TODO: Add variables, bvec_var(ITER begin, ITER end, bitlen) #endif // ADIAR_BVEC_H From 2b646e6221526108f89b8d7e21bb71aebb53bc28 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Fri, 27 Mar 2026 15:30:37 +0100 Subject: [PATCH 11/35] Split bvec implementations from bvec.h into bvec.cpp --- src/adiar/CMakeLists.txt | 1 + src/adiar/bvec.cpp | 201 +++++++++++++++++++++++++++++++++++++++ src/adiar/bvec.h | 182 +++++++++-------------------------- 3 files changed, 245 insertions(+), 139 deletions(-) create mode 100644 src/adiar/bvec.cpp diff --git a/src/adiar/CMakeLists.txt b/src/adiar/CMakeLists.txt index 890f64b35..aeacd924d 100644 --- a/src/adiar/CMakeLists.txt +++ b/src/adiar/CMakeLists.txt @@ -107,6 +107,7 @@ set(HEADERS set(SOURCES # adiar/ adiar.cpp + bvec.cpp domain.cpp statistics.cpp diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp new file mode 100644 index 000000000..fc6e5ec37 --- /dev/null +++ b/src/adiar/bvec.cpp @@ -0,0 +1,201 @@ +#include +#include +#include +#include +#include +#include + +namespace adiar { + ///////////////////////////////////////////////////////////////////////// + /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(size_t bitlen) + : _bits(0), _bitlen(bitlen) + {} + ///////////////////////////////////////////////////////////////////////// + /// \brief Copy constructor + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(const bvec& fs) + : _bits(fs._bits), _bitlen(fs._bitlen) + {} + ///////////////////////////////////////////////////////////////////////// + /// \brief Move constructor for right-hand values + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(bvec&& fs) + : _bits(std::move(fs._bits)), _bitlen(fs._bitlen) + {} + + ///////////////////////////////////////////////////////////////////////// + /// \brief Conversion constructor from a raw bit-vector + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(const std::vector& bits, size_t bitlen) + : _bits(bits), _bitlen(bitlen) + {} + ///////////////////////////////////////////////////////////////////////// + /// \brief Conversion constructor from a raw bit-vector for right-hand values + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(std::vector&& bits, size_t bitlen) + : _bits(std::move(bits)), _bitlen(bitlen) + {} + + ///////////////////////////////////////////////////////////////////////// + /// \brief Parameterized constructor with length `bitlen` and given initial value `f` + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(const size_t bitlen, const bdd& f) + : _bits(bitlen,f), _bitlen(bitlen) + {} + + const bdd& // return type + bvec::at(size_t index) const //name(...) context + { + if (_bits.size() <= index) { return default_value; } //TODO: This warns that we are returning a local temp. Can we move it? + 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(); + } + + // 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 = bvec::MAX_BITLEN) { + return bvec(std::vector(0,bdd_false()),bitlen); + } + + bvec + bvec_true(size_t bitlen = bvec::MAX_BITLEN) { + return bvec(std::vector(bitlen,bdd_true()),bitlen); + } + + bvec + bvec_const(size_t value, size_t bitlen) { + size_t max = std::max(std::ceil(std::log2(value)),1.0); + size_t msb = std::min( value != 0 ? max : 0,bitlen); + std::vector res; + res.reserve(msb); + // Should be able to compute the most significant bit position and stop after that + for (size_t i = 0; i < msb; i++) { + res.push_back(value & 1 ? bdd_true() : bdd_false()); + + value >>= 1; + } + + return bvec(res,bitlen); + } + + // 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; + + for(size_t i = 0; i < size; i++) { + const bdd bit = op(i); + if (!bdd_isfalse(bit)) { + while(res.size() < i) { + res.push_back(bdd_false()); + } + res.push_back(bit); + } + } + + return bvec(res, bitlen); + } + + template + bvec _bvec_bitwise_op(bvec x, bvec y, const BDD_OP& op) { + const size_t size = std::max(x.size(),y.size()); + const size_t bitlen = std::max(x.bitlen(),y.bitlen()); + + return _bvec_bitwise_op(size,bitlen,op); + } + + bvec bvec_and(bvec x, bvec y) { + return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_and(x.at(i),y.at(i)); }); + } + + bvec bvec_or(bvec x, bvec y) { + return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_or(x.at(i),y.at(i)); }); + } + + bvec bvec_xor(bvec x, bvec y) { + return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_xor(x.at(i),y.at(i)); }); + } + + bvec bvec_not(bvec x) { + return _bvec_bitwise_op(x.bitlen(),x.bitlen(),[&](size_t i){ return bdd_not(x.at(i)); }); + } + + //Arithmetic operations + +} +//TODO: Move implementation to bvec.cpp +//TODO: Use "const bvec&" instead of "bvec" (call-by-reference instead of call-by-value) +//TODO: Rebase from main, then use (if(f) instead of if(!bdd_isfalse(f))) +//TODO: Test overview both existing and missing, test bvec_equal, use bvec_equal instead of bitwise assertions +//TODO: bvec_truncate(new_bitlen); use _bvec_bitwise_op(...new_bitlen...) to truncate +//TODO: Implement arithmetic operations +//TODO: Add variables, bvec_var(ITER begin, ITER end, bitlen) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 56d23ac99..7f6083d40 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -20,205 +20,109 @@ namespace adiar { ///////////////////////////////////////////////////////////////////////// /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" ///////////////////////////////////////////////////////////////////////// - bvec(size_t bitlen = MAX_BITLEN) - : _bits(0), _bitlen(bitlen) - {} + bvec(size_t bitlen = MAX_BITLEN); ///////////////////////////////////////////////////////////////////////// /// \brief Copy constructor ///////////////////////////////////////////////////////////////////////// - bvec(const bvec& fs) - : _bits(fs._bits), _bitlen(fs._bitlen) - {} + bvec(const bvec& fs); ///////////////////////////////////////////////////////////////////////// /// \brief Move constructor for right-hand values ///////////////////////////////////////////////////////////////////////// - bvec(bvec&& fs) - : _bits(std::move(fs._bits)), _bitlen(fs._bitlen) - {} + bvec(bvec&& fs); ///////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector ///////////////////////////////////////////////////////////////////////// - bvec(const std::vector& bits, size_t bitlen = MAX_BITLEN) - : _bits(bits), _bitlen(bitlen) - {} + bvec(const std::vector& bits, size_t bitlen = MAX_BITLEN); ///////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector for right-hand values ///////////////////////////////////////////////////////////////////////// - bvec(std::vector&& bits, size_t bitlen = MAX_BITLEN) - : _bits(std::move(bits)), _bitlen(bitlen) - {} + bvec(std::vector&& bits, size_t bitlen = MAX_BITLEN); ///////////////////////////////////////////////////////////////////////// /// \brief Parameterized constructor with length `bitlen` and given initial value `f` ///////////////////////////////////////////////////////////////////////// - bvec(const size_t bitlen, const bdd& f) - : _bits(bitlen,f), _bitlen(bitlen) - {} + bvec(const size_t bitlen, const bdd& f); - public: - size_t bitlen() const { return _bitlen; } - size_t size() const { return _bits.size(); } + inline size_t bitlen() const { return _bitlen; } + inline size_t size() const { return _bits.size(); } - const bdd& // return type - at(size_t index) const //name(...) context - { - if (_bits.size() <= index) { return default_value; } //TODO: This warns that we are returning a local temp. Can we move it? - return _bits.at(index); - } + const bdd& + at(size_t index) const; std::vector::const_iterator - begin() const - { - return _bits.cbegin(); - } + begin() const; std::vector::const_iterator - end() const - { - return _bits.cend(); - } + end() const; std::vector::const_reverse_iterator - rbegin() const - { - return _bits.crbegin(); - } + rbegin() const; std::vector::const_reverse_iterator - rend() const - { - return _bits.crend(); - } + rend() const; std::string - 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(); - } + to_string() const; }; - inline std::ostream& - operator<<(std::ostream& os, const bvec& a) - { - return os << a.to_string(); - } + std::ostream& + operator<<(std::ostream& os, const bvec& a); // Constructors - bvec bvec_false(size_t bitlen = bvec::MAX_BITLEN) { - return bvec(std::vector(0,bdd_false()),bitlen); - } - - bvec bvec_true(size_t bitlen = bvec::MAX_BITLEN) { - return bvec(std::vector(bitlen,bdd_true()),bitlen); - } - - bvec bvec_const(size_t value, size_t bitlen) { - size_t max = std::max(std::ceil(std::log2(value)),1.0); - size_t msb = std::min( value != 0 ? max : 0,bitlen); - std::vector res; - res.reserve(msb); - // Should be able to compute the most significant bit position and stop after that - for (size_t i = 0; i < msb; i++) { - res.push_back(value & 1 ? bdd_true() : bdd_false()); + bvec + bvec_false(size_t bitlen); - value >>= 1; - } + bvec + bvec_true(size_t bitlen); - return bvec(res,bitlen); - } + bvec + bvec_const(size_t value, size_t bitlen); template - bvec bvec_const(Integer i) { + bvec + bvec_const(Integer i) { return bvec_const(i,8 * sizeof(Integer)); } - - - + //Comparators 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; - } + bvec_equal(const bvec& x, const bvec& y); bool - operator==(const bvec& x, const bvec& y) { - return bvec_equal(x,y); - } - + operator==(const bvec& x, const bvec& y); // 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; - - for(size_t i = 0; i < size; i++) { - const bdd bit = op(i); - if (!bdd_isfalse(bit)) { - while(res.size() < i) { - res.push_back(bdd_false()); - } - res.push_back(bit); - } - } - - return bvec(res, bitlen); - } + bvec + _bvec_bitwise_op(size_t size, size_t bitlen, const BDD_OP& op); template - bvec _bvec_bitwise_op(bvec x, bvec y, const BDD_OP& op) { - const size_t size = std::max(x.size(),y.size()); - const size_t bitlen = std::max(x.bitlen(),y.bitlen()); - - return _bvec_bitwise_op(size,bitlen,op); - } - - bvec bvec_and(bvec x, bvec y) { - return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_and(x.at(i),y.at(i)); }); - } - - bvec bvec_or(bvec x, bvec y) { - return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_or(x.at(i),y.at(i)); }); - } + bvec + _bvec_bitwise_op(bvec x, bvec y, const BDD_OP& op); - bvec bvec_xor(bvec x, bvec y) { - return _bvec_bitwise_op(x,y,[&](size_t i){ return bdd_xor(x.at(i),y.at(i)); }); - } + bvec + bvec_and(bvec x, bvec y); + + bvec + bvec_or(bvec x, bvec y); + + bvec + bvec_xor(bvec x, bvec y); - bvec bvec_not(bvec x) { - return _bvec_bitwise_op(x.bitlen(),x.bitlen(),[&](size_t i){ return bdd_not(x.at(i)); }); - } + bvec + bvec_not(bvec x); //Arithmetic operations - bvec - bvec_plus(bvec x, bvec y) {} } -//TODO: Move implementation to bvec.cpp + //TODO: Use "const bvec&" instead of "bvec" (call-by-reference instead of call-by-value) //TODO: Rebase from main, then use (if(f) instead of if(!bdd_isfalse(f))) //TODO: Test overview both existing and missing, test bvec_equal, use bvec_equal instead of bitwise assertions From 251ad8d30b77854c0062dba4f300368bcb798c08 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Fri, 27 Mar 2026 15:35:39 +0100 Subject: [PATCH 12/35] Switch bvec operation arguments to using call-by-reference --- src/adiar/bvec.cpp | 10 +++++----- src/adiar/bvec.h | 11 +++++------ 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index fc6e5ec37..ce5fe5a5d 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -166,26 +166,26 @@ namespace adiar { } template - bvec _bvec_bitwise_op(bvec x, bvec y, const BDD_OP& op) { + 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 = std::max(x.bitlen(),y.bitlen()); return _bvec_bitwise_op(size,bitlen,op); } - bvec bvec_and(bvec x, bvec y) { + 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(bvec x, bvec y) { + 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(bvec x, bvec y) { + 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(bvec x) { + bvec bvec_not(const bvec& x) { return _bvec_bitwise_op(x.bitlen(),x.bitlen(),[&](size_t i){ return bdd_not(x.at(i)); }); } diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 7f6083d40..7ea64213b 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -104,26 +104,25 @@ namespace adiar { template bvec - _bvec_bitwise_op(bvec x, bvec y, const BDD_OP& op); + _bvec_bitwise_op(const bvec& x, const bvec& y, const BDD_OP& op); bvec - bvec_and(bvec x, bvec y); + bvec_and(const bvec& x, const bvec& y); bvec - bvec_or(bvec x, bvec y); + bvec_or(const bvec& x, const bvec& y); bvec - bvec_xor(bvec x, bvec y); + bvec_xor(const bvec& x, const bvec& y); bvec - bvec_not(bvec x); + bvec_not(const bvec& x); //Arithmetic operations } -//TODO: Use "const bvec&" instead of "bvec" (call-by-reference instead of call-by-value) //TODO: Rebase from main, then use (if(f) instead of if(!bdd_isfalse(f))) //TODO: Test overview both existing and missing, test bvec_equal, use bvec_equal instead of bitwise assertions //TODO: bvec_truncate(new_bitlen); use _bvec_bitwise_op(...new_bitlen...) to truncate From d2c00d00c9ed9ac8703ec10b31c786f0b44eb2e6 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Fri, 27 Mar 2026 15:50:31 +0100 Subject: [PATCH 13/35] Rebase and use new bool operator --- src/adiar/bvec.cpp | 9 +-------- src/adiar/bvec.h | 1 - 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index ce5fe5a5d..8656885b9 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -154,7 +154,7 @@ namespace adiar { for(size_t i = 0; i < size; i++) { const bdd bit = op(i); - if (!bdd_isfalse(bit)) { + if (bit) { while(res.size() < i) { res.push_back(bdd_false()); } @@ -192,10 +192,3 @@ namespace adiar { //Arithmetic operations } -//TODO: Move implementation to bvec.cpp -//TODO: Use "const bvec&" instead of "bvec" (call-by-reference instead of call-by-value) -//TODO: Rebase from main, then use (if(f) instead of if(!bdd_isfalse(f))) -//TODO: Test overview both existing and missing, test bvec_equal, use bvec_equal instead of bitwise assertions -//TODO: bvec_truncate(new_bitlen); use _bvec_bitwise_op(...new_bitlen...) to truncate -//TODO: Implement arithmetic operations -//TODO: Add variables, bvec_var(ITER begin, ITER end, bitlen) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 7ea64213b..dbfb05e57 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -123,7 +123,6 @@ namespace adiar { } -//TODO: Rebase from main, then use (if(f) instead of if(!bdd_isfalse(f))) //TODO: Test overview both existing and missing, test bvec_equal, use bvec_equal instead of bitwise assertions //TODO: bvec_truncate(new_bitlen); use _bvec_bitwise_op(...new_bitlen...) to truncate //TODO: Implement arithmetic operations From af9e021de0db51163e15e9f20937ba142f414c53 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 16 Apr 2026 13:24:59 +0200 Subject: [PATCH 14/35] Fix test descriptions and utilize bvec_equal instead of manual bitwise comparison --- tests/adiar/bvec.test.cpp | 46 +++++++++++++++------------------------ 1 file changed, 18 insertions(+), 28 deletions(-) diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index 234ff7687..c406cde83 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -2,39 +2,39 @@ #include go_bandit([]() { describe("adiar/bvec.h", []() { - describe("bdd_false()", []() { + describe("bvec_false()", []() { it("has 16 bits when asked", [&]() { AssertThat(bvec_false(16).bitlen(), Is().EqualTo(16u)); }); }); - describe("bdd_true()", []() { + describe("bvec_true()", []() { it("has 32 bits when asked", [&]() { AssertThat(bvec_true(32).bitlen(), Is().EqualTo(32u)); }); }); - describe("bdd_const", []() { + describe("bvec_const", []() { describe("bitlength inference", []() { - it("has 0 bitlen when constructed with 0", [&]() { + it("has 32 bitlen 0 size when constructed with 0", [&]() { const bvec x = bvec_const(0); AssertThat(x.size(), Is().EqualTo(0u)); AssertThat(x.bitlen(), Is().EqualTo(32u)); }); - it("has 8 bitlen when constructed with max unsigned char", [&]() { + it("has 8 size and bitlen when constructed with max unsigned char", [&]() { const bvec x = bvec_const((unsigned char)255); AssertThat(x.size(), Is().EqualTo(8u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); }); - it("has 8 bitlen when constructed with overflowing char", [&]() { + it("has 8 size and bitlen when constructed with overflowing char", [&]() { const bvec x = bvec_const((char)253); AssertThat(x.size(), Is().EqualTo(8u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); }); - it("has 8 bitlen when constructed with negative char", [&]() { + it("has 8 size and bitlen when constructed with negative char", [&]() { const bvec x = bvec_const((char)-52); AssertThat(x.size(), Is().EqualTo(8u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); }); - it("has 8 bitlen when constructed with max signed char", [&]() { + it("has 7 size and 8 bitlen when constructed with max signed char", [&]() { const bvec x = bvec_const((char)127); AssertThat(x.size(), Is().EqualTo(7u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); @@ -102,9 +102,7 @@ go_bandit([]() { const bvec res = bvec_and(x,y); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + AssertThat(res, Is().EqualTo(expected)); }); }); }); @@ -118,9 +116,7 @@ go_bandit([]() { const bvec res = bvec_or(x,y); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + AssertThat(res, Is().EqualTo(expected)); }); it("computes 0 | 3 == 3 (000 | 011 == 011)", [&]() { const bvec x = bvec_const((char)0); @@ -129,9 +125,7 @@ go_bandit([]() { const bvec res = bvec_or(x,y); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + AssertThat(res, Is().EqualTo(expected)); }); }); }); @@ -144,8 +138,8 @@ go_bandit([]() { const bvec expected = bvec_const((char)6); //Is this expected, or should we check bdd structure? const bvec res = bvec_xor(x,y); - - AssertThat(res, Is().EqualTo(expected)); + + AssertThat(res, Is().EqualTo(expected)); }); it("computes 0 ^ 3 == 3 (000 ^ 011 == 011)", [&]() { @@ -155,9 +149,7 @@ go_bandit([]() { const bvec res = bvec_xor(x,y); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + AssertThat(res, Is().EqualTo(expected)); }); it("computes 255 ^ 3 == 252 (11111111 ^ 00000011 == 11111100)", [&]() { const bvec x = bvec_const((char)255); @@ -166,9 +158,7 @@ go_bandit([]() { const bvec res = bvec_xor(x,y); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + AssertThat(res, Is().EqualTo(expected)); }); }); }); @@ -189,9 +179,9 @@ go_bandit([]() { const bvec res = bvec_not(x); - for(size_t i = 0; i < x.bitlen(); i++) { - AssertThat(res.at(i), Is().EqualTo(expected.at(i))); - } + + AssertThat(res, Is().EqualTo(expected)); + }); }); }); From 5b842d1477f7cbad1b45cca1829439315d5ec055 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 16 Apr 2026 14:44:10 +0200 Subject: [PATCH 15/35] Enforce truncation of false prefix when constructing from vector --- src/adiar/bvec.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 8656885b9..296c1c665 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -30,7 +30,11 @@ namespace adiar { ///////////////////////////////////////////////////////////////////////// bvec::bvec(const std::vector& bits, size_t bitlen) : _bits(bits), _bitlen(bitlen) - {} + { + while (this->_bits.size() > 0 && !this->_bits.back()) { + this->_bits.pop_back(); + } + } ///////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector for right-hand values ///////////////////////////////////////////////////////////////////////// From 7767005fe67621b3991ab3dce731bb5432ffa4f5 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 16 Apr 2026 14:44:22 +0200 Subject: [PATCH 16/35] Test bvec_equal --- tests/adiar/bvec.test.cpp | 58 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 57 insertions(+), 1 deletion(-) diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index c406cde83..c6f2666fa 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -171,7 +171,7 @@ go_bandit([]() { const bvec res = bvec_not(x); - AssertThat(res, Is().EqualTo(expected)); + AssertThat(res, Is().EqualTo(expected)); }); it("computes ~3 == (65535 - 3) for bitlength 16 (~0000000000000011 == 1111111111111100)", [&]() { const bvec x = bvec_const((short)3); @@ -185,5 +185,61 @@ go_bandit([]() { }); }); }); + describe("bvec_equal", []() { + it("compares 101 == 101", [&]() { + std::vector raw1 = {bdd_true(),bdd_false(),bdd_true()}; + std::vector raw2 = {bdd_true(),bdd_false(),bdd_true()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().True()); + }); + it("compares 0101 == 101", [&]() { + std::vector raw1 = {bdd_true(),bdd_false(),bdd_true()}; + std::vector raw2 = {bdd_true(),bdd_false(),bdd_true(),bdd_false()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().True()); + }); + it("compares 101 == 0101", [&]() { + std::vector raw1 = {bdd_true(),bdd_false(),bdd_true(),bdd_false()}; + std::vector raw2 = {bdd_true(),bdd_false(),bdd_true()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().True()); + }); + it("compares 101 != 1101", [&]() { + std::vector raw1 = {bdd_true(),bdd_false(),bdd_true(),bdd_true()}; + std::vector raw2 = {bdd_true(),bdd_false(),bdd_true()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + }); + it("compares 1101 != 101", [&]() { + std::vector raw1 = {bdd_true(),bdd_false(),bdd_true()}; + std::vector raw2 = {bdd_true(),bdd_false(),bdd_true(),bdd_true()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + }); + it("compares 1101 != 1110", [&]() { + std::vector raw1 = {bdd_true(),bdd_false(),bdd_true(),bdd_true()}; + std::vector raw2 = {bdd_false(),bdd_true(),bdd_true(),bdd_true()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + }); + it("compares 1100 != 1110", [&]() { + std::vector raw1 = {bdd_false(),bdd_false(),bdd_true(),bdd_true()}; + std::vector raw2 = {bdd_false(),bdd_true(),bdd_true(),bdd_true()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + }); + it("compares 1x0 == 1x0", [&]() { + std::vector raw1 = {bdd_false(),bdd_ithvar(42),bdd_true()}; + std::vector raw2 = {bdd_false(),bdd_ithvar(42),bdd_true()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().True()); + }); + it("compares 1x0 != 1y0", [&]() { + std::vector raw1 = {bdd_false(),bdd_ithvar(42),bdd_true()}; + std::vector raw2 = {bdd_false(),bdd_ithvar(11),bdd_true()}; + + AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + }); + }); }); }); \ No newline at end of file From 2bb5f8c6c01bdf068bd16740cc4733cc25145380 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 23 Apr 2026 13:19:35 +0200 Subject: [PATCH 17/35] add bvec_add(bdd,bdd) --- src/adiar/bvec.cpp | 21 +++++++++++- src/adiar/bvec.h | 4 +-- tests/adiar/bvec.test.cpp | 71 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 93 insertions(+), 3 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 296c1c665..a37b29649 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -31,7 +31,8 @@ namespace adiar { bvec::bvec(const std::vector& bits, size_t bitlen) : _bits(bits), _bitlen(bitlen) { - while (this->_bits.size() > 0 && !this->_bits.back()) { + //Truncates to bitlen and removes any prefix of false + while (this->_bits.size() > 0 && (!this->_bits.back() || this->_bitlen < this->_bits.size())) { this->_bits.pop_back(); } } @@ -195,4 +196,22 @@ namespace adiar { //Arithmetic operations + bvec + bvec_add(const bvec& x, const bvec& y) { + bdd carry = bdd_false(); + const size_t bitlen = std::max(x.bitlen(),y.bitlen()); + std::vector res; + const size_t size = std::max(x.size(),y.size())+1; + res.reserve(size); + for (size_t i = 0; i raw_expected = {bdd_false(),bdd_false(),bdd_false(),bdd_true()}; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a,b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8)); + AssertThat(res.size(), Is().EqualTo(4)); + }); + + it("computes (int) 5 + (char) 3 = (int) 8", [&]() { + bvec a = bvec_const((int)5); + bvec b = bvec_const((char)3); + // 00000000000000000000000000000101 + + // 00000011 = + // 00000000000000000000000000001000 + std::vector raw_expected = {bdd_false(),bdd_false(),bdd_false(),bdd_true()}; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a,b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32)); + AssertThat(res.size(), Is().EqualTo(4)); + }); + + it("computes (int) 0 + (char) 3 = (int) 3", [&]() { + bvec a = bvec_const((int)0); + bvec b = bvec_const((char)3); + // 00000000000000000000000000000000 + + // 00000011 = + // 00000000000000000000000000000011 + std::vector raw_expected = {bdd_true(),bdd_true()}; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a,b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32)); + AssertThat(res.size(), Is().EqualTo(2)); + }); + + it("computes (char) 0 + (int) 3 = (int) 3", [&]() { + bvec a = bvec_const((char)0); + bvec b = bvec_const((int)3); + // 00000000 + + // 00000000000000000000000000000011 = + // 00000000000000000000000000000011 + std::vector raw_expected = {bdd_true(),bdd_true()}; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a,b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32)); + AssertThat(res.size(), Is().EqualTo(2)); + }); + + it("computes (char) 255 + (char) 1 = (char) 0", [&]() { + bvec a = bvec_const((char)255); + bvec b = bvec_const((char)1); + // 11111111 + + // 00000001 = + // 00000000 + std::vector raw_expected = {}; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a,b); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8)); + AssertThat(res.size(), Is().EqualTo(0)); + }); + }); }); }); \ No newline at end of file From 12e895adb14af0d8c4d39febe31adb98a4f8efe7 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 23 Apr 2026 15:04:09 +0200 Subject: [PATCH 18/35] fix off by one when constructing with powers of two --- src/adiar/bvec.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index a37b29649..9dc4e982d 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -135,7 +135,7 @@ namespace adiar { bvec bvec_const(size_t value, size_t bitlen) { - size_t max = std::max(std::ceil(std::log2(value)),1.0); + size_t max = std::ceil(std::log2(value))+1; size_t msb = std::min( value != 0 ? max : 0,bitlen); std::vector res; res.reserve(msb); From ca8719273522199d3f6c14650b4ee0fcf30ab78b Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 23 Apr 2026 15:05:36 +0200 Subject: [PATCH 19/35] skip computation of overflowed carry --- src/adiar/bvec.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 9dc4e982d..b493292bb 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -198,19 +198,26 @@ namespace adiar { bvec bvec_add(const bvec& x, const bvec& y) { - bdd carry = bdd_false(); const size_t bitlen = std::max(x.bitlen(),y.bitlen()); - std::vector res; const size_t size = std::max(x.size(),y.size())+1; + + bdd carry = bdd_false(); + + std::vector res; res.reserve(size); + for (size_t i = 0; i= size, "is not last bit with overflow"); + carry = bdd_or(bdd_and(carry, bdd_or(x.at(i),y.at(i))), bdd_and(x.at(i),y.at(i))); + } } + // This assumes that the vector constructor truncates size above bitlen and false prefix. res.push_back(carry); - // Maybe we should check that we cannot increase size above bitlen? + return bvec(res, bitlen); } From c730f17dae1c98e442ed51d4801c108c5f2bfcf9 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 23 Apr 2026 15:07:50 +0200 Subject: [PATCH 20/35] implement truncate --- src/adiar/bvec.cpp | 29 ++++++++++++++++++++++++----- src/adiar/bvec.h | 8 +++++++- tests/adiar/bvec.test.cpp | 35 +++++++++++++++++++++++++++++++++-- 3 files changed, 64 insertions(+), 8 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index b493292bb..a62f6703f 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -31,17 +31,16 @@ namespace adiar { bvec::bvec(const std::vector& bits, size_t bitlen) : _bits(bits), _bitlen(bitlen) { - //Truncates to bitlen and removes any prefix of false - while (this->_bits.size() > 0 && (!this->_bits.back() || this->_bitlen < this->_bits.size())) { - this->_bits.pop_back(); - } + this->truncate(bitlen); } ///////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector for right-hand values ///////////////////////////////////////////////////////////////////////// bvec::bvec(std::vector&& bits, size_t bitlen) : _bits(std::move(bits)), _bitlen(bitlen) - {} + { + this->truncate(bitlen); + } ///////////////////////////////////////////////////////////////////////// /// \brief Parameterized constructor with length `bitlen` and given initial value `f` @@ -99,6 +98,19 @@ namespace adiar { return out.str(); } + + void + bvec::truncate(size_t bitlen) { + this->_bitlen = bitlen; + //Truncates to bitlen and removes any prefix of false + while (this->_bitlen < this->_bits.size()) { + this->_bits.pop_back(); + } + while (this->_bits.size() > 0 && !this->_bits.back()) { + this->_bits.pop_back(); + } + } + // Comparators @@ -221,4 +233,11 @@ namespace adiar { return bvec(res, bitlen); } + //Helper + bvec + bvec_truncate(const bvec& x, const size_t bitlen) { + bvec y = x; + y.truncate(bitlen); + return y; + } } diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 82cd22735..91eabb71c 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -64,6 +64,9 @@ namespace adiar { std::string to_string() const; + + void + truncate(size_t bitlen); }; std::ostream& @@ -122,9 +125,12 @@ namespace adiar { bvec bvec_add(const bvec& x, const bvec& y); + + //Utility + bvec + bvec_truncate(const bvec& x, const size_t bitlen); } -//TODO: bvec_truncate(new_bitlen); use _bvec_bitwise_op(...new_bitlen...) to truncate //TODO: Implement arithmetic operations //TODO: Add variables, bvec_var(ITER begin, ITER end, bitlen) diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index 1049caa31..dc80a8fd0 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -308,8 +308,39 @@ go_bandit([]() { bvec expected = bvec(raw_expected); bvec res = bvec_add(a,b); AssertThat(res, Is().EqualTo(expected)); - AssertThat(res.bitlen(), Is().EqualTo(8)); - AssertThat(res.size(), Is().EqualTo(0)); + }); + }); + describe("bvec_truncate", []() { + it("truncates to bitlen", [&](){ + bvec x = bvec_true(32); + + + bvec expected = bvec_true(8); + bvec res = bvec_truncate(x,8); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(8u)); + }); + + it("extends to bitlen", [&](){ + bvec x = bvec_true(4); + AssertThat(x.bitlen(), Is().EqualTo(4u)); + + bvec expected = bvec_true(4); + bvec res = bvec_truncate(x,8); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(4u)); + }); + + it("truncates false prefix", [&](){ + bvec x = bvec_const(18); + + bvec expected = bvec_const(2); + bvec res = bvec_truncate(x,4); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(4u)); + AssertThat(res.size(), Is().EqualTo(2u)); }); }); }); From 69d1e3a03370a6110c5ad29fd1ae66f293fb4ab9 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 23 Apr 2026 15:08:28 +0200 Subject: [PATCH 21/35] remove private helper function from public interface --- src/adiar/bvec.h | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 91eabb71c..984f63473 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -100,15 +100,6 @@ namespace adiar { // Bitwise operations - //Helper function for bitwise operations - template - bvec - _bvec_bitwise_op(size_t size, size_t bitlen, const BDD_OP& op); - - template - bvec - _bvec_bitwise_op(const bvec& x, const bvec& y, const BDD_OP& op); - bvec bvec_and(const bvec& x, const bvec& y); From 2d39c56f00dbb4d35bfab8b817f5965e9cab4641 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 23 Apr 2026 15:10:03 +0200 Subject: [PATCH 22/35] fix signed/unsigned warnings in tests and add missing assertions --- tests/adiar/bvec.test.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index dc80a8fd0..b2c733f9d 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -252,8 +252,8 @@ go_bandit([]() { bvec expected = bvec(raw_expected); bvec res = bvec_add(a,b); AssertThat(res, Is().EqualTo(expected)); - AssertThat(res.bitlen(), Is().EqualTo(8)); - AssertThat(res.size(), Is().EqualTo(4)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(4u)); }); it("computes (int) 5 + (char) 3 = (int) 8", [&]() { @@ -266,8 +266,8 @@ go_bandit([]() { bvec expected = bvec(raw_expected); bvec res = bvec_add(a,b); AssertThat(res, Is().EqualTo(expected)); - AssertThat(res.bitlen(), Is().EqualTo(32)); - AssertThat(res.size(), Is().EqualTo(4)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(4u)); }); it("computes (int) 0 + (char) 3 = (int) 3", [&]() { @@ -280,8 +280,8 @@ go_bandit([]() { bvec expected = bvec(raw_expected); bvec res = bvec_add(a,b); AssertThat(res, Is().EqualTo(expected)); - AssertThat(res.bitlen(), Is().EqualTo(32)); - AssertThat(res.size(), Is().EqualTo(2)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(2u)); }); it("computes (char) 0 + (int) 3 = (int) 3", [&]() { @@ -294,8 +294,8 @@ go_bandit([]() { bvec expected = bvec(raw_expected); bvec res = bvec_add(a,b); AssertThat(res, Is().EqualTo(expected)); - AssertThat(res.bitlen(), Is().EqualTo(32)); - AssertThat(res.size(), Is().EqualTo(2)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(2u)); }); it("computes (char) 255 + (char) 1 = (char) 0", [&]() { @@ -308,6 +308,8 @@ go_bandit([]() { bvec expected = bvec(raw_expected); bvec res = bvec_add(a,b); AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(0u)); }); }); describe("bvec_truncate", []() { From 2386fb11fb58162a808d581ed63681cfb624f059 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 23 Apr 2026 15:39:23 +0200 Subject: [PATCH 23/35] implements + operator and bvec_add for bdd and const --- src/adiar/bvec.h | 29 +++++++++++++++++++++++ tests/adiar/bvec.test.cpp | 50 +++++++++++++++++++++++++++++++++++---- 2 files changed, 74 insertions(+), 5 deletions(-) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 984f63473..6cd23dfa9 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -117,6 +117,35 @@ namespace adiar { bvec bvec_add(const bvec& x, const bvec& y); + template + bvec + bvec_add(const bvec& x, Integer i) { + return bvec_add(x,bvec_const(i)); + } + + template + bvec + bvec_add(Integer i,const bvec& x) { + return bvec_add(x,i); + } + + inline bvec + operator+(const bvec& x, const bvec& y) { + return bvec_add(x,y); + } + + template + bvec + operator+(const bvec& x, Integer i) { + return bvec_add(x,i); + } + template + bvec + operator+(Integer i,const bvec& x) { + return bvec_add(i,x); + } + + //Utility bvec bvec_truncate(const bvec& x, const size_t bitlen); diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index b2c733f9d..cb81afc46 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -242,7 +242,7 @@ go_bandit([]() { }); }); describe("bvec_add", []() { - it("computes (char) 5 + (char) 3 = (char) 8", [&]() { + it("computes bvec[8](5) + bvec[8](3)", [&]() { bvec a = bvec_const((char)5); bvec b = bvec_const((char)3); // 00000101 + @@ -256,7 +256,7 @@ go_bandit([]() { AssertThat(res.size(), Is().EqualTo(4u)); }); - it("computes (int) 5 + (char) 3 = (int) 8", [&]() { + it("computes bvec[32](5) + bvec[8](3)", [&]() { bvec a = bvec_const((int)5); bvec b = bvec_const((char)3); // 00000000000000000000000000000101 + @@ -270,7 +270,7 @@ go_bandit([]() { AssertThat(res.size(), Is().EqualTo(4u)); }); - it("computes (int) 0 + (char) 3 = (int) 3", [&]() { + it("computes bvec[32](0) + bvec[8](3)", [&]() { bvec a = bvec_const((int)0); bvec b = bvec_const((char)3); // 00000000000000000000000000000000 + @@ -284,7 +284,7 @@ go_bandit([]() { AssertThat(res.size(), Is().EqualTo(2u)); }); - it("computes (char) 0 + (int) 3 = (int) 3", [&]() { + it("computes bvec[8](0) + bvec[32](3)", [&]() { bvec a = bvec_const((char)0); bvec b = bvec_const((int)3); // 00000000 + @@ -298,7 +298,7 @@ go_bandit([]() { AssertThat(res.size(), Is().EqualTo(2u)); }); - it("computes (char) 255 + (char) 1 = (char) 0", [&]() { + it("computes bvec[8](255) + bvec[8](1)", [&]() { bvec a = bvec_const((char)255); bvec b = bvec_const((char)1); // 11111111 + @@ -311,6 +311,46 @@ go_bandit([]() { AssertThat(res.bitlen(), Is().EqualTo(8u)); AssertThat(res.size(), Is().EqualTo(0u)); }); + + it("computes bvec[8](255) + bvec[8](1)", [&]() { + bvec a = bvec_const((char)255); + bvec b = bvec_const((char)1); + // 11111111 + + // 00000001 = + // 00000000 + std::vector raw_expected = {}; + bvec expected = bvec(raw_expected); + bvec res = a+b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(0u)); + }); + + it("computes bvec[8](42) + char(3)", [&]() { + bvec a = bvec_const((char)42); + char b = 3; + // 00101010 + + // 00000011 = + // 00101101 + bvec expected = bvec_const(45); + bvec res = a+b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(6u)); + }); + + it("computes int(17) + bvec[8](42)", [&]() { + int a = 17; + bvec b = bvec_const((char)42); + // 00010001 + + // 00101010 = + // 00111011 + bvec expected = bvec_const(59); + bvec res = a+b; + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(6u)); + }); }); describe("bvec_truncate", []() { it("truncates to bitlen", [&](){ From 842e9a9740521d9ccff72fb65eb43effbee30c37 Mon Sep 17 00:00:00 2001 From: pallehpetersen <44908184+pallehpetersen@users.noreply.github.com> Date: Thu, 23 Apr 2026 17:28:02 +0200 Subject: [PATCH 24/35] implement bvec_sub --- src/adiar/bvec.cpp | 25 +++++++++++++++++++++++++ src/adiar/bvec.h | 2 ++ tests/adiar/bvec.test.cpp | 32 ++++++++++++++++++++++++++++++++ 3 files changed, 59 insertions(+) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index a62f6703f..85aa415b3 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -233,6 +233,31 @@ namespace adiar { return bvec(res, bitlen); } + bvec + bvec_sub(const bvec& x, const bvec& y) { + const size_t bitlen = std::max(x.bitlen(),y.bitlen()); + const size_t size = std::max(x.size(),bvec_not(y).size())+1; + + bdd carry = bdd_true(); + + std::vector res; + res.reserve(size); + + for (size_t i = 0; i= size, "is not last bit with overflow"); + carry = (carry & (x.at(i) | ~y.at(i))) | (x.at(i) & ~y.at(i)); + } + } + + // This assumes that the vector constructor truncates size above bitlen and false prefix. + res.push_back(carry); + + return bvec(res, bitlen); + } + //Helper bvec bvec_truncate(const bvec& x, const size_t bitlen) { diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 6cd23dfa9..2302f515b 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -145,6 +145,8 @@ namespace adiar { return bvec_add(i,x); } + bvec + bvec_sub(const bvec& x, const bvec& y); //Utility bvec diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index cb81afc46..f66e4d187 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -352,6 +352,38 @@ go_bandit([]() { AssertThat(res.size(), Is().EqualTo(6u)); }); }); + describe("bvec_sub", []() { + it("compute bvec[8](42) - bvec[8](3)", [&](){ + bvec x = bvec_const((char)42); + bvec y = bvec_const((char)3); + + bvec expected = bvec_const((char)39); + 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)", [&](){ + bvec x = bvec_const((char)140); + bvec y = bvec_const((char)4); + + bvec expected = bvec_const((char)136); + bvec res = bvec_sub(x,y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(8u)); + AssertThat(res.size(), Is().EqualTo(8u)); + }); + it("compute bvec[8](4) - bvec[32](7000)", [&](){ + bvec x = bvec_const((char)4); + bvec y = bvec_const((int)7000); + + bvec expected = bvec_const((int)-6996); + bvec res = bvec_sub(x,y); + AssertThat(res, Is().EqualTo(expected)); + AssertThat(res.bitlen(), Is().EqualTo(32u)); + AssertThat(res.size(), Is().EqualTo(32u)); + }); + }); describe("bvec_truncate", []() { it("truncates to bitlen", [&](){ bvec x = bvec_true(32); From 5a993134435df1fbb7181a89d3a4dca49c467933 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 15:13:19 +0200 Subject: [PATCH 25/35] Format bvec --- src/adiar/bvec.cpp | 511 ++++++++++++++++++++------------------ src/adiar/bvec.h | 291 ++++++++++++---------- tests/adiar/bvec.test.cpp | 302 ++++++++++++---------- 3 files changed, 588 insertions(+), 516 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 85aa415b3..18651404a 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -1,268 +1,295 @@ -#include -#include -#include -#include #include +#include #include +#include -namespace adiar { - ///////////////////////////////////////////////////////////////////////// - /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" - ///////////////////////////////////////////////////////////////////////// - bvec::bvec(size_t bitlen) - : _bits(0), _bitlen(bitlen) - {} - ///////////////////////////////////////////////////////////////////////// - /// \brief Copy constructor - ///////////////////////////////////////////////////////////////////////// - bvec::bvec(const bvec& fs) - : _bits(fs._bits), _bitlen(fs._bitlen) - {} - ///////////////////////////////////////////////////////////////////////// - /// \brief Move constructor for right-hand values - ///////////////////////////////////////////////////////////////////////// - bvec::bvec(bvec&& fs) - : _bits(std::move(fs._bits)), _bitlen(fs._bitlen) - {} - - ///////////////////////////////////////////////////////////////////////// - /// \brief Conversion constructor from a raw bit-vector - ///////////////////////////////////////////////////////////////////////// - bvec::bvec(const std::vector& bits, size_t bitlen) - : _bits(bits), _bitlen(bitlen) - { - this->truncate(bitlen); - } - ///////////////////////////////////////////////////////////////////////// - /// \brief Conversion constructor from a raw bit-vector for right-hand values - ///////////////////////////////////////////////////////////////////////// - bvec::bvec(std::vector&& bits, size_t bitlen) - : _bits(std::move(bits)), _bitlen(bitlen) - { - this->truncate(bitlen); - } - - ///////////////////////////////////////////////////////////////////////// - /// \brief Parameterized constructor with length `bitlen` and given initial value `f` - ///////////////////////////////////////////////////////////////////////// - bvec::bvec(const size_t bitlen, const bdd& f) - : _bits(bitlen,f), _bitlen(bitlen) - {} - - const bdd& // return type - bvec::at(size_t index) const //name(...) context - { - if (_bits.size() <= index) { return default_value; } //TODO: This warns that we are returning a local temp. Can we move it? - 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; - //Truncates to bitlen and removes any prefix of false - while (this->_bitlen < this->_bits.size()) { - this->_bits.pop_back(); - } - 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(); - } +#include +#include - bool - operator==(const bvec& x, const bvec& y) { - return bvec_equal(x,y); +namespace adiar +{ + ///////////////////////////////////////////////////////////////////////// + /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(size_t bitlen) + : _bits(0) + , _bitlen(bitlen) + {} + + ///////////////////////////////////////////////////////////////////////// + /// \brief Copy constructor + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(const bvec& fs) + : _bits(fs._bits) + , _bitlen(fs._bitlen) + {} + + ///////////////////////////////////////////////////////////////////////// + /// \brief Move constructor for right-hand values + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(bvec&& fs) + : _bits(std::move(fs._bits)) + , _bitlen(fs._bitlen) + {} + + ///////////////////////////////////////////////////////////////////////// + /// \brief Conversion constructor from a raw bit-vector + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(const std::vector& bits, size_t bitlen) + : _bits(bits) + , _bitlen(bitlen) + { + this->truncate(bitlen); + } + + ///////////////////////////////////////////////////////////////////////// + /// \brief Conversion constructor from a raw bit-vector for right-hand values + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(std::vector&& bits, size_t bitlen) + : _bits(std::move(bits)) + , _bitlen(bitlen) + { + this->truncate(bitlen); + } + + ///////////////////////////////////////////////////////////////////////// + /// \brief Parameterized constructor with length `bitlen` and given initial value `f` + ///////////////////////////////////////////////////////////////////////// + bvec::bvec(const size_t bitlen, const bdd& f) + : _bits(bitlen, f) + , _bitlen(bitlen) + {} + + const bdd& // return type + bvec::at(size_t index) const // name(...) context + { + if (_bits.size() <= index) { + return default_value; + } // TODO: This warns that we are returning a local temp. Can we move it? + 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 << "_"; + } } - 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; + return out.str(); + } + + void + bvec::truncate(size_t bitlen) + { + this->_bitlen = bitlen; + // Truncates to bitlen and removes any prefix of false + while (this->_bitlen < this->_bits.size()) { this->_bits.pop_back(); } + 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; } } - - // Constructors - bvec bvec_false(size_t bitlen = bvec::MAX_BITLEN) { - return bvec(std::vector(0,bdd_false()),bitlen); + return true; + } + + // Constructors + bvec + bvec_false(size_t bitlen = bvec::MAX_BITLEN) + { + return bvec(std::vector(0, bdd_false()), bitlen); + } + + bvec + bvec_true(size_t bitlen = bvec::MAX_BITLEN) + { + return bvec(std::vector(bitlen, bdd_true()), bitlen); + } + + bvec + bvec_const(size_t value, size_t bitlen) + { + size_t max = std::ceil(std::log2(value)) + 1; + size_t msb = std::min(value != 0 ? max : 0, bitlen); + std::vector res; + res.reserve(msb); + // Should be able to compute the most significant bit position and stop after that + for (size_t i = 0; i < msb; i++) { + res.push_back(value & 1 ? bdd_true() : bdd_false()); + + value >>= 1; } - bvec - bvec_true(size_t bitlen = bvec::MAX_BITLEN) { - return bvec(std::vector(bitlen,bdd_true()),bitlen); - } + return bvec(res, bitlen); + } - bvec - bvec_const(size_t value, size_t bitlen) { - size_t max = std::ceil(std::log2(value))+1; - size_t msb = std::min( value != 0 ? max : 0,bitlen); - std::vector res; - res.reserve(msb); - // Should be able to compute the most significant bit position and stop after that - for (size_t i = 0; i < msb; i++) { - res.push_back(value & 1 ? bdd_true() : bdd_false()); + // Bitwise operations - value >>= 1; - } + // Helper function for bitwise operations + template + bvec + _bvec_bitwise_op(size_t size, size_t bitlen, const BDD_OP& op) + { + std::vector res; - return bvec(res,bitlen); + 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); + } } - - // 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; - - 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(res, bitlen); - } - - 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 = std::max(x.bitlen(),y.bitlen()); - return _bvec_bitwise_op(size,bitlen,op); + return bvec(res, bitlen); + } + + 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 = std::max(x.bitlen(), y.bitlen()); + + 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(x.bitlen(), x.bitlen(), [&](size_t i) { return bdd_not(x.at(i)); }); + } + + // Arithmetic operations + + bvec + bvec_add(const bvec& x, const bvec& y) + { + const size_t bitlen = std::max(x.bitlen(), y.bitlen()); + const size_t size = std::max(x.size(), y.size()) + 1; + + bdd carry = bdd_false(); + + std::vector res; + res.reserve(size); + + for (size_t i = 0; i < size; ++i) { + const bdd xors = bdd_xor(bdd_xor(x.at(i), y.at(i)), carry); + res.push_back(xors); + if (i + 1 <= bitlen) { + adiar_assert(i != size - 1 || bitlen >= size, "is not last bit with overflow"); + carry = bdd_or(bdd_and(carry, bdd_or(x.at(i), y.at(i))), bdd_and(x.at(i), y.at(i))); + } } - 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)); }); - } + // This assumes that the vector constructor truncates size above bitlen and false prefix. + res.push_back(carry); - 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)); }); - } + return bvec(res, bitlen); + } - bvec bvec_not(const bvec& x) { - return _bvec_bitwise_op(x.bitlen(),x.bitlen(),[&](size_t i){ return bdd_not(x.at(i)); }); - } + bvec + bvec_sub(const bvec& x, const bvec& y) + { + const size_t bitlen = std::max(x.bitlen(), y.bitlen()); + const size_t size = std::max(x.size(), bvec_not(y).size()) + 1; - //Arithmetic operations + bdd carry = bdd_true(); - bvec - bvec_add(const bvec& x, const bvec& y) { - const size_t bitlen = std::max(x.bitlen(),y.bitlen()); - const size_t size = std::max(x.size(),y.size())+1; + std::vector res; + res.reserve(size); - bdd carry = bdd_false(); - - std::vector res; - res.reserve(size); - - for (size_t i = 0; i= size, "is not last bit with overflow"); - carry = bdd_or(bdd_and(carry, bdd_or(x.at(i),y.at(i))), bdd_and(x.at(i),y.at(i))); - } - } - - // This assumes that the vector constructor truncates size above bitlen and false prefix. - res.push_back(carry); - - return bvec(res, bitlen); + for (size_t i = 0; i < size; ++i) { + const bdd xors = x.at(i) ^ ~y.at(i) ^ carry; + res.push_back(xors); + if (i + 1 <= bitlen) { + adiar_assert(i != size - 1 || bitlen >= size, "is not last bit with overflow"); + carry = (carry & (x.at(i) | ~y.at(i))) | (x.at(i) & ~y.at(i)); + } } - bvec - bvec_sub(const bvec& x, const bvec& y) { - const size_t bitlen = std::max(x.bitlen(),y.bitlen()); - const size_t size = std::max(x.size(),bvec_not(y).size())+1; - - bdd carry = bdd_true(); + // This assumes that the vector constructor truncates size above bitlen and false prefix. + res.push_back(carry); - std::vector res; - res.reserve(size); + return bvec(res, bitlen); + } - for (size_t i = 0; i= size, "is not last bit with overflow"); - carry = (carry & (x.at(i) | ~y.at(i))) | (x.at(i) & ~y.at(i)); - } - } - - // This assumes that the vector constructor truncates size above bitlen and false prefix. - res.push_back(carry); - - return bvec(res, bitlen); - } - - //Helper - bvec - bvec_truncate(const bvec& x, const size_t bitlen) { - bvec y = x; - y.truncate(bitlen); - return y; - } + // Helper + bvec + bvec_truncate(const bvec& x, const size_t bitlen) + { + bvec y = x; + y.truncate(bitlen); + return y; + } } diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 2302f515b..60cc75263 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -1,159 +1,178 @@ #ifndef ADIAR_BVEC_H #define ADIAR_BVEC_H -#include -#include -#include #include +#include #include +#include -namespace adiar { - class bvec +#include + +namespace adiar +{ + class bvec + { + public: + static constexpr size_t MAX_BITLEN = 128; + + private: + std::vector _bits; + size_t _bitlen; + const bdd default_value = bdd(); + + public: + ///////////////////////////////////////////////////////////////////////// + /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" + ///////////////////////////////////////////////////////////////////////// + bvec(size_t bitlen = MAX_BITLEN); + ///////////////////////////////////////////////////////////////////////// + /// \brief Copy constructor + ///////////////////////////////////////////////////////////////////////// + bvec(const bvec& fs); + ///////////////////////////////////////////////////////////////////////// + /// \brief Move constructor for right-hand values + ///////////////////////////////////////////////////////////////////////// + bvec(bvec&& fs); + + ///////////////////////////////////////////////////////////////////////// + /// \brief Conversion constructor from a raw bit-vector + ///////////////////////////////////////////////////////////////////////// + bvec(const std::vector& bits, size_t bitlen = MAX_BITLEN); + ///////////////////////////////////////////////////////////////////////// + /// \brief Conversion constructor from a raw bit-vector for right-hand values + ///////////////////////////////////////////////////////////////////////// + bvec(std::vector&& bits, size_t bitlen = MAX_BITLEN); + + ///////////////////////////////////////////////////////////////////////// + /// \brief Parameterized constructor with length `bitlen` and given initial value `f` + ///////////////////////////////////////////////////////////////////////// + bvec(const size_t bitlen, const bdd& f); + + inline size_t + bitlen() const { - public: static constexpr size_t MAX_BITLEN = 128; - private: - std::vector _bits; - size_t _bitlen; - const bdd default_value = bdd(); - - public: - ///////////////////////////////////////////////////////////////////////// - /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" - ///////////////////////////////////////////////////////////////////////// - bvec(size_t bitlen = MAX_BITLEN); - ///////////////////////////////////////////////////////////////////////// - /// \brief Copy constructor - ///////////////////////////////////////////////////////////////////////// - bvec(const bvec& fs); - ///////////////////////////////////////////////////////////////////////// - /// \brief Move constructor for right-hand values - ///////////////////////////////////////////////////////////////////////// - bvec(bvec&& fs); - - ///////////////////////////////////////////////////////////////////////// - /// \brief Conversion constructor from a raw bit-vector - ///////////////////////////////////////////////////////////////////////// - bvec(const std::vector& bits, size_t bitlen = MAX_BITLEN); - ///////////////////////////////////////////////////////////////////////// - /// \brief Conversion constructor from a raw bit-vector for right-hand values - ///////////////////////////////////////////////////////////////////////// - bvec(std::vector&& bits, size_t bitlen = MAX_BITLEN); - - ///////////////////////////////////////////////////////////////////////// - /// \brief Parameterized constructor with length `bitlen` and given initial value `f` - ///////////////////////////////////////////////////////////////////////// - bvec(const size_t bitlen, const bdd& f); - - inline size_t bitlen() const { return _bitlen; } - inline size_t size() const { return _bits.size(); } - - const bdd& - at(size_t index) const; - - std::vector::const_iterator - begin() const; - - std::vector::const_iterator - end() const; - - std::vector::const_reverse_iterator - rbegin() const; - - std::vector::const_reverse_iterator - rend() const; - - std::string - to_string() const; - - void - truncate(size_t bitlen); - }; - - std::ostream& - operator<<(std::ostream& os, const bvec& a); - - // Constructors - - bvec - bvec_false(size_t bitlen); - - bvec - bvec_true(size_t bitlen); - - bvec - bvec_const(size_t value, size_t bitlen); - - template - bvec - bvec_const(Integer i) { - return bvec_const(i,8 * sizeof(Integer)); + return _bitlen; } - - //Comparators - bool - bvec_equal(const bvec& x, const bvec& y); + inline size_t + size() const + { + return _bits.size(); + } - bool - operator==(const bvec& x, const bvec& y); + const bdd& + at(size_t index) const; - - // Bitwise operations + std::vector::const_iterator + begin() const; - bvec - bvec_and(const bvec& x, const bvec& y); - - bvec - bvec_or(const bvec& x, const bvec& y); - - bvec - bvec_xor(const bvec& x, const bvec& y); + std::vector::const_iterator + end() const; - bvec - bvec_not(const bvec& x); + std::vector::const_reverse_iterator + rbegin() const; - //Arithmetic operations + std::vector::const_reverse_iterator + rend() const; - bvec - bvec_add(const bvec& x, const bvec& y); + std::string + to_string() const; - template - bvec - bvec_add(const bvec& x, Integer i) { - return bvec_add(x,bvec_const(i)); - } + void + truncate(size_t bitlen); + }; - template - bvec - bvec_add(Integer i,const bvec& x) { - return bvec_add(x,i); - } + std::ostream& + operator<<(std::ostream& os, const bvec& a); - inline bvec - operator+(const bvec& x, const bvec& y) { - return bvec_add(x,y); - } - - template - bvec - operator+(const bvec& x, Integer i) { - return bvec_add(x,i); - } - template - bvec - operator+(Integer i,const bvec& x) { - return bvec_add(i,x); - } + // Constructors + + bvec + bvec_false(size_t bitlen); + + bvec + bvec_true(size_t bitlen); + + bvec + bvec_const(size_t value, size_t bitlen); + + template + bvec + bvec_const(Integer i) + { + return bvec_const(i, 8 * sizeof(Integer)); + } + + // Comparators + + bool + bvec_equal(const bvec& x, const bvec& y); + + bool + operator==(const bvec& x, const bvec& y); + + // Bitwise operations + + bvec + bvec_and(const bvec& x, const bvec& y); + + bvec + bvec_or(const bvec& x, const bvec& y); + + bvec + bvec_xor(const bvec& x, const bvec& y); + + bvec + bvec_not(const bvec& x); + + // Arithmetic operations + + bvec + bvec_add(const bvec& x, const bvec& y); + + template + bvec + bvec_add(const bvec& x, Integer i) + { + return bvec_add(x, bvec_const(i)); + } + + template + bvec + bvec_add(Integer i, const bvec& x) + { + return bvec_add(x, i); + } + + inline bvec + operator+(const bvec& x, const bvec& y) + { + return bvec_add(x, y); + } + + template + bvec + operator+(const bvec& x, Integer i) + { + return bvec_add(x, i); + } + + template + bvec + operator+(Integer i, const bvec& x) + { + return bvec_add(i, x); + } - bvec - bvec_sub(const bvec& x, const bvec& y); + bvec + bvec_sub(const bvec& x, const bvec& y); - //Utility - bvec - bvec_truncate(const bvec& x, const size_t bitlen); + // Utility + bvec + bvec_truncate(const bvec& x, const size_t bitlen); } -//TODO: Implement arithmetic operations -//TODO: Add variables, bvec_var(ITER begin, ITER end, bitlen) +// TODO: Implement arithmetic operations +// TODO: Add variables, bvec_var(ITER begin, ITER end, bitlen) -#endif // ADIAR_BVEC_H +#endif // ADIAR_BVEC_H diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index f66e4d187..c44d272df 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -1,17 +1,18 @@ #include "../test.h" + #include go_bandit([]() { describe("adiar/bvec.h", []() { describe("bvec_false()", []() { - it("has 16 bits when asked", [&]() { - AssertThat(bvec_false(16).bitlen(), Is().EqualTo(16u)); - }); + it("has 16 bits when asked", + [&]() { AssertThat(bvec_false(16).bitlen(), Is().EqualTo(16u)); }); }); + describe("bvec_true()", []() { - it("has 32 bits when asked", [&]() { - AssertThat(bvec_true(32).bitlen(), Is().EqualTo(32u)); - }); + it("has 32 bits when asked", + [&]() { AssertThat(bvec_true(32).bitlen(), Is().EqualTo(32u)); }); }); + describe("bvec_const", []() { describe("bitlength inference", []() { it("has 32 bitlen 0 size when constructed with 0", [&]() { @@ -19,21 +20,25 @@ go_bandit([]() { AssertThat(x.size(), Is().EqualTo(0u)); AssertThat(x.bitlen(), Is().EqualTo(32u)); }); + it("has 8 size and bitlen when constructed with max unsigned char", [&]() { const bvec x = bvec_const((unsigned char)255); AssertThat(x.size(), Is().EqualTo(8u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); }); + it("has 8 size and bitlen when constructed with overflowing char", [&]() { const bvec x = bvec_const((char)253); AssertThat(x.size(), Is().EqualTo(8u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); }); + it("has 8 size and bitlen when constructed with negative char", [&]() { const bvec x = bvec_const((char)-52); AssertThat(x.size(), Is().EqualTo(8u)); AssertThat(x.bitlen(), Is().EqualTo(8u)); }); + it("has 7 size and 8 bitlen when constructed with max signed char", [&]() { const bvec x = bvec_const((char)127); AssertThat(x.size(), Is().EqualTo(7u)); @@ -43,7 +48,7 @@ go_bandit([]() { describe("int encoding", []() { it("is the binary encoding of 42 (101010)", [&]() { - // + // const bvec x = bvec_const(42); // Check that encoding is 101010 @@ -55,30 +60,27 @@ go_bandit([]() { 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++) { + for (size_t i = 6; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_false())); } }); it("is the binary encoding of -1 ", [&]() { - // + // const bvec x = bvec_const(-1); - for( size_t i = 0; i < x.bitlen(); i++) { - AssertThat(x.at(i), Is().EqualTo(bdd_true())); - } - + for (size_t i = 0; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_true())); } }); it("is the binary encoding of -2^32", [&]() { - // + // const bvec x = bvec_const(INT32_MIN); - - for( size_t i = 0; i < x.bitlen()-1; i++) { + + 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())); + AssertThat(x.at(x.bitlen() - 1), Is().EqualTo(bdd_true())); }); }); }); @@ -88,20 +90,22 @@ go_bandit([]() { it("computes 5 & 3 == 1 (101 & 011 == 001)", [&]() { const bvec x = bvec_const((char)5); const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)1); //Is this expected, or should we check bdd structure? + const bvec expected = + bvec_const((char)1); // Is this expected, or should we check bdd structure? + + const bvec res = bvec_and(x, y); - 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((char)0); const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)0); //Is this expected, or should we check bdd structure? + const bvec expected = + bvec_const((char)0); // Is this expected, or should we check bdd structure? + + const bvec res = bvec_and(x, y); - const bvec res = bvec_and(x,y); - AssertThat(res, Is().EqualTo(expected)); }); }); @@ -112,19 +116,22 @@ go_bandit([]() { it("computes 5 | 3 == 7 (101 | 011 == 111)", [&]() { const bvec x = bvec_const((char)5); const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)7); //Is this expected, or should we check bdd structure? + const bvec expected = + bvec_const((char)7); // Is this expected, or should we check bdd structure? + + const bvec res = bvec_or(x, y); - 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((char)0); const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)3); //Is this expected, or should we check bdd structure? + const bvec expected = + bvec_const((char)3); // Is this expected, or should we check bdd structure? + + const bvec res = bvec_or(x, y); - const bvec res = bvec_or(x,y); - AssertThat(res, Is().EqualTo(expected)); }); }); @@ -135,29 +142,33 @@ go_bandit([]() { it("computes 5 ^ 3 == 6 (101 ^ 011 == 110)", [&]() { const bvec x = bvec_const((char)5); const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)6); //Is this expected, or should we check bdd structure? + const bvec expected = + bvec_const((char)6); // Is this expected, or should we check bdd structure? + + const bvec res = bvec_xor(x, y); - 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((char)0); const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)3); //Is this expected, or should we check bdd structure? + const bvec expected = + bvec_const((char)3); // Is this expected, or should we check bdd structure? + + const bvec res = bvec_xor(x, y); - 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((char)255); const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)252); //Is this expected, or should we check bdd structure? + const bvec expected = + bvec_const((char)252); // Is this expected, or should we check bdd structure? + + const bvec res = bvec_xor(x, y); - const bvec res = bvec_xor(x,y); - AssertThat(res, Is().EqualTo(expected)); }); }); @@ -167,80 +178,92 @@ go_bandit([]() { describe("constants", []() { it("computes ~3 == 252 for bitlength 8 (~00000011 == 11111100)", [&]() { const bvec x = bvec_const((char)3); - const bvec expected = bvec_const((u_char)252); //Is this expected, or should we check bdd structure? + const bvec expected = + bvec_const((u_char)252); // Is this expected, or should we check bdd structure? 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((short)3); - const bvec expected = bvec_const((short)(USHRT_MAX-3)); //Is this expected, or should we check bdd structure? - 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((short)3); + const bvec expected = bvec_const( + (short)(USHRT_MAX - 3)); // Is this expected, or should we check bdd structure? + + const bvec res = bvec_not(x); + + AssertThat(res, Is().EqualTo(expected)); + }); }); }); + describe("bvec_equal", []() { it("compares 101 == 101", [&]() { - std::vector raw1 = {bdd_true(),bdd_false(),bdd_true()}; - std::vector raw2 = {bdd_true(),bdd_false(),bdd_true()}; - - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().True()); + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); }); + it("compares 0101 == 101", [&]() { - std::vector raw1 = {bdd_true(),bdd_false(),bdd_true()}; - std::vector raw2 = {bdd_true(),bdd_false(),bdd_true(),bdd_false()}; - - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().True()); + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true(), bdd_false() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); }); + it("compares 101 == 0101", [&]() { - std::vector raw1 = {bdd_true(),bdd_false(),bdd_true(),bdd_false()}; - std::vector raw2 = {bdd_true(),bdd_false(),bdd_true()}; - - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().True()); + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_false() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); }); + it("compares 101 != 1101", [&]() { - std::vector raw1 = {bdd_true(),bdd_false(),bdd_true(),bdd_true()}; - std::vector raw2 = {bdd_true(),bdd_false(),bdd_true()}; - - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); }); + it("compares 1101 != 101", [&]() { - std::vector raw1 = {bdd_true(),bdd_false(),bdd_true()}; - std::vector raw2 = {bdd_true(),bdd_false(),bdd_true(),bdd_true()}; - - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); }); + it("compares 1101 != 1110", [&]() { - std::vector raw1 = {bdd_true(),bdd_false(),bdd_true(),bdd_true()}; - std::vector raw2 = {bdd_false(),bdd_true(),bdd_true(),bdd_true()}; - - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; + std::vector raw2 = { bdd_false(), bdd_true(), bdd_true(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); }); + it("compares 1100 != 1110", [&]() { - std::vector raw1 = {bdd_false(),bdd_false(),bdd_true(),bdd_true()}; - std::vector raw2 = {bdd_false(),bdd_true(),bdd_true(),bdd_true()}; - - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + std::vector raw1 = { bdd_false(), bdd_false(), bdd_true(), bdd_true() }; + std::vector raw2 = { bdd_false(), bdd_true(), bdd_true(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); }); + it("compares 1x0 == 1x0", [&]() { - std::vector raw1 = {bdd_false(),bdd_ithvar(42),bdd_true()}; - std::vector raw2 = {bdd_false(),bdd_ithvar(42),bdd_true()}; + std::vector raw1 = { bdd_false(), bdd_ithvar(42), bdd_true() }; + std::vector raw2 = { bdd_false(), bdd_ithvar(42), bdd_true() }; - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().True()); + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); }); + it("compares 1x0 != 1y0", [&]() { - std::vector raw1 = {bdd_false(),bdd_ithvar(42),bdd_true()}; - std::vector raw2 = {bdd_false(),bdd_ithvar(11),bdd_true()}; - - AssertThat(bvec_equal(bvec(raw1),bvec(raw2)), Is().False()); + std::vector raw1 = { bdd_false(), bdd_ithvar(42), bdd_true() }; + std::vector raw2 = { bdd_false(), bdd_ithvar(11), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); }); }); + describe("bvec_add", []() { it("computes bvec[8](5) + bvec[8](3)", [&]() { bvec a = bvec_const((char)5); @@ -248,10 +271,10 @@ go_bandit([]() { // 00000101 + // 00000011 = // 00001000 - std::vector raw_expected = {bdd_false(),bdd_false(),bdd_false(),bdd_true()}; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a,b); - AssertThat(res, Is().EqualTo(expected)); + std::vector raw_expected = { bdd_false(), bdd_false(), bdd_false(), bdd_true() }; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(8u)); AssertThat(res.size(), Is().EqualTo(4u)); }); @@ -262,10 +285,10 @@ go_bandit([]() { // 00000000000000000000000000000101 + // 00000011 = // 00000000000000000000000000001000 - std::vector raw_expected = {bdd_false(),bdd_false(),bdd_false(),bdd_true()}; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a,b); - AssertThat(res, Is().EqualTo(expected)); + std::vector raw_expected = { bdd_false(), bdd_false(), bdd_false(), bdd_true() }; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(32u)); AssertThat(res.size(), Is().EqualTo(4u)); }); @@ -276,10 +299,10 @@ go_bandit([]() { // 00000000000000000000000000000000 + // 00000011 = // 00000000000000000000000000000011 - std::vector raw_expected = {bdd_true(),bdd_true()}; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a,b); - AssertThat(res, Is().EqualTo(expected)); + std::vector raw_expected = { bdd_true(), bdd_true() }; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(32u)); AssertThat(res.size(), Is().EqualTo(2u)); }); @@ -290,10 +313,10 @@ go_bandit([]() { // 00000000 + // 00000000000000000000000000000011 = // 00000000000000000000000000000011 - std::vector raw_expected = {bdd_true(),bdd_true()}; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a,b); - AssertThat(res, Is().EqualTo(expected)); + std::vector raw_expected = { bdd_true(), bdd_true() }; + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(32u)); AssertThat(res.size(), Is().EqualTo(2u)); }); @@ -305,13 +328,13 @@ go_bandit([]() { // 00000001 = // 00000000 std::vector raw_expected = {}; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a,b); - AssertThat(res, Is().EqualTo(expected)); + bvec expected = bvec(raw_expected); + bvec res = bvec_add(a, b); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(8u)); AssertThat(res.size(), Is().EqualTo(0u)); }); - + it("computes bvec[8](255) + bvec[8](1)", [&]() { bvec a = bvec_const((char)255); bvec b = bvec_const((char)1); @@ -319,13 +342,13 @@ go_bandit([]() { // 00000001 = // 00000000 std::vector raw_expected = {}; - bvec expected = bvec(raw_expected); - bvec res = a+b; - AssertThat(res, Is().EqualTo(expected)); + bvec expected = bvec(raw_expected); + bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(8u)); AssertThat(res.size(), Is().EqualTo(0u)); }); - + it("computes bvec[8](42) + char(3)", [&]() { bvec a = bvec_const((char)42); char b = 3; @@ -333,89 +356,92 @@ go_bandit([]() { // 00000011 = // 00101101 bvec expected = bvec_const(45); - bvec res = a+b; - AssertThat(res, Is().EqualTo(expected)); + bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(8u)); AssertThat(res.size(), Is().EqualTo(6u)); }); - + it("computes int(17) + bvec[8](42)", [&]() { - int a = 17; + int a = 17; bvec b = bvec_const((char)42); // 00010001 + // 00101010 = // 00111011 bvec expected = bvec_const(59); - bvec res = a+b; - AssertThat(res, Is().EqualTo(expected)); + bvec res = a + b; + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(32u)); AssertThat(res.size(), Is().EqualTo(6u)); }); }); - describe("bvec_sub", []() { - it("compute bvec[8](42) - bvec[8](3)", [&](){ + + describe("bvec_sub", []() { + it("compute bvec[8](42) - bvec[8](3)", [&]() { bvec x = bvec_const((char)42); bvec y = bvec_const((char)3); bvec expected = bvec_const((char)39); - bvec res = bvec_sub(x,y); - AssertThat(res, Is().EqualTo(expected)); + 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)", [&](){ + + it("compute bvec[8](140) - bvec[8](4)", [&]() { bvec x = bvec_const((char)140); bvec y = bvec_const((char)4); bvec expected = bvec_const((char)136); - bvec res = bvec_sub(x,y); - AssertThat(res, Is().EqualTo(expected)); + bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(8u)); AssertThat(res.size(), Is().EqualTo(8u)); }); - it("compute bvec[8](4) - bvec[32](7000)", [&](){ + + it("compute bvec[8](4) - bvec[32](7000)", [&]() { bvec x = bvec_const((char)4); bvec y = bvec_const((int)7000); bvec expected = bvec_const((int)-6996); - bvec res = bvec_sub(x,y); - AssertThat(res, Is().EqualTo(expected)); + bvec res = bvec_sub(x, y); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(32u)); AssertThat(res.size(), Is().EqualTo(32u)); }); }); + describe("bvec_truncate", []() { - it("truncates to bitlen", [&](){ + it("truncates to bitlen", [&]() { bvec x = bvec_true(32); - bvec expected = bvec_true(8); - bvec res = bvec_truncate(x,8); - AssertThat(res, Is().EqualTo(expected)); + bvec res = bvec_truncate(x, 8); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(8u)); AssertThat(res.size(), Is().EqualTo(8u)); }); - - it("extends to bitlen", [&](){ + + it("extends to bitlen", [&]() { bvec x = bvec_true(4); AssertThat(x.bitlen(), Is().EqualTo(4u)); bvec expected = bvec_true(4); - bvec res = bvec_truncate(x,8); - AssertThat(res, Is().EqualTo(expected)); + bvec res = bvec_truncate(x, 8); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(8u)); AssertThat(res.size(), Is().EqualTo(4u)); }); - it("truncates false prefix", [&](){ + it("truncates false prefix", [&]() { bvec x = bvec_const(18); bvec expected = bvec_const(2); - bvec res = bvec_truncate(x,4); - AssertThat(res, Is().EqualTo(expected)); + bvec res = bvec_truncate(x, 4); + AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(4u)); AssertThat(res.size(), Is().EqualTo(2u)); }); }); }); -}); \ No newline at end of file +}); From 651c794d3b80064e0b3bf90d9028bed36af91cc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 16:04:08 +0200 Subject: [PATCH 26/35] Set up documentation for symbolic bitvectors --- src/adiar/bvec.cpp | 34 +++---- src/adiar/bvec.h | 242 ++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 228 insertions(+), 48 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 18651404a..3fb26af1c 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -8,33 +8,24 @@ namespace adiar { - ///////////////////////////////////////////////////////////////////////// - /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" - ///////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// + // `bvec` class + bvec::bvec(size_t bitlen) : _bits(0) , _bitlen(bitlen) {} - ///////////////////////////////////////////////////////////////////////// - /// \brief Copy constructor - ///////////////////////////////////////////////////////////////////////// bvec::bvec(const bvec& fs) : _bits(fs._bits) , _bitlen(fs._bitlen) {} - ///////////////////////////////////////////////////////////////////////// - /// \brief Move constructor for right-hand values - ///////////////////////////////////////////////////////////////////////// bvec::bvec(bvec&& fs) : _bits(std::move(fs._bits)) , _bitlen(fs._bitlen) {} - ///////////////////////////////////////////////////////////////////////// - /// \brief Conversion constructor from a raw bit-vector - ///////////////////////////////////////////////////////////////////////// bvec::bvec(const std::vector& bits, size_t bitlen) : _bits(bits) , _bitlen(bitlen) @@ -42,9 +33,6 @@ namespace adiar this->truncate(bitlen); } - ///////////////////////////////////////////////////////////////////////// - /// \brief Conversion constructor from a raw bit-vector for right-hand values - ///////////////////////////////////////////////////////////////////////// bvec::bvec(std::vector&& bits, size_t bitlen) : _bits(std::move(bits)) , _bitlen(bitlen) @@ -52,20 +40,17 @@ namespace adiar this->truncate(bitlen); } - ///////////////////////////////////////////////////////////////////////// - /// \brief Parameterized constructor with length `bitlen` and given initial value `f` - ///////////////////////////////////////////////////////////////////////// bvec::bvec(const size_t bitlen, const bdd& f) : _bits(bitlen, f) , _bitlen(bitlen) {} - const bdd& // return type - bvec::at(size_t index) const // name(...) context + const bdd& + bvec::at(size_t index) const { if (_bits.size() <= index) { - return default_value; - } // TODO: This warns that we are returning a local temp. Can we move it? + return this->default_value; + } return _bits.at(index); } @@ -121,6 +106,7 @@ namespace adiar while (this->_bits.size() > 0 && !this->_bits.back()) { this->_bits.pop_back(); } } + ////////////////////////////////////////////////////////////////////////////////////////////////// // Comparators std::ostream& @@ -146,7 +132,9 @@ namespace adiar return true; } + ////////////////////////////////////////////////////////////////////////////////////////////////// // Constructors + bvec bvec_false(size_t bitlen = bvec::MAX_BITLEN) { @@ -176,6 +164,7 @@ namespace adiar return bvec(res, bitlen); } + ////////////////////////////////////////////////////////////////////////////////////////////////// // Bitwise operations // Helper function for bitwise operations @@ -230,6 +219,7 @@ namespace adiar return _bvec_bitwise_op(x.bitlen(), x.bitlen(), [&](size_t i) { return bdd_not(x.at(i)); }); } + ////////////////////////////////////////////////////////////////////////////////////////////////// // Arithmetic operations bvec diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 60cc75263..8367c9f76 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -1,6 +1,16 @@ #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 @@ -10,92 +20,174 @@ namespace adiar { + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Symbolic Bitvector + ////////////////////////////////////////////////////////////////////////////////////////////////// class bvec { public: static constexpr size_t MAX_BITLEN = 128; 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 const bdd default_value = bdd(); public: - ///////////////////////////////////////////////////////////////////////// - /// \brief Zero-length bvec constructor, effectively a "safe nullpointer" - ///////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Zero-valued bvec of a given bitlength. + //////////////////////////////////////////////////////////////////////////////////////////////// bvec(size_t bitlen = MAX_BITLEN); - ///////////////////////////////////////////////////////////////////////// + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Construct a bitvector with initial value `f` for all `bitlen` many bits. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(size_t bitlen, const bdd& f); + + //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Copy constructor - ///////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////////////////////// bvec(const bvec& fs); - ///////////////////////////////////////////////////////////////////////// + + //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Move constructor for right-hand values - ///////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////////////////////// bvec(bvec&& fs); - ///////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector - ///////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////////////////////// bvec(const std::vector& bits, size_t bitlen = MAX_BITLEN); - ///////////////////////////////////////////////////////////////////////// + + //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Conversion constructor from a raw bit-vector for right-hand values - ///////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////////////////////////// bvec(std::vector&& bits, size_t bitlen = MAX_BITLEN); - ///////////////////////////////////////////////////////////////////////// - /// \brief Parameterized constructor with length `bitlen` and given initial value `f` - ///////////////////////////////////////////////////////////////////////// - bvec(const size_t bitlen, const bdd& f); - + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \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 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); }; + /// \cond std::ostream& operator<<(std::ostream& os, const bvec& a); - - // Constructors - + /// \endcond + + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__constructors Constructors + /// + /// \hidegroupgraph + /// + /// \{ + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief The all-zero bitvector. + /// + /// \param bitlen The width of the bit-vector. + //////////////////////////////////////////////////////////////////////////////////////////////// bvec bvec_false(size_t bitlen); + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief The all-one bitvector. + /// + /// \param bitlen The width of the bit-vector, i.e. the number of 1 bits. + //////////////////////////////////////////////////////////////////////////////////////////////// bvec bvec_true(size_t bitlen); + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Create a bitvector which contains the given (non-negative) integer. + /// + /// \param value The integer to be represented. + /// + /// \param bitlen The width of the bit-vector, possibly truncating `value` if there is not enough + /// space for it. + //////////////////////////////////////////////////////////////////////////////////////////////// bvec bvec_const(size_t value, size_t bitlen); + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Create a bitvector which contains the given (non-negative) integer. + /// + /// \details This automatically derives the `bitlen` based on the number of bits needed for the + /// given type. That is, the result is a 32-bit bitvector if using an `int`. + /// + /// \param value The integer to be represented. + //////////////////////////////////////////////////////////////////////////////////////////////// template bvec bvec_const(Integer i) @@ -103,33 +195,95 @@ namespace adiar return bvec_const(i, 8 * sizeof(Integer)); } - // Comparators - + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \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); - // Bitwise operations - + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__logical Logical Operations + /// + /// \hidegroupgraph + /// + /// \{ + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \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); - // Arithmetic operations - + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__arithmetic Arithmetic Operations + /// + /// \hidegroupgraph + /// + /// \{ + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Arithmetic addition of two symbolic bit-vectors. + //////////////////////////////////////////////////////////////////////////////////////////////// bvec bvec_add(const bvec& x, const bvec& y); + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Arithmetic addition of a symbolic bit-vector with a constant. + /// + /// \details The bitlength of the constant is derived based on its type. + //////////////////////////////////////////////////////////////////////////////////////////////// template bvec bvec_add(const bvec& x, Integer i) @@ -137,6 +291,11 @@ namespace adiar return bvec_add(x, bvec_const(i)); } + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Arithmetic addition of a symbolic bit-vector with a constant. + /// + /// \details The bitlength of the constant is derived based on its type. + //////////////////////////////////////////////////////////////////////////////////////////////// template bvec bvec_add(Integer i, const bvec& x) @@ -144,12 +303,18 @@ namespace adiar return bvec_add(x, i); } + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bvec_add + ////////////////////////////////////////////////////////////////////////////////////////////////// inline bvec operator+(const bvec& x, const bvec& y) { return bvec_add(x, y); } + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bvec_add + ////////////////////////////////////////////////////////////////////////////////////////////////// template bvec operator+(const bvec& x, Integer i) @@ -157,6 +322,9 @@ namespace adiar return bvec_add(x, i); } + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bvec_add + ////////////////////////////////////////////////////////////////////////////////////////////////// template bvec operator+(Integer i, const bvec& x) @@ -164,12 +332,34 @@ namespace adiar return bvec_add(i, x); } + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \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); - // Utility + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \addtogroup module__bvec + /// \{ + /// + /// \defgroup module__bvec__utility Utility + /// + /// \hidegroupgraph + /// + /// \{ + bvec bvec_truncate(const bvec& x, const size_t bitlen); + + /// \} + /// \} + ////////////////////////////////////////////////////////////////////////////////////////////////// } // TODO: Implement arithmetic operations From 3aa5bb29c73f48c53b02babf57a5d4a40d555068 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 16:23:33 +0200 Subject: [PATCH 27/35] Some clean up in the current unit tests for bitvectors --- src/adiar/bvec.cpp | 4 +- tests/adiar/bvec.test.cpp | 258 +++++++++++++++++++++++--------------- 2 files changed, 156 insertions(+), 106 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 3fb26af1c..308da44de 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -48,9 +48,7 @@ namespace adiar const bdd& bvec::at(size_t index) const { - if (_bits.size() <= index) { - return this->default_value; - } + if (_bits.size() <= index) { return this->default_value; } return _bits.at(index); } diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index c44d272df..7a383a549 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -6,11 +6,40 @@ go_bandit([]() { describe("bvec_false()", []() { it("has 16 bits when asked", [&]() { AssertThat(bvec_false(16).bitlen(), Is().EqualTo(16u)); }); + + it("has all bits set to false", [&]() { + const bvec x = bvec_false(8); + + AssertThat(x.at(0), Is().False()); + AssertThat(x.at(1), Is().False()); + AssertThat(x.at(2), Is().False()); + AssertThat(x.at(3), Is().False()); + AssertThat(x.at(4), Is().False()); + AssertThat(x.at(5), Is().False()); + AssertThat(x.at(6), Is().False()); + AssertThat(x.at(7), Is().False()); + }); }); describe("bvec_true()", []() { it("has 32 bits when asked", [&]() { AssertThat(bvec_true(32).bitlen(), Is().EqualTo(32u)); }); + + it("has all bits set to true", [&]() { + const bvec x = bvec_true(8); + + AssertThat(x.at(0), Is().True()); + AssertThat(x.at(1), Is().True()); + AssertThat(x.at(2), Is().True()); + AssertThat(x.at(3), Is().True()); + AssertThat(x.at(4), Is().True()); + AssertThat(x.at(5), Is().True()); + AssertThat(x.at(6), Is().True()); + AssertThat(x.at(7), Is().True()); + }); + + it("has out-of-bound bit set to false", + [&]() { AssertThat(bvec_true(8).at(8), Is().False()); }); }); describe("bvec_const", []() { @@ -46,9 +75,41 @@ go_bandit([]() { }); }); - describe("int encoding", []() { - it("is the binary encoding of 42 (101010)", [&]() { - // + describe("bit encoding", []() { + it("derives 0 ()", [&]() { + 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("derives 1 (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("derives 2 (01)", [&]() { + 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("derives 42 (101010)", [&]() { const bvec x = bvec_const(42); // Check that encoding is 101010 @@ -65,14 +126,14 @@ go_bandit([]() { } }); - it("is the binary encoding of -1 ", [&]() { + it("derives -1 (111...1)", [&]() { // const bvec x = bvec_const(-1); for (size_t i = 0; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_true())); } }); - it("is the binary encoding of -2^32", [&]() { + it("derives -2^32 (000..01)", [&]() { // const bvec x = bvec_const(INT32_MIN); @@ -85,13 +146,77 @@ go_bandit([]() { }); }); + describe("bvec_equal", []() { + it("compares 101 == 101", [&]() { + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); + }); + + it("compares 0101 == 101", [&]() { + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true(), bdd_false() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); + }); + + it("compares 101 == 0101", [&]() { + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_false() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); + }); + + it("compares 101 != 1101", [&]() { + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); + }); + + it("compares 1101 != 101", [&]() { + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; + std::vector raw2 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); + }); + + it("compares 1101 != 1110", [&]() { + std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; + std::vector raw2 = { bdd_false(), bdd_true(), bdd_true(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); + }); + + it("compares 1100 != 1110", [&]() { + std::vector raw1 = { bdd_false(), bdd_false(), bdd_true(), bdd_true() }; + std::vector raw2 = { bdd_false(), bdd_true(), bdd_true(), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); + }); + + it("compares 1x0 == 1x0", [&]() { + std::vector raw1 = { bdd_false(), bdd_ithvar(42), bdd_true() }; + std::vector raw2 = { bdd_false(), bdd_ithvar(42), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); + }); + + it("compares 1x0 != 1y0", [&]() { + std::vector raw1 = { bdd_false(), bdd_ithvar(42), bdd_true() }; + std::vector raw2 = { bdd_false(), bdd_ithvar(11), bdd_true() }; + + AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); + }); + }); + describe("bvec_and", []() { describe("constants", []() { it("computes 5 & 3 == 1 (101 & 011 == 001)", [&]() { - const bvec x = bvec_const((char)5); - const bvec y = bvec_const((char)3); - const bvec expected = - bvec_const((char)1); // Is this expected, or should we check bdd structure? + const bvec x = bvec_const((char)5); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)1); const bvec res = bvec_and(x, y); @@ -99,10 +224,9 @@ go_bandit([]() { }); it("computes 0 & 3 == 0 (000 & 011 == 000)", [&]() { - const bvec x = bvec_const((char)0); - const bvec y = bvec_const((char)3); - const bvec expected = - bvec_const((char)0); // Is this expected, or should we check bdd structure? + const bvec x = bvec_const((char)0); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)0); const bvec res = bvec_and(x, y); @@ -114,10 +238,9 @@ go_bandit([]() { describe("bvec_or", []() { describe("constants", []() { it("computes 5 | 3 == 7 (101 | 011 == 111)", [&]() { - const bvec x = bvec_const((char)5); - const bvec y = bvec_const((char)3); - const bvec expected = - bvec_const((char)7); // Is this expected, or should we check bdd structure? + const bvec x = bvec_const((char)5); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)7); const bvec res = bvec_or(x, y); @@ -125,10 +248,9 @@ go_bandit([]() { }); it("computes 0 | 3 == 3 (000 | 011 == 011)", [&]() { - const bvec x = bvec_const((char)0); - const bvec y = bvec_const((char)3); - const bvec expected = - bvec_const((char)3); // Is this expected, or should we check bdd structure? + const bvec x = bvec_const((char)0); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)3); const bvec res = bvec_or(x, y); @@ -140,10 +262,9 @@ go_bandit([]() { describe("bvec_xor", []() { describe("constants", []() { it("computes 5 ^ 3 == 6 (101 ^ 011 == 110)", [&]() { - const bvec x = bvec_const((char)5); - const bvec y = bvec_const((char)3); - const bvec expected = - bvec_const((char)6); // Is this expected, or should we check bdd structure? + const bvec x = bvec_const((char)5); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)6); const bvec res = bvec_xor(x, y); @@ -151,10 +272,9 @@ go_bandit([]() { }); it("computes 0 ^ 3 == 3 (000 ^ 011 == 011)", [&]() { - const bvec x = bvec_const((char)0); - const bvec y = bvec_const((char)3); - const bvec expected = - bvec_const((char)3); // Is this expected, or should we check bdd structure? + const bvec x = bvec_const((char)0); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)3); const bvec res = bvec_xor(x, y); @@ -162,10 +282,9 @@ go_bandit([]() { }); it("computes 255 ^ 3 == 252 (11111111 ^ 00000011 == 11111100)", [&]() { - const bvec x = bvec_const((char)255); - const bvec y = bvec_const((char)3); - const bvec expected = - bvec_const((char)252); // Is this expected, or should we check bdd structure? + const bvec x = bvec_const((char)255); + const bvec y = bvec_const((char)3); + const bvec expected = bvec_const((char)252); const bvec res = bvec_xor(x, y); @@ -177,9 +296,8 @@ go_bandit([]() { describe("bvec_not", []() { describe("constants", []() { it("computes ~3 == 252 for bitlength 8 (~00000011 == 11111100)", [&]() { - const bvec x = bvec_const((char)3); - const bvec expected = - bvec_const((u_char)252); // Is this expected, or should we check bdd structure? + const bvec x = bvec_const((char)3); + const bvec expected = bvec_const((u_char)252); const bvec res = bvec_not(x); @@ -189,8 +307,7 @@ go_bandit([]() { it("computes ~3 == (65535 - 3) for bitlength 16 (~0000000000000011 == 1111111111111100)", [&]() { const bvec x = bvec_const((short)3); - const bvec expected = bvec_const( - (short)(USHRT_MAX - 3)); // Is this expected, or should we check bdd structure? + const bvec expected = bvec_const((short)(USHRT_MAX - 3)); const bvec res = bvec_not(x); @@ -199,71 +316,6 @@ go_bandit([]() { }); }); - describe("bvec_equal", []() { - it("compares 101 == 101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); - }); - - it("compares 0101 == 101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true(), bdd_false() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); - }); - - it("compares 101 == 0101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_false() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); - }); - - it("compares 101 != 1101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); - }); - - it("compares 1101 != 101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); - }); - - it("compares 1101 != 1110", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; - std::vector raw2 = { bdd_false(), bdd_true(), bdd_true(), bdd_true() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); - }); - - it("compares 1100 != 1110", [&]() { - std::vector raw1 = { bdd_false(), bdd_false(), bdd_true(), bdd_true() }; - std::vector raw2 = { bdd_false(), bdd_true(), bdd_true(), bdd_true() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); - }); - - it("compares 1x0 == 1x0", [&]() { - std::vector raw1 = { bdd_false(), bdd_ithvar(42), bdd_true() }; - std::vector raw2 = { bdd_false(), bdd_ithvar(42), bdd_true() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); - }); - - it("compares 1x0 != 1y0", [&]() { - std::vector raw1 = { bdd_false(), bdd_ithvar(42), bdd_true() }; - std::vector raw2 = { bdd_false(), bdd_ithvar(11), bdd_true() }; - - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); - }); - }); - describe("bvec_add", []() { it("computes bvec[8](5) + bvec[8](3)", [&]() { bvec a = bvec_const((char)5); From a9777c640ff086b772e5465807a070adf08b0607 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 18:44:36 +0200 Subject: [PATCH 28/35] Fix missing/incorrect import of type traits --- src/adiar/bdd.h | 2 +- src/adiar/zdd.h | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) 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/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 From d43008ffc8acfa325d0fab7ea64a8e3684cb5225 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 17:46:50 +0200 Subject: [PATCH 29/35] Change (semantics) default value for bit length While the other thing was cool, we have multiple issues: - It seems more likely, that the end user wants to do a `bvec x = 42` than to specify the bit length as `bvec x(32)`. If anything, we should investigate whether one can move the `bitlen` into a template parameter. - By changing the above, we have an implicit conversion of constants to bit vectors. This removes the need to have `template ` overloads for each operator. - To make this not have any unforseen consequences, the bit length derived is as conservative as possible, i.e. it is only the number of bits needed to represent the number. Alternatively, we could have set the bit length to its default size which is used in other operations. Yet, if you do so then `x + 42` where `x` is an 8-bit integer would suddenly be extended to 64 by mistake. - To make sure that the default is both 0 and makes all operations have no side-effects, its length is also 0. --- src/adiar/bvec.cpp | 117 ++++-- src/adiar/bvec.h | 149 ++++---- tests/adiar/bvec.test.cpp | 727 ++++++++++++++++++++++++++------------ 3 files changed, 655 insertions(+), 338 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 308da44de..66de007bd 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -8,12 +8,34 @@ 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(size_t bitlen) + bvec::bvec() : _bits(0) - , _bitlen(bitlen) + , _bitlen(bvec::variadic_bitlen) {} bvec::bvec(const bvec& fs) @@ -26,25 +48,41 @@ namespace adiar , _bitlen(fs._bitlen) {} - bvec::bvec(const std::vector& bits, size_t 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(size_t bitlen, const bdd& f) + : _bits(bitlen, f) + , _bitlen(bitlen) + {} + + 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, size_t 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); } - bvec::bvec(const size_t bitlen, const bdd& f) - : _bits(bitlen, f) - , _bitlen(bitlen) - {} - const bdd& bvec::at(size_t index) const { @@ -99,8 +137,13 @@ namespace adiar bvec::truncate(size_t bitlen) { this->_bitlen = bitlen; - // Truncates to bitlen and removes any prefix of false - while (this->_bitlen < this->_bits.size()) { this->_bits.pop_back(); } + + 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(); } } @@ -134,32 +177,40 @@ namespace adiar // Constructors bvec - bvec_false(size_t bitlen = bvec::MAX_BITLEN) + bvec_false(size_t bitlen) + { + return bvec(bitlen, std::vector(0, bdd_false())); + } + + bvec + bvec_true(size_t bits) { - return bvec(std::vector(0, bdd_false()), bitlen); + return bvec_true(bvec::variadic_bitlen, bits); } bvec - bvec_true(size_t bitlen = bvec::MAX_BITLEN) + bvec_true(size_t bitlen, size_t bits) { - return bvec(std::vector(bitlen, bdd_true()), bitlen); + return bvec(bitlen, + std::vector(bitlen == bvec::variadic_bitlen ? bits : std::min(bitlen, bits), + bdd_true())); } bvec - bvec_const(size_t value, size_t bitlen) + bvec_const(size_t bitlen, size_t value) { - size_t max = std::ceil(std::log2(value)) + 1; - size_t msb = std::min(value != 0 ? max : 0, bitlen); std::vector res; - res.reserve(msb); - // Should be able to compute the most significant bit position and stop after that - for (size_t i = 0; i < msb; i++) { - res.push_back(value & 1 ? bdd_true() : bdd_false()); + res.reserve(msb(value)); - value >>= 1; - } + for (; value != 0; value >>= 1) { res.push_back(value & 1 ? bdd_true() : bdd_false()); } + + return bvec(bitlen, res); + } - return bvec(res, bitlen); + bvec + bvec_const(size_t value) + { + return bvec_const(bvec::variadic_bitlen, value); } ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -171,6 +222,7 @@ namespace adiar _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); @@ -180,7 +232,7 @@ namespace adiar } } - return bvec(res, bitlen); + return bvec(bitlen, res); } template @@ -188,7 +240,7 @@ namespace adiar _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 = std::max(x.bitlen(), y.bitlen()); + const size_t bitlen = join_bitlen(x, y); return _bvec_bitwise_op(size, bitlen, op); } @@ -214,7 +266,8 @@ namespace adiar bvec bvec_not(const bvec& x) { - return _bvec_bitwise_op(x.bitlen(), x.bitlen(), [&](size_t i) { return bdd_not(x.at(i)); }); + return _bvec_bitwise_op( + std::max(x.bitlen(), x.size()), x.bitlen(), [&](size_t i) { return ~x.at(i); }); } ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -223,8 +276,8 @@ namespace adiar bvec bvec_add(const bvec& x, const bvec& y) { - const size_t bitlen = std::max(x.bitlen(), y.bitlen()); const size_t size = std::max(x.size(), y.size()) + 1; + const size_t bitlen = join_bitlen(x, y); bdd carry = bdd_false(); @@ -243,7 +296,7 @@ namespace adiar // This assumes that the vector constructor truncates size above bitlen and false prefix. res.push_back(carry); - return bvec(res, bitlen); + return bvec(bitlen, res); } bvec @@ -269,12 +322,12 @@ namespace adiar // This assumes that the vector constructor truncates size above bitlen and false prefix. res.push_back(carry); - return bvec(res, bitlen); + return bvec(bitlen, res); } // Helper bvec - bvec_truncate(const bvec& x, const size_t bitlen) + bvec_truncate(size_t bitlen, const bvec& x) { bvec y = x; y.truncate(bitlen); diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 8367c9f76..867c729e0 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -30,7 +30,16 @@ namespace adiar class bvec { public: - static constexpr size_t MAX_BITLEN = 128; + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \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 @@ -40,14 +49,34 @@ namespace adiar /// \brief The total number of bits, including the only-false suffix. size_t _bitlen; - /// \brief The default BDD to be returned if asking + /// \brief The default BDD to be returned if asking out of bounds. const bdd default_value = bdd(); public: //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Zero-valued bvec of a given bitlength. + /// \brief The variable-sized zero-valued bitvector. + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(); + + //////////////////////////////////////////////////////////////////////////////////////////////// + bvec(const bvec& fs); + //////////////////////////////////////////////////////////////////////////////////////////////// - bvec(size_t bitlen = MAX_BITLEN); + 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 bitvector with initial value `f` for all `bitlen` many bits. @@ -55,24 +84,28 @@ namespace adiar bvec(size_t bitlen, const bdd& f); //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Copy constructor + /// \brief Construct a variable-size from a raw vector (least to most significant bit) and with + /// a variadic number of bits. //////////////////////////////////////////////////////////////////////////////////////////////// - bvec(const bvec& fs); + bvec(const std::vector& bits); //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Move constructor for right-hand values + /// \brief Construct a fixed-size bitvector from a raw vector (least to most significant bit) + /// and a certain bit length. //////////////////////////////////////////////////////////////////////////////////////////////// - bvec(bvec&& fs); + bvec(size_t bitlen, const std::vector& bits); //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Conversion constructor from a raw bit-vector + /// \brief Construct variable-size bitvector from a movable raw vector (least to most + /// significant bit) and with a variadic number of bits. //////////////////////////////////////////////////////////////////////////////////////////////// - bvec(const std::vector& bits, size_t bitlen = MAX_BITLEN); + bvec(std::vector&& bits); //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Conversion constructor from a raw bit-vector for right-hand values + /// \brief Construct a fixed-size bitvector from a movable raw vector (least to most significant + /// bit) and a certain bit length. //////////////////////////////////////////////////////////////////////////////////////////////// - bvec(std::vector&& bits, size_t bitlen = MAX_BITLEN); + bvec(size_t bitlen, std::vector&& bits); //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Width of the symbolic bit vector. @@ -93,7 +126,7 @@ namespace adiar } //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The BDD at a certain position. + /// \brief The BDD at a certain bit position. //////////////////////////////////////////////////////////////////////////////////////////////// const bdd& at(size_t index) const; @@ -132,7 +165,7 @@ namespace adiar /// \brief Changes the width of the vector, discarding bits if decreasing in size. //////////////////////////////////////////////////////////////////////////////////////////////// void - truncate(size_t bitlen); + truncate(size_t bitlen = bvec::variadic_bitlen); }; /// \cond @@ -156,44 +189,42 @@ namespace adiar //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The all-zero bitvector. /// - /// \param bitlen The width of the bit-vector. + /// \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_false(size_t bitlen = bvec::variadic_bitlen); //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief The all-one bitvector. - /// - /// \param bitlen The width of the bit-vector, i.e. the number of 1 bits. + /// \brief The variable-sized bitvector with the first `bits` set to 1. //////////////////////////////////////////////////////////////////////////////////////////////// bvec - bvec_true(size_t bitlen); + bvec_true(size_t bits); //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Create a bitvector which contains the given (non-negative) integer. - /// - /// \param value The integer to be represented. + /// \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 bitlen The width of the bit-vector, possibly truncating `value` if there is not enough - /// space for it. + /// \param value The integer to be represented. //////////////////////////////////////////////////////////////////////////////////////////////// bvec - bvec_const(size_t value, size_t bitlen); + bvec_const(size_t value); //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Create a bitvector which contains the given (non-negative) integer. + /// \brief Create a fixed-size bitvector which contains the given (non-negative) integer. /// - /// \details This automatically derives the `bitlen` based on the number of bits needed for the - /// given type. That is, the result is a 32-bit bitvector if using an `int`. + /// \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. //////////////////////////////////////////////////////////////////////////////////////////////// - template bvec - bvec_const(Integer i) - { - return bvec_const(i, 8 * sizeof(Integer)); - } + bvec_const(size_t bitlen, size_t value); /// \} /// \} @@ -235,6 +266,8 @@ namespace adiar /// /// \{ + // TODO: Add optional `bitlen` as a first argument. + //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Bitwise conjunction of two bitvectors, upcasting the `bitlen` if needed. //////////////////////////////////////////////////////////////////////////////////////////////// @@ -273,36 +306,14 @@ namespace adiar /// /// \{ + // 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); - //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Arithmetic addition of a symbolic bit-vector with a constant. - /// - /// \details The bitlength of the constant is derived based on its type. - //////////////////////////////////////////////////////////////////////////////////////////////// - template - bvec - bvec_add(const bvec& x, Integer i) - { - return bvec_add(x, bvec_const(i)); - } - - //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Arithmetic addition of a symbolic bit-vector with a constant. - /// - /// \details The bitlength of the constant is derived based on its type. - //////////////////////////////////////////////////////////////////////////////////////////////// - template - bvec - bvec_add(Integer i, const bvec& x) - { - return bvec_add(x, i); - } - ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see bvec_add ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -312,26 +323,6 @@ namespace adiar return bvec_add(x, y); } - ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \see bvec_add - ////////////////////////////////////////////////////////////////////////////////////////////////// - template - bvec - operator+(const bvec& x, Integer i) - { - return bvec_add(x, i); - } - - ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \see bvec_add - ////////////////////////////////////////////////////////////////////////////////////////////////// - template - bvec - operator+(Integer i, const bvec& x) - { - return bvec_add(i, x); - } - //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Arithmetic subtraction of two symbolic bit-vectors. /// @@ -355,7 +346,7 @@ namespace adiar /// \{ bvec - bvec_truncate(const bvec& x, const size_t bitlen); + bvec_truncate(size_t bitlen, const bvec& x); /// \} /// \} diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index 7a383a549..f57f9bf4c 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -1,116 +1,269 @@ #include "../test.h" #include + go_bandit([]() { describe("adiar/bvec.h", []() { describe("bvec_false()", []() { - it("has 16 bits when asked", - [&]() { AssertThat(bvec_false(16).bitlen(), Is().EqualTo(16u)); }); + 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 bits set to false", [&]() { + it("has all its bits set to false", [&]() { const bvec x = bvec_false(8); - AssertThat(x.at(0), Is().False()); - AssertThat(x.at(1), Is().False()); - AssertThat(x.at(2), Is().False()); - AssertThat(x.at(3), Is().False()); - AssertThat(x.at(4), Is().False()); - AssertThat(x.at(5), Is().False()); - AssertThat(x.at(6), Is().False()); - AssertThat(x.at(7), Is().False()); + for (size_t i = 0; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_false())); } }); }); describe("bvec_true()", []() { - it("has 32 bits when asked", - [&]() { AssertThat(bvec_true(32).bitlen(), Is().EqualTo(32u)); }); - - it("has all bits set to 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())); } + }); - AssertThat(x.at(0), Is().True()); - AssertThat(x.at(1), Is().True()); - AssertThat(x.at(2), Is().True()); - AssertThat(x.at(3), Is().True()); - AssertThat(x.at(4), Is().True()); - AssertThat(x.at(5), Is().True()); - AssertThat(x.at(6), Is().True()); - AssertThat(x.at(7), Is().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("has out-of-bound bit set to false", - [&]() { AssertThat(bvec_true(8).at(8), Is().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", []() { - describe("bitlength inference", []() { - it("has 32 bitlen 0 size when constructed with 0", [&]() { - const bvec x = bvec_const(0); + 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(32u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); }); - it("has 8 size and bitlen when constructed with max unsigned char", [&]() { - const bvec x = bvec_const((unsigned char)255); - AssertThat(x.size(), Is().EqualTo(8u)); - AssertThat(x.bitlen(), Is().EqualTo(8u)); - }); + it("derives 1 to be (1) with 1 bit required", [&]() { + const bvec x(1); - it("has 8 size and bitlen when constructed with overflowing char", [&]() { - const bvec x = bvec_const((char)253); - AssertThat(x.size(), Is().EqualTo(8u)); - AssertThat(x.bitlen(), Is().EqualTo(8u)); + 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("has 8 size and bitlen when constructed with negative char", [&]() { - const bvec x = bvec_const((char)-52); - AssertThat(x.size(), Is().EqualTo(8u)); - AssertThat(x.bitlen(), Is().EqualTo(8u)); + 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("has 7 size and 8 bitlen when constructed with max signed char", [&]() { - const bvec x = bvec_const((char)127); - AssertThat(x.size(), Is().EqualTo(7u)); - AssertThat(x.bitlen(), Is().EqualTo(8u)); + 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())); }); - }); - describe("bit encoding", []() { - it("derives 0 ()", [&]() { - const bvec x = bvec_const(0); + it("derives 42 to be (010101) with 6 bits required", [&]() { + const bvec x(42); - // Check that all bits are zero - for (size_t i = 0; i < x.bitlen(); i++) { - AssertThat(x.at(i), Is().EqualTo(bdd_false())); - } + 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())); }); + }); - it("derives 1 (1)", [&]() { - const bvec x = bvec_const(1); + describe("bvec::bvec(bitlen, value)", []() { + it("derives 0 to be () with 7 number of bits", [&]() { + const bvec x(7, 0); - // Check that the first bit is set - AssertThat(x.at(0), Is().EqualTo(bdd_true())); + AssertThat(x.size(), Is().EqualTo(0u)); + AssertThat(x.bitlen(), Is().EqualTo(7u)); - // Check that all bits are zero - for (size_t i = 1; i < x.bitlen(); i++) { + // 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 2 (01)", [&]() { - const bvec x = bvec_const(1); + 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 the first bit is set + // Check that encoding is 1 AssertThat(x.at(0), Is().EqualTo(bdd_true())); - // Check that all bits are zero + // 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 (101010)", [&]() { - const bvec x = bvec_const(42); + 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())); @@ -126,97 +279,179 @@ go_bandit([]() { } }); - it("derives -1 (111...1)", [&]() { - // - const bvec x = bvec_const(-1); + 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)); - for (size_t i = 0; i < x.bitlen(); i++) { AssertThat(x.at(i), Is().EqualTo(bdd_true())); } + 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("derives -2^32 (000..01)", [&]() { - // - const bvec x = bvec_const(INT32_MIN); + it("copies over bits (1011)", [&]() { + const bvec x({ bdd_true(), bdd_false(), bdd_true(), bdd_true() }); - for (size_t i = 0; i < x.bitlen() - 1; i++) { - AssertThat(x.at(i), Is().EqualTo(bdd_false())); - } + AssertThat(x.size(), Is().EqualTo(4u)); + AssertThat(x.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); - AssertThat(x.at(x.bitlen() - 1), Is().EqualTo(bdd_true())); + 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_equal", []() { it("compares 101 == 101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + const bvec x({ bdd_true(), bdd_false(), bdd_true() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true() }); - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); + AssertThat(bvec_equal(x, y), Is().True()); }); it("compares 0101 == 101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true(), bdd_false() }; + const bvec x({ bdd_true(), bdd_false(), bdd_true() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true(), bdd_false() }); - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); + AssertThat(bvec_equal(x, y), Is().True()); }); it("compares 101 == 0101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_false() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + const bvec x({ bdd_true(), bdd_false(), bdd_true(), bdd_false() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true() }); - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); + AssertThat(bvec_equal(x, y), Is().True()); }); it("compares 101 != 1101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true() }; + const bvec x({ bdd_true(), bdd_false(), bdd_true(), bdd_true() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true() }); - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); + AssertThat(bvec_equal(x, y), Is().False()); }); it("compares 1101 != 101", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true() }; - std::vector raw2 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; + const bvec x({ bdd_true(), bdd_false(), bdd_true() }); + const bvec y({ bdd_true(), bdd_false(), bdd_true(), bdd_true() }); - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); + AssertThat(bvec_equal(x, y), Is().False()); }); it("compares 1101 != 1110", [&]() { - std::vector raw1 = { bdd_true(), bdd_false(), bdd_true(), bdd_true() }; - std::vector raw2 = { bdd_false(), bdd_true(), bdd_true(), bdd_true() }; + 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(bvec(raw1), bvec(raw2)), Is().False()); + AssertThat(bvec_equal(x, y), Is().False()); }); it("compares 1100 != 1110", [&]() { - std::vector raw1 = { bdd_false(), bdd_false(), bdd_true(), bdd_true() }; - std::vector raw2 = { bdd_false(), bdd_true(), bdd_true(), bdd_true() }; + 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(bvec(raw1), bvec(raw2)), Is().False()); + AssertThat(bvec_equal(x, y), Is().False()); }); it("compares 1x0 == 1x0", [&]() { - std::vector raw1 = { bdd_false(), bdd_ithvar(42), bdd_true() }; - std::vector raw2 = { bdd_false(), bdd_ithvar(42), bdd_true() }; + const bvec x({ bdd_false(), bdd_ithvar(42), bdd_true() }); + const bvec y({ bdd_false(), bdd_ithvar(42), bdd_true() }); - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().True()); + AssertThat(bvec_equal(x, y), Is().True()); }); it("compares 1x0 != 1y0", [&]() { - std::vector raw1 = { bdd_false(), bdd_ithvar(42), bdd_true() }; - std::vector raw2 = { bdd_false(), bdd_ithvar(11), bdd_true() }; + const bvec x({ bdd_false(), bdd_ithvar(42), bdd_true() }); + const bvec y({ bdd_false(), bdd_ithvar(11), bdd_true() }); - AssertThat(bvec_equal(bvec(raw1), bvec(raw2)), Is().False()); + 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((char)5); - const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)1); + 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); @@ -224,9 +459,9 @@ go_bandit([]() { }); it("computes 0 & 3 == 0 (000 & 011 == 000)", [&]() { - const bvec x = bvec_const((char)0); - const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)0); + 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); @@ -238,9 +473,9 @@ go_bandit([]() { describe("bvec_or", []() { describe("constants", []() { it("computes 5 | 3 == 7 (101 | 011 == 111)", [&]() { - const bvec x = bvec_const((char)5); - const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)7); + 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); @@ -248,9 +483,9 @@ go_bandit([]() { }); it("computes 0 | 3 == 3 (000 | 011 == 011)", [&]() { - const bvec x = bvec_const((char)0); - const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)3); + 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); @@ -262,9 +497,9 @@ go_bandit([]() { describe("bvec_xor", []() { describe("constants", []() { it("computes 5 ^ 3 == 6 (101 ^ 011 == 110)", [&]() { - const bvec x = bvec_const((char)5); - const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)6); + 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); @@ -272,9 +507,9 @@ go_bandit([]() { }); it("computes 0 ^ 3 == 3 (000 ^ 011 == 011)", [&]() { - const bvec x = bvec_const((char)0); - const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)3); + 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); @@ -282,9 +517,9 @@ go_bandit([]() { }); it("computes 255 ^ 3 == 252 (11111111 ^ 00000011 == 11111100)", [&]() { - const bvec x = bvec_const((char)255); - const bvec y = bvec_const((char)3); - const bvec expected = bvec_const((char)252); + 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); @@ -296,8 +531,8 @@ go_bandit([]() { describe("bvec_not", []() { describe("constants", []() { it("computes ~3 == 252 for bitlength 8 (~00000011 == 11111100)", [&]() { - const bvec x = bvec_const((char)3); - const bvec expected = bvec_const((u_char)252); + const bvec x = bvec_const(8, 3); + const bvec expected = bvec_const(8, 252); const bvec res = bvec_not(x); @@ -306,157 +541,195 @@ go_bandit([]() { it("computes ~3 == (65535 - 3) for bitlength 16 (~0000000000000011 == 1111111111111100)", [&]() { - const bvec x = bvec_const((short)3); - const bvec expected = bvec_const((short)(USHRT_MAX - 3)); + 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)", [&]() { - bvec a = bvec_const((char)5); - bvec b = bvec_const((char)3); - // 00000101 + - // 00000011 = - // 00001000 - std::vector raw_expected = { bdd_false(), bdd_false(), bdd_false(), bdd_true() }; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a, b); + 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[32](5) + bvec[8](3)", [&]() { - bvec a = bvec_const((int)5); - bvec b = bvec_const((char)3); - // 00000000000000000000000000000101 + - // 00000011 = - // 00000000000000000000000000001000 - std::vector raw_expected = { bdd_false(), bdd_false(), bdd_false(), bdd_true() }; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a, b); + 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("computes bvec[32](0) + bvec[8](3)", [&]() { - bvec a = bvec_const((int)0); - bvec b = bvec_const((char)3); - // 00000000000000000000000000000000 + - // 00000011 = - // 00000000000000000000000000000011 - std::vector raw_expected = { bdd_true(), bdd_true() }; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a, b); + 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("computes bvec[8](0) + bvec[32](3)", [&]() { - bvec a = bvec_const((char)0); - bvec b = bvec_const((int)3); - // 00000000 + - // 00000000000000000000000000000011 = - // 00000000000000000000000000000011 - std::vector raw_expected = { bdd_true(), bdd_true() }; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a, b); + 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("computes bvec[8](255) + bvec[8](1)", [&]() { - bvec a = bvec_const((char)255); - bvec b = bvec_const((char)1); - // 11111111 + - // 00000001 = - // 00000000 - std::vector raw_expected = {}; - bvec expected = bvec(raw_expected); - bvec res = bvec_add(a, b); + 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(0u)); + AssertThat(res.size(), Is().EqualTo(5u)); }); - it("computes bvec[8](255) + bvec[8](1)", [&]() { - bvec a = bvec_const((char)255); - bvec b = bvec_const((char)1); - // 11111111 + - // 00000001 = - // 00000000 - std::vector raw_expected = {}; - bvec expected = bvec(raw_expected); - bvec res = a + b; + 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(8u)); - AssertThat(res.size(), Is().EqualTo(0u)); + AssertThat(res.bitlen(), Is().EqualTo(16u)); + AssertThat(res.size(), Is().EqualTo(3u)); }); - it("computes bvec[8](42) + char(3)", [&]() { - bvec a = bvec_const((char)42); - char b = 3; - // 00101010 + - // 00000011 = - // 00101101 - bvec expected = bvec_const(45); - bvec res = a + b; + 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(8u)); - AssertThat(res.size(), Is().EqualTo(6u)); + AssertThat(res.bitlen(), Is().EqualTo(bvec::variadic_bitlen)); + AssertThat(res.size(), Is().EqualTo(10u)); }); - it("computes int(17) + bvec[8](42)", [&]() { - int a = 17; - bvec b = bvec_const((char)42); - // 00010001 + - // 00101010 = - // 00111011 - bvec expected = bvec_const(59); - bvec res = a + b; + 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(32u)); - AssertThat(res.size(), Is().EqualTo(6u)); + 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)", [&]() { - bvec x = bvec_const((char)42); - bvec y = bvec_const((char)3); + const bvec x = bvec_const(8, 42); + const bvec y = bvec_const(8, 3); - bvec expected = bvec_const((char)39); - bvec res = bvec_sub(x, y); + 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)", [&]() { - bvec x = bvec_const((char)140); - bvec y = bvec_const((char)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](4) - bvec[8](7)", [&]() { + const bvec x = bvec_const(8, 4); + const bvec y = bvec_const(8, 7); - bvec expected = bvec_const((char)136); - bvec res = bvec_sub(x, y); + 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("compute bvec[8](4) - bvec[32](7000)", [&]() { - bvec x = bvec_const((char)4); - bvec y = bvec_const((int)7000); + it("underflows bvec[16](21) - bvec[8](42)", [&]() { + const bvec x = bvec_const(16, 21); + const bvec y = bvec_const(8, 42); - bvec expected = bvec_const((int)-6996); - bvec res = bvec_sub(x, y); + const bvec expected = bvec_const(16, -21); + const bvec res = bvec_sub(x, y); AssertThat(res, Is().EqualTo(expected)); AssertThat(res.bitlen(), Is().EqualTo(32u)); AssertThat(res.size(), Is().EqualTo(32u)); @@ -465,31 +738,31 @@ go_bandit([]() { describe("bvec_truncate", []() { it("truncates to bitlen", [&]() { - bvec x = bvec_true(32); + const bvec x = bvec_true(32, 32); - bvec expected = bvec_true(8); - bvec res = bvec_truncate(x, 8); + 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", [&]() { - bvec x = bvec_true(4); + const bvec x = bvec_true(4, 4); AssertThat(x.bitlen(), Is().EqualTo(4u)); - bvec expected = bvec_true(4); - bvec res = bvec_truncate(x, 8); + 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", [&]() { - bvec x = bvec_const(18); + const bvec x = bvec_const(18); - bvec expected = bvec_const(2); - bvec res = bvec_truncate(x, 4); + 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)); From a2588b96bd8d318c21bddfad45cc2e6ae7b1eefe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 19:07:16 +0200 Subject: [PATCH 30/35] Make underflow in 'bvec_sub' more well behaved --- src/adiar/bvec.cpp | 2 +- tests/adiar/bvec.test.cpp | 26 ++++++++++++++++++++++++-- 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 66de007bd..9985baea7 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -303,7 +303,7 @@ namespace adiar bvec_sub(const bvec& x, const bvec& y) { const size_t bitlen = std::max(x.bitlen(), y.bitlen()); - const size_t size = std::max(x.size(), bvec_not(y).size()) + 1; + const size_t size = bitlen; bdd carry = bdd_true(); diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index f57f9bf4c..ea9ac4ade 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -713,6 +713,17 @@ go_bandit([]() { 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); @@ -731,8 +742,19 @@ go_bandit([]() { const bvec expected = bvec_const(16, -21); const bvec res = bvec_sub(x, y); AssertThat(res, Is().EqualTo(expected)); - AssertThat(res.bitlen(), Is().EqualTo(32u)); - AssertThat(res.size(), Is().EqualTo(32u)); + 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)); }); }); From e300c58975e143f0e752cca631daed55cd6a8a31 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 18:46:06 +0200 Subject: [PATCH 31/35] Add iterator-based construction of bit vectors --- src/adiar/bvec.h | 41 ++++++++++++++++++++++++++++++ tests/adiar/bvec.test.cpp | 53 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 94 insertions(+) diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 867c729e0..608876ffe 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -17,6 +17,7 @@ #include #include +#include namespace adiar { @@ -107,6 +108,24 @@ namespace adiar //////////////////////////////////////////////////////////////////////////////////////////////// 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. //////////////////////////////////////////////////////////////////////////////////////////////// @@ -226,6 +245,28 @@ namespace adiar 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)); + } + /// \} /// \} ////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index ea9ac4ade..3bd5e0396 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -379,6 +379,59 @@ go_bandit([]() { 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", []() { From b2e5532f9707cd11fae4619e05b8e8324444902e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 20:41:01 +0200 Subject: [PATCH 32/35] Remove unused constructor with no well-defined use case --- src/adiar/bvec.cpp | 5 ----- src/adiar/bvec.h | 5 ----- 2 files changed, 10 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 9985baea7..1cc30a88e 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -56,11 +56,6 @@ namespace adiar : bvec(bvec_const(bitlen, value)) {} - bvec::bvec(size_t bitlen, const bdd& f) - : _bits(bitlen, f) - , _bitlen(bitlen) - {} - bvec::bvec(const std::vector& bits) : bvec(bvec::variadic_bitlen, bits) {} diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index 608876ffe..ab28bf59d 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -79,11 +79,6 @@ namespace adiar //////////////////////////////////////////////////////////////////////////////////////////////// bvec(size_t bitlen, size_t value); - //////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Construct a bitvector with initial value `f` for all `bitlen` many bits. - //////////////////////////////////////////////////////////////////////////////////////////////// - bvec(size_t bitlen, const bdd& f); - //////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Construct a variable-size from a raw vector (least to most significant bit) and with /// a variadic number of bits. From 204a2369f481a99a4b08f594ccd5a13b58105186 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 21:27:31 +0200 Subject: [PATCH 33/35] Merge logic for 'bvec_add' and 'bvec_sub' This also fixes the issue that 'bvec_sub' does not properly deal with variable length bit vectors. --- src/adiar/bvec.cpp | 57 +++++++++++++++++---------------------- tests/adiar/bvec.test.cpp | 44 ++++++++++++++++++++++++++++++ 2 files changed, 69 insertions(+), 32 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 1cc30a88e..2894aaec6 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -268,56 +268,49 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// // Arithmetic operations + template bvec - bvec_add(const bvec& x, const bvec& y) + __bvec_add(const bvec& x, const bvec& y) { - const size_t size = std::max(x.size(), y.size()) + 1; 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_false(); + bdd carry = bdd_const(Subtract); std::vector res; res.reserve(size); for (size_t i = 0; i < size; ++i) { - const bdd xors = bdd_xor(bdd_xor(x.at(i), y.at(i)), carry); - res.push_back(xors); - if (i + 1 <= bitlen) { - adiar_assert(i != size - 1 || bitlen >= size, "is not last bit with overflow"); - carry = bdd_or(bdd_and(carry, bdd_or(x.at(i), y.at(i))), bdd_and(x.at(i), y.at(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); } - // This assumes that the vector constructor truncates size above bitlen and false prefix. - res.push_back(carry); + 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_sub(const bvec& x, const bvec& y) + bvec_add(const bvec& x, const bvec& y) { - const size_t bitlen = std::max(x.bitlen(), y.bitlen()); - const size_t size = bitlen; - - bdd carry = bdd_true(); - - std::vector res; - res.reserve(size); - - for (size_t i = 0; i < size; ++i) { - const bdd xors = x.at(i) ^ ~y.at(i) ^ carry; - res.push_back(xors); - if (i + 1 <= bitlen) { - adiar_assert(i != size - 1 || bitlen >= size, "is not last bit with overflow"); - carry = (carry & (x.at(i) | ~y.at(i))) | (x.at(i) & ~y.at(i)); - } - } - - // This assumes that the vector constructor truncates size above bitlen and false prefix. - res.push_back(carry); + return __bvec_add(x, y); + } - return bvec(bitlen, res); + bvec + bvec_sub(const bvec& x, const bvec& y) + { + return __bvec_add(x, y); } // Helper diff --git a/tests/adiar/bvec.test.cpp b/tests/adiar/bvec.test.cpp index 3bd5e0396..996e702f8 100644 --- a/tests/adiar/bvec.test.cpp +++ b/tests/adiar/bvec.test.cpp @@ -809,6 +809,50 @@ go_bandit([]() { 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", []() { From 4c2adbb3497bfff6b2677f22a9c56ea7ba50d4ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 21:58:41 +0200 Subject: [PATCH 34/35] Fix 'bvec::default_value' member variable is missing leading '_' --- src/adiar/bvec.cpp | 2 +- src/adiar/bvec.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/adiar/bvec.cpp b/src/adiar/bvec.cpp index 2894aaec6..edb451e8e 100644 --- a/src/adiar/bvec.cpp +++ b/src/adiar/bvec.cpp @@ -81,7 +81,7 @@ namespace adiar const bdd& bvec::at(size_t index) const { - if (_bits.size() <= index) { return this->default_value; } + if (_bits.size() <= index) { return this->_default_value; } return _bits.at(index); } diff --git a/src/adiar/bvec.h b/src/adiar/bvec.h index ab28bf59d..774fa22b4 100644 --- a/src/adiar/bvec.h +++ b/src/adiar/bvec.h @@ -51,7 +51,7 @@ namespace adiar size_t _bitlen; /// \brief The default BDD to be returned if asking out of bounds. - const bdd default_value = bdd(); + const bdd _default_value = bdd(); public: //////////////////////////////////////////////////////////////////////////////////////////////// From db3135e200d35c82b45fd30c241464fcbd0152fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 24 Jun 2026 22:29:13 +0200 Subject: [PATCH 35/35] Add bvec tests to the full test suite --- tests/all.cpp | 4 ++++ 1 file changed, 4 insertions(+) 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([]() {