From f249c727d49ab6c6623e8ac1ba044272be795b8e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Wed, 12 Jun 2024 11:11:22 +0200 Subject: [PATCH] Prune subtrees and nodes during initial And-Transposition (WIP) --- src/adiar/bdd/apply.cpp | 5 + src/adiar/bdd/relprod.cpp | 174 +++- src/adiar/internal/algorithms/prod2.h | 7 +- src/adiar/zdd/binop.cpp | 5 + test/adiar/bdd/test_relprod.cpp | 1144 +++++++++++++++++++++++-- 5 files changed, 1259 insertions(+), 76 deletions(-) diff --git a/src/adiar/bdd/apply.cpp b/src/adiar/bdd/apply.cpp index 780910a3e..337049d5d 100644 --- a/src/adiar/bdd/apply.cpp +++ b/src/adiar/bdd/apply.cpp @@ -31,6 +31,11 @@ namespace adiar : _op(op) {} + public: + void + setup_next_level(const bdd::label_type /*next_level*/) const + {} + public: /// \brief Flip internal copy of operator void diff --git a/src/adiar/bdd/relprod.cpp b/src/adiar/bdd/relprod.cpp index ebeee77af..232def16a 100644 --- a/src/adiar/bdd/relprod.cpp +++ b/src/adiar/bdd/relprod.cpp @@ -2,17 +2,185 @@ #include #include +#include #include +#include namespace adiar { + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Product Construction policy for the BDD Relational Product. + /// + /// \details To improve performance, the `bdd_and` can be replaced with a special version that + /// simultaneously prunes its subtrees based on the quantification predicate. + ////////////////////////////////////////////////////////////////////////////////////////////////// + template + class relprod_prod2_policy + : public bdd_policy + , public internal::and_op + , public internal::prod2_mixed_level_merger + { + private: + const LevelPredicate& _pred; + bool _prune_level = false; + + public: + relprod_prod2_policy(const LevelPredicate& pred) + : _pred(pred) + {} + + public: + void + setup_next_level(const bdd::label_type next_level) + { + using result_type = typename LevelPredicate::result_type; + constexpr bool is_total_map = is_convertible; + + if constexpr (is_total_map) { + this->_prune_level = this->_pred(next_level); + } else { + this->_prune_level = !this->_pred(next_level).has_value(); + } + } + + public: + /// \brief Flip internal copy of operator + void + flip() + { + adiar_assert(internal::and_op::is_commutative()); + /* Do nothing... */ + } + + public: + /// \brief Hook for case of two BDDs with the same node file. + __bdd + resolve_same_file(const bdd& bdd_1, const bdd& bdd_2) const + { + return bdd_1.is_negated() == bdd_2.is_negated() ? bdd_1 : bdd_terminal(false); + } + + /// \brief Hook for either of the two BDDs being a terminal. + __bdd + resolve_terminal_root(const bdd& bdd_1, const bdd& bdd_2) const + { + adiar_assert(bdd_isterminal(bdd_1) || bdd_isterminal(bdd_2)); + + if (bdd_isterminal(bdd_1) && bdd_isterminal(bdd_2)) { + return bdd_terminal(internal::and_op::operator()(dd_valueof(bdd_1), dd_valueof(bdd_2))); + } else if (bdd_isterminal(bdd_1) && dd_valueof(bdd_1)) { + adiar_assert(internal::and_op::is_left_idempotent(dd_valueof(bdd_1))); + return bdd_2; + } else if (bdd_isterminal(bdd_2) && dd_valueof(bdd_2)) { + adiar_assert(internal::and_op::is_right_idempotent(dd_valueof(bdd_2))); + return bdd_1; + } + // and_op::can_left_shortcut(bdd_1) || and_op::can_right_shortcut(bdd_2) + return bdd_terminal(false); + } + + private: + /// \brief Applies shortcutting on a recursion target, if possible. + pair, bool> + __resolve_request(const internal::tuple& r) const + { + if (internal::and_op::can_left_shortcut(r[0]) || internal::and_op::can_right_shortcut(r[1])) { + return {{ bdd::pointer_type(false), bdd::pointer_type(false) }, true}; + } + return { r, false }; + } + + bool + __is_true(const internal::tuple& t) const + { + return (t[0] == bdd::pointer_type(true) && t[1] == bdd::pointer_type(true)); + } + + public: + /// \brief Hook for changing the targets of a new node's children. + internal::prod2_rec + resolve_request(const internal::tuple& r_low, + const internal::tuple& r_high) const + { + const auto [low, low_false] = this->__resolve_request(r_low); + const auto [high, high_false] = this->__resolve_request(r_high); + + // Prune subtree(s) if either child is 'false' and is quantified later. + if (this->_prune_level && (low_false || high_false)) { + return internal::prod2_rec_skipto{ low_false ? high : low }; + } + // Prune subtree(s) if either child is 'true' and is quantified later. + if (this->_prune_level && (this->__is_true(low) || this->__is_true(high))) { + return internal::prod2_rec_skipto{ bdd::pointer_type(true) }; + } + // Skip node with duplicated children requests + // + // NOTE: One could think to also prune 'redundant' nodes. Yet, these cannot be created as the + // tuples `(f1,f2)` and `(g1,g2)` could only have `(f1,g1) = (f2,g2)` if `f1 = f2` and + // `g1 = g2`. + // + // The only exception would be if `f1`, `f2`, `g1`, and `g2` are terminals. Yet, with + // the would 'and' operation, this can only happen if they are shortcutting to the + // 'false' terminal. Yet, this would only happen at the very bottom. With most variable + // orderings, this would be the next-state variable at the very bottom. + // + // In practice, it seems very unlikely these few edges are not cheaper to handle, than + // having this additional branch in the code (even if it is very predictable). + /* + if (low == high) { return internal::prod2_rec_skipto{ low }; } + */ + + return internal::prod2_rec_output{ low, high }; + } + + /// \brief Hook for applying an operator to a pair of terminals. + bdd::pointer_type + operator()(const bdd::pointer_type& a, const bdd::pointer_type& b) const + { + return internal::and_op::operator()(a, b); + } + + public: + /// \brief Hook for deriving the cut type of the left-hand-side. + internal::cut + left_cut() const + { + return internal::cut(!internal::and_op::can_left_shortcut(false), + !internal::and_op::can_left_shortcut(true)); + } + + /// \brief Hook for deriving the cut type of the right-hand-side. + internal::cut + right_cut() const + { + return internal::cut(!internal::and_op::can_right_shortcut(false), + !internal::and_op::can_right_shortcut(true)); + } + + /// \brief Due to pruning, this prod2 policy may introduce skipping of nodes. + static constexpr bool no_skip = false; + }; + + ////////////////////////////////////////////////////////////////////////////////////////////////// + template + __bdd + bdd_relprod__and(const exec_policy& ep, + const bdd& states, + const bdd& relation, + const LevelPredicate& pred) + { + relprod_prod2_policy policy(pred); + return internal::prod2(ep, states, relation, policy); + } + + ////////////////////////////////////////////////////////////////////////////////////////////////// bdd bdd_relprod(const exec_policy& ep, const bdd& states, const bdd& relation, const predicate& pred) { - return bdd_exists(ep, bdd_and(ep, states, relation), pred); + return bdd_exists(ep, bdd_relprod__and(ep, states, relation, pred), pred); } bdd @@ -28,7 +196,7 @@ namespace adiar const function(bdd::label_type)>& m, replace_type m_type) { - __bdd tmp_1 = bdd_and(ep, states, relation); + __bdd tmp_1 = bdd_relprod__and(ep, states, relation, m); const bdd tmp_2 = bdd_exists(ep, std::move(tmp_1), [&m](bdd::label_type x) { return !m(x).has_value(); }); @@ -80,7 +248,7 @@ namespace adiar const bdd tmp_1 = bdd_replace( ep, states, [&m](bdd::label_type x) { return m(x).value(); }, m_type); - __bdd tmp_2 = bdd_and(ep, std::move(tmp_1), relation); + __bdd tmp_2 = bdd_relprod__and(ep, std::move(tmp_1), relation, m); const bdd tmp_3 = bdd_exists(ep, std::move(tmp_2), [&m](bdd::label_type x) { return !m(x).has_value(); }); diff --git a/src/adiar/internal/algorithms/prod2.h b/src/adiar/internal/algorithms/prod2.h index 45d0c90b7..c9a1d7f94 100644 --- a/src/adiar/internal/algorithms/prod2.h +++ b/src/adiar/internal/algorithms/prod2.h @@ -279,7 +279,7 @@ namespace adiar::internal __prod2_ra(const exec_policy& ep, const typename Policy::dd_type& in_pq, const typename Policy::dd_type& in_ra, - const Policy& policy, + Policy& policy, const size_t pq_memory, const size_t max_pq_size) { @@ -311,6 +311,7 @@ namespace adiar::internal typename Policy::label_type out_label = prod_pq.current_level(); typename Policy::id_type out_id = 0; + policy.setup_next_level(out_label); in_nodes_ra.setup_next_level(out_label); // Update maximum 1-level cut @@ -401,7 +402,7 @@ namespace adiar::internal __prod2_pq(const exec_policy& ep, const typename Policy::dd_type& in_0, const typename Policy::dd_type& in_1, - const Policy& policy, + Policy& policy, const size_t pq_1_memory, const size_t max_pq_1_size, const size_t pq_2_memory, @@ -436,6 +437,8 @@ namespace adiar::internal const typename Policy::label_type out_label = prod_pq_1.current_level(); typename Policy::id_type out_id = 0; + policy.setup_next_level(out_label); + // Update max 1-level cut out_arcs->max_1level_cut = std::max(out_arcs->max_1level_cut, prod_pq_1.size()); diff --git a/src/adiar/zdd/binop.cpp b/src/adiar/zdd/binop.cpp index dcb8bed65..224c76137 100644 --- a/src/adiar/zdd/binop.cpp +++ b/src/adiar/zdd/binop.cpp @@ -81,6 +81,11 @@ namespace adiar , _can_right_shortcut{ zdd_prod2_policy::can_right_shortcut(op) } {} + public: + void + setup_next_level(const bdd::label_type /*next_level*/) const + {} + public: /// \brief Flip internal copy of operator void diff --git a/test/adiar/bdd/test_relprod.cpp b/test/adiar/bdd/test_relprod.cpp index c4f95451d..80ffe34db 100644 --- a/test/adiar/bdd/test_relprod.cpp +++ b/test/adiar/bdd/test_relprod.cpp @@ -276,7 +276,7 @@ go_bandit([]() { // '--' */ - // Here, they use a zipped variable ordering 'pre' and 'post' + // Here, they use a interleave variable ordering 'pre' and 'post' const auto huth_relnext_pred = [](int x) -> bool { return x % 2 == 0; }; const auto huth_relnext_map = [&huth_relnext_pred](int x) -> optional { @@ -2567,6 +2567,69 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); }); + it("has no successors for empty set of states []", [&]() { + const bdd out = bdd_relprod(false, true, kalin_relnext_pred); + + // 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_relprod(bdd_not(T), T, kalin_relnext_pred); + + // 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_relprod(false, kalin_fig9, kalin_relnext_pred); @@ -2660,7 +2723,70 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no successors for empty set of states [K&D Fig. 9]", [&]() { + it("has no predecessors for empty set of states []", [&]() { + const bdd out = bdd_relprod(false, true, kalin_relprev_pred); + + // 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 predecessors for empty set of states [] [~]", [&]() { + const bdd T = true; + const bdd out = bdd_relprod(bdd_not(T), T, kalin_relprev_pred); + + // 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 predecessors for empty set of states [K&D Fig. 9]", [&]() { const bdd out = bdd_relprod(false, kalin_fig9, kalin_relprev_pred); // Check it looks all right @@ -2691,7 +2817,7 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no successors for empty set of states [H&R Fig. 6.28]", [&]() { + it("has no predecessors for empty set of states [H&R Fig. 6.28]", [&]() { const bdd out = bdd_relprod(false, huth_fig28, huth_relprev_pred); // Check it looks all right @@ -2722,7 +2848,7 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); - it("has no successors for empty set of states [B Fig. 6.28]", [&]() { + it("has no predecessors for empty set of states [B Fig. 6.28]", [&]() { const bdd out = bdd_relprod(false, bryant_fig18, bryant_relprev_pred); // Check it looks all right @@ -2752,6 +2878,254 @@ go_bandit([]() { 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_relprod(kalin_fig11, false, kalin_relnext_pred); + + // 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_relprod(bdd_not(F), F, kalin_relnext_pred); + + // 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_relprod(F, F, kalin_relnext_pred); + + AssertThat(out.file_ptr(), Is().EqualTo(F.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("has no predecessors for empty set of edges [K&D Fig. 11 + ]", [&]() { + shared_levelized_file shifted_states; + /* + // Figure 11 of Kalin's & Dahlsen-Jensen's BSc Thesis "Symbolic Algorithms for Computing + // Strongly Connected Components" + // + // 1 ---- x3 (1') + // / \ + // F T + */ + { // Garbage collect early and free write-lock + node_writer nw(shifted_states); + nw << node(3, bdd::max_id, terminal_F, terminal_T); + } + + const bdd out = bdd_relprod(shifted_states, false, kalin_relprev_pred); + + // 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 predecessors for empty set of edges [~ + ]", [&]() { + const bdd F = false; + const bdd out = bdd_relprod(bdd_not(F), F, kalin_relprev_pred); + + // 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 predecessors for empty set of nodes and edges []", [&]() { + const bdd F = false; + const bdd out = bdd_relprod(F, F, kalin_relprev_pred); + + 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_relprod(kalin_fig11, true, kalin_relnext_pred); + + // 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_relprod(T, T, kalin_relnext_pred); + + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); + + it("has all predecessors for total graph [K&D Fig. 11 + ]", [&]() { + shared_levelized_file shifted_states; + /* + // Figure 11 of Kalin's & Dahlsen-Jensen's BSc Thesis "Symbolic Algorithms for Computing + // Strongly Connected Components" + // + // 1 ---- x3 (1') + // / \ + // F T + */ + { // Garbage collect early and free write-lock + node_writer nw(shifted_states); + nw << node(3, bdd::max_id, terminal_F, terminal_T); + } + + const bdd out = bdd_relprod(shifted_states, true, kalin_relprev_pred); + + // 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 predecessors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relprod(T, T, kalin_relprev_pred); + + AssertThat(out.file_ptr(), Is().EqualTo(T.file_ptr())); + AssertThat(out.is_negated(), Is().False()); + }); }); describe("bdd_relnext(const bdd&, const bdd&, )", [&]() { @@ -3418,105 +3792,261 @@ go_bandit([]() { 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(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); + + // 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); + + // 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); + + // 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); + + // 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); + + // 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(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 [{01,10} + B Fig. 18 (x:=1)]", [&]() { - const bdd out = bdd_relnext(bryant_01_10, bryant_fig18_x1, bryant_relnext_map); + 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); // 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().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_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().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->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("excludes source states [{__} + B Fig. 18]", [&]() { - const bdd out = bdd_relnext(true, bryant_fig18, bryant_relnext_map); + it("has no successors for empty set of states [B Fig. 6.28]", [&]() { + const bdd out = bdd_relnext(false, bryant_fig18, bryant_relnext_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 no successors for empty set of states [K&D Fig. 9]", [&]() { - const bdd out = bdd_relnext(false, kalin_fig9, kalin_relnext_map); + it("has no successors for empty set of edges [K&D Fig. 11 + ]", [&]() { + const bdd out = bdd_relnext(kalin_fig11, false, kalin_relnext_map); // Check it looks all right node_test_stream out_nodes(out); @@ -3546,8 +4076,9 @@ go_bandit([]() { 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); + 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); // Check it looks all right node_test_stream out_nodes(out); @@ -3577,14 +4108,22 @@ go_bandit([]() { 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); + 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); + + 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); // 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()); @@ -3595,17 +4134,25 @@ 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 all successors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relnext(T, T, kalin_relnext_map); + + 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]", [&]() { @@ -4075,6 +4622,69 @@ go_bandit([]() { 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); @@ -4161,12 +4771,122 @@ go_bandit([]() { 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(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(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 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]", [&]() { @@ -5080,6 +5800,37 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); + 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(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 predecessors for empty set of states [K&D Fig. 9]", [&]() { const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map); @@ -5173,6 +5924,116 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); + 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); + + 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 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); + + 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 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(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); @@ -5763,6 +6624,37 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(1u)); }); + it("has no predecessors for empty set of states []", [&]() { + const bdd out = bdd_relprev(false, true, 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(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 predecessors for empty set of states [K&D Fig. 9]", [&]() { const bdd out = bdd_relprev(false, kalin_fig9, kalin_relprev_map, replace_type::Monotone); @@ -5857,6 +6749,116 @@ go_bandit([]() { AssertThat(out->number_of_terminals[true], Is().EqualTo(0u)); }); + 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); + + // 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 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); + + // 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 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); + + 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); + + // 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 predecessors for all nodes and total graph []", [&]() { + const bdd T = true; + const bdd out = bdd_relprev(T, T, kalin_relprev_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 [{01} + K&D Fig. 9]", [&]() { // NOTE: We actually provide a Monotone map, but do not claim to do so! AssertThrows(