From 2f3942c806fe31cdd272a5fcc027a79ebb5916db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Tue, 5 Mar 2024 16:58:19 +0100 Subject: [PATCH] Add compile-time 'xnor_op' to expose code-pruning to the compiler --- src/adiar/bdd/apply.cpp | 6 ++- src/adiar/internal/bool_op.h | 70 ++++++++++++++++++++++++ test/adiar/internal/test_bool_op.cpp | 79 ++++++++++++++++++++++++++++ 3 files changed, 153 insertions(+), 2 deletions(-) diff --git a/src/adiar/bdd/apply.cpp b/src/adiar/bdd/apply.cpp index 856765fe2..4f835093e 100644 --- a/src/adiar/bdd/apply.cpp +++ b/src/adiar/bdd/apply.cpp @@ -223,7 +223,8 @@ namespace adiar __bdd bdd_xnor(const exec_policy& ep, const bdd& f, const bdd& g) { - return bdd_apply(ep, f, g, xnor_op); + apply_prod2_policy policy; + return internal::prod2(ep, f, g, policy); } __bdd @@ -259,7 +260,8 @@ namespace adiar __bdd bdd_equiv(const exec_policy& ep, const bdd& f, const bdd& g) { - return bdd_apply(ep, f, g, equiv_op); + apply_prod2_policy policy; + return internal::prod2(ep, f, g, policy); } __bdd diff --git a/src/adiar/internal/bool_op.h b/src/adiar/internal/bool_op.h index 7dc01245d..359bda5c6 100644 --- a/src/adiar/internal/bool_op.h +++ b/src/adiar/internal/bool_op.h @@ -641,6 +641,76 @@ namespace adiar::internal return is_negating(p.value()); } }; + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Alternative for `binary_op` hardcoded for a logical 'xnor'. + /// + /// \details The benefit of this over `binary_op` is to skip pre-computations and to expose + /// optimisations and simplifications to the compiler. + ////////////////////////////////////////////////////////////////////////////////////////////////// + class xnor_op + : public commutative_op + { + //////////////////////////////////////////////////////////////////////////////////////////////// + public: + bool + operator ()(const bool lhs, const bool rhs) const + { + return !(lhs ^ rhs); + } + + template + Pointer + operator ()(const Pointer& lhs, const Pointer& rhs) const + { + return !(lhs ^ rhs); + } + + //////////////////////////////////////////////////////////////////////////////////////////////// + protected: + friend commutative_op; + + template + static constexpr bool + can_shortcut(const T&/*t*/) + { + return false; + } + + static constexpr bool + is_idempotent(const bool p) + { + return p; + } + + template + static bool + is_idempotent(const Pointer& p) + { + return is_idempotent(p.value()); + } + + static constexpr bool + is_negating(const bool p) + { + return !p; + } + + template + static constexpr bool + is_negating(const Pointer& p) + { + return is_negating(p.value()); + } + }; + + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Alternative for `binary_op` hardcoded for a logical 'equiv'. + /// + /// \details The benefit of this over `binary_op` is to skip pre-computations and to expose + /// optimisations and simplifications to the compiler. + ////////////////////////////////////////////////////////////////////////////////////////////////// + using equiv_op = xnor_op; } #endif // ADIAR_INTERNAL_BOOL_OP_H diff --git a/test/adiar/internal/test_bool_op.cpp b/test/adiar/internal/test_bool_op.cpp index f03b420ef..17e5dacda 100644 --- a/test/adiar/internal/test_bool_op.cpp +++ b/test/adiar/internal/test_bool_op.cpp @@ -46,6 +46,14 @@ go_bandit([]() { AssertThat(can_right_shortcut(adiar::xor_op, true), Is().False()); }); + it("is correct for 'adiar::xnor_op'", []() { + AssertThat(can_left_shortcut(adiar::xnor_op, false), Is().False()); + AssertThat(can_left_shortcut(adiar::xnor_op, true), Is().False()); + + AssertThat(can_right_shortcut(adiar::xnor_op, false), Is().False()); + AssertThat(can_right_shortcut(adiar::xnor_op, true), Is().False()); + }); + it("is correct for 'adiar::imp_op'", []() { AssertThat(can_left_shortcut(adiar::imp_op, false), Is().True()); AssertThat(can_left_shortcut(adiar::imp_op, true), Is().False()); @@ -104,6 +112,14 @@ go_bandit([]() { AssertThat(is_right_idempotent(adiar::xor_op, true), Is().False()); }); + it("is correct for 'adiar::xnor_op'", []() { + AssertThat(is_left_idempotent(adiar::xnor_op, false), Is().False()); + AssertThat(is_left_idempotent(adiar::xnor_op, true), Is().True()); + + AssertThat(is_right_idempotent(adiar::xnor_op, false), Is().False()); + AssertThat(is_right_idempotent(adiar::xnor_op, true), Is().True()); + }); + it("is correct for 'adiar::imp_op'", []() { AssertThat(is_left_idempotent(adiar::imp_op, false), Is().False()); AssertThat(is_left_idempotent(adiar::imp_op, true), Is().True()); @@ -162,6 +178,14 @@ go_bandit([]() { AssertThat(is_right_negating(adiar::xor_op, true), Is().True()); }); + it("is correct for 'adiar::xnor_op'", []() { + AssertThat(is_left_negating(adiar::xnor_op, false), Is().True()); + AssertThat(is_left_negating(adiar::xnor_op, true), Is().False()); + + AssertThat(is_right_negating(adiar::xnor_op, false), Is().True()); + AssertThat(is_right_negating(adiar::xnor_op, true), Is().False()); + }); + it("is correct for 'adiar::imp_op'", []() { AssertThat(is_left_negating(adiar::imp_op, false), Is().False()); AssertThat(is_left_negating(adiar::imp_op, true), Is().False()); @@ -894,5 +918,60 @@ go_bandit([]() { AssertThat(op.is_commutative(), Is().True()); }); }); + + describe("xnor_op, equiv_op", []() { + const adiar::internal::xnor_op op; + + constexpr ptr_uint64 ptr_false(false); + constexpr ptr_uint64 ptr_true(true); + + it("operator() (const bool, const bool)", [&]() { + AssertThat(op(false, false), Is().EqualTo(true)); + AssertThat(op(false, true), Is().EqualTo(false)); + AssertThat(op(true, false), Is().EqualTo(false)); + AssertThat(op(true, true), Is().EqualTo(true)); + }); + + it("operator() (const Pointer&, const Pointer&)", [&]() { + AssertThat(op(ptr_false, ptr_false), Is().EqualTo(ptr_true)); + AssertThat(op(ptr_false, ptr_true), Is().EqualTo(ptr_false)); + AssertThat(op(ptr_true, ptr_false), Is().EqualTo(ptr_false)); + AssertThat(op(ptr_true, ptr_true), Is().EqualTo(ptr_true)); + }); + + it(".can_left_shortcut(const Pointer&)", [&]() { + AssertThat(op.can_left_shortcut(ptr_false), Is().False()); + AssertThat(op.can_left_shortcut(ptr_true), Is().False()); + }); + + it(".can_right_shortcut(const Pointer&)", [&]() { + AssertThat(op.can_right_shortcut(ptr_false), Is().False()); + AssertThat(op.can_right_shortcut(ptr_true), Is().False()); + }); + + it(".is_left_idempotent(const Pointer&)", [&]() { + AssertThat(op.is_left_idempotent(ptr_false), Is().False()); + AssertThat(op.is_left_idempotent(ptr_true), Is().True()); + }); + + it(".is_right_idempotent(const Pointer&)", [&]() { + AssertThat(op.is_right_idempotent(ptr_false), Is().False()); + AssertThat(op.is_right_idempotent(ptr_true), Is().True()); + }); + + it(".is_left_negating(const Pointer&)", [&]() { + AssertThat(op.is_left_negating(ptr_false), Is().True()); + AssertThat(op.is_left_negating(ptr_true), Is().False()); + }); + + it(".is_right_negating(const Pointer&)", [&]() { + AssertThat(op.is_right_negating(ptr_false), Is().True()); + AssertThat(op.is_right_negating(ptr_true), Is().False()); + }); + + it(".is_commutative()", [&]() { + AssertThat(op.is_commutative(), Is().True()); + }); + }); }); });