diff --git a/src/adiar/internal/algorithms/quantify.h b/src/adiar/internal/algorithms/quantify.h index 4ef0d2aea..a09f1585e 100644 --- a/src/adiar/internal/algorithms/quantify.h +++ b/src/adiar/internal/algorithms/quantify.h @@ -1418,7 +1418,7 @@ namespace adiar::internal }; ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Obtain the deepest level that satisfies (or not) the requested level. + /// \brief Obtain statistics on the variables in a Decision Diagram satisfying the predicate. ////////////////////////////////////////////////////////////////////////////////////////////////// template inline quantify__pred_profile @@ -1557,7 +1557,7 @@ namespace adiar::internal unreduced_t transposed; - // If transposition__max_iterations is 0, then only quantify the lowest level (with pruning). + // If transposition__max_iterations is 0, then only prune quantified levels. if (transposition__max_iterations == 0) { // Singleton Quantification of bottom-most level #ifdef ADIAR_STATS diff --git a/src/adiar/internal/algorithms/select.h b/src/adiar/internal/algorithms/select.h index 79a5c67c4..70fcdfe88 100644 --- a/src/adiar/internal/algorithms/select.h +++ b/src/adiar/internal/algorithms/select.h @@ -21,12 +21,12 @@ namespace adiar::internal { - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // Select Algorithm // ================== // - // Given a Decision Diagram, a subset of the levels are removed and bridged - // over in either the 'high' or the 'low' direction. + // Given a Decision Diagram, a subset of the levels are removed and bridged over in either the + // 'high' or the 'low' direction. /* // _( )_ ---- xi _( )_ ---- xi // / \ / \ @@ -36,18 +36,17 @@ namespace adiar::internal */ // Examples of uses are `bdd_restrict` and `zdd_onset` / `zdd_offset` // - // As such, this is merely a niche-case of the Intercut algorithm, where the - // *onset* levels are removed and bridged over in a uniform direction (and the - // edges crossing said level only have suppressed nodes added). Yet compared - // to the Intercut algorithm, this implementation is optimised both in terms - // of time and space. - ////////////////////////////////////////////////////////////////////////////// - - ////////////////////////////////////////////////////////////////////////////// + // As such, this is merely a niche-case of the Intercut algorithm, where the *onset* levels are + // removed and bridged over in a uniform direction (and the edges crossing said level only have + // suppressed nodes added). Yet compared to the Intercut algorithm, this implementation is + // optimised both in terms of time and space. + ////////////////////////////////////////////////////////////////////////////////////////////////// + + ////////////////////////////////////////////////////////////////////////////////////////////////// /// Struct to hold statistics extern statistics::select_t stats_select; - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // Data Structures using select_request = request_data<1, with_parent>; @@ -60,11 +59,10 @@ namespace adiar::internal 1u, 0u>; - /// Return a desired `node` to be output or a `node::pointer_type` to skip to - /// one of its children. + /// Return a desired `node` to be output or a `node::pointer_type` to skip to one of its children. using select_rec = std::variant; - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// // Helper functions template inline void @@ -80,7 +78,7 @@ namespace adiar::internal } } - ////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////////////////////// template typename Policy::__dd_type __select(const exec_policy& ep, @@ -192,12 +190,11 @@ namespace adiar::internal typename Policy::__dd_type select(const exec_policy& ep, const typename Policy::dd_type& dd, Policy& policy) { - // Compute amount of memory available for auxiliary data structures after - // having opened all streams. + // Compute amount of memory available for auxiliary data structures after having opened all + // streams. // - // We then may derive an upper bound on the size of auxiliary data - // structures and check whether we can run them with a faster internal - // memory variant. + // We then may derive an upper bound on the size of auxiliary data structures and check whether + // we can run them with a faster internal memory variant. const tpie::memory_size_type aux_available_memory = memory_available() - node_stream<>::memory_usage() - arc_writer::memory_usage(); diff --git a/src/adiar/internal/data_types/ptr.h b/src/adiar/internal/data_types/ptr.h index 5bedd4f5c..7fb8fefa2 100644 --- a/src/adiar/internal/data_types/ptr.h +++ b/src/adiar/internal/data_types/ptr.h @@ -818,8 +818,8 @@ namespace adiar::internal inline ptr_uint64 cnot(const ptr_uint64& p, const bool negate) { - const ptr_uint64::raw_type shifted_negate = - static_cast(negate) << ptr_uint64::data_shift; + const ptr_uint64::raw_type shifted_negate = static_cast(negate) + << ptr_uint64::data_shift; return p.is_terminal() ? p._raw ^ shifted_negate : p._raw; } @@ -870,18 +870,19 @@ namespace adiar::internal inline ptr_uint64 shift_replace(const ptr_uint64& p, const ptr_uint64::signed_level_type levels) { - // Evil type hacks (Thanks, Quake III) + // Evil type hack to obtain `p.level()` as a signed integer (Thanks, Quake III) const ptr_uint64::level_type p_level__unsigned = p.level(); const ptr_uint64::signed_level_type p_level__signed = - (*reinterpret_cast(&p_level__unsigned)); + (*reinterpret_cast(&p_level__unsigned)); + // Evil type hack to obtain `p.level() + levels` as an unsigned integer (Thanks, Quake III) const ptr_uint64::signed_level_type p_new_level__signed = p_level__signed + levels; const ptr_uint64::level_type p_new_level__unsigned = - (*reinterpret_cast(&p_new_level__signed)); + (*reinterpret_cast(&p_new_level__signed)); // Shift levels back and combine with other bits - const ptr_uint64::raw_type level_bits = - static_cast(p_new_level__unsigned) << ptr_uint64::level_shift; + const ptr_uint64::raw_type level_bits = static_cast(p_new_level__unsigned) + << ptr_uint64::level_shift; constexpr ptr_uint64::raw_type non_levels_mask = ~(static_cast(ptr_uint64::max_level) << ptr_uint64::level_shift); diff --git a/test/adiar/bdd/test_negate.cpp b/test/adiar/bdd/test_negate.cpp index fba7d6118..48f75ed0e 100644 --- a/test/adiar/bdd/test_negate.cpp +++ b/test/adiar/bdd/test_negate.cpp @@ -73,89 +73,105 @@ go_bandit([]() { bdd bdd_2(bdd_2_nf); - it("should doube-negate a T terminal-only BDD back into a T terminal-only BDD", [&]() { - bdd out = bdd_not(bdd_not(terminal_T)); - - // Check if it is correct - node_test_stream ns(out); + describe("bdd_not(const bdd&)", [&]() { + it("negates a T terminal BDD into an F terminal BDD", [&]() { + bdd out = bdd_not(terminal_T); - AssertThat(ns.can_pull(), Is().True()); - AssertThat(ns.pull(), Is().EqualTo(node(true))); - AssertThat(ns.can_pull(), Is().False()); - }); + // Check if it is correct + node_test_stream ns(out); - it("should doube-negate an F terminal-only BDD back into an F terminal-only BDD", [&]() { - bdd out = bdd_not(bdd_not(terminal_T)); + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), Is().EqualTo(node(false))); + AssertThat(ns.can_pull(), Is().False()); + }); - // Check if it is correct - node_test_stream ns(out); + it("double-negates T terminal BDD back into T terminal", [&]() { + bdd temp = bdd_not(bdd_1); + bdd out = bdd_not(temp); - AssertThat(ns.can_pull(), Is().True()); - AssertThat(ns.pull(), Is().EqualTo(node(true))); - AssertThat(ns.can_pull(), Is().False()); - }); + // Check if it is correct + node_test_stream ns(out); - it("should double-negate terminal-children in BDD 1 back to the original", [&]() { - // Checkmate, constructivists... + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_F_ptr, terminal_T_ptr))); - bdd out = bdd_not(bdd_not(bdd_1)); + AssertThat(ns.can_pull(), Is().True()); + AssertThat( + ns.pull(), + Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_T_ptr))); - // Check if it is correct - node_test_stream ns(out); + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), + Is().EqualTo(node(0, + node::max_id, + ptr_uint64(2, ptr_uint64::max_id), + ptr_uint64(1, ptr_uint64::max_id)))); - AssertThat(ns.can_pull(), Is().True()); - AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_F_ptr, terminal_T_ptr))); + AssertThat(ns.can_pull(), Is().False()); + }); - AssertThat(ns.can_pull(), Is().True()); - AssertThat( - ns.pull(), - Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_T_ptr))); + it("negates a F terminal BDD into an T terminal BDD", [&]() { + bdd out = bdd_not(terminal_F); - AssertThat(ns.can_pull(), Is().True()); - AssertThat( - ns.pull(), - Is().EqualTo(node( - 0, node::max_id, ptr_uint64(2, ptr_uint64::max_id), ptr_uint64(1, ptr_uint64::max_id)))); + // Check if it is correct + node_test_stream ns(out); - AssertThat(ns.can_pull(), Is().False()); - }); + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), Is().EqualTo(node(true))); + AssertThat(ns.can_pull(), Is().False()); + }); - describe("bdd_not(const &)", [&]() { - it("should negate a T terminal-only BDD into an F terminal-only BDD", [&]() { - bdd out = bdd_not(terminal_T); + it("double-negates F terminal BDD back into F terminal", [&]() { + bdd temp = bdd_not(terminal_F); + bdd out = bdd_not(temp); // Check if it is correct node_test_stream ns(out); AssertThat(ns.can_pull(), Is().True()); AssertThat(ns.pull(), Is().EqualTo(node(false))); + AssertThat(ns.can_pull(), Is().False()); }); - it("should negate a F terminal-only BDD into an T terminal-only BDD", [&]() { - bdd out = bdd_not(terminal_F); + it("negates terminal-children in BDD 1", [&]() { + bdd out = bdd_not(bdd_1); // Check if it is correct node_test_stream ns(out); AssertThat(ns.can_pull(), Is().True()); - AssertThat(ns.pull(), Is().EqualTo(node(true))); + AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_T_ptr, terminal_F_ptr))); + + AssertThat(ns.can_pull(), Is().True()); + AssertThat( + ns.pull(), + Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_F_ptr))); + + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), + Is().EqualTo(node(0, + node::max_id, + ptr_uint64(2, ptr_uint64::max_id), + ptr_uint64(1, ptr_uint64::max_id)))); + AssertThat(ns.can_pull(), Is().False()); }); - it("should negate terminal-children in BDD 1", [&]() { - bdd out = bdd_not(bdd_1); + it("unnegates terminal-children in negated BDD 1", [&]() { + bdd temp(bdd_1_nf, true); + bdd out = bdd_not(temp); // Check if it is correct node_test_stream ns(out); AssertThat(ns.can_pull(), Is().True()); - AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_T_ptr, terminal_F_ptr))); + AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_F_ptr, terminal_T_ptr))); AssertThat(ns.can_pull(), Is().True()); AssertThat( ns.pull(), - Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_F_ptr))); + Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_T_ptr))); AssertThat(ns.can_pull(), Is().True()); AssertThat(ns.pull(), @@ -167,7 +183,7 @@ go_bandit([]() { AssertThat(ns.can_pull(), Is().False()); }); - it("should double-negate terminal-children in BDD 1 back to the original", [&]() { + it("double-negates terminal-children in BDD 1 back to the original", [&]() { bdd temp = bdd_not(bdd_1); bdd out = bdd_not(temp); @@ -192,7 +208,7 @@ go_bandit([]() { AssertThat(ns.can_pull(), Is().False()); }); - it("should negate terminal-children in BDD 2", [&]() { + it("negates terminal-children in BDD 2", [&]() { bdd out = bdd_not(bdd_2_nf); node_test_stream ns(out); @@ -221,8 +237,8 @@ go_bandit([]() { }); }); - describe("bdd_not(&&)", [&]() { - it("should negate a T terminal-only BDD into an F terminal-only BDD", [&]() { + describe("bdd_not(bdd&&)", [&]() { + it("negates a T terminal into an F terminal", [&]() { bdd out = bdd_not(terminal_T_nf); // Check if it is correct @@ -233,7 +249,18 @@ go_bandit([]() { AssertThat(ns.can_pull(), Is().False()); }); - it("should negate a F terminal-only BDD into an T terminal-only BDD", [&]() { + it("double-negates a T terminal back into a T terminal", [&]() { + bdd out = bdd_not(bdd_not(terminal_T)); + + // Check if it is correct + node_test_stream ns(out); + + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), Is().EqualTo(node(true))); + AssertThat(ns.can_pull(), Is().False()); + }); + + it("negates a F terminal into an T terminal", [&]() { bdd out = bdd_not(terminal_F); // Check if it is correct @@ -244,7 +271,18 @@ go_bandit([]() { AssertThat(ns.can_pull(), Is().False()); }); - it("should negate terminal-children in BDD 1", [&]() { + it("double-negates an F terminal back into an F terminal", [&]() { + bdd out = bdd_not(bdd_not(terminal_F)); + + // Check if it is correct + node_test_stream ns(out); + + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), Is().EqualTo(node(false))); + AssertThat(ns.can_pull(), Is().False()); + }); + + it("negates terminal-children in BDD 1", [&]() { bdd out = bdd_not(bdd_1_nf); // Check if it is correct @@ -268,7 +306,33 @@ go_bandit([]() { AssertThat(ns.can_pull(), Is().False()); }); - it("should negate terminal-children in BDD 2", [&]() { + it("double-negates terminal-children in BDD 1 back to the original", [&]() { + // Checkmate, constructivists... + + bdd out = bdd_not(bdd_not(bdd_1)); + + // Check if it is correct + node_test_stream ns(out); + + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_F_ptr, terminal_T_ptr))); + + AssertThat(ns.can_pull(), Is().True()); + AssertThat( + ns.pull(), + Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_T_ptr))); + + AssertThat(ns.can_pull(), Is().True()); + AssertThat(ns.pull(), + Is().EqualTo(node(0, + node::max_id, + ptr_uint64(2, ptr_uint64::max_id), + ptr_uint64(1, ptr_uint64::max_id)))); + + AssertThat(ns.can_pull(), Is().False()); + }); + + it("negates terminal-children in BDD 2", [&]() { bdd out = bdd_not(bdd_2_nf); node_test_stream ns(out);