From 9542de2c8067d375c866835101e540f75d6780ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 19 Jun 2024 16:43:09 +0200 Subject: [PATCH] Add O(1) shifting case to 'bdd_replace' --- src/adiar/bdd/relprod.cpp | 1 + src/adiar/internal/algorithms/replace.h | 46 +- src/adiar/statistics.h | 6 + src/adiar/types.h | 9 +- test/adiar/bdd/test_relprod.cpp | 3569 ++++++++++++++++------- test/adiar/bdd/test_replace.cpp | 592 +++- 6 files changed, 3082 insertions(+), 1141 deletions(-) diff --git a/src/adiar/bdd/relprod.cpp b/src/adiar/bdd/relprod.cpp index 3ddb7a59c..8063d7236 100644 --- a/src/adiar/bdd/relprod.cpp +++ b/src/adiar/bdd/relprod.cpp @@ -307,6 +307,7 @@ namespace adiar throw invalid_argument("Non-monotonic variable replacement not (yet) supported."); case replace_type::Monotone: + case replace_type::Shift: case replace_type::Identity: #ifdef ADIAR_STATS internal::stats_replace.monotonic_reduces += 1u; diff --git a/src/adiar/internal/algorithms/replace.h b/src/adiar/internal/algorithms/replace.h index fb73fd290..9472c4132 100644 --- a/src/adiar/internal/algorithms/replace.h +++ b/src/adiar/internal/algorithms/replace.h @@ -10,6 +10,7 @@ #include #include +#include #include #include #include @@ -60,8 +61,9 @@ namespace adiar::internal replace_type __replace__infer_type(LevelInfoStream& ls, const ReplaceFunction& m) { - using label_type = typename Policy::label_type; - using result_type = typename ReplaceFunction::result_type; + using label_type = typename Policy::label_type; + using signed_label_type = typename Policy::signed_label_type; + using result_type = typename ReplaceFunction::result_type; constexpr bool is_total_map = is_same; constexpr bool is_partial_map = is_same>; @@ -69,10 +71,14 @@ namespace adiar::internal static_assert(is_total_map || is_partial_map); bool identity = true; + bool shift = true; bool monotone = true; label_type prev_before = Policy::max_label + 1; label_type prev_after = Policy::max_label + 1; + + signed_label_type prev_diff = 0; + while (ls.can_pull()) { const label_type next_before = ls.pull().level(); const result_type next_after_opt = m(next_before); @@ -89,6 +95,14 @@ namespace adiar::internal next_after = next_after_opt; } + if (shift) { + const signed_label_type next_diff = + static_cast(next_before) - static_cast(next_after); + + shift &= Policy::max_label < prev_before || prev_diff == next_diff; + prev_diff = next_diff; + } + identity &= next_before == next_after; monotone &= Policy::max_label < prev_before || prev_after < next_after; @@ -97,13 +111,32 @@ namespace adiar::internal } if (!monotone) { return replace_type::Non_Monotone; } - if (!identity) { return replace_type::Monotone; } + if (!shift) { return replace_type::Monotone; } + if (!identity) { return replace_type::Shift; } return replace_type::Identity; } ////////////////////////////////////////////////////////////////////////////////////////////////// // Algorithms + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Replace the level in constant time + /// + /// \remark This requires that the mapping, `m`, is *monotonic*. + ////////////////////////////////////////////////////////////////////////////////////////////////// + template + inline typename Policy::dd_type + __replace__shift_return(const typename Policy::dd_type& dd, const replace_func& m) + { + adiar_assert(!dd->is_terminal()); + + const typename Policy::signed_label_type topvar = dd_topvar(dd); + const typename Policy::signed_label_type shifted_topvar = m(topvar); + + return typename Policy::dd_type( + dd.file_ptr(), dd.is_negated(), dd.shift() + (shifted_topvar - topvar)); + } + ////////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Replace the level of all nodes in a single linear scan. /// @@ -211,6 +244,12 @@ namespace adiar::internal #endif return __replace__monotonic_scan(dd, m); + case replace_type::Shift: +#ifdef ADIAR_STATS + stats_replace.shift_returns += 1u; +#endif + return __replace__shift_return(dd, m); + case replace_type::Identity: #ifdef ADIAR_STATS stats_replace.identity_returns += 1u; @@ -263,6 +302,7 @@ namespace adiar::internal throw invalid_argument("Non-monotonic variable replacement not (yet) supported."); case replace_type::Monotone: + case replace_type::Shift: #ifdef ADIAR_STATS stats_replace.monotonic_reduces += 1u; #endif diff --git a/src/adiar/statistics.h b/src/adiar/statistics.h index 1ca27b8fb..207d3bcce 100644 --- a/src/adiar/statistics.h +++ b/src/adiar/statistics.h @@ -546,6 +546,12 @@ namespace adiar //////////////////////////////////////////////////////////////////////////////////////////// uintwide identity_reduces = 0; + //////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of runs using 0 I/Os due to the variables are replaced according to a + /// simple linear shift. + //////////////////////////////////////////////////////////////////////////////////////////// + uintwide shift_returns = 0; + //////////////////////////////////////////////////////////////////////////////////////////// /// \brief Number of runs using a 2N/B linear copy-paste. //////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/adiar/types.h b/src/adiar/types.h index f296223fe..bcffb3f64 100644 --- a/src/adiar/types.h +++ b/src/adiar/types.h @@ -36,12 +36,11 @@ namespace adiar /** For any `x < y` then the mapped values preserve that order, i.e. `m(x) < m(y)`. */ Monotone = 2, - /* TODO (constant time variable replacement): `m(x)` is of the form `ax + b` for a positive - fraction `a` and integer `b`. */ - // Affine = 1, + /* TODO (faster version of 'Monotone'): `m(x) = ax + b` for some integers `a` and `b`. */ + // Affine = 1, - /* TODO (faster version of 'Affine'): `m(x)` is of the form `x + b` for an integer `b`. */ - // Shift = 0, + /** (faster version of 'Monotone'): `m(x) = x + b` for an integer `b`. */ + Shift = 0, /** Nothing needs to be done, as `m(x) = x`. */ Identity = -1 diff --git a/test/adiar/bdd/test_relprod.cpp b/test/adiar/bdd/test_relprod.cpp index 85f2c5607..b40cc90d6 100644 --- a/test/adiar/bdd/test_relprod.cpp +++ b/test/adiar/bdd/test_relprod.cpp @@ -4707,10 +4707,1557 @@ go_bandit([]() { }); }); - describe("bdd_relnext(const bdd&, const bdd&, , replace_type)", [&]() { - it("has single successor [{00} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relnext(kalin_00, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + describe( + "bdd_relnext(const bdd&, const bdd&, , replace_type::Non_Monotone)", [&]() { + it("throws exception if mapping is not monotone [{10} + K&D Fig. 9]", [&]() { + // NOTE: We actually provide a Monotone map, but do not claim to do so! + AssertThrows( + invalid_argument, + bdd_relnext(kalin_10, kalin_fig9, kalin_relnext_map, replace_type::Non_Monotone)); + }); + }); + + describe( + "bdd_relnext(const bdd&, const bdd&, , replace_type::Monotone)", [&]() { + it("has single successor [{00} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relnext(kalin_00, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single successor [{01} + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relnext(huth_01, huth_fig28, huth_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has no successors [{11} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relnext(kalin_11, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + AssertThat(out->sorted, Is().True()); + AssertThat(out->indexable, Is().True()); + AssertThat(bdd_iscanonical(out), Is().True()); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors of non-current states [{01} + K&D Fig. 7(a)]", [&]() { + const bdd out = + bdd_relnext(kalin_01, kalin_fig7_a, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + AssertThat(out->sorted, Is().True()); + AssertThat(out->indexable, Is().True()); + AssertThat(bdd_iscanonical(out), Is().True()); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has multiple successors [{10} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relnext(kalin_10, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + // + // NOTE: Fig. 11 in Kalin's and Dahlsen-Jensen's BSc Thesis + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has multiple successors [{00} + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relnext(huth_00, huth_fig28, huth_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has multiple successors [{00} + B Fig. 18]", [&]() { + const bdd out = + bdd_relnext(bryant_00, bryant_fig18, bryant_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has successors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relnext(kalin_fig11, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_F, bdd::pointer_type(1, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has successors of all current states [{01,10} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relnext(kalin_01_10, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + + it("has successors of all current states [H&R Fig. 6.26(b) + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relnext(huth_fig26_b, huth_fig28, huth_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has successors of all current states [{01,10} + B Fig. 18 (x:=1)]", [&]() { + const bdd out = + bdd_relnext(bryant_01_10, bryant_fig18_x1, bryant_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("excludes source states [{__} + B Fig. 18]", [&]() { + const bdd out = + bdd_relnext(true, bryant_fig18, bryant_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has no successors for empty set of states []", [&]() { + const bdd out = bdd_relnext(false, true, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of states [] [~]", [&]() { + const bdd T = true; + const bdd out = bdd_relnext(bdd_not(T), T, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of states [K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(false, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of states [H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(false, huth_fig28, huth_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of states [B Fig. 6.28]", [&]() { + const bdd out = + bdd_relnext(false, bryant_fig18, bryant_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = + bdd_relnext(kalin_fig11, false, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relnext(bdd_not(F), F, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relnext(F, F, kalin_relnext_map, replace_type::Monotone); + + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("has all successors for total graph [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relnext(kalin_fig11, true, kalin_relnext_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has all successors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relnext(T, T, kalin_relnext_map, replace_type::Monotone); + + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + }); + + describe( + "bdd_relnext(const bdd&, const bdd&, , replace_type::Monotone)", [&]() { + it("has single successor [{00} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_00, kalin_fig9, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single successor [{01} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(huth_01, huth_fig28, huth_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has no successors [{11} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_11, kalin_fig9, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + AssertThat(out->sorted, Is().True()); + AssertThat(out->indexable, Is().True()); + AssertThat(bdd_iscanonical(out), Is().True()); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors of non-current states [{01} + K&D Fig. 7(a)]", [&]() { + const bdd out = + bdd_relnext(kalin_01, kalin_fig7_a, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + AssertThat(out->sorted, Is().True()); + AssertThat(out->indexable, Is().True()); + AssertThat(bdd_iscanonical(out), Is().True()); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has multiple successors [{10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(kalin_10, kalin_fig9, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + // + // NOTE: Fig. 11 in Kalin's and Dahlsen-Jensen's BSc Thesis + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has multiple successors [{00} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(huth_00, huth_fig28, huth_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has multiple successors [{00} + B Fig. 18]", [&]() { + const bdd out = + bdd_relnext(bryant_00, bryant_fig18, bryant_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has successors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relnext(kalin_fig11, kalin_fig9, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_F, bdd::pointer_type(1, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has successors of all current states [{01,10} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relnext(kalin_01_10, kalin_fig9, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + + it("has successors of all current states [H&R Fig. 6.26(b) + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relnext(huth_fig26_b, huth_fig28, huth_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has successors of all current states [{01,10} + B Fig. 18 (x:=1)]", [&]() { + const bdd out = + bdd_relnext(bryant_01_10, bryant_fig18_x1, bryant_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("excludes source states [{__} + B Fig. 18]", [&]() { + const bdd out = bdd_relnext(true, bryant_fig18, bryant_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has no successors for empty set of states []", [&]() { + const bdd out = bdd_relnext(false, true, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of states [] [~]", [&]() { + const bdd T = true; + const bdd out = bdd_relnext(bdd_not(T), T, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of states [K&D Fig. 9]", [&]() { + const bdd out = bdd_relnext(false, kalin_fig9, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of states [H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(false, huth_fig28, huth_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of states [B Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(false, bryant_fig18, bryant_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relnext(kalin_fig11, false, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relnext(bdd_not(F), F, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); + + it("has no successors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relnext(F, F, kalin_relnext_map, replace_type::Shift); + + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("has all successors for total graph [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relnext(kalin_fig11, true, kalin_relnext_map, replace_type::Shift); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has all successors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relnext(T, T, kalin_relnext_map, replace_type::Shift); + + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + }); + + describe("bdd_relprev(const bdd&, const bdd&, )", [&]() { + it("has single predecessor [{01} + K&D Fig. 7(a)]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig7_a, kalin_relprev_map); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single predecessor [{10} + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig7_b, kalin_relprev_map); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single predecessor [{10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -4728,7 +6275,83 @@ go_bandit([]() { level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_01, huth_fig28, huth_relprev_map); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single predecessor [{10} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_10, huth_fig28, huth_relprev_map); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); @@ -4738,12 +6361,14 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); @@ -4751,8 +6376,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single successor [{01} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relnext(huth_01, huth_fig28, huth_relnext_map, replace_type::Monotone); + it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { + const bdd out = bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -4763,7 +6388,7 @@ go_bandit([]() { AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -4773,19 +6398,21 @@ go_bandit([]() { AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); @@ -4793,22 +6420,19 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no successors [{11} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relnext(kalin_11, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + it("has no predecessors [{00} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map); // Check it looks all right - AssertThat(out->sorted, Is().True()); - AssertThat(out->indexable, Is().True()); - AssertThat(bdd_iscanonical(out), Is().True()); - node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(0u)); @@ -4827,22 +6451,19 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no successors of non-current states [{01} + K&D Fig. 7(a)]", [&]() { - const bdd out = - bdd_relnext(kalin_01, kalin_fig7_a, kalin_relnext_map, replace_type::Monotone); + it("has no predecessors [{01} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map); // Check it looks all right - AssertThat(out->sorted, Is().True()); - AssertThat(out->indexable, Is().True()); - AssertThat(bdd_iscanonical(out), Is().True()); - node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(0u)); @@ -4861,115 +6482,101 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has multiple successors [{10} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relnext(kalin_10, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + it("has no predecessors of non-current states [{10} + K&D Fig. 7(a)]", [&]() { + const bdd out = bdd_relprev(kalin_10, kalin_fig7_a, kalin_relprev_map); // Check it looks all right - // - // NOTE: Fig. 11 in Kalin's and Dahlsen-Jensen's BSc Thesis node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has multiple successors [{00} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relnext(huth_00, huth_fig28, huth_relnext_map, replace_type::Monotone); + it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has multiple successors [{00} + B Fig. 18]", [&]() { - const bdd out = - bdd_relnext(bryant_00, bryant_fig18, bryant_relnext_map, replace_type::Monotone); + it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { + const bdd out = bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has successors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relnext(kalin_fig11, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -4977,54 +6584,6 @@ go_bandit([]() { AssertThat(out_nodes.can_pull(), Is().True()); AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_F, bdd::pointer_type(1, bdd::max_id)))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(1u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); - - it("has successors of all current states [{01,10} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relnext(kalin_01_10, kalin_fig9, kalin_relnext_map, replace_type::Monotone); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_T))); - AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); @@ -5032,44 +6591,6 @@ go_bandit([]() { AssertThat(out_meta.can_pull(), Is().True()); AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(1u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); - - it("has successors of all current states [H&R Fig. 6.26(b) + H&R Fig. 6.28]", [&]() { - const bdd out = - bdd_relnext(huth_fig26_b, huth_fig28, huth_relnext_map, replace_type::Monotone); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); AssertThat(out->width, Is().EqualTo(1u)); @@ -5088,20 +6609,19 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has successors of all current states [{01,10} + B Fig. 18 (x:=1)]", [&]() { - const bdd out = - bdd_relnext(bryant_01_10, bryant_fig18_x1, bryant_relnext_map, replace_type::Monotone); + it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_00, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -5111,41 +6631,7 @@ go_bandit([]() { AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(1u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); - - it("excludes source states [{__} + B Fig. 18]", [&]() { - const bdd out = bdd_relnext(true, bryant_fig18, bryant_relnext_map, replace_type::Monotone); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); AssertThat(out_meta.can_pull(), Is().False()); @@ -5153,26 +6639,26 @@ go_bandit([]() { AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has no successors for empty set of states []", [&]() { - const bdd out = bdd_relnext(false, true, kalin_relnext_map, replace_type::Monotone); + it("has multiple predecessors [{00} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -5183,28 +6669,27 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no successors for empty set of states [] [~]", [&]() { - const bdd T = true; - const bdd out = bdd_relnext(bdd_not(T), T, kalin_relnext_map, replace_type::Monotone); + it("has multiple predecessors [{10} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(bryant_10, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -5215,186 +6700,219 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no successors for empty set of states [K&D Fig. 9]", [&]() { - const bdd out = bdd_relnext(false, kalin_fig9, kalin_relnext_map, replace_type::Monotone); + it("has predecessors of all current states [{00,10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_00_01, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no successors for empty set of states [H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relnext(false, huth_fig28, huth_relnext_map, replace_type::Monotone); + it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has no successors for empty set of states [B Fig. 6.28]", [&]() { - const bdd out = - bdd_relnext(false, bryant_fig18, bryant_relnext_map, replace_type::Monotone); + it("has predecessors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has no successors for empty set of edges [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relnext(kalin_fig11, false, kalin_relnext_map, replace_type::Monotone); + it("has predecessors of all current states [H&R Fig.6.26(a) + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has no successors for empty set of edges [~ + ]", [&]() { - const bdd F = false; - const bdd out = bdd_relnext(bdd_not(F), F, kalin_relnext_map, replace_type::Monotone); + it("has predecessors of all current states [H&R Fig.6.26(b) + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_fig26_b, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); - - it("has no successors for empty set of nodes and edges []", [&]() { - const bdd F = false; - const bdd out = bdd_relnext(F, F, kalin_relnext_map, replace_type::Monotone); - - AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); - AssertThat(out.is_negated(), Is().False()); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has all successors for total graph [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relnext(kalin_fig11, true, kalin_relnext_map, replace_type::Monotone); + it("has predecessors of all current states [{00,01} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(huth_00_01, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -5421,123 +6939,52 @@ go_bandit([]() { AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); - - it("has all successors for all nodes and total graph []", [&]() { - const bdd T = true; - const bdd out = bdd_relnext(T, T, kalin_relnext_map, replace_type::Monotone); - - AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); - AssertThat(out.is_negated(), Is().False()); - }); - - it("throws exception if mapping is not monotone [{10} + K&D Fig. 9]", [&]() { - // NOTE: We actually provide a Monotone map, but do not claim to do so! - AssertThrows( - invalid_argument, - bdd_relnext(kalin_10, kalin_fig9, kalin_relnext_map, replace_type::Non_Monotone)); - }); - }); - - describe("bdd_relprev(const bdd&, const bdd&, )", [&]() { - it("has single predecessor [{01} + K&D Fig. 7(a)]", [&]() { - const bdd out = bdd_relprev(kalin_01, kalin_fig7_a, kalin_relprev_map); - - // Check it looks all right - node_test_stream out_nodes(out); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().False()); - - level_info_test_stream out_meta(out); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(1u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); - - it("has single predecessor [{10} + K&D Fig. 7(b)]", [&]() { - const bdd out = bdd_relprev(kalin_10, kalin_fig7_b, kalin_relprev_map); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + it("has predecessors of all current states [{00,10} + B Fig. 18 (x:=0)]", [&]() { + const bdd out = bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{10} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map); + it("excludes deadlocks [{__} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); AssertThat(out_nodes.can_pull(), Is().True()); AssertThat( out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); @@ -5554,143 +7001,112 @@ go_bandit([]() { AssertThat(out->width, Is().EqualTo(1u)); AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); - it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_01, huth_fig28, huth_relprev_map); + it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{10} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_10, huth_fig28, huth_relprev_map); + it("has no deadlocks [{__} + B Fig. 18]", [&]() { + const bdd out = bdd_relprev(true, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - - AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { - const bdd out = bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map); + it("has no predecessors for empty set of states []", [&]() { + const bdd out = bdd_relprev(false, true, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors [{00} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map); + it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -5720,8 +7136,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors [{01} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map); + it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -5751,8 +7167,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors of non-current states [{10} + K&D Fig. 7(a)]", [&]() { - const bdd out = bdd_relprev(kalin_10, kalin_fig7_a, kalin_relprev_map); + it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(false, bryant_fig18, bryant_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -5782,8 +7198,8 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { - const bdd out = bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map); + it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, false, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -5813,8 +7229,9 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { - const bdd out = bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map); + it("has no predecessors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); @@ -5844,752 +7261,897 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map); + it("has no predecessors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(F, F, kalin_relprev_map); + + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map); // Check it looks all right node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(0u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has all predecessors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relprev(T, T, kalin_relprev_map); + + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("throws exception if mapping is not monotone [{01} + K&D Fig. 9]", [&]() { + const auto kalin_relprev_map__flipped = [&kalin_relprev_pred](int x) -> optional { + return kalin_relprev_pred(x) ? make_optional() : make_optional(2 + !x); + }; + AssertThrows(invalid_argument, + bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map__flipped)); + }); + }); + + describe( + "bdd_relprev(const bdd&, const bdd&, , replace_type::Non_Monotone)", [&]() { + it("throws exception if mapping is not monotone [{01} + K&D Fig. 9]", [&]() { + // NOTE: We actually provide a Monotone map, but do not claim to do so! + AssertThrows( + invalid_argument, + bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Non_Monotone)); + }); + }); + + describe( + "bdd_relprev(const bdd&, const bdd&, , replace_type::Monotone)", [&]() { + it("has single predecessor [{10} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(1, bdd::max_id), terminal_F))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + + it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relprev(huth_01, huth_fig28, huth_relprev_map, replace_type::Monotone); + + // Check it looks all right + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(0, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - AssertThat(out_nodes.can_pull(), Is().False()); + it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { + const bdd out = + bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map, replace_type::Monotone); - level_info_test_stream out_meta(out); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(1, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_F))); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_00, huth_fig28, huth_relprev_map); + AssertThat(out_meta.can_pull(), Is().False()); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - level_info_test_stream out_meta(out); + it("has no predecessors [{00} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(1u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - it("has multiple predecessors [{00} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + it("has no predecessors [{01} + B Fig. 18]", [&]() { + const bdd out = + bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().False()); + // Check it looks all right + node_test_stream out_nodes(out); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - it("has multiple predecessors [{10} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(bryant_10, bryant_fig18, bryant_relprev_map); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { + const bdd out = + bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().False()); + // Check it looks all right + node_test_stream out_nodes(out); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - it("has predecessors of all current states [{00,10} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_00_01, kalin_fig9, kalin_relprev_map); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { + const bdd out = + bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().False()); + // Check it looks all right + node_test_stream out_nodes(out); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - level_info_test_stream out_meta(out); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); + it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relprev(huth_00, huth_fig28, huth_relprev_map, replace_type::Monotone); - it("has predecessors of all current states [K&D Fig. 11 + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, kalin_fig9, kalin_relprev_map); + // Check it looks all right + node_test_stream out_nodes(out); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(2, bdd::max_id)))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - level_info_test_stream out_meta(out); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - it("has predecessors of all current states [H&R Fig.6.26(a) + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has multiple predecessors [{00} + B Fig. 18]", [&]() { + const bdd out = + bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().False()); - level_info_test_stream out_meta(out); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { + const bdd out = + bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map, replace_type::Monotone); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); + // Check it looks all right + node_test_stream out_nodes(out); - it("has predecessors of all current states [H&R Fig.6.26(b) + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_fig26_b, huth_fig28, huth_relprev_map); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); + level_info_test_stream out_meta(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + it("has predecessors of all current states [H&R Fig.6.26(a) + H&R Fig. 6.28]", [&]() { + const bdd out = + bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map, replace_type::Monotone); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); + // Check it looks all right + node_test_stream out_nodes(out); - it("has predecessors of all current states [{00,01} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_00_01, huth_fig28, huth_relprev_map); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, bdd::pointer_type(2, bdd::max_id), terminal_T))); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_nodes.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - level_info_test_stream out_meta(out); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - it("has predecessors of all current states [{00,10} + B Fig. 18 (x:=0)]", [&]() { - const bdd out = bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map); - // Check it looks all right - node_test_stream out_nodes(out); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + it("has predecessors of all current states [{00,10} + B Fig. 18 (x:=0)]", [&]() { + const bdd out = + bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("excludes deadlocks [{__} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("excludes deadlocks [{__} + K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat( - out_nodes.pull(), - Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_T, terminal_F))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(0, bdd::max_id, terminal_T, bdd::pointer_type(1, bdd::max_id)))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); - AssertThat(out->width, Is().EqualTo(1u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->width, Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u)); - it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no deadlocks [{__} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(true, bryant_fig18, bryant_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no deadlocks [{__} + B Fig. 18]", [&]() { + const bdd out = + bdd_relprev(true, bryant_fig18, bryant_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(0u)); + level_info_test_stream out_meta(out); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of states []", [&]() { - const bdd out = bdd_relprev(false, true, kalin_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of states []", [&]() { + const bdd out = bdd_relprev(false, true, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { + const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { + const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(false, bryant_fig18, bryant_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { + const bdd out = + bdd_relprev(false, bryant_fig18, bryant_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, false, kalin_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = + bdd_relprev(kalin_fig11, false, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of edges [~ + ]", [&]() { - const bdd F = false; - const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has no predecessors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has no predecessors for empty set of nodes and edges []", [&]() { - const bdd F = false; - const bdd out = bdd_relprev(F, F, kalin_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); + }); - AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); - AssertThat(out.is_negated(), Is().False()); - }); + it("has no predecessors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relprev(F, F, kalin_relprev_map, replace_type::Monotone); - it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map); + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); - // Check it looks all right - node_test_stream out_nodes(out); + it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map, replace_type::Monotone); - AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); + // Check it looks all right + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(true))); - level_info_test_stream out_meta(out); + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out_meta.can_pull(), Is().False()); + level_info_test_stream out_meta(out); - AssertThat(out->width, Is().EqualTo(0u)); + AssertThat(out_meta.can_pull(), Is().False()); - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->width, Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); - }); + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(0u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(1u)); - it("has all predecessors for all nodes and total graph []", [&]() { - const bdd T = true; - const bdd out = bdd_relprev(T, T, kalin_relprev_map); + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); - AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); - AssertThat(out.is_negated(), Is().False()); - }); + it("has all predecessors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relprev(T, T, kalin_relprev_map, replace_type::Monotone); - it("throws exception if mapping is not monotone [{01} + K&D Fig. 9]", [&]() { - const auto kalin_relprev_map__flipped = [&kalin_relprev_pred](int x) -> optional { - return kalin_relprev_pred(x) ? make_optional() : make_optional(2 + !x); - }; - AssertThrows(invalid_argument, - bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map__flipped)); + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); }); - }); - describe("bdd_relprev(const bdd&, const bdd&, , replace_type)", [&]() { + describe("bdd_relprev(const bdd&, const bdd&, , replace_type::Shift)", [&]() { it("has single predecessor [{10} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(kalin_10, kalin_fig9, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6631,7 +8193,7 @@ go_bandit([]() { }); it("has single predecessor [{01} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_01, huth_fig28, huth_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(huth_01, huth_fig28, huth_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6666,7 +8228,7 @@ go_bandit([]() { it("has single predecessor [{00} + B Fig. 18 (x:=0)]", [&]() { const bdd out = - bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map, replace_type::Monotone); + bdd_relprev(bryant_00, bryant_fig18_x0, bryant_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6710,8 +8272,7 @@ go_bandit([]() { }); it("has no predecessors [{00} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(kalin_00, kalin_fig9, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6743,7 +8304,7 @@ go_bandit([]() { it("has no predecessors [{01} + B Fig. 18]", [&]() { const bdd out = - bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + bdd_relprev(bryant_01, bryant_fig18, bryant_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6774,8 +8335,7 @@ go_bandit([]() { }); it("has no predecessors of non-current states [{01} + K&D Fig. 7(b)]", [&]() { - const bdd out = - bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(kalin_01, kalin_fig7_b, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6807,7 +8367,7 @@ go_bandit([]() { it("has no predecessors of non-current states [{10} + B Fig. 18 (x:=1)]", [&]() { const bdd out = - bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map, replace_type::Monotone); + bdd_relprev(bryant_10, bryant_fig18_x1, bryant_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6838,8 +8398,7 @@ go_bandit([]() { }); it("has multiple predecessors [{01} + K&D Fig. 9]", [&]() { - const bdd out = - bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6873,7 +8432,7 @@ go_bandit([]() { }); it("has multiple predecessors [{00} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(huth_00, huth_fig28, huth_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(huth_00, huth_fig28, huth_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6916,7 +8475,7 @@ go_bandit([]() { it("has multiple predecessors [{00} + B Fig. 18]", [&]() { const bdd out = - bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + bdd_relprev(bryant_00, bryant_fig18, bryant_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6948,7 +8507,7 @@ go_bandit([]() { it("has predecessors of all current states [{01,10} + K&D Fig. 9]", [&]() { const bdd out = - bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + bdd_relprev(kalin_01_10, kalin_fig9, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -6991,7 +8550,7 @@ go_bandit([]() { it("has predecessors of all current states [H&R Fig.6.26(a) + H&R Fig. 6.28]", [&]() { const bdd out = - bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map, replace_type::Monotone); + bdd_relprev(huth_fig26_a, huth_fig28, huth_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7036,7 +8595,7 @@ go_bandit([]() { it("has predecessors of all current states [{00,10} + B Fig. 18 (x:=0)]", [&]() { const bdd out = - bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + bdd_relprev(bryant_00_10, bryant_fig18, bryant_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7066,7 +8625,7 @@ go_bandit([]() { }); it("excludes deadlocks [{__} + K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(true, kalin_fig9, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7108,7 +8667,7 @@ go_bandit([]() { }); it("has no deadlocks [{__} + H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(true, huth_fig28, huth_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7139,7 +8698,7 @@ go_bandit([]() { }); it("has no deadlocks [{__} + B Fig. 18]", [&]() { - const bdd out = bdd_relprev(true, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(true, bryant_fig18, bryant_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7168,7 +8727,7 @@ go_bandit([]() { }); it("has no predecessors for empty set of states []", [&]() { - const bdd out = bdd_relprev(false, true, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(false, true, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7199,7 +8758,7 @@ go_bandit([]() { }); it("has no predecessors for empty set of states [K&D Fig. 9]", [&]() { - const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7230,7 +8789,7 @@ go_bandit([]() { }); it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { - const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(false, huth_fig28, huth_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7261,8 +8820,7 @@ go_bandit([]() { }); it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { - const bdd out = - bdd_relprev(false, bryant_fig18, bryant_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(false, bryant_fig18, bryant_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7293,7 +8851,7 @@ go_bandit([]() { }); it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, false, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(kalin_fig11, false, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7325,7 +8883,7 @@ go_bandit([]() { it("has no predecessors for empty set of edges [~ + ]", [&]() { const bdd F = false; - const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(bdd_not(F), F, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7357,14 +8915,14 @@ go_bandit([]() { it("has no predecessors for empty set of nodes and edges []", [&]() { const bdd F = false; - const bdd out = bdd_relprev(F, F, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(F, F, kalin_relprev_map, replace_type::Shift); AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); AssertThat(out.is_negated(), Is().False()); }); it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { - const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(kalin_fig11, true, kalin_relprev_map, replace_type::Shift); // Check it looks all right node_test_stream out_nodes(out); @@ -7396,18 +8954,11 @@ go_bandit([]() { it("has all predecessors for all nodes and total graph []", [&]() { const bdd T = true; - const bdd out = bdd_relprev(T, T, kalin_relprev_map, replace_type::Monotone); + const bdd out = bdd_relprev(T, T, kalin_relprev_map, replace_type::Shift); AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); AssertThat(out.is_negated(), Is().False()); }); - - it("throws exception if mapping is not monotone [{01} + K&D Fig. 9]", [&]() { - // NOTE: We actually provide a Monotone map, but do not claim to do so! - AssertThrows( - invalid_argument, - bdd_relprev(kalin_01, kalin_fig9, kalin_relprev_map, replace_type::Non_Monotone)); - }); }); }); }); diff --git a/test/adiar/bdd/test_replace.cpp b/test/adiar/bdd/test_replace.cpp index 461572334..a58d7cf66 100644 --- a/test/adiar/bdd/test_replace.cpp +++ b/test/adiar/bdd/test_replace.cpp @@ -159,15 +159,16 @@ go_bandit([]() { AssertThat(out.is_negated(), Is().True()); }); - it("returns 'x(4-0)' when given 'x0'", [&]() { + it("identifies 'x(4-0)' as a mere shift on 'x0'", [&]() { const mapping_type m = [](const int x) { return 4 - x; }; const bdd out = bdd_replace(bdd_x0, m); - // Check it looks all right - AssertThat(out->sorted, Is().True()); - AssertThat(out->indexable, Is().True()); - AssertThat(bdd_iscanonical(out), Is().True()); + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_x0_nf)); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(4)); + // Check it is read correctly node_test_stream out_nodes(out); // n1 @@ -182,29 +183,6 @@ go_bandit([]() { AssertThat(out_meta.pull(), Is().EqualTo(level_info(4, 1u))); AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(bdd_x0->width)); - - AssertThat(out->max_1level_cut[cut::Internal], - Is().EqualTo(bdd_x0->max_1level_cut[cut::Internal])); - AssertThat(out->max_1level_cut[cut::Internal_False], - Is().EqualTo(bdd_x0->max_1level_cut[cut::Internal_False])); - AssertThat(out->max_1level_cut[cut::Internal_True], - Is().EqualTo(bdd_x0->max_1level_cut[cut::Internal_True])); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(bdd_x0->max_1level_cut[cut::All])); - - AssertThat(out->max_2level_cut[cut::Internal], - Is().EqualTo(bdd_x0->max_2level_cut[cut::Internal])); - AssertThat(out->max_2level_cut[cut::Internal_False], - Is().EqualTo(bdd_x0->max_2level_cut[cut::Internal_False])); - AssertThat(out->max_2level_cut[cut::Internal_True], - Is().EqualTo(bdd_x0->max_2level_cut[cut::Internal_True])); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(bdd_x0->max_2level_cut[cut::All])); - - AssertThat(out->number_of_terminals[false], - Is().EqualTo(bdd_x0->number_of_terminals[false])); - AssertThat(out->number_of_terminals[true], - Is().EqualTo(bdd_x0->number_of_terminals[true])); }); it("throws exception if levels have to be swapped [bdd_1]", [&]() { @@ -416,14 +394,16 @@ go_bandit([]() { AssertThat(out.is_negated(), Is().True()); }); - it("shifts 'x0' into 'x1'", [&]() { + it("identifies 'x(2x+1)' as a mere shift for 'x0'", [&]() { const mapping_type m = [](const int x) { return 2 * x + 1; }; const bdd out = bdd_replace(bdd_x0, m); - // Check it looks all right - AssertThat(out->sorted, Is().EqualTo(bdd_x0->sorted)); - AssertThat(out->indexable, Is().EqualTo(bdd_x0->indexable)); + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_x0_nf)); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(1)); + // Check it is read correctly node_test_stream out_nodes(out); // n1 @@ -438,39 +418,83 @@ go_bandit([]() { AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().False()); + }); + + it("doubles variables in 'BDD 2'", [&]() { + const mapping_type m = [](const int x) { return 2 * x; }; + const bdd out = bdd_replace(bdd_2, m); + + // Check it looks all right + AssertThat(out->sorted, Is().EqualTo(bdd_2->sorted)); + AssertThat(out->indexable, Is().EqualTo(bdd_2->indexable)); + + node_test_stream out_nodes(out); + + // n3 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + + // n2 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(2, bdd::max_id - 2, terminal_F, terminal_T))); + + // n1 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(0, + bdd::max_id, + bdd::pointer_type(2, bdd::max_id - 2), + bdd::pointer_type(2, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); - AssertThat(out->width, Is().EqualTo(bdd_x0->width)); + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 2u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(bdd_2->width)); AssertThat(out->max_1level_cut[cut::Internal], - Is().EqualTo(bdd_x0->max_1level_cut[cut::Internal])); + Is().EqualTo(bdd_2->max_1level_cut[cut::Internal])); AssertThat(out->max_1level_cut[cut::Internal_False], - Is().EqualTo(bdd_x0->max_1level_cut[cut::Internal_True])); + Is().EqualTo(bdd_2->max_1level_cut[cut::Internal_False])); AssertThat(out->max_1level_cut[cut::Internal_True], - Is().EqualTo(bdd_x0->max_1level_cut[cut::Internal_False])); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(bdd_x0->max_1level_cut[cut::All])); + Is().EqualTo(bdd_2->max_1level_cut[cut::Internal_True])); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(bdd_2->max_1level_cut[cut::All])); AssertThat(out->max_2level_cut[cut::Internal], - Is().EqualTo(bdd_x0->max_2level_cut[cut::Internal])); + Is().EqualTo(bdd_2->max_2level_cut[cut::Internal])); AssertThat(out->max_2level_cut[cut::Internal_False], - Is().EqualTo(bdd_x0->max_2level_cut[cut::Internal_True])); + Is().EqualTo(bdd_2->max_2level_cut[cut::Internal_False])); AssertThat(out->max_2level_cut[cut::Internal_True], - Is().EqualTo(bdd_x0->max_2level_cut[cut::Internal_False])); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(bdd_x0->max_2level_cut[cut::All])); + Is().EqualTo(bdd_2->max_2level_cut[cut::Internal_True])); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(bdd_2->max_2level_cut[cut::All])); AssertThat(out->number_of_terminals[false], - Is().EqualTo(bdd_x0->number_of_terminals[true])); + Is().EqualTo(bdd_2->number_of_terminals[false])); AssertThat(out->number_of_terminals[true], - Is().EqualTo(bdd_x0->number_of_terminals[false])); + Is().EqualTo(bdd_2->number_of_terminals[true])); }); + }); + describe("", [&]() { it("shifts variables in 'BDD 1'", [&]() { const mapping_type m = [](const int x) { return x + 1; }; const bdd out = bdd_replace(bdd_1, m); - // Check it looks all right - AssertThat(out->sorted, Is().EqualTo(bdd_1->sorted)); - AssertThat(out->indexable, Is().EqualTo(bdd_1->indexable)); + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_1_nf)); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(1)); + // Check it is read correctly node_test_stream out_nodes(out); // n3 @@ -505,93 +529,149 @@ go_bandit([]() { AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); AssertThat(out_meta.can_pull(), Is().False()); + }); - AssertThat(out->width, Is().EqualTo(bdd_1->width)); + it("shifts variables in 'BDD 2'", [&]() { + const mapping_type m = [](const int x) { return x + 4; }; + const bdd out = bdd_replace(bdd_2, m); - AssertThat(out->max_1level_cut[cut::Internal], - Is().EqualTo(bdd_1->max_1level_cut[cut::Internal])); - AssertThat(out->max_1level_cut[cut::Internal_False], - Is().EqualTo(bdd_1->max_1level_cut[cut::Internal_False])); - AssertThat(out->max_1level_cut[cut::Internal_True], - Is().EqualTo(bdd_1->max_1level_cut[cut::Internal_True])); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(bdd_1->max_1level_cut[cut::All])); + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_2_nf)); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(4)); - AssertThat(out->max_2level_cut[cut::Internal], - Is().EqualTo(bdd_1->max_2level_cut[cut::Internal])); - AssertThat(out->max_2level_cut[cut::Internal_False], - Is().EqualTo(bdd_1->max_2level_cut[cut::Internal_False])); - AssertThat(out->max_2level_cut[cut::Internal_True], - Is().EqualTo(bdd_1->max_2level_cut[cut::Internal_True])); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(bdd_1->max_2level_cut[cut::All])); + // Check it is read correctly + node_test_stream out_nodes(out); - AssertThat(out->number_of_terminals[false], - Is().EqualTo(bdd_1->number_of_terminals[false])); - AssertThat(out->number_of_terminals[true], - Is().EqualTo(bdd_1->number_of_terminals[true])); + // n3 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(5, bdd::max_id, terminal_T, terminal_F))); + + // n2 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(5, bdd::max_id - 2, terminal_F, terminal_T))); + + // n1 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(4, + bdd::max_id, + bdd::pointer_type(5, bdd::max_id - 2), + bdd::pointer_type(5, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(5, 2u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(4, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); }); - it("doubles variables in 'BDD 2'", [&]() { - const mapping_type m = [](const int x) { return 2 * x; }; - const bdd out = bdd_replace(bdd_2, m); + it("shifts variables in 'BDD 3' multiple times [+3, +3]", [&]() { + const mapping_type m = [](const int x) { return x + 3; }; + const bdd out = bdd_replace(bdd_replace(bdd_3, m), m); - // Check it looks all right - AssertThat(out->sorted, Is().EqualTo(bdd_2->sorted)); - AssertThat(out->indexable, Is().EqualTo(bdd_2->indexable)); + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_3_nf)); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(6)); + // Check it is read correctly node_test_stream out_nodes(out); + // n4 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(8, bdd::max_id, terminal_T, terminal_F))); + // n3 AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_T, terminal_F))); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(7, bdd::max_id, terminal_F, bdd::pointer_type(8, bdd::max_id)))); // n2 AssertThat(out_nodes.can_pull(), Is().True()); - AssertThat(out_nodes.pull(), - Is().EqualTo(node(2, bdd::max_id - 2, terminal_F, terminal_T))); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(7, bdd::max_id - 1, bdd::pointer_type(8, bdd::max_id), terminal_F))); // n1 AssertThat(out_nodes.can_pull(), Is().True()); AssertThat(out_nodes.pull(), - Is().EqualTo(node(0, + Is().EqualTo(node(6, bdd::max_id, - bdd::pointer_type(2, bdd::max_id - 2), - bdd::pointer_type(2, bdd::max_id)))); + bdd::pointer_type(7, bdd::max_id - 1), + bdd::pointer_type(7, bdd::max_id)))); AssertThat(out_nodes.can_pull(), Is().False()); level_info_test_stream out_meta(out); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 2u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(8, 1u))); AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0, 1u))); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(7, 2u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(6, 1u))); AssertThat(out_meta.can_pull(), Is().False()); + }); - AssertThat(out->width, Is().EqualTo(bdd_2->width)); + it("shifts variables in 'BDD 1' multiple times [+2, -1]", [&]() { + const bdd out = bdd_replace(bdd_replace(bdd_1, [](const int x) { return x + 2; }), + [](const int x) { return x - 1; }); - AssertThat(out->max_1level_cut[cut::Internal], - Is().EqualTo(bdd_2->max_1level_cut[cut::Internal])); - AssertThat(out->max_1level_cut[cut::Internal_False], - Is().EqualTo(bdd_2->max_1level_cut[cut::Internal_False])); - AssertThat(out->max_1level_cut[cut::Internal_True], - Is().EqualTo(bdd_2->max_1level_cut[cut::Internal_True])); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(bdd_2->max_1level_cut[cut::All])); + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_1_nf)); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(1)); - AssertThat(out->max_2level_cut[cut::Internal], - Is().EqualTo(bdd_2->max_2level_cut[cut::Internal])); - AssertThat(out->max_2level_cut[cut::Internal_False], - Is().EqualTo(bdd_2->max_2level_cut[cut::Internal_False])); - AssertThat(out->max_2level_cut[cut::Internal_True], - Is().EqualTo(bdd_2->max_2level_cut[cut::Internal_True])); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(bdd_2->max_2level_cut[cut::All])); + // Check it is read correctly + node_test_stream out_nodes(out); - AssertThat(out->number_of_terminals[false], - Is().EqualTo(bdd_2->number_of_terminals[false])); - AssertThat(out->number_of_terminals[true], - Is().EqualTo(bdd_2->number_of_terminals[true])); + // n3 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(5, bdd::max_id, terminal_F, terminal_T))); + + // n2 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(3, bdd::max_id, bdd::pointer_type(5, bdd::max_id), terminal_T))); + + // n1 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(1, + bdd::max_id, + bdd::pointer_type(5, bdd::max_id), + bdd::pointer_type(3, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(5, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(3, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); }); + + // TODO: Accumulation of shifts }); describe("", [&]() { @@ -796,6 +876,74 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(bdd_2->number_of_terminals[true])); }); + it("shifts variables in 'BDD 1' if 'replace_type' is 'Shift'", [&]() { + // NOTE: This function is in fact *not* a shift! + const mapping_type m = [](const int x) { return 2 * x + 1; }; + const bdd out = bdd_replace(bdd_1, m, replace_type::Shift); + + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_1.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(+1)); + + // Check it is read correctly + node_test_stream out_nodes(out); + + // n3 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(5, bdd::max_id, terminal_F, terminal_T))); + + // n2 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node(3, bdd::max_id, bdd::pointer_type(5, bdd::max_id), terminal_T))); + + // n1 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat( + out_nodes.pull(), + Is().EqualTo(node( + 1, bdd::max_id, bdd::pointer_type(5, bdd::max_id), bdd::pointer_type(3, bdd::max_id)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(5, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(3, 1u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(bdd_1->width)); + + AssertThat(out->max_1level_cut[cut::Internal], + Is().EqualTo(bdd_1->max_1level_cut[cut::Internal])); + AssertThat(out->max_1level_cut[cut::Internal_False], + Is().EqualTo(bdd_1->max_1level_cut[cut::Internal_False])); + AssertThat(out->max_1level_cut[cut::Internal_True], + Is().EqualTo(bdd_1->max_1level_cut[cut::Internal_True])); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(bdd_1->max_1level_cut[cut::All])); + + AssertThat(out->max_2level_cut[cut::Internal], + Is().EqualTo(bdd_1->max_2level_cut[cut::Internal])); + AssertThat(out->max_2level_cut[cut::Internal_False], + Is().EqualTo(bdd_1->max_2level_cut[cut::Internal_False])); + AssertThat(out->max_2level_cut[cut::Internal_True], + Is().EqualTo(bdd_1->max_2level_cut[cut::Internal_True])); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(bdd_1->max_2level_cut[cut::All])); + + AssertThat(out->number_of_terminals[false], + Is().EqualTo(bdd_1->number_of_terminals[false])); + AssertThat(out->number_of_terminals[true], Is().EqualTo(bdd_1->number_of_terminals[true])); + }); + it("returns the original file if 'replace_type is 'Identity'", [&]() { // NOTE: This function is in fact *not* the identity! const mapping_type m = [](const int x) { return x + 1; }; @@ -1025,14 +1173,16 @@ go_bandit([]() { AssertThat(out.is_negated(), Is().False()); }); - it("reverses 'x0' into 'x4' [bdd_x0]", [&]() { + it("identifies 'x(4-0)' as a mere shift on reduced 'x0' [bdd_x0]", [&]() { const mapping_type m = [](const int x) { return 4 - x; }; const bdd out = bdd_replace(exec_policy(), __bdd(bdd_x0_nf), m); - // Check it looks all right - AssertThat(out->sorted, Is().True()); - AssertThat(out->indexable, Is().True()); + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_x0_nf)); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(4)); + // Check it looks all right node_test_stream out_nodes(out); // n1 @@ -1064,10 +1214,15 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("preserves negation flag when reversing 'x0' into 'x4' [bdd_x0]", [&]() { + it("preserves negation flag when identiftying 'x(4-0)' is a mere shift [bdd_x0]", [&]() { const mapping_type m = [](const int x) { return 4 - x; }; const bdd out = bdd_replace(__bdd(bdd(bdd_x0_nf, true)), m); + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_x0_nf)); + AssertThat(out.is_negated(), Is().True()); + AssertThat(out.shift(), Is().EqualTo(4)); + // Check it looks all right AssertThat(out->sorted, Is().True()); AssertThat(out->indexable, Is().True()); @@ -1086,21 +1241,6 @@ go_bandit([]() { AssertThat(out_meta.pull(), Is().EqualTo(level_info(4, 1u))); AssertThat(out_meta.can_pull(), Is().False()); - - AssertThat(out->width, Is().EqualTo(1u)); - - AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); - - AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); - AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); - - AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); - AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); it("reverses 'x0' into 'x4' [__bdd_x0]", [&]() { @@ -1170,7 +1310,7 @@ go_bandit([]() { }); }); - describe(" / ", [&]() { + describe(" / / ", [&]() { it("returns the original file for 'F'", [&]() { const mapping_type m = [](const int x) { return 2 * x + 1; }; const bdd out = bdd_replace(__bdd(bdd_F), m); @@ -1250,6 +1390,84 @@ go_bandit([]() { Is().EqualTo(bdd_2->number_of_terminals[true])); }); + it("returns shifted original file [bdd_x0]", [&]() { + int m_calls = 0; + const mapping_type m = [&m_calls](const int x) { + m_calls++; + return x + 1; + }; + const bdd out = bdd_replace(__bdd(bdd_x0), m); + + // Check only called once to determine type of mapping and then once to obtain the amount + // to shift + AssertThat(m_calls, Is().EqualTo(1 + 1)); + + // Check it returns the same file but shifted + AssertThat(out.file_ptr(), Is().EqualTo(bdd_x0_nf)); + AssertThat(out.is_negated(), Is().False()); + AssertThat(out.shift(), Is().EqualTo(1)); + + // Check it looks all right + node_test_stream out_nodes(out); + + // n1 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + }); + + it("reduces and shifts variables [__bdd_x0]", [&]() { + int m_calls = 0; + const mapping_type m = [&m_calls](const int x) { + m_calls++; + return x + 1; + }; + const bdd out = bdd_replace(__bdd(__bdd_x0, exec_policy()), m); + + // Check only called once to determine type of mapping and then once to obtain the amount + // to shift + AssertThat(m_calls, Is().EqualTo(1 + 1)); + + // Check it looks all right + node_test_stream out_nodes(out); + + // n1 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(1, bdd::max_id, terminal_F, terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(1u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(1u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); + }); + it("reduces and shifts variables at once [__bdd_x0_unreduced]", [&]() { int m_calls = 0; const mapping_type m = [&m_calls](const int x) { @@ -1259,7 +1477,7 @@ go_bandit([]() { const bdd out = bdd_replace(__bdd(__bdd_x0_unreduced, exec_policy()), m); // Check only called once to determine type of mapping and then for each level - AssertThat(m_calls, Is().EqualTo(2 * 2)); + AssertThat(m_calls, Is().EqualTo(2 + 2)); // Check it looks all right AssertThat(out->sorted, Is().True()); @@ -1296,7 +1514,7 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); - it("reduces and doubles variables at once [__bdd_2]", [&]() { + it("doubles variables [__bdd_2]", [&]() { int m_calls = 0; const mapping_type m = [&m_calls](const int x) { m_calls++; @@ -1305,7 +1523,7 @@ go_bandit([]() { const bdd out = bdd_replace(__bdd(__bdd_2, exec_policy()), m); // Check only called once to determine type of mapping and then for each level - AssertThat(m_calls, Is().EqualTo(2 * 2)); + AssertThat(m_calls, Is().EqualTo(2 + 2)); // Check it looks all right AssertThat(out->sorted, Is().True()); @@ -1367,7 +1585,7 @@ go_bandit([]() { const bdd out = bdd_replace(__bdd(__bdd_3_unreduced, exec_policy()), m); // Check only called once to determine type of mapping and then for each level - AssertThat(m_calls, Is().EqualTo(2 * 3)); + AssertThat(m_calls, Is().EqualTo(3 + 3)); // Check it looks all right AssertThat(out->sorted, Is().True()); @@ -1704,7 +1922,7 @@ go_bandit([]() { bdd_replace(__bdd(__bdd_3_unreduced, exec_policy()), m, replace_type::Non_Monotone)); }); - it("reduces and shifts 'x0' if 'replace_type' is 'Monotone'", [&]() { + it("reduces and affinely maps 'x0' if 'replace_type' is 'Monotone'", [&]() { int m_calls = 0; const mapping_type m = [&m_calls](const int x) { m_calls++; @@ -1830,6 +2048,132 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); + it("reduces and maps shifted of variables in 'BDD 2' if 'replace_type' is 'Monotone' " + "[__bdd_2]", + [&]() { + int m_calls = 0; + const mapping_type m = [&m_calls](const int x) { + m_calls++; + return x + 1; + }; + const bdd out = bdd_replace(__bdd(__bdd_2, exec_policy()), m, replace_type::Monotone); + + // Check only called once per level + AssertThat(m_calls, Is().EqualTo(2)); + + // Check it looks all right + AssertThat(out->sorted, Is().True()); + AssertThat(out->indexable, Is().True()); + + node_test_stream out_nodes(out); + + // n2 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + + // n3 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(2, bdd::max_id - 1, terminal_T, terminal_F))); + + // n1 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(1, + bdd::max_id, + bdd::pointer_type(2, bdd::max_id), + bdd::pointer_type(2, bdd::max_id - 1)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 2u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(2u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(4u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(4u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + + it("reduces and shifts variables in 'BDD 2' if 'replace_type' is 'Shift' [__bdd_2]", [&]() { + int m_calls = 0; + const mapping_type m = [&m_calls](const int x) { + m_calls++; + return x + 1; + }; + const bdd out = bdd_replace(__bdd(__bdd_2, exec_policy()), m, replace_type::Shift); + + // Check is still called once per level + AssertThat(m_calls, Is().EqualTo(2)); + + // Check it looks all right + AssertThat(out->sorted, Is().True()); + AssertThat(out->indexable, Is().True()); + + node_test_stream out_nodes(out); + + // n2 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(2, bdd::max_id, terminal_F, terminal_T))); + + // n3 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(2, bdd::max_id - 1, terminal_T, terminal_F))); + + // n1 + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), + Is().EqualTo(node(1, + bdd::max_id, + bdd::pointer_type(2, bdd::max_id), + bdd::pointer_type(2, bdd::max_id - 1)))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(2, 2u))); + + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(1, 1u))); + + AssertThat(out_meta.can_pull(), Is().False()); + + AssertThat(out->width, Is().EqualTo(2u)); + + AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(4u)); + + AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(2u)); + AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(3u)); + AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(4u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(2u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); + it("returns the original file of 'x0' if 'replace_type' is 'Identity' with no calls", [&]() { // NOTE: This function is in fact *not* the identity! int m_calls = 0;