From 2097f51492699643b1819d189e237fb27b490cc3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 14:12:45 +0200 Subject: [PATCH 01/10] Clean up BDD operation overloads and its tests --- src/adiar/bdd/bdd.cpp | 12 +- test/adiar/bdd/test_bdd.cpp | 253 +++++++++++++++++++++++------------- 2 files changed, 168 insertions(+), 97 deletions(-) diff --git a/src/adiar/bdd/bdd.cpp b/src/adiar/bdd/bdd.cpp index 41b471b90..8feecb4ce 100644 --- a/src/adiar/bdd/bdd.cpp +++ b/src/adiar/bdd/bdd.cpp @@ -61,7 +61,7 @@ namespace adiar return ~bdd(std::move(in)); } -#define __bdd_oper(out_t, op) \ +#define __BDD_OPER(out_t, op) \ out_t operator op(__bdd&& lhs, __bdd&& rhs) \ { \ return bdd(std::move(lhs)) op bdd(std::move(rhs)); \ @@ -77,10 +77,14 @@ namespace adiar return bdd(std::move(lhs)) op rhs; \ } - __bdd_oper(__bdd, &) __bdd_oper(__bdd, |) __bdd_oper(__bdd, ^) __bdd_oper(bool, ==) - __bdd_oper(bool, !=) + __BDD_OPER(__bdd, &); + __BDD_OPER(__bdd, |); + __BDD_OPER(__bdd, ^); + __BDD_OPER(bool, ==); + __BDD_OPER(bool, !=); - bdd& bdd::operator=(const bdd & other) + bdd& + bdd::operator=(const bdd& other) { this->negate = other.negate; this->file = other.file; diff --git a/test/adiar/bdd/test_bdd.cpp b/test/adiar/bdd/test_bdd.cpp index 51fbbc8bf..0190626e4 100644 --- a/test/adiar/bdd/test_bdd.cpp +++ b/test/adiar/bdd/test_bdd.cpp @@ -5,8 +5,8 @@ go_bandit([]() { shared_levelized_file x0_nf; { - node_writer nw_0(x0_nf); - nw_0 << node(0, node::max_id, ptr_uint64(false), ptr_uint64(true)); + node_writer nw(x0_nf); + nw << node(0, node::max_id, ptr_uint64(false), ptr_uint64(true)); } bdd x0(x0_nf); @@ -14,8 +14,8 @@ go_bandit([]() { shared_levelized_file x1_nf; { - node_writer nw_1(x1_nf); - nw_1 << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)); + node_writer nw(x1_nf); + nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)); } bdd x1(x1_nf); @@ -23,30 +23,26 @@ go_bandit([]() { shared_levelized_file x0_and_x1_nf; { - node_writer nw_01(x0_and_x1_nf); - - nw_01 << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)); - - nw_01 << node(0, node::max_id, ptr_uint64(false), ptr_uint64(1, ptr_uint64::max_id)); + node_writer nw(x0_and_x1_nf); + nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)) + << node(0, node::max_id, ptr_uint64(false), ptr_uint64(1, ptr_uint64::max_id)); } bdd x0_and_x1(x0_and_x1_nf); bdd x0_nand_x1(x0_and_x1_nf, true); shared_levelized_file terminal_T_nf; - { - node_writer nw_T(terminal_T_nf); - nw_T << node(true); + node_writer nw(terminal_T_nf); + nw << node(true); } bdd terminal_T(terminal_T_nf); shared_levelized_file terminal_F_nf; - { - node_writer nw_F(terminal_F_nf); - nw_F << node(false); + node_writer nw(terminal_F_nf); + nw << node(false); } bdd terminal_F(terminal_F_nf); @@ -128,97 +124,168 @@ go_bandit([]() { AssertThat(t2.is_negated(), Is().False()); }); - describe("operators", [&]() { - it("should check terminal_F != terminal_T", - [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); }); + describe("operator overloading", [&]() { + describe("==, !=", [&]() { + it("checks F != T", [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); }); - it("should check terminal_F != ~terminal_F", - [&]() { AssertThat(terminal_F, Is().Not().EqualTo(~terminal_F)); }); + it("checks F != ~F", [&]() { AssertThat(terminal_F, Is().Not().EqualTo(~terminal_F)); }); - it("should check terminal_F == ~terminal_T", - [&]() { AssertThat(terminal_F, Is().EqualTo(~terminal_T)); }); + it("checks F != (x0 & x1)", + [&]() { AssertThat(terminal_F, Is().Not().EqualTo(x0_and_x1)); }); - it("should check ~(x0 & x1) != (x0 & x1)", - [&]() { AssertThat(x0_and_x1, Is().Not().EqualTo(x0_nand_x1)); }); + it("checks (x0 & x1) != T", + [&]() { AssertThat(x0_and_x1, Is().Not().EqualTo(terminal_T)); }); - shared_levelized_file x0_and_x1_nf2; + it("checks '(x0 & x1) != ~(x0 & x1)'", + [&]() { AssertThat(x0_and_x1, Is().Not().EqualTo(x0_nand_x1)); }); - { - node_writer nw_01(x0_and_x1_nf2); + it("checks (x0 & x1) matches itself", + [&]() { AssertThat(x0_and_x1, Is().EqualTo(x0_and_x1)); }); - nw_01 << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)); - - nw_01 << node(0, node::max_id, ptr_uint64(false), ptr_uint64(1, ptr_uint64::max_id)); - } - - it("should check (x0 & x1) == (x0 & x1)", [&]() { - bdd other(x0_and_x1_nf2); - AssertThat(x0_and_x1, Is().EqualTo(other)); + it("checks (x0 & x1) matches a copy", [&]() { + shared_levelized_file other_nf; + { + node_writer nw(other_nf); + nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)) + << node(0, node::max_id, ptr_uint64(false), ptr_uint64(1, ptr_uint64::max_id)); + } + const bdd other(other_nf); + AssertThat(x0_and_x1, Is().EqualTo(other)); + }); }); - it("should compute x0 & x1", [&]() { AssertThat(x0_and_x1 == (x0 & x1), Is().True()); }); - - it("should compute bdd& in x0 ?= x1", [&]() { - bdd out1 = x0; - out1 &= x1; - AssertThat(out1 == (x0 & x1), Is().True()); - AssertThat(out1 != (x0 & x1), Is().False()); - - bdd out2 = x0; - out2 |= x1; - AssertThat(out2 == (x0 | x1), Is().True()); - AssertThat(out2 != (x0 | x1), Is().False()); - AssertThat(out2 != (x0 & x1), Is().True()); - - bdd out3 = x0; - out3 ^= x1; - AssertThat(out3 == (x0 ^ x1), Is().True()); - AssertThat(out3 != (x0 ^ x1), Is().False()); - AssertThat(out3 != (x0 | x1), Is().True()); + describe("~, &, |, ^", [&]() { + it("negates 'T' into 'F'", [&]() { AssertThat(terminal_F, Is().EqualTo(~terminal_T)); }); + + it("negates '(x0 & x1)' into ~(x0 & x1)'", + [&]() { AssertThat(~x0_and_x1, Is().EqualTo(x0_nand_x1)); }); + + it("negates '~(x0 & x1)' into '(x0 & x1)'", + [&]() { AssertThat(~x0_and_x1, Is().EqualTo(x0_nand_x1)); }); + + it("computes 'x0 & x1'", [&]() { + const bdd f = x0 & x1; + AssertThat(f, Is().EqualTo(x0_and_x1)); + }); + + it("computes '~(~x0 | ~x1)'", [&]() { + const bdd f = ~(~x0 | ~x1); + AssertThat(f, Is().EqualTo(x0_and_x1)); + }); + + it("computes 'x0 ^ x1' to be '(~x0 & x1) | (x0 & ~x1)'", [&]() { + const bdd f = x0 ^ x1; + + const bdd g1 = ~x0 & x1; + const bdd g2 = x0 & ~x1; + const bdd g = g1 | g2; + + AssertThat(f, Is().EqualTo(g)); + }); + + it("negates 'x0 & x1' __bdd&& into '~(x0 & x1)", [&]() { + AssertThat(x0_nand_x1 == ~(x0 & x1), Is().True()); + AssertThat(x0_nand_x1 != ~(x0 & x1), Is().False()); + }); + + it("resolves 'x0 ^ x1' to be '(~x0 & x1) | (x0 & ~x1)'", [&]() { + const bdd f = x0 ^ x1; + const bdd g = (~x0 & x1) | (x0 & ~x1); + AssertThat(f, Is().EqualTo(g)); + }); + + it("accumulates with '&=(bdd&)' operator", [&]() { + bdd f = x0; + AssertThat(f == x0, Is().True()); + + f &= x1; + AssertThat(f == (x0 & x1), Is().True()); + + f &= terminal_F; + AssertThat(f == terminal_F, Is().True()); + }); + + it("accumulates with '&=(__bdd&&)' operator", [&]() { + bdd f = terminal_T; + f &= x0 & x1; + AssertThat((x0 & x1) == f, Is().True()); + }); + + it("accumulates with '|=(bdd&)' operator", [&]() { + bdd f = x0; + AssertThat(f == x0, Is().True()); + + f |= x1; + AssertThat(f == (x0 | x1), Is().True()); + + f |= terminal_T; + AssertThat(terminal_T == f, Is().True()); + }); + + it("accumulates with '|=(__bdd&&)' operator", [&]() { + bdd f = terminal_F; + f |= x0 & x1; + AssertThat(f == (x0 & x1), Is().True()); + }); + + it("accumulates with '^=(bdd&)' operator", [&]() { + bdd f = x0; + AssertThat(f == x0, Is().True()); + + f ^= x1; + AssertThat(f == (x0 ^ x1), Is().True()); + + f ^= x0; + AssertThat(f == x1, Is().True()); + }); + + it("accumulates with '^=(__bdd&&)' operator", [&]() { + bdd f = terminal_T; + f ^= x0 & x1; + AssertThat(~(x0 & x1) == f, Is().True()); + }); + + it("computes with __bdd&& operators [1]", [&]() { + const bdd f = ((x0 & ~x1) | (~x0 & x1)) ^ ((x1 ^ x0) & (~x0 & x1)); + AssertThat(f == (x0 & ~x1), Is().True()); + AssertThat((x0 & ~x1) == f, Is().True()); + }); + + it("computes with __bdd&& operators [2]", [&]() { + const bdd f = ((x0 & ~x1) | (~x0 & x1)) ^ ((x1 ^ x0) & (~x0 & x1)); + AssertThat(f == (x0 & ~x1), Is().True()); + AssertThat((x0 & ~x1) == f, Is().True()); + }); + + it("computes with __bdd&& and bdd& operators [1]", [&]() { + // Notice, that the two expressions with terminal_T and terminal_F + // shortcut with the operator for a bdd with the negation flag + // set correctly. + const bdd f = ((x0 & x1) | (~x0 & x1)) ^ ((terminal_T ^ x0) & (terminal_F | x1)); + AssertThat(f == (x0 & x1), Is().True()); + AssertThat((x0 & x1) == f, Is().True()); + }); + + it("computes with __bdd&& and bdd& operators [2]", [&]() { + // The right-hand-side will evaluate to a bdd, since terminal_T negates. + const bdd f = ((~x0 | (x0 & x1)) ^ (terminal_T ^ (x1 ^ x0))); + AssertThat(f == (~x0 & x1), Is().True()); + AssertThat((~x0 & x1) == f, Is().True()); + }); }); - it("should negate __bdd&& in ~(x0 & x1)", [&]() { - AssertThat(x0_nand_x1 == ~(x0 & x1), Is().True()); - AssertThat(x0_nand_x1 != ~(x0 & x1), Is().False()); - }); + describe("==, !=", [&]() { + it("check two derivations of same __bdd&& [==]", + [&]() { AssertThat((x0 ^ x1) == ((x0 & ~x1) | (~x0 & x1)), Is().True()); }); - it("should compute with __bdd&& operators", [&]() { - bdd out = ((x0 & ~x1) | (~x0 & x1)) ^ ((x1 ^ x0) & (~x0 & x1)); - AssertThat((x0 & ~x1) == out, Is().True()); - AssertThat((x0 & ~x1) != out, Is().False()); - }); - - it("should compute with __bdd&& and bdd& in operators [1]", [&]() { - // Notice, that the two expressions with terminal_T and terminal_F - // shortcut with the operator for a bdd with the negation flag - // set correctly. - bdd out = ((x0 & x1) | (~x0 & x1)) ^ ((terminal_T ^ x0) & (terminal_F | x1)); - AssertThat((x0 & x1) == out, Is().True()); - AssertThat((x0 & x1) != out, Is().False()); - }); - - it("should compute with __bdd&& and bdd& in operators [2]", [&]() { - // The right-hand-side will evaluate to a bdd, since terminal_F negates. - bdd out = ((~x0 | (x0 & x1)) ^ (terminal_T ^ (x1 ^ x0))); - AssertThat((~x0 & x1) == out, Is().True()); - AssertThat((~x0 & x1) != out, Is().False()); - }); - - it("should x0 ?= __bdd&&", [&]() { - bdd out = x0; - out &= x0 & x1; - AssertThat((x0 & x1) == out, Is().True()); - AssertThat((x0 & x1) != out, Is().False()); - }); + it("check two derivations of same __bdd&& [!=]", + [&]() { AssertThat((x0 ^ x1) != ((x0 & ~x1) | (~x0 & x1)), Is().False()); }); - it("should check two derivations of same __bdd&&", [&]() { - AssertThat((x0 ^ x1) == ((x0 & ~x1) | (~x0 & x1)), Is().True()); - AssertThat((x0 ^ x1) != ((x0 & ~x1) | (~x0 & x1)), Is().False()); - }); + it("checks two derivations of different __bdd&& [==]", + [&]() { AssertThat((x0 | x1) == ((x0 & x1) | (~x0 & x1)), Is().False()); }); - it("should check two derivations of different __bdd&&", [&]() { - AssertThat((x0 | x1) == ((x0 & x1) | (~x0 & x1)), Is().False()); - AssertThat((x0 | x1) != ((x0 & x1) | (~x0 & x1)), Is().True()); + it("checks two derivations of different __bdd&& [!=]", + [&]() { AssertThat((x0 | x1) != ((x0 & x1) | (~x0 & x1)), Is().True()); }); }); }); }); From 35bad4100faad2a68652dcb1d3b3aa0f92744a5f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 14:13:24 +0200 Subject: [PATCH 02/10] Add '-' operator as an alias for 'bdd_diff' --- src/adiar/bdd.h | 27 ++++++++++++++++++++++++++ src/adiar/bdd/bdd.cpp | 33 ++++++++++++++++++++++++++++++++ src/adiar/bdd/bdd.h | 11 +++++++++++ test/adiar/bdd/test_bdd.cpp | 38 +++++++++++++++++++++++++++++++++++++ 4 files changed, 109 insertions(+) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index 8d1ae737e..d1788dd01 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -575,6 +575,33 @@ namespace adiar __bdd bdd_diff(const exec_policy& ep, const bdd& f, const bdd& g); + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_diff, bdd_not + ////////////////////////////////////////////////////////////////////////////////////////////////// + bdd + operator-(const bdd& f); + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_diff, bdd_not + ////////////////////////////////////////////////////////////////////////////////////////////////// + __bdd + operator-(__bdd&& f); + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_diff + ////////////////////////////////////////////////////////////////////////////////////////////////// + __bdd + operator-(const bdd& lhs, const bdd& rhs); + + /// \cond + __bdd + operator-(const bdd&, __bdd&&); + __bdd + operator-(__bdd&&, const bdd&); + __bdd + operator-(__bdd&&, __bdd&&); + /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'less than' operator. /// diff --git a/src/adiar/bdd/bdd.cpp b/src/adiar/bdd/bdd.cpp index 8feecb4ce..fd79c45f3 100644 --- a/src/adiar/bdd/bdd.cpp +++ b/src/adiar/bdd/bdd.cpp @@ -80,6 +80,7 @@ namespace adiar __BDD_OPER(__bdd, &); __BDD_OPER(__bdd, |); __BDD_OPER(__bdd, ^); + __BDD_OPER(__bdd, -); __BDD_OPER(bool, ==); __BDD_OPER(bool, !=); @@ -140,6 +141,20 @@ namespace adiar return (*this = std::move(temp)); } + bdd& + bdd::operator-=(const bdd& other) + { + return (*this = bdd_diff(*this, other)); + } + + bdd& + bdd::operator-=(bdd&& other) + { + __bdd temp = bdd_diff(*this, other); + other.deref(); + return (*this = std::move(temp)); + } + bool operator==(const bdd& lhs, const bdd& rhs) { @@ -182,6 +197,24 @@ namespace adiar return bdd_xor(lhs, rhs); } + bdd + operator-(const bdd& f) + { + return bdd_not(f); + } + + __bdd + operator-(__bdd&& f) + { + return bdd_not(std::move(f)); + } + + __bdd + operator-(const bdd& lhs, const bdd& rhs) + { + return bdd_diff(lhs, rhs); + } + ////////////////////////////////////////////////////////////////////////////// // Input variables bdd::label_type diff --git a/src/adiar/bdd/bdd.h b/src/adiar/bdd/bdd.h index a6893b62f..7d2b4847f 100644 --- a/src/adiar/bdd/bdd.h +++ b/src/adiar/bdd/bdd.h @@ -183,6 +183,17 @@ namespace adiar bdd& operator^=(bdd&& other); /// \endcond + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_diff + //////////////////////////////////////////////////////////////////////////////////////////////// + bdd& + operator-=(const bdd& other); + + /// \cond + bdd& + operator-=(bdd&& other); + /// \endcond }; } diff --git a/test/adiar/bdd/test_bdd.cpp b/test/adiar/bdd/test_bdd.cpp index 0190626e4..68a51e927 100644 --- a/test/adiar/bdd/test_bdd.cpp +++ b/test/adiar/bdd/test_bdd.cpp @@ -287,6 +287,44 @@ go_bandit([]() { it("checks two derivations of different __bdd&& [!=]", [&]() { AssertThat((x0 | x1) != ((x0 & x1) | (~x0 & x1)), Is().True()); }); }); + + describe("-", [&]() { + it("negates with '-(bdd&)' [x0]", [&]() { AssertThat(-x0 == ~x0, Is().True()); }); + + it("negates with '-(bdd&)' [x0 & x1]", + [&]() { AssertThat(-x0_and_x1 == ~x0_and_x1, Is().True()); }); + + it("negates with '-(__bdd&) [x0 & x1]", + [&]() { AssertThat(-(x0 & x1) == ~x0_and_x1, Is().True()); }); + + it("computes 'x0 - x1'", [&]() { + const bdd f = x0 - x1; + AssertThat(f == (x0 & ~x1), Is().True()); + }); + + it("accumulates with '-=(bdd&)' operator", [&]() { + bdd f = x0; + f -= x1; + AssertThat(f == (x0 & ~x1), Is().True()); + AssertThat(f != (x0 & ~x1), Is().False()); + + f -= x0; + AssertThat(f == terminal_F, Is().True()); + }); + + it("accumulates with '-=(__bdd&&)' operator", [&]() { + bdd f = terminal_T; + f -= x0 & x1; + AssertThat(f == ~(x0 & x1), Is().True()); + AssertThat(f != ~(x0 & x1), Is().False()); + }); + + it("computes with __bdd&& and bdd& operators", [&]() { + const bdd f = x0_and_x1 - x0 - x1; + AssertThat(f == terminal_F, Is().True()); + AssertThat(terminal_F == f, Is().True()); + }); + }); }); }); }); From 61a3453a1ac652b91d5605896a541dc8c74b20e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 14:51:49 +0200 Subject: [PATCH 03/10] Add '+' operator as an alias for 'bdd_or' Further cleans up src/adiar/bdd/bdd.cpp to make it more maintainable --- src/adiar/bdd.h | 27 ++++++ src/adiar/bdd/bdd.cpp | 177 +++++++++++++++++++++++------------- src/adiar/bdd/bdd.h | 11 +++ test/adiar/bdd/test_bdd.cpp | 29 +++++- 4 files changed, 178 insertions(+), 66 deletions(-) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index d1788dd01..d07ddc6d6 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -448,6 +448,33 @@ namespace adiar operator|(__bdd&&, __bdd&&); /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_or + ////////////////////////////////////////////////////////////////////////////////////////////////// + bdd + operator+(const bdd& f); + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_or + ////////////////////////////////////////////////////////////////////////////////////////////////// + __bdd + operator+(__bdd&& f); + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_or + ////////////////////////////////////////////////////////////////////////////////////////////////// + __bdd + operator+(const bdd& lhs, const bdd& rhs); + + /// \cond + __bdd + operator+(const bdd&, __bdd&&); + __bdd + operator+(__bdd&&, const bdd&); + __bdd + operator+(__bdd&&, __bdd&&); + /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'nor' operator. /// diff --git a/src/adiar/bdd/bdd.cpp b/src/adiar/bdd/bdd.cpp index fd79c45f3..ab71fac01 100644 --- a/src/adiar/bdd/bdd.cpp +++ b/src/adiar/bdd/bdd.cpp @@ -11,7 +11,7 @@ namespace adiar { - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // '__bdd' Constructors __bdd::__bdd() = default; @@ -27,7 +27,7 @@ namespace adiar : internal::__dd(dd) {} - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // 'bdd' Constructors bdd::bdd(bool t) : bdd(bdd_terminal(t)) @@ -53,36 +53,26 @@ namespace adiar : internal::dd(internal::reduce(std::move(f))) {} - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // Operators - bdd - operator~(__bdd&& in) - { - return ~bdd(std::move(in)); - } - -#define __BDD_OPER(out_t, op) \ - out_t operator op(__bdd&& lhs, __bdd&& rhs) \ - { \ - return bdd(std::move(lhs)) op bdd(std::move(rhs)); \ - } \ - \ - out_t operator op(const bdd& lhs, __bdd&& rhs) \ - { \ - return lhs op bdd(std::move(rhs)); \ - } \ - \ - out_t operator op(__bdd&& lhs, const bdd& rhs) \ - { \ - return bdd(std::move(lhs)) op rhs; \ +#define __BDD_OPER(out_t, op) \ + out_t operator op(__bdd&& lhs, __bdd&& rhs) \ + { \ + return bdd(std::move(lhs)) op bdd(std::move(rhs)); \ + } \ + \ + out_t operator op(const bdd& lhs, __bdd&& rhs) \ + { \ + return lhs op bdd(std::move(rhs)); \ + } \ + \ + out_t operator op(__bdd&& lhs, const bdd& rhs) \ + { \ + return bdd(std::move(lhs)) op rhs; \ } - __BDD_OPER(__bdd, &); - __BDD_OPER(__bdd, |); - __BDD_OPER(__bdd, ^); - __BDD_OPER(__bdd, -); - __BDD_OPER(bool, ==); - __BDD_OPER(bool, !=); + ////////////////////////////////////////////////////////////////////////////// + // Operators (Assignment) bdd& bdd::operator=(const bdd& other) @@ -99,6 +89,54 @@ namespace adiar return (*this = internal::reduce(std::move(other))); } + ////////////////////////////////////////////////////////////////////////////// + // Operators (Equality Checking) + + __BDD_OPER(bool, ==); + + bool + operator==(const bdd& lhs, const bdd& rhs) + { + return bdd_equal(lhs, rhs); + } + + __BDD_OPER(bool, !=); + + bool + operator!=(const bdd& lhs, const bdd& rhs) + { + return bdd_unequal(lhs, rhs); + } + + ////////////////////////////////////////////////////////////////////////////// + // Operators (Bit) + + bdd + operator~(const bdd& f) + { + return bdd_not(f); + } + + bdd + operator~(bdd&& f) + { + return bdd_not(std::move(f)); + } + + bdd + operator~(__bdd&& in) + { + return ~bdd(std::move(in)); + } + + __BDD_OPER(__bdd, &); + + __bdd + operator&(const bdd& lhs, const bdd& rhs) + { + return bdd_and(lhs, rhs); + } + bdd& bdd::operator&=(const bdd& other) { @@ -113,6 +151,14 @@ namespace adiar return (*this = std::move(temp)); } + __BDD_OPER(__bdd, |); + + __bdd + operator|(const bdd& lhs, const bdd& rhs) + { + return bdd_or(lhs, rhs); + } + bdd& bdd::operator|=(const bdd& other) { @@ -127,6 +173,14 @@ namespace adiar return (*this = std::move(temp)); } + __BDD_OPER(__bdd, ^); + + __bdd + operator^(const bdd& lhs, const bdd& rhs) + { + return bdd_xor(lhs, rhs); + } + bdd& bdd::operator^=(const bdd& other) { @@ -141,60 +195,57 @@ namespace adiar return (*this = std::move(temp)); } - bdd& - bdd::operator-=(const bdd& other) - { - return (*this = bdd_diff(*this, other)); - } + ////////////////////////////////////////////////////////////////////////////// + // Operators (Set/Arithmetic) - bdd& - bdd::operator-=(bdd&& other) - { - __bdd temp = bdd_diff(*this, other); - other.deref(); - return (*this = std::move(temp)); - } + __BDD_OPER(__bdd, +); - bool - operator==(const bdd& lhs, const bdd& rhs) + bdd + operator+(const bdd& f) { - return bdd_equal(lhs, rhs); + return f; } - bool - operator!=(const bdd& lhs, const bdd& rhs) + __bdd + operator+(__bdd&& f) { - return bdd_unequal(lhs, rhs); + return f; } - bdd - operator~(const bdd& f) + __bdd + operator+(const bdd& lhs, const bdd& rhs) { - return bdd_not(f); + return bdd_or(lhs, rhs); } - bdd - operator~(bdd&& f) + bdd& + bdd::operator+=(const bdd& other) { - return bdd_not(std::forward(f)); + return (*this = bdd_or(*this, other)); } - __bdd - operator&(const bdd& lhs, const bdd& rhs) + bdd& + bdd::operator+=(bdd&& other) { - return bdd_and(lhs, rhs); + __bdd temp = bdd_or(*this, other); + other.deref(); + return (*this = std::move(temp)); } - __bdd - operator|(const bdd& lhs, const bdd& rhs) + __BDD_OPER(__bdd, -); + + bdd& + bdd::operator-=(const bdd& other) { - return bdd_or(lhs, rhs); + return (*this = bdd_diff(*this, other)); } - __bdd - operator^(const bdd& lhs, const bdd& rhs) + bdd& + bdd::operator-=(bdd&& other) { - return bdd_xor(lhs, rhs); + __bdd temp = bdd_diff(*this, other); + other.deref(); + return (*this = std::move(temp)); } bdd @@ -215,7 +266,7 @@ namespace adiar return bdd_diff(lhs, rhs); } - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // Input variables bdd::label_type bdd_topvar(const bdd& f) diff --git a/src/adiar/bdd/bdd.h b/src/adiar/bdd/bdd.h index 7d2b4847f..36797bf72 100644 --- a/src/adiar/bdd/bdd.h +++ b/src/adiar/bdd/bdd.h @@ -184,6 +184,17 @@ namespace adiar operator^=(bdd&& other); /// \endcond + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_or + //////////////////////////////////////////////////////////////////////////////////////////////// + bdd& + operator+=(const bdd& other); + + /// \cond + bdd& + operator+=(bdd&& other); + /// \endcond + //////////////////////////////////////////////////////////////////////////////////////////////// /// \see bdd_diff //////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/test/adiar/bdd/test_bdd.cpp b/test/adiar/bdd/test_bdd.cpp index 68a51e927..b51eac097 100644 --- a/test/adiar/bdd/test_bdd.cpp +++ b/test/adiar/bdd/test_bdd.cpp @@ -289,6 +289,31 @@ go_bandit([]() { }); describe("-", [&]() { + it("does nothing with '+(bdd&)' [x0]", [&]() { AssertThat(+x0 == x0, Is().True()); }); + + it("does nothing with '+(__bdd&) [x0 & x1]", + [&]() { AssertThat(+(x0 & x1) == x0_and_x1, Is().True()); }); + + it("computes 'x0 + x1'", [&]() { + const bdd f = x0 + x1; + AssertThat(f == (x0 | x1), Is().True()); + }); + + it("accumulates with '+=(bdd&)' operator", [&]() { + bdd f = x0; + f += x1; + AssertThat(f == (x0 | x1), Is().True()); + + f += terminal_T; + AssertThat(f == terminal_T, Is().True()); + }); + + it("accumulates with '+=(__bdd&&)' operator", [&]() { + bdd f = terminal_F; + f += x0 & x1; + AssertThat(f == (x0 & x1), Is().True()); + }); + it("negates with '-(bdd&)' [x0]", [&]() { AssertThat(-x0 == ~x0, Is().True()); }); it("negates with '-(bdd&)' [x0 & x1]", @@ -306,7 +331,6 @@ go_bandit([]() { bdd f = x0; f -= x1; AssertThat(f == (x0 & ~x1), Is().True()); - AssertThat(f != (x0 & ~x1), Is().False()); f -= x0; AssertThat(f == terminal_F, Is().True()); @@ -316,10 +340,9 @@ go_bandit([]() { bdd f = terminal_T; f -= x0 & x1; AssertThat(f == ~(x0 & x1), Is().True()); - AssertThat(f != ~(x0 & x1), Is().False()); }); - it("computes with __bdd&& and bdd& operators", [&]() { + it("computes with '-(__bdd&&)' and '-(bdd&)' operators", [&]() { const bdd f = x0_and_x1 - x0 - x1; AssertThat(f == terminal_F, Is().True()); AssertThat(terminal_F == f, Is().True()); From 86773e38181cea9152f7a66ad56b4e581949a4b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 14:57:53 +0200 Subject: [PATCH 04/10] Add '*' operator as an alias for 'bdd_and' --- src/adiar/bdd.h | 15 ++++++++++++++ src/adiar/bdd/bdd.cpp | 40 ++++++++++++++++++++++++++++--------- src/adiar/bdd/bdd.h | 11 ++++++++++ test/adiar/bdd/test_bdd.cpp | 20 +++++++++++++++++++ 4 files changed, 77 insertions(+), 9 deletions(-) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index d07ddc6d6..9430063e6 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -401,6 +401,21 @@ namespace adiar operator&(__bdd&&, __bdd&&); /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_and + ////////////////////////////////////////////////////////////////////////////////////////////////// + __bdd + operator*(const bdd& lhs, const bdd& rhs); + + /// \cond + __bdd + operator*(const bdd&, __bdd&&); + __bdd + operator*(__bdd&&, const bdd&); + __bdd + operator*(__bdd&&, __bdd&&); + /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Logical 'nand' operator. /// diff --git a/src/adiar/bdd/bdd.cpp b/src/adiar/bdd/bdd.cpp index ab71fac01..769b6a79b 100644 --- a/src/adiar/bdd/bdd.cpp +++ b/src/adiar/bdd/bdd.cpp @@ -234,6 +234,24 @@ namespace adiar __BDD_OPER(__bdd, -); + bdd + operator-(const bdd& f) + { + return bdd_not(f); + } + + __bdd + operator-(__bdd&& f) + { + return bdd_not(std::move(f)); + } + + __bdd + operator-(const bdd& lhs, const bdd& rhs) + { + return bdd_diff(lhs, rhs); + } + bdd& bdd::operator-=(const bdd& other) { @@ -248,22 +266,26 @@ namespace adiar return (*this = std::move(temp)); } - bdd - operator-(const bdd& f) + __BDD_OPER(__bdd, *); + + __bdd + operator*(const bdd& lhs, const bdd& rhs) { - return bdd_not(f); + return bdd_and(lhs, rhs); } - __bdd - operator-(__bdd&& f) + bdd& + bdd::operator*=(const bdd& other) { - return bdd_not(std::move(f)); + return (*this = bdd_and(*this, other)); } - __bdd - operator-(const bdd& lhs, const bdd& rhs) + bdd& + bdd::operator*=(bdd&& other) { - return bdd_diff(lhs, rhs); + __bdd temp = bdd_and(*this, other); + other.deref(); + return (*this = std::move(temp)); } ////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/adiar/bdd/bdd.h b/src/adiar/bdd/bdd.h index 36797bf72..a57b36b3c 100644 --- a/src/adiar/bdd/bdd.h +++ b/src/adiar/bdd/bdd.h @@ -205,6 +205,17 @@ namespace adiar bdd& operator-=(bdd&& other); /// \endcond + + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \see bdd_and + //////////////////////////////////////////////////////////////////////////////////////////////// + bdd& + operator*=(const bdd& other); + + /// \cond + bdd& + operator*=(bdd&& other); + /// \endcond }; } diff --git a/test/adiar/bdd/test_bdd.cpp b/test/adiar/bdd/test_bdd.cpp index b51eac097..fa205cce5 100644 --- a/test/adiar/bdd/test_bdd.cpp +++ b/test/adiar/bdd/test_bdd.cpp @@ -314,6 +314,26 @@ go_bandit([]() { AssertThat(f == (x0 & x1), Is().True()); }); + it("computes 'x0 + x1'", [&]() { + const bdd f = x0 * x1; + AssertThat(f == (x0 & x1), Is().True()); + }); + + it("accumulates with '+=(bdd&)' operator", [&]() { + bdd f = x0; + f *= x1; + AssertThat(f == (x0 & x1), Is().True()); + + f *= terminal_F; + AssertThat(f == terminal_F, Is().True()); + }); + + it("accumulates with '+=(__bdd&&)' operator", [&]() { + bdd f = terminal_T; + f *= x0 & x1; + AssertThat(f == (x0 & x1), Is().True()); + }); + it("negates with '-(bdd&)' [x0]", [&]() { AssertThat(-x0 == ~x0, Is().True()); }); it("negates with '-(bdd&)' [x0 & x1]", From 555cf7d2bb16580a245927421c24ba18ec336984 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 15:36:11 +0200 Subject: [PATCH 05/10] Clean up ZDD operation overloads and their tests --- src/adiar/bdd/bdd.cpp | 2 +- src/adiar/zdd.h | 2 +- src/adiar/zdd/zdd.cpp | 118 ++++++++++++--------- test/adiar/zdd/test_zdd.cpp | 197 ++++++++++++++++++++++++------------ 4 files changed, 209 insertions(+), 110 deletions(-) diff --git a/src/adiar/bdd/bdd.cpp b/src/adiar/bdd/bdd.cpp index 769b6a79b..157541573 100644 --- a/src/adiar/bdd/bdd.cpp +++ b/src/adiar/bdd/bdd.cpp @@ -90,7 +90,7 @@ namespace adiar } ////////////////////////////////////////////////////////////////////////////// - // Operators (Equality Checking) + // Operators (Relational) __BDD_OPER(bool, ==); diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index 920d1cc06..5a73c275d 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -499,7 +499,7 @@ namespace adiar __zdd operator&(const zdd&, __zdd&&); __zdd - operator&(__zdd&&, const __zdd&); + operator&(__zdd&&, const zdd&); /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/adiar/zdd/zdd.cpp b/src/adiar/zdd/zdd.cpp index 6062d7d01..adadf1ee1 100644 --- a/src/adiar/zdd/zdd.cpp +++ b/src/adiar/zdd/zdd.cpp @@ -17,7 +17,7 @@ namespace adiar { - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // '__zdd' Constructors __zdd::__zdd() : internal::__dd() @@ -35,7 +35,7 @@ namespace adiar : internal::__dd(dd) {} - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // 'zdd' Constructors zdd::zdd() : zdd(zdd_empty()) @@ -63,9 +63,9 @@ namespace adiar : internal::dd(internal::reduce(std::move(A))) {} - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // Operators -#define __zdd_oper(out_t, op) \ +#define __ZDD_OPER(out_t, op) \ out_t operator op(__zdd&& lhs, __zdd&& rhs) \ { \ return zdd(std::move(lhs)) op zdd(std::move(rhs)); \ @@ -81,12 +81,11 @@ namespace adiar return zdd(std::move(lhs)) op rhs; \ } - __zdd_oper(__zdd, &) __zdd_oper(__zdd, |) __zdd_oper(__zdd, -) - - __zdd_oper(bool, ==) __zdd_oper(bool, !=) __zdd_oper(bool, <=) __zdd_oper(bool, >=) - __zdd_oper(bool, <) __zdd_oper(bool, >) + ////////////////////////////////////////////////////////////////////////////// + // Operators (Assignment) - zdd& zdd::operator=(const zdd & other) + zdd& + zdd::operator=(const zdd & other) { this->negate = other.negate; this->file = other.file; @@ -100,6 +99,60 @@ namespace adiar return (*this = internal::reduce(std::move(other))); } + ////////////////////////////////////////////////////////////////////////////// + // Operators (Relational) + + __ZDD_OPER(bool, ==); + + bool + operator==(const zdd& lhs, const zdd& rhs) + { + return zdd_equal(lhs, rhs); + } + + __ZDD_OPER(bool, !=); + + bool + operator!=(const zdd& lhs, const zdd& rhs) + { + return zdd_unequal(lhs, rhs); + } + + __ZDD_OPER(bool, <=); + + bool + operator<=(const zdd& lhs, const zdd& rhs) + { + return zdd_subseteq(lhs, rhs); + } + + __ZDD_OPER(bool, >=); + + bool + operator>=(const zdd& lhs, const zdd& rhs) + { + return zdd_subseteq(rhs, lhs); + } + + __ZDD_OPER(bool, <); + + bool + operator<(const zdd& lhs, const zdd& rhs) + { + return zdd_subset(lhs, rhs); + } + + __ZDD_OPER(bool, >); + + bool + operator>(const zdd& lhs, const zdd& rhs) + { + return zdd_subset(rhs, lhs); + } + + ////////////////////////////////////////////////////////////////////////////// + // Operators (Bit) + __zdd operator~(const zdd& A) { @@ -112,6 +165,8 @@ namespace adiar return ~zdd(std::move(A)); } + __ZDD_OPER(__zdd, &); + __zdd operator&(const zdd& lhs, const zdd& rhs) { @@ -132,6 +187,8 @@ namespace adiar return (*this = std::move(temp)); } + __ZDD_OPER(__zdd, |); + __zdd operator|(const zdd& lhs, const zdd& rhs) { @@ -152,6 +209,11 @@ namespace adiar return (*this = std::move(temp)); } + ////////////////////////////////////////////////////////////////////////////// + // Operators (Set/Arithmetic) + + __ZDD_OPER(__zdd, -); + __zdd operator-(const zdd& lhs, const zdd& rhs) { @@ -172,43 +234,7 @@ namespace adiar return (*this = std::move(temp)); } - bool - operator==(const zdd& lhs, const zdd& rhs) - { - return zdd_equal(lhs, rhs); - } - - bool - operator!=(const zdd& lhs, const zdd& rhs) - { - return zdd_unequal(lhs, rhs); - } - - bool - operator<=(const zdd& lhs, const zdd& rhs) - { - return zdd_subseteq(lhs, rhs); - } - - bool - operator>=(const zdd& lhs, const zdd& rhs) - { - return zdd_subseteq(rhs, lhs); - } - - bool - operator<(const zdd& lhs, const zdd& rhs) - { - return zdd_subset(lhs, rhs); - } - - bool - operator>(const zdd& lhs, const zdd& rhs) - { - return zdd_subset(rhs, lhs); - } - - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // Input variables zdd::label_type zdd_topvar(const zdd& A) diff --git a/test/adiar/zdd/test_zdd.cpp b/test/adiar/zdd/test_zdd.cpp index 9934867a2..9e65cc697 100644 --- a/test/adiar/zdd/test_zdd.cpp +++ b/test/adiar/zdd/test_zdd.cpp @@ -46,14 +46,14 @@ go_bandit([]() { zdd terminal_F(terminal_F_nf); describe("__zdd class", [&]() { - it("should copy-construct values from zdd", [&]() { + it("copy-constructs values from zdd", [&]() { __zdd t1 = x0_or_x1; AssertThat(t1.has>(), Is().True()); AssertThat(t1.get>(), Is().EqualTo(x0_or_x1_nf)); AssertThat(t1.negate, Is().False()); }); - it("should copy-construct values from __zdd", [&]() { + it("copy-constructs values from __zdd", [&]() { __zdd t1 = x0_or_x1; __zdd t2 = t1; AssertThat(t2.has>(), Is().True()); @@ -61,7 +61,7 @@ go_bandit([]() { AssertThat(t2.negate, Is().False()); }); - it("should copy-construct values from shared_levelized_file", [&]() { + it("copy-constructs values from shared_levelized_file", [&]() { __zdd t1 = x0_or_x1; AssertThat(t1.has>(), Is().True()); AssertThat(t1.get>(), Is().EqualTo(x0_or_x1_nf)); @@ -84,7 +84,7 @@ go_bandit([]() { af->max_1level_cut = 1; - it("should copy-construct values from __zdd::shared_arc_file_type", [&]() { + it("copy-constructs values from __zdd::shared_arc_file_type", [&]() { __zdd t1 = __zdd(af, exec_policy::access::Random_Access); AssertThat(t1.has<__zdd::shared_arc_file_type>(), Is().True()); AssertThat(t1.get<__zdd::shared_arc_file_type>(), Is().EqualTo(af)); @@ -92,96 +92,169 @@ go_bandit([]() { AssertThat(t1._policy, Is().EqualTo(exec_policy(exec_policy::access::Random_Access))); }); - it("should reduce on copy construct to zdd with __zdd::shared_arc_file_type", [&]() { + it("reduces on copy construct to zdd with __zdd::shared_arc_file_type", [&]() { zdd out = __zdd(af, exec_policy()); AssertThat(out, Is().EqualTo(x0_or_x1)); }); }); describe("operators", [&]() { - it("should reject Ø == {Ø}", - [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); }); - - it("should accept {{0}} == {{0}} (different files)", [&]() { - shared_levelized_file x0_nf_2; - - { - node_writer nw_0(x0_nf_2); - nw_0 << node(0, node::max_id, ptr_uint64(false), ptr_uint64(true)); - } - - zdd x0_2(x0_nf); + describe("==, !=", [&]() { + it("rejects Ø == {Ø}", + [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); }); + + it("accepts {{0}} == {{0}} (different files)", [&]() { + shared_levelized_file other_nf; + { + node_writer nw(other_nf); + nw << node(0, node::max_id, ptr_uint64(false), ptr_uint64(true)); + } + zdd other(other_nf); + + AssertThat(x0, Is().EqualTo(other)); + }); + + it("rejects {{0}} == {{1}}", [&]() { + AssertThat(x0, Is().Not().EqualTo(x1)); + }); + + it("rejects {{0}, {1}} == {{0}}", [&]() { + AssertThat(x0_or_x1, Is().Not().EqualTo(x0)); + }); + }); - AssertThat(x0, Is().EqualTo(x0_2)); + describe("~, &, |", [&]() { + it("computes ~{{0},{1}} == {Ø,{0,1}} with {0,1} domain", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); + + shared_levelized_file expected; + { + node_writer nw(expected); + nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)) + << node(0, node::max_id, ptr_uint64(true), ptr_uint64(1, ptr_uint64::max_id)); + } + AssertThat(~x0_or_x1 == zdd(expected), Is().True()); + }); + + it("computes {{0}} | {{1}} == {{0}, {1}}", + [&]() { AssertThat((x0 | x1) == x0_or_x1, Is().True()); }); + + it("accumulates with '|=(zdd&)' operator", [&]() { + zdd A = terminal_F; + A |= x0; + AssertThat(A, Is().EqualTo(x0)); + + A |= x1; + AssertThat(A, Is().EqualTo(x0_or_x1)); + }); + + it("computes {{0}} & {{0},{1}} == {{0}}", + [&]() { AssertThat((x0 & x0_or_x1) == x0, Is().True()); }); + + it("accumulates with '&=(zdd&)' operator", [&]() { + zdd A = x0_or_x1; + A &= x0; + AssertThat(A, Is().EqualTo(x0)); + + A &= x1; + AssertThat(A, Is().EqualTo(terminal_F)); + }); + + it("accumulates with '|=(__zdd&&)' and '&=(__zdd&&)'", [&]() { + zdd A = x0; + + A |= x0_or_x1 & x1; + AssertThat(A, Is().EqualTo(x0_or_x1)); + + A &= x0_or_x1 & x1; + AssertThat(A, Is().EqualTo(x1)); + }); + + it("computes with __zdd&& operators [~]", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); + + const zdd A = ~(x0 | x1); + AssertThat(~x0_or_x1 == A, Is().True()); + }); + + it("computes with __zdd&& operators [&]", [&]() { + const zdd A = (x0 & (x0_or_x1 & x0)) & x1; + AssertThat(A, Is().EqualTo(terminal_F)); + }); + + it("computes with __zdd&& operators [|]", [&]() { + const zdd A = (x0_or_x1 | (x0 | x1)) | x0; + AssertThat(A, Is().EqualTo(x0_or_x1)); + }); + + it("computes with __zdd&& operators [|,&]", [&]() { + const zdd A = ((x0_or_x1 | x0) | ((x0 & x1) | x1)) & x0; + AssertThat(A, Is().EqualTo(x0)); + }); }); - it("should compute {{0}} /\\ {{1}} == {{0}, {1}}", - [&]() { AssertThat((x0 | x1) == x0_or_x1, Is().True()); }); + describe("-", [&]() { + // TODO: Unary Minus - it("should compute {{0}} \\/ {{0},{1}} == {{0}}", - [&]() { AssertThat((x0 & x0_or_x1) == x0, Is().True()); }); + it("computes {{0},{1}} - {{0}} == {{1}}", + [&]() { AssertThat((x0_or_x1 - x0) == x1, Is().True()); }); - it("should compute {{0},{1}} \\ {{0}} == {{1}}", - [&]() { AssertThat((x0_or_x1 - x0) == x1, Is().True()); }); + it("accumulates with '-=(zdd&)'", [&]() { + zdd A = x0_or_x1; - it("should compute {{0},{1}}' == {Ø,{0,1}} with dom {0,1}", [&]() { - shared_file dom; - { - label_writer lw(dom); - lw << 0 << 1; - } + A -= x0; + AssertThat(A == x1, Is().True()); - domain_set(dom); + A -= x1; + AssertThat(A == terminal_F, Is().True()); + }); - shared_levelized_file expected; - { - node_writer nw(expected); - nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)) - << node(0, node::max_id, ptr_uint64(true), ptr_uint64(1, ptr_uint64::max_id)); - } + it("accumulates with '-=(__zdd&&)'", [&]() { + zdd A = x0_or_x1; - AssertThat(~x0_or_x1 == zdd(expected), Is().True()); + A -= x0 | x1; + AssertThat(A == terminal_F, Is().True()); + }); + + // TODO: Unary Plus, Plus, Multiply }); - it("should compute with __zdd&& operators [|,&,-]", [&]() { + it("computes with __zdd&& operators [|,&,-]", [&]() { zdd out = ((x0_or_x1 - x0) | ((x0 | x1) & (x0_or_x1 - x1))) - (x0_or_x1 - x0); AssertThat(x0, Is().EqualTo(out)); }); - it("should compute with __zdd&& operators [|,~,-,]", [&]() { - shared_file dom; - { - label_writer lw(dom); - lw << 0 << 1; - } - - domain_set(dom); + it("computes with __zdd&& operators [|,~,-,]", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); zdd out = ~(~(x0 | x1) - terminal_T); zdd expected = x0 | x1 | terminal_T; AssertThat(expected, Is().EqualTo(out)); }); - it("should ?= __zdd&&", [&]() { - zdd out = x0_or_x1; - out -= x0_or_x1 & x1; - AssertThat(out, Is().EqualTo(x0)); + describe("==, !=", [&]() { + it("checks two derivations of same __bdd&& [==]", [&]() { + AssertThat((x0 | x1) == ((x0_or_x1 - x1) | x1), Is().True()); + }); - out |= x0_or_x1 & x1; - AssertThat(out, Is().EqualTo(x0_or_x1)); + it("checks two derivations of same __bdd&& [!=]", [&]() { + AssertThat((x0 | x1) != ((x0_or_x1 - x1) | x1), Is().False()); + }); - out &= x0_or_x1 & x1; - AssertThat(out, Is().EqualTo(x1)); - }); + it("checks two derivations of different __bdd&& [==]", [&]() { + AssertThat((x0 | x1) == (x0_or_x1 - x1), Is().False()); + }); - it("should check two derivations of same __bdd&&", [&]() { - AssertThat((x0 | x1) == ((x0_or_x1 - x1) | x1), Is().True()); - AssertThat((x0 | x1) != ((x0_or_x1 - x1) | x1), Is().False()); + it("checks two derivations of different __bdd&& [!=]", [&]() { + AssertThat((x0 | x1) != (x0_or_x1 - x1), Is().True()); + }); }); - it("should check two derivations of different __bdd&&", [&]() { - AssertThat((x0 | x1) == (x0_or_x1 - x1), Is().False()); - AssertThat((x0 | x1) != (x0_or_x1 - x1), Is().True()); + describe("<, <=, >, >=", [&]() { + // TODO }); }); From 9e9c4002142224110a3845a7abdc68676fb50073 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 15:44:11 +0200 Subject: [PATCH 06/10] Add missing unit tests for '<', '<=', '>', and '>=' ZDD operator overloads --- test/adiar/zdd/test_zdd.cpp | 60 ++++++++++++++++++++++++++++++++++++- 1 file changed, 59 insertions(+), 1 deletion(-) diff --git a/test/adiar/zdd/test_zdd.cpp b/test/adiar/zdd/test_zdd.cpp index 9e65cc697..fde00b74d 100644 --- a/test/adiar/zdd/test_zdd.cpp +++ b/test/adiar/zdd/test_zdd.cpp @@ -254,7 +254,65 @@ go_bandit([]() { }); describe("<, <=, >, >=", [&]() { - // TODO + it("checks {{0}} < {{0}, {1}}", [&]() { + AssertThat(x0 < x0_or_x1, Is().True()); + AssertThat(x0 < (x0 | x1), Is().True()); + }); + + it("checks {{0}} < {{1}}", [&]() { + AssertThat(x0 < x1, Is().False()); + }); + + it("checks {{0}, {1}} < {{0}, {1}}", [&]() { + AssertThat((x0 | x1) < x0_or_x1, Is().False()); + AssertThat(x0_or_x1 < (x0 | x1), Is().False()); + AssertThat((x0 | x1) < (x0 | x1), Is().False()); + }); + + it("checks {{0}} <= {{0}, {1}}", [&]() { + AssertThat(x0 <= x0_or_x1, Is().True()); + AssertThat(x0 <= (x0 | x1), Is().True()); + }); + + it("checks {{0}, {1}} <= {{0}, {1}}", [&]() { + AssertThat((x0 | x1) <= x0_or_x1, Is().True()); + AssertThat((x0 | x1) <= (x0 | x1), Is().True()); + }); + + it("checks {{0}} <= {{1}}", [&]() { + AssertThat(x0 <= x1, Is().False()); + }); + + it("checks {{0}, {1}} > {{0}}", [&]() { + AssertThat(x0_or_x1 > x0, Is().True()); + }); + + it("checks {{0}} > {{1}}", [&]() { + AssertThat(x0 > x1, Is().False()); + }); + + it("checks {{0}, {1}} > {{0}, {1}}", [&]() { + AssertThat((x0 | x1) > x0_or_x1, Is().False()); + AssertThat(x0_or_x1 > (x0 | x1), Is().False()); + AssertThat((x0 | x1) > (x0 | x1), Is().False()); + }); + + it("checks {{0}, {1}} >= {{0}}", [&]() { + AssertThat(x0_or_x1 >= x0, Is().True()); + }); + + it("checks {{0}, {1}} >= {{0}, {1}}", [&]() { + AssertThat((x0 | x1) >= x0_or_x1, Is().True()); + AssertThat(x0_or_x1 >= (x0 | x1), Is().True()); + AssertThat((x0 | x1) >= (x0 | x1), Is().True()); + }); + + it("checks {{0}} >= {{1}}", [&]() { + AssertThat(x0 >= x1, Is().False()); + AssertThat(x0 >= (x0_or_x1 & x1), Is().False()); + AssertThat((x0_or_x1 & x0) >= x1, Is().False()); + AssertThat((x0_or_x1 & x0) >= (x0_or_x1 & x1), Is().False()); + }); }); }); From b27ea1c19a914b0a3fc261b593b42ac969cf9faa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 15:48:54 +0200 Subject: [PATCH 07/10] Add unary '-' ZDD operator --- src/adiar/bdd.h | 5 ++--- src/adiar/zdd.h | 11 +++++++++++ src/adiar/zdd/zdd.cpp | 12 ++++++++++++ test/adiar/zdd/test_zdd.cpp | 26 +++++++++++++++++++++++++- 4 files changed, 50 insertions(+), 4 deletions(-) diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h index 9430063e6..48caeef29 100644 --- a/src/adiar/bdd.h +++ b/src/adiar/bdd.h @@ -623,11 +623,10 @@ namespace adiar bdd operator-(const bdd& f); - ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \see bdd_diff, bdd_not - ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \cond __bdd operator-(__bdd&& f); + /// \endcond ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see bdd_diff diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index 5a73c275d..b356955cb 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -516,6 +516,17 @@ namespace adiar __zdd zdd_diff(const exec_policy& ep, const zdd& A, const zdd& B); + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see zdd_diff, zdd_complement + ////////////////////////////////////////////////////////////////////////////////////////////////// + __zdd + operator-(const zdd& A); + + /// \cond + __zdd + operator-(__zdd&& A); + /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_diff ////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/adiar/zdd/zdd.cpp b/src/adiar/zdd/zdd.cpp index adadf1ee1..3fdd66076 100644 --- a/src/adiar/zdd/zdd.cpp +++ b/src/adiar/zdd/zdd.cpp @@ -214,6 +214,18 @@ namespace adiar __ZDD_OPER(__zdd, -); + __zdd + operator-(const zdd& A) + { + return zdd_complement(A); + } + + __zdd + operator-(__zdd&& A) + { + return -zdd(std::move(A)); + } + __zdd operator-(const zdd& lhs, const zdd& rhs) { diff --git a/test/adiar/zdd/test_zdd.cpp b/test/adiar/zdd/test_zdd.cpp index fde00b74d..ac9445a2a 100644 --- a/test/adiar/zdd/test_zdd.cpp +++ b/test/adiar/zdd/test_zdd.cpp @@ -196,7 +196,31 @@ go_bandit([]() { }); describe("-", [&]() { - // TODO: Unary Minus + it("computes -{{0},{1}} == {Ø,{0,1}} [zdd&] with {0,1} domain", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); + + shared_levelized_file expected; + { + node_writer nw(expected); + nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)) + << node(0, node::max_id, ptr_uint64(true), ptr_uint64(1, ptr_uint64::max_id)); + } + AssertThat(-x0_or_x1 == zdd(expected), Is().True()); + }); + + it("computes -{{0},{1}} == {Ø,{0,1}} [__zdd&&] with {0,1} domain", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); + + shared_levelized_file expected; + { + node_writer nw(expected); + nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true)) + << node(0, node::max_id, ptr_uint64(true), ptr_uint64(1, ptr_uint64::max_id)); + } + AssertThat(-(x0 | x1) == zdd(expected), Is().True()); + }); it("computes {{0},{1}} - {{0}} == {{1}}", [&]() { AssertThat((x0_or_x1 - x0) == x1, Is().True()); }); From 95619b2de0586c22faef9177fb3fb772b4aa284c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 16:01:50 +0200 Subject: [PATCH 08/10] Add '+' ZDD operator alias for 'zdd_union' --- src/adiar/zdd.h | 23 +++++++++++++++++++++++ src/adiar/zdd/zdd.cpp | 34 ++++++++++++++++++++++++++++++++++ src/adiar/zdd/zdd.h | 11 +++++++++++ test/adiar/zdd/test_zdd.cpp | 33 ++++++++++++++++++++++++++++++++- 4 files changed, 100 insertions(+), 1 deletion(-) diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index b356955cb..9e95b8ce3 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -473,6 +473,29 @@ namespace adiar operator|(__zdd&&, const zdd&); /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see zdd_union + ////////////////////////////////////////////////////////////////////////////////////////////////// + zdd + operator+(const zdd& A); + + /// \cond + __zdd + operator+(__zdd&& A); + /// \endcond + + __zdd + operator+(const zdd& lhs, const zdd& rhs); + + /// \cond + __zdd + operator+(__zdd&&, __zdd&&); + __zdd + operator+(const zdd&, __zdd&&); + __zdd + operator+(__zdd&&, const zdd&); + /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The intersection of two families of sets. /// diff --git a/src/adiar/zdd/zdd.cpp b/src/adiar/zdd/zdd.cpp index 3fdd66076..3452637be 100644 --- a/src/adiar/zdd/zdd.cpp +++ b/src/adiar/zdd/zdd.cpp @@ -246,6 +246,40 @@ namespace adiar return (*this = std::move(temp)); } + __ZDD_OPER(__zdd, +); + + zdd + operator+(const zdd& A) + { + return A; + } + + __zdd + operator+(__zdd&& A) + { + return A; + } + + __zdd + operator+(const zdd& lhs, const zdd& rhs) + { + return zdd_union(lhs, rhs); + } + + zdd& + zdd::operator+=(const zdd& other) + { + return (*this = zdd_union(*this, other)); + } + + zdd& + zdd::operator+=(zdd&& other) + { + __zdd temp = zdd_union(*this, other); + other.deref(); + return (*this = std::move(temp)); + } + ////////////////////////////////////////////////////////////////////////////////////////////////// // Input variables zdd::label_type diff --git a/src/adiar/zdd/zdd.h b/src/adiar/zdd/zdd.h index 3fd9ed43d..0f7881e25 100644 --- a/src/adiar/zdd/zdd.h +++ b/src/adiar/zdd/zdd.h @@ -238,6 +238,17 @@ namespace adiar operator|=(zdd&& other); /// \endcond + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \see zdd_union + //////////////////////////////////////////////////////////////////////////////////////////////// + zdd& + operator+=(const zdd& other); + + /// \cond + zdd& + operator+=(zdd&& other); + /// \endcond + //////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_diff //////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/test/adiar/zdd/test_zdd.cpp b/test/adiar/zdd/test_zdd.cpp index ac9445a2a..963e518da 100644 --- a/test/adiar/zdd/test_zdd.cpp +++ b/test/adiar/zdd/test_zdd.cpp @@ -242,7 +242,38 @@ go_bandit([]() { AssertThat(A == terminal_F, Is().True()); }); - // TODO: Unary Plus, Plus, Multiply + it("computes +{{0}} == {{0}} [zdd&] with {0,1} domain", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); + + AssertThat(+x0 == x0, Is().True()); + }); + + it("computes +{{0}} == {{0}} [__zdd&&] with {0,1} domain", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); + + AssertThat(+(x0 & x0_or_x1) == x0, Is().True()); + }); + + it("computes {{0}} + {{1}} == {{0}, {1}}", + [&]() { AssertThat((x0 + x1) == x0_or_x1, Is().True()); }); + + it("accumulates with '+=(zdd&)' operator", [&]() { + zdd A = terminal_F; + A += x0; + AssertThat(A, Is().EqualTo(x0)); + + A += x1; + AssertThat(A, Is().EqualTo(x0_or_x1)); + }); + + it("computes with __zdd&& operators [+]", [&]() { + const zdd A = (x0_or_x1 + (x0 + x1)) + x0; + AssertThat(A, Is().EqualTo(x0_or_x1)); + }); + + // TODO: Multiply }); it("computes with __zdd&& operators [|,&,-]", [&]() { From 74c87b0fa9f479fa3a900e256572940811ff6c05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 16:11:59 +0200 Subject: [PATCH 09/10] Add '*' ZDD operator alias for 'zdd_intsec' --- src/adiar/zdd.h | 15 ++++++ src/adiar/zdd/zdd.cpp | 22 ++++++++ src/adiar/zdd/zdd.h | 11 ++++ test/adiar/zdd/test_zdd.cpp | 104 +++++++++++++++++++++++------------- 4 files changed, 116 insertions(+), 36 deletions(-) diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h index 9e95b8ce3..139a9c69a 100644 --- a/src/adiar/zdd.h +++ b/src/adiar/zdd.h @@ -525,6 +525,21 @@ namespace adiar operator&(__zdd&&, const zdd&); /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \see zdd_intsec + ////////////////////////////////////////////////////////////////////////////////////////////////// + __zdd + operator*(const zdd& lhs, const zdd& rhs); + + /// \cond + __zdd + operator*(__zdd&&, __zdd&&); + __zdd + operator*(const zdd&, __zdd&&); + __zdd + operator*(__zdd&&, const zdd&); + /// \endcond + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief The set difference of two families of sets. /// diff --git a/src/adiar/zdd/zdd.cpp b/src/adiar/zdd/zdd.cpp index 3452637be..3fbd3bd7b 100644 --- a/src/adiar/zdd/zdd.cpp +++ b/src/adiar/zdd/zdd.cpp @@ -280,6 +280,28 @@ namespace adiar return (*this = std::move(temp)); } + __ZDD_OPER(__zdd, *); + + __zdd + operator*(const zdd& lhs, const zdd& rhs) + { + return zdd_intsec(lhs, rhs); + } + + zdd& + zdd::operator*=(const zdd& other) + { + return (*this = zdd_intsec(*this, other)); + } + + zdd& + zdd::operator*=(zdd&& other) + { + __zdd temp = zdd_intsec(*this, other); + other.deref(); + return (*this = std::move(temp)); + } + ////////////////////////////////////////////////////////////////////////////////////////////////// // Input variables zdd::label_type diff --git a/src/adiar/zdd/zdd.h b/src/adiar/zdd/zdd.h index 0f7881e25..7907eae4d 100644 --- a/src/adiar/zdd/zdd.h +++ b/src/adiar/zdd/zdd.h @@ -227,6 +227,17 @@ namespace adiar operator&=(zdd&& other); /// \endcond + //////////////////////////////////////////////////////////////////////////////////////////////// + /// \see zdd_union + //////////////////////////////////////////////////////////////////////////////////////////////// + zdd& + operator*=(const zdd& other); + + /// \cond + zdd& + operator*=(zdd&& other); + /// \endcond + //////////////////////////////////////////////////////////////////////////////////////////////// /// \see zdd_union //////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/test/adiar/zdd/test_zdd.cpp b/test/adiar/zdd/test_zdd.cpp index 963e518da..4fa5e4f72 100644 --- a/test/adiar/zdd/test_zdd.cpp +++ b/test/adiar/zdd/test_zdd.cpp @@ -149,6 +149,11 @@ go_bandit([]() { AssertThat(A, Is().EqualTo(x0_or_x1)); }); + it("computes with __zdd&& operators [|]", [&]() { + const zdd A = (x0_or_x1 | (x0 | x1)) | x0; + AssertThat(A, Is().EqualTo(x0_or_x1)); + }); + it("computes {{0}} & {{0},{1}} == {{0}}", [&]() { AssertThat((x0 & x0_or_x1) == x0, Is().True()); }); @@ -161,6 +166,11 @@ go_bandit([]() { AssertThat(A, Is().EqualTo(terminal_F)); }); + it("computes with __zdd&& operators [&]", [&]() { + const zdd A = (x0 & (x0_or_x1 & x0)) & x1; + AssertThat(A, Is().EqualTo(terminal_F)); + }); + it("accumulates with '|=(__zdd&&)' and '&=(__zdd&&)'", [&]() { zdd A = x0; @@ -171,6 +181,11 @@ go_bandit([]() { AssertThat(A, Is().EqualTo(x1)); }); + it("computes with __zdd&& operators [|,&]", [&]() { + const zdd A = ((x0_or_x1 | x0) | ((x0 & x1) | x1)) & x0; + AssertThat(A, Is().EqualTo(x0)); + }); + it("computes with __zdd&& operators [~]", [&]() { const std::vector dom = { 0, 1 }; domain_set(dom.begin(), dom.end()); @@ -178,24 +193,9 @@ go_bandit([]() { const zdd A = ~(x0 | x1); AssertThat(~x0_or_x1 == A, Is().True()); }); - - it("computes with __zdd&& operators [&]", [&]() { - const zdd A = (x0 & (x0_or_x1 & x0)) & x1; - AssertThat(A, Is().EqualTo(terminal_F)); - }); - - it("computes with __zdd&& operators [|]", [&]() { - const zdd A = (x0_or_x1 | (x0 | x1)) | x0; - AssertThat(A, Is().EqualTo(x0_or_x1)); - }); - - it("computes with __zdd&& operators [|,&]", [&]() { - const zdd A = ((x0_or_x1 | x0) | ((x0 & x1) | x1)) & x0; - AssertThat(A, Is().EqualTo(x0)); - }); }); - describe("-", [&]() { + describe("-, +, *", [&]() { it("computes -{{0},{1}} == {Ø,{0,1}} [zdd&] with {0,1} domain", [&]() { const std::vector dom = { 0, 1 }; domain_set(dom.begin(), dom.end()); @@ -242,17 +242,11 @@ go_bandit([]() { AssertThat(A == terminal_F, Is().True()); }); - it("computes +{{0}} == {{0}} [zdd&] with {0,1} domain", [&]() { - const std::vector dom = { 0, 1 }; - domain_set(dom.begin(), dom.end()); - + it("computes +{{0}} == {{0}} [zdd&]", [&]() { AssertThat(+x0 == x0, Is().True()); }); - it("computes +{{0}} == {{0}} [__zdd&&] with {0,1} domain", [&]() { - const std::vector dom = { 0, 1 }; - domain_set(dom.begin(), dom.end()); - + it("computes +{{0}} == {{0}} [__zdd&&]", [&]() { AssertThat(+(x0 & x0_or_x1) == x0, Is().True()); }); @@ -273,21 +267,59 @@ go_bandit([]() { AssertThat(A, Is().EqualTo(x0_or_x1)); }); - // TODO: Multiply - }); + it("computes {{0}} * {{0},{1}} == {{0}}", + [&]() { AssertThat((x0 * x0_or_x1) == x0, Is().True()); }); - it("computes with __zdd&& operators [|,&,-]", [&]() { - zdd out = ((x0_or_x1 - x0) | ((x0 | x1) & (x0_or_x1 - x1))) - (x0_or_x1 - x0); - AssertThat(x0, Is().EqualTo(out)); - }); + it("accumulates with '*=(zdd&)' operator", [&]() { + zdd A = x0_or_x1; + A *= x0; + AssertThat(A, Is().EqualTo(x0)); - it("computes with __zdd&& operators [|,~,-,]", [&]() { - const std::vector dom = { 0, 1 }; - domain_set(dom.begin(), dom.end()); + A *= x1; + AssertThat(A, Is().EqualTo(terminal_F)); + }); - zdd out = ~(~(x0 | x1) - terminal_T); - zdd expected = x0 | x1 | terminal_T; - AssertThat(expected, Is().EqualTo(out)); + it("computes with __zdd&& operators [*]", [&]() { + const zdd A = (x0 * (x0_or_x1 & x0)) & x1; + AssertThat(A, Is().EqualTo(terminal_F)); + }); + + it("accumulates with '+=(__zdd&&)' and '*=(__zdd&&)'", [&]() { + zdd A = x0; + + A += x0_or_x1 & x1; + AssertThat(A, Is().EqualTo(x0_or_x1)); + + A *= x0_or_x1 & x1; + AssertThat(A, Is().EqualTo(x1)); + }); + + it("computes with __zdd&& operators [+,*]", [&]() { + const zdd A = ((x0_or_x1 + x0) + ((x0 * x1) + x1)) * x0; + AssertThat(A, Is().EqualTo(x0)); + }); + + it("computes with __zdd&& operators [-]", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); + + const zdd A = -(x0 | x1); + AssertThat(-x0_or_x1 == A, Is().True()); + }); + + it("computes with __zdd&& operators [|,-,]", [&]() { + const std::vector dom = { 0, 1 }; + domain_set(dom.begin(), dom.end()); + + const zdd out = -(-(x0 | x1) - terminal_T); + const zdd expected = x0 | x1 | terminal_T; + AssertThat(expected, Is().EqualTo(out)); + }); + + it("computes with __zdd&& operators [-,+,*]", [&]() { + const zdd A = ((x0_or_x1 - x0) + ((x0 + x1) * (x0_or_x1 + x1))) - (x0_or_x1 - x0); + AssertThat(x0, Is().EqualTo(A)); + }); }); describe("==, !=", [&]() { From 59832cbff839b42e33663489234a5bd1b3219f63 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 30 May 2024 16:13:21 +0200 Subject: [PATCH 10/10] Format latest changes --- src/adiar/bdd/bdd.cpp | 28 ++++++++--------- src/adiar/zdd/zdd.cpp | 2 +- test/adiar/zdd/test_zdd.cpp | 60 ++++++++++++------------------------- 3 files changed, 34 insertions(+), 56 deletions(-) diff --git a/src/adiar/bdd/bdd.cpp b/src/adiar/bdd/bdd.cpp index 157541573..47e1d2cc4 100644 --- a/src/adiar/bdd/bdd.cpp +++ b/src/adiar/bdd/bdd.cpp @@ -55,20 +55,20 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// // Operators -#define __BDD_OPER(out_t, op) \ - out_t operator op(__bdd&& lhs, __bdd&& rhs) \ - { \ - return bdd(std::move(lhs)) op bdd(std::move(rhs)); \ - } \ - \ - out_t operator op(const bdd& lhs, __bdd&& rhs) \ - { \ - return lhs op bdd(std::move(rhs)); \ - } \ - \ - out_t operator op(__bdd&& lhs, const bdd& rhs) \ - { \ - return bdd(std::move(lhs)) op rhs; \ +#define __BDD_OPER(out_t, op) \ + out_t operator op(__bdd&& lhs, __bdd&& rhs) \ + { \ + return bdd(std::move(lhs)) op bdd(std::move(rhs)); \ + } \ + \ + out_t operator op(const bdd& lhs, __bdd&& rhs) \ + { \ + return lhs op bdd(std::move(rhs)); \ + } \ + \ + out_t operator op(__bdd&& lhs, const bdd& rhs) \ + { \ + return bdd(std::move(lhs)) op rhs; \ } ////////////////////////////////////////////////////////////////////////////// diff --git a/src/adiar/zdd/zdd.cpp b/src/adiar/zdd/zdd.cpp index 3fbd3bd7b..bab9075e0 100644 --- a/src/adiar/zdd/zdd.cpp +++ b/src/adiar/zdd/zdd.cpp @@ -85,7 +85,7 @@ namespace adiar // Operators (Assignment) zdd& - zdd::operator=(const zdd & other) + zdd::operator=(const zdd& other) { this->negate = other.negate; this->file = other.file; diff --git a/test/adiar/zdd/test_zdd.cpp b/test/adiar/zdd/test_zdd.cpp index 4fa5e4f72..06b7bb25e 100644 --- a/test/adiar/zdd/test_zdd.cpp +++ b/test/adiar/zdd/test_zdd.cpp @@ -100,8 +100,7 @@ go_bandit([]() { describe("operators", [&]() { describe("==, !=", [&]() { - it("rejects Ø == {Ø}", - [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); }); + it("rejects Ø == {Ø}", [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); }); it("accepts {{0}} == {{0}} (different files)", [&]() { shared_levelized_file other_nf; @@ -114,13 +113,9 @@ go_bandit([]() { AssertThat(x0, Is().EqualTo(other)); }); - it("rejects {{0}} == {{1}}", [&]() { - AssertThat(x0, Is().Not().EqualTo(x1)); - }); + it("rejects {{0}} == {{1}}", [&]() { AssertThat(x0, Is().Not().EqualTo(x1)); }); - it("rejects {{0}, {1}} == {{0}}", [&]() { - AssertThat(x0_or_x1, Is().Not().EqualTo(x0)); - }); + it("rejects {{0}, {1}} == {{0}}", [&]() { AssertThat(x0_or_x1, Is().Not().EqualTo(x0)); }); }); describe("~, &, |", [&]() { @@ -242,13 +237,10 @@ go_bandit([]() { AssertThat(A == terminal_F, Is().True()); }); - it("computes +{{0}} == {{0}} [zdd&]", [&]() { - AssertThat(+x0 == x0, Is().True()); - }); + it("computes +{{0}} == {{0}} [zdd&]", [&]() { AssertThat(+x0 == x0, Is().True()); }); - it("computes +{{0}} == {{0}} [__zdd&&]", [&]() { - AssertThat(+(x0 & x0_or_x1) == x0, Is().True()); - }); + it("computes +{{0}} == {{0}} [__zdd&&]", + [&]() { AssertThat(+(x0 & x0_or_x1) == x0, Is().True()); }); it("computes {{0}} + {{1}} == {{0}, {1}}", [&]() { AssertThat((x0 + x1) == x0_or_x1, Is().True()); }); @@ -323,21 +315,17 @@ go_bandit([]() { }); describe("==, !=", [&]() { - it("checks two derivations of same __bdd&& [==]", [&]() { - AssertThat((x0 | x1) == ((x0_or_x1 - x1) | x1), Is().True()); - }); + it("checks two derivations of same __bdd&& [==]", + [&]() { AssertThat((x0 | x1) == ((x0_or_x1 - x1) | x1), Is().True()); }); - it("checks two derivations of same __bdd&& [!=]", [&]() { - AssertThat((x0 | x1) != ((x0_or_x1 - x1) | x1), Is().False()); - }); + it("checks two derivations of same __bdd&& [!=]", + [&]() { AssertThat((x0 | x1) != ((x0_or_x1 - x1) | x1), Is().False()); }); - it("checks two derivations of different __bdd&& [==]", [&]() { - AssertThat((x0 | x1) == (x0_or_x1 - x1), Is().False()); - }); + it("checks two derivations of different __bdd&& [==]", + [&]() { AssertThat((x0 | x1) == (x0_or_x1 - x1), Is().False()); }); - it("checks two derivations of different __bdd&& [!=]", [&]() { - AssertThat((x0 | x1) != (x0_or_x1 - x1), Is().True()); - }); + it("checks two derivations of different __bdd&& [!=]", + [&]() { AssertThat((x0 | x1) != (x0_or_x1 - x1), Is().True()); }); }); describe("<, <=, >, >=", [&]() { @@ -346,9 +334,7 @@ go_bandit([]() { AssertThat(x0 < (x0 | x1), Is().True()); }); - it("checks {{0}} < {{1}}", [&]() { - AssertThat(x0 < x1, Is().False()); - }); + it("checks {{0}} < {{1}}", [&]() { AssertThat(x0 < x1, Is().False()); }); it("checks {{0}, {1}} < {{0}, {1}}", [&]() { AssertThat((x0 | x1) < x0_or_x1, Is().False()); @@ -366,17 +352,11 @@ go_bandit([]() { AssertThat((x0 | x1) <= (x0 | x1), Is().True()); }); - it("checks {{0}} <= {{1}}", [&]() { - AssertThat(x0 <= x1, Is().False()); - }); + it("checks {{0}} <= {{1}}", [&]() { AssertThat(x0 <= x1, Is().False()); }); - it("checks {{0}, {1}} > {{0}}", [&]() { - AssertThat(x0_or_x1 > x0, Is().True()); - }); + it("checks {{0}, {1}} > {{0}}", [&]() { AssertThat(x0_or_x1 > x0, Is().True()); }); - it("checks {{0}} > {{1}}", [&]() { - AssertThat(x0 > x1, Is().False()); - }); + it("checks {{0}} > {{1}}", [&]() { AssertThat(x0 > x1, Is().False()); }); it("checks {{0}, {1}} > {{0}, {1}}", [&]() { AssertThat((x0 | x1) > x0_or_x1, Is().False()); @@ -384,9 +364,7 @@ go_bandit([]() { AssertThat((x0 | x1) > (x0 | x1), Is().False()); }); - it("checks {{0}, {1}} >= {{0}}", [&]() { - AssertThat(x0_or_x1 >= x0, Is().True()); - }); + it("checks {{0}, {1}} >= {{0}}", [&]() { AssertThat(x0_or_x1 >= x0, Is().True()); }); it("checks {{0}, {1}} >= {{0}, {1}}", [&]() { AssertThat((x0 | x1) >= x0_or_x1, Is().True());