From d2a9498cb3b233118aec4fce3927580dbb43c69f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Tue, 30 Apr 2024 16:43:44 +0200 Subject: [PATCH 1/6] Fix GitHub action for Mac is out-of-date --- .github/workflows/mac.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/mac.yml b/.github/workflows/mac.yml index 506027e5a..8703eb215 100644 --- a/.github/workflows/mac.yml +++ b/.github/workflows/mac.yml @@ -36,14 +36,14 @@ jobs: os: [macos-latest] cc: # GNU Compiler - - { cc: gcc, v: 10, cxx: g++, xcode: latest } + - { cc: gcc, v: 11, cxx: g++, xcode: latest } # oldest supported on Apple Silicon - { cc: gcc, v: 12, cxx: g++, xcode: latest } + - { cc: gcc, v: 13, cxx: g++, xcode: latest } # Clang Compiler - - { cc: clang, cxx: clang++, xcode: 13.1 } # oldest - - { cc: clang, cxx: clang++, xcode: 13.4 } - - { cc: clang, cxx: clang++, xcode: 14.0 } - - { cc: clang, cxx: clang++, xcode: 14.2 } # newest + - { cc: clang, cxx: clang++, xcode: 14.3 } # oldest supported + - { cc: clang, cxx: clang++, xcode: 15.0 } + - { cc: clang, cxx: clang++, xcode: latest } steps: # Git repo set up @@ -68,7 +68,7 @@ jobs: run: | if [ "${{matrix.cc.cc}}" = "gcc" ]; then echo "================================" - echo "Compiler" + echo GCC "Compiler" brew install ${{matrix.cc.cc}}@${{matrix.cc.v}} fi From ed1cf5f28cab85cbfd230145d94ba15674e1ccab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Tue, 30 Apr 2024 14:23:54 +0200 Subject: [PATCH 2/6] Add 'quantify pred-profile' to have more information for heuristics --- src/adiar/internal/algorithms/quantify.h | 191 ++++-- src/adiar/internal/dd_func.h | 10 + test/adiar/bdd/test_quantify.cpp | 791 ++++++++++------------- test/adiar/zdd/test_project.cpp | 228 +++---- 4 files changed, 605 insertions(+), 615 deletions(-) diff --git a/src/adiar/internal/algorithms/quantify.h b/src/adiar/internal/algorithms/quantify.h index a2245a7e5..10f596ebd 100644 --- a/src/adiar/internal/algorithms/quantify.h +++ b/src/adiar/internal/algorithms/quantify.h @@ -1359,72 +1359,149 @@ namespace adiar::internal }; ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Obtain the deepest level that satisfies (or not) the requested level. - ////////////////////////////////////////////////////////////////////////////////////////////////// - // TODO: optimisations - // - initial cheap check on is_terminal. - // - initial '__quantify__get_deepest' should not terminate early but - // determine whether any variable may "survive". template - inline typename Policy::label_type - __quantify__get_deepest(const typename Policy::dd_type& dd, - const predicate& pred) + struct quantify__pred_profile { - level_info_stream lis(dd); + private: - while (lis.can_pull()) { - const typename Policy::label_type l = lis.pull().label(); - if (pred(l) == Policy::quantify_onset) { return l; } - } - return Policy::max_label + 1; - } + public: + /// \brief Total number of nodes in the diagram. + size_t dd_size; + + /// \brief Width of the diagram. + size_t dd_width; + + /// \brief Total number of variables in the diagram. + size_t dd_vars; + + /// \brief Number of nodes of *all* to-be quantified levels. + size_t quant_all_size = 0u; + + /// \brief Number of *all* to-be quantified levels. + size_t quant_all_vars = 0u; + + /// \brief Number of *deep* to-be quantified levels, i.e. the last N/3 nodes. + size_t quant_deep_vars = 0u; + + /// \brief Number of *shallow* to-be quantified levels, i.e. the first N/3 nodes. + size_t quant_shallow_vars = 0u; + + struct var_data + { + /// \brief The to-be quantified variable. + typename Policy::label_type level; + + /// \brief Number of nodes below this level (not inclusive) + size_t nodes_below; + + /// \brief Number of nodes on said level + typename Policy::id_type width; + }; + + /// \brief The *deepest* to-be quantified level. + var_data deepest_var + { + 0, + std::numeric_limits::max(), + Policy::max_id+1 + }; + + /// \brief The *shallowest* to-be quantified level. + var_data shallowest_var + { + Policy::max_label+1, + std::numeric_limits::max(), + Policy::max_id+1 + }; + + /// \brief The *widest* to-be quantified level. + var_data widest_var + { + Policy::max_label+1, + std::numeric_limits::max(), + 0, + }; + + /// \brief The *narrowest* to-be quantified level. + var_data narrowest_var + { + Policy::max_label+1, + std::numeric_limits::max(), + Policy::max_id+1 + }; + }; ////////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Heuristically derive a bound for the number of partial sweeps based on the graph meta - /// data. + /// \brief Obtain the deepest level that satisfies (or not) the requested level. ////////////////////////////////////////////////////////////////////////////////////////////////// template - inline typename Policy::label_type - __quantify__max_partial_sweeps(const typename Policy::dd_type& dd, - const predicate& pred) + inline quantify__pred_profile + __quantify__pred_profile(const typename Policy::dd_type& dd, + const predicate& pred) { - // Extract meta data constants about the DAG - const size_t size = dd.size(); - const size_t width = dd.width(); - - // --------------------------------------------------------------------------------------------- - // Shallow Variables Heuristic - - // Keep track of the number of nodes on the top-most levels in relation to the total size - size_t seen_nodes = 0u; + // TODO: tighten definition of 'shallow' and 'deep' variables based on widest level - // Threshold to stop after the first n/3 nodes. - const size_t max_nodes = size / 3; + quantify__pred_profile res; + res.dd_size = dd_nodecount(dd); + res.dd_width = dd_width(dd); + res.dd_vars = dd_varcount(dd); - // TODO: Turn `shallow_variables` into a double and decrease the weight of to-be quantified - // variables depending on `seen_nodes`, the number of levels of width `width`, and/or in - // general using a (quadratic?) decay. - typename Policy::label_type shallow_variables = 0u; + level_info_stream lis(dd); - level_info_stream lis(dd); + const size_t third_dd_size = res.dd_size / 3; + size_t nodes_below = 0u; while (lis.can_pull()) { const level_info li = lis.pull(); + if (pred(li.label()) == Policy::quantify_onset) { + res.quant_all_vars += 1u; + res.quant_all_size += li.width(); + res.quant_deep_vars += nodes_below + 1 <= third_dd_size; + res.quant_shallow_vars += res.dd_size - third_dd_size <= nodes_below + li.width(); + + { // Shallowest variable (always updated due to bottom-up direction). + res.shallowest_var.level = li.level(); + res.shallowest_var.nodes_below = nodes_below; + res.shallowest_var.width = li.width(); + } + // Deepest variable. + if (res.deepest_var.level < li.level()) { + res.deepest_var = res.shallowest_var; + } + // Widest variable + if (res.widest_var.width < li.width()) { + res.widest_var = res.shallowest_var; + } + // Narrowest variable + if (li.width() < res.narrowest_var.width) { + res.narrowest_var = res.shallowest_var; + } + } - if (pred(li.label()) == Policy::quantify_onset) { shallow_variables++; } - - // Stop at the (first) widest level - if (li.width() == width) { break; } - - // Stop when having seen too many nodes - seen_nodes += li.width(); - if (max_nodes < seen_nodes) { break; } + nodes_below += li.width(); } + return res; + } - adiar_assert(shallow_variables <= Policy::max_label); + ////////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Obtain the deepest level that satisfies (or not) the requested level. + ////////////////////////////////////////////////////////////////////////////////////////////////// + // TODO: optimisations + // - initial cheap check on is_terminal. + // - initial '__quantify__get_deepest' should not terminate early but + // determine whether any variable may "survive". + template + inline typename Policy::label_type + __quantify__get_deepest(const typename Policy::dd_type& dd, + const predicate& pred) + { + level_info_stream lis(dd); - // --------------------------------------------------------------------------------------------- - return shallow_variables; + while (lis.can_pull()) { + const typename Policy::label_type l = lis.pull().label(); + if (pred(l) == Policy::quantify_onset) { return l; } + } + return Policy::max_label + 1; } ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1439,15 +1516,22 @@ namespace adiar::internal using unreduced_t = typename Policy::__dd_type; // TODO: check for missing std::move(...) - typename Policy::label_type label = __quantify__get_deepest(dd, pred); + const quantify__pred_profile pred_profile = __quantify__pred_profile(dd, pred); - if (Policy::max_label < label) { + // ----------------------------------------------------------------------- + // Case: Nothing to do + if (pred_profile.quant_all_vars == 0u) { #ifdef ADIAR_STATS stats_quantify.skipped += 1u; #endif return dd; } + // ----------------------------------------------------------------------- + // Case: Only one variable to quantify + // + // TODO: pred_profile.quant_all_vars == 1u + switch (ep.template get()) { case exec_policy::quantify::Singleton: { // --------------------------------------------------------------------- @@ -1455,6 +1539,8 @@ namespace adiar::internal #ifdef ADIAR_STATS stats_quantify.singleton_sweeps += 1u; #endif + typename Policy::label_type label = pred_profile.deepest_var.level; + while (label <= Policy::max_label) { dd = quantify(ep, dd, label); if (dd_isterminal(dd)) { return dd; } @@ -1467,19 +1553,18 @@ namespace adiar::internal case exec_policy::quantify::Nested: { // --------------------------------------------------------------------- // Case: Nested Sweeping - const size_t dd_size = dd.size(); // Do Partial Quantification as long as... // 1. ... it stays smaller than 1+epsilon of the input size. const size_t transposition__size_threshold = (std::min( static_cast(std::numeric_limits::max() / 2u), static_cast(ep.template get()) - * static_cast(dd_size))); + * static_cast(pred_profile.dd_size))); // 2. ... it has not run more than the maximum number of iterations. const size_t transposition__max_iterations = std::min({ ep.template get(), - __quantify__max_partial_sweeps(dd, pred) }); + pred_profile.quant_shallow_vars }); unreduced_t transposed; diff --git a/src/adiar/internal/dd_func.h b/src/adiar/internal/dd_func.h index a9eebd566..160fa9e51 100644 --- a/src/adiar/internal/dd_func.h +++ b/src/adiar/internal/dd_func.h @@ -131,6 +131,16 @@ namespace adiar::internal return dd->levels(); } + //////////////////////////////////////////////////////////////////////////// + /// \brief Number of nodes on the widest level of a decision diagram. + //////////////////////////////////////////////////////////////////////////// + template + size_t + dd_width(const DD& dd) + { + return dd.width(); + } + //////////////////////////////////////////////////////////////////////////// /// \brief The variable labels (in order of their level) that are present in a /// decision diagram. diff --git a/test/adiar/bdd/test_quantify.cpp b/test/adiar/bdd/test_quantify.cpp index 42fdb05e1..4e74a5b30 100644 --- a/test/adiar/bdd/test_quantify.cpp +++ b/test/adiar/bdd/test_quantify.cpp @@ -2516,8 +2516,6 @@ go_bandit([]() { return true; }); - AssertThat(calls, Is().EqualTo(1)); - node_test_stream out_nodes(out); AssertThat(out_nodes.can_pull(), Is().True()); @@ -2529,6 +2527,9 @@ go_bandit([]() { AssertThat(out_meta.can_pull(), Is().False()); // TODO: meta variables... + + // One call per level for the profile + AssertThat(calls, Is().EqualTo(2)); }); it("quantifies with always-true predicate in BDD 4 [&&]", [&]() { @@ -2610,26 +2611,24 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(10u)); + AssertThat(call_history.size(), Is().EqualTo(11u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 5 nodes + AssertThat(call_history.at(1), Is().EqualTo(2u)); + AssertThat(call_history.at(2), Is().EqualTo(1u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(5), Is().EqualTo(1u)); + AssertThat(call_history.at(6), Is().EqualTo(2u)); + AssertThat(call_history.at(7), Is().EqualTo(3u)); // - Nested sweep looking for the 'next_inner' bottom-up - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(1u)); - AssertThat(call_history.at(9), Is().EqualTo(0u)); + AssertThat(call_history.at(8), Is().EqualTo(2u)); + AssertThat(call_history.at(9), Is().EqualTo(1u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); }); it("prunes to-be quantified nodes with true terminals", [&]() { @@ -2661,25 +2660,24 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(9u)); + AssertThat(call_history.size(), Is().EqualTo(11u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(2), Is().EqualTo(0u)); // ? + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(3u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); // - Nested sweep (nothing to be done) - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(0u)); + AssertThat(call_history.at(9), Is().EqualTo(2u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); }); it("collapses root with true terminal during pruning transposition", [&]() { @@ -2705,13 +2703,10 @@ go_bandit([]() { // verify that this change makes sense and is as intended. AssertThat(call_history.size(), Is().EqualTo(4u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 4 nodes + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(0u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -2752,27 +2747,26 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(11u)); + AssertThat(call_history.size(), Is().EqualTo(13u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(2), Is().EqualTo(0u)); // ? + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(3u)); - AssertThat(call_history.at(7), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); // - Nested sweep (nothing to be done) - AssertThat(call_history.at(8), Is().EqualTo(4u)); - AssertThat(call_history.at(9), Is().EqualTo(2u)); - AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(0u)); }); it("collapses to terminal during transposition as root with false is pruned", [&]() { @@ -2798,13 +2792,10 @@ go_bandit([]() { // verify that this change makes sense and is as intended. AssertThat(call_history.size(), Is().EqualTo(7u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 4 nodes + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(0u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -2872,26 +2863,24 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(10u)); + AssertThat(call_history.size(), Is().EqualTo(11u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 5 nodes + AssertThat(call_history.at(1), Is().EqualTo(2u)); + AssertThat(call_history.at(2), Is().EqualTo(1u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(5), Is().EqualTo(1u)); + AssertThat(call_history.at(6), Is().EqualTo(2u)); + AssertThat(call_history.at(7), Is().EqualTo(3u)); // - Nested sweep looking for the 'next_inner' bottom-up - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(1u)); - AssertThat(call_history.at(9), Is().EqualTo(0u)); + AssertThat(call_history.at(8), Is().EqualTo(2u)); + AssertThat(call_history.at(9), Is().EqualTo(1u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); }); it("prunes to-be quantified nodes with true terminals", [&]() { @@ -2923,25 +2912,24 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(9u)); + AssertThat(call_history.size(), Is().EqualTo(11u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(2), Is().EqualTo(0u)); // ? + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(3u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); // - Nested sweep (nothing to be done) - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(0u)); + AssertThat(call_history.at(9), Is().EqualTo(2u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); }); it("collapses root with true terminal during pruning transposition", [&]() { @@ -2967,13 +2955,10 @@ go_bandit([]() { // verify that this change makes sense and is as intended. AssertThat(call_history.size(), Is().EqualTo(4u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 4 nodes + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(0u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -3014,27 +2999,26 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(11u)); + AssertThat(call_history.size(), Is().EqualTo(13u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(2), Is().EqualTo(0u)); // ? + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(3u)); - AssertThat(call_history.at(7), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); // - Nested sweep (nothing to be done) - AssertThat(call_history.at(8), Is().EqualTo(4u)); - AssertThat(call_history.at(9), Is().EqualTo(2u)); - AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(0u)); }); it("collapses to terminal during transposition as root with false is pruned", [&]() { @@ -3060,13 +3044,10 @@ go_bandit([]() { // verify that this change makes sense and is as intended. AssertThat(call_history.size(), Is().EqualTo(7u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 4 nodes + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(0u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -3208,15 +3189,12 @@ go_bandit([]() { // that this change makes sense and is as intended. AssertThat(call_history.size(), Is().EqualTo(15u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(2), Is().EqualTo(0u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(2u)); // 4 out of 8 nodes + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - Pruning sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -3573,19 +3551,18 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(6u)); + AssertThat(call_history.size(), Is().EqualTo(7u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 5 nodes + AssertThat(call_history.at(1), Is().EqualTo(2u)); + AssertThat(call_history.at(2), Is().EqualTo(1u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(5), Is().EqualTo(1u)); + AssertThat(call_history.at(6), Is().EqualTo(2u)); }); it("finishes during initial transposition of even variables in BDD 4 [const &]", [&]() { @@ -3630,13 +3607,11 @@ go_bandit([]() { // verify that this change makes sense and is as intended. AssertThat(call_history.size(), Is().EqualTo(8u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(3u)); AssertThat(call_history.at(1), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(2), Is().EqualTo(0u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); // 2 out of 5 nodes + AssertThat(call_history.at(2), Is().EqualTo(1u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); // - First top-down sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -3645,7 +3620,7 @@ go_bandit([]() { AssertThat(call_history.at(7), Is().EqualTo(3u)); }); - it("collapses during repeated transposition with variables 1 and 2 in BDD 12a [&&]", + it("collapses during repeated transposition in BDD 12a [&&]", [&]() { std::vector call_history; bdd out = bdd_exists(ep & exec_policy::access::Random_Access, @@ -3670,33 +3645,29 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(14u)); + AssertThat(call_history.size(), Is().EqualTo(13u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); // width + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(6), Is().EqualTo(0u)); - AssertThat(call_history.at(7), Is().EqualTo(1u)); - AssertThat(call_history.at(8), Is().EqualTo(2u)); - AssertThat(call_history.at(9), Is().EqualTo(3u)); - AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); // - Second top-down sweep - AssertThat(call_history.at(11), Is().EqualTo(0u)); - AssertThat(call_history.at(12), Is().EqualTo(2u)); - AssertThat(call_history.at(13), Is().EqualTo(3u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(3u)); }); - it( - "finishes during repeated transposition with variables 1 and 2 in BDD 12b [&&]", [&]() { + it("finishes during repeated transposition in BDD 12b [&&]", [&]() { std::vector call_history; bdd out = bdd_exists(ep & exec_policy::access::Random_Access, bdd_12b, @@ -3778,30 +3749,27 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(15u)); + AssertThat(call_history.size(), Is().EqualTo(14u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); // width + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(6), Is().EqualTo(0u)); - AssertThat(call_history.at(7), Is().EqualTo(1u)); - AssertThat(call_history.at(8), Is().EqualTo(2u)); - AssertThat(call_history.at(9), Is().EqualTo(3u)); - AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); // - Second top-down sweep - AssertThat(call_history.at(11), Is().EqualTo(0u)); - AssertThat(call_history.at(12), Is().EqualTo(2u)); - AssertThat(call_history.at(13), Is().EqualTo(3u)); - AssertThat(call_history.at(14), Is().EqualTo(4u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(3u)); + AssertThat(call_history.at(13), Is().EqualTo(4u)); }); it("finishes during repeated transposition with variables 1 and 2 in BDD 13 [&&]", [&]() { @@ -3965,9 +3933,9 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(26u)); + AssertThat(call_history.size(), Is().EqualTo(23u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(7u)); AssertThat(call_history.at(1), Is().EqualTo(6u)); AssertThat(call_history.at(2), Is().EqualTo(5u)); @@ -3975,31 +3943,26 @@ go_bandit([]() { AssertThat(call_history.at(4), Is().EqualTo(3u)); AssertThat(call_history.at(5), Is().EqualTo(2u)); AssertThat(call_history.at(6), Is().EqualTo(1u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. AssertThat(call_history.at(7), Is().EqualTo(0u)); - AssertThat(call_history.at(8), Is().EqualTo(1u)); - AssertThat(call_history.at(9), Is().EqualTo(2u)); - AssertThat(call_history.at(10), Is().EqualTo(3u)); // 7 out of 16 nodes // - First top-down sweep - AssertThat(call_history.at(11), Is().EqualTo(0u)); - AssertThat(call_history.at(12), Is().EqualTo(1u)); - AssertThat(call_history.at(13), Is().EqualTo(2u)); - AssertThat(call_history.at(14), Is().EqualTo(3u)); - AssertThat(call_history.at(15), Is().EqualTo(4u)); - AssertThat(call_history.at(16), Is().EqualTo(5u)); - AssertThat(call_history.at(17), Is().EqualTo(6u)); - AssertThat(call_history.at(18), Is().EqualTo(7u)); + AssertThat(call_history.at(8), Is().EqualTo(0u)); + AssertThat(call_history.at(9), Is().EqualTo(1u)); + AssertThat(call_history.at(10), Is().EqualTo(2u)); + AssertThat(call_history.at(11), Is().EqualTo(3u)); + AssertThat(call_history.at(12), Is().EqualTo(4u)); + AssertThat(call_history.at(13), Is().EqualTo(5u)); + AssertThat(call_history.at(14), Is().EqualTo(6u)); + AssertThat(call_history.at(15), Is().EqualTo(7u)); // - Second top-down sweep - AssertThat(call_history.at(19), Is().EqualTo(1u)); - AssertThat(call_history.at(20), Is().EqualTo(2u)); - AssertThat(call_history.at(21), Is().EqualTo(3u)); - AssertThat(call_history.at(22), Is().EqualTo(4u)); - AssertThat(call_history.at(23), Is().EqualTo(5u)); - AssertThat(call_history.at(24), Is().EqualTo(6u)); - AssertThat(call_history.at(25), Is().EqualTo(7u)); + AssertThat(call_history.at(16), Is().EqualTo(1u)); + AssertThat(call_history.at(17), Is().EqualTo(2u)); + AssertThat(call_history.at(18), Is().EqualTo(3u)); + AssertThat(call_history.at(19), Is().EqualTo(4u)); + AssertThat(call_history.at(20), Is().EqualTo(5u)); + AssertThat(call_history.at(21), Is().EqualTo(6u)); + AssertThat(call_history.at(22), Is().EqualTo(7u)); }); it("finishes early during repeated transposition [&&]", [&]() { @@ -4033,21 +3996,20 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(8u)); + AssertThat(call_history.size(), Is().EqualTo(9u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(2u)); // width + AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(4), Is().EqualTo(0u)); - AssertThat(call_history.at(5), Is().EqualTo(1u)); - AssertThat(call_history.at(6), Is().EqualTo(2u)); - AssertThat(call_history.at(7), Is().EqualTo(3u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); // NOTE: Even though there are three levels that should be quantified, we only do one // partial quantification. @@ -4327,9 +4289,9 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(47u)); + AssertThat(call_history.size(), Is().EqualTo(41u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(13u)); AssertThat(call_history.at(1), Is().EqualTo(12u)); AssertThat(call_history.at(2), Is().EqualTo(11u)); @@ -4343,46 +4305,38 @@ go_bandit([]() { AssertThat(call_history.at(10), Is().EqualTo(3u)); AssertThat(call_history.at(11), Is().EqualTo(2u)); AssertThat(call_history.at(12), Is().EqualTo(1u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. AssertThat(call_history.at(13), Is().EqualTo(0u)); - AssertThat(call_history.at(14), Is().EqualTo(1u)); - AssertThat(call_history.at(15), Is().EqualTo(2u)); - AssertThat(call_history.at(16), Is().EqualTo(3u)); - AssertThat(call_history.at(17), Is().EqualTo(4u)); - AssertThat(call_history.at(18), Is().EqualTo(5u)); - AssertThat(call_history.at(19), Is().EqualTo(6u)); // 13 out of 34 nodes // - First top-down sweep - AssertThat(call_history.at(20), Is().EqualTo(0u)); - AssertThat(call_history.at(21), Is().EqualTo(1u)); - AssertThat(call_history.at(22), Is().EqualTo(2u)); - AssertThat(call_history.at(23), Is().EqualTo(3u)); - AssertThat(call_history.at(24), Is().EqualTo(4u)); - AssertThat(call_history.at(25), Is().EqualTo(5u)); - AssertThat(call_history.at(26), Is().EqualTo(6u)); - AssertThat(call_history.at(27), Is().EqualTo(7u)); - AssertThat(call_history.at(28), Is().EqualTo(8u)); - AssertThat(call_history.at(29), Is().EqualTo(9u)); - AssertThat(call_history.at(30), Is().EqualTo(10u)); - AssertThat(call_history.at(31), Is().EqualTo(11u)); - AssertThat(call_history.at(32), Is().EqualTo(12u)); - AssertThat(call_history.at(33), Is().EqualTo(13u)); + AssertThat(call_history.at(14), Is().EqualTo(0u)); + AssertThat(call_history.at(15), Is().EqualTo(1u)); + AssertThat(call_history.at(16), Is().EqualTo(2u)); + AssertThat(call_history.at(17), Is().EqualTo(3u)); + AssertThat(call_history.at(18), Is().EqualTo(4u)); + AssertThat(call_history.at(19), Is().EqualTo(5u)); + AssertThat(call_history.at(20), Is().EqualTo(6u)); + AssertThat(call_history.at(21), Is().EqualTo(7u)); + AssertThat(call_history.at(22), Is().EqualTo(8u)); + AssertThat(call_history.at(23), Is().EqualTo(9u)); + AssertThat(call_history.at(24), Is().EqualTo(10u)); + AssertThat(call_history.at(25), Is().EqualTo(11u)); + AssertThat(call_history.at(26), Is().EqualTo(12u)); + AssertThat(call_history.at(27), Is().EqualTo(13u)); // - Second top-down sweep - AssertThat(call_history.at(34), Is().EqualTo(1u)); - AssertThat(call_history.at(35), Is().EqualTo(2u)); - AssertThat(call_history.at(36), Is().EqualTo(3u)); - AssertThat(call_history.at(37), Is().EqualTo(4u)); - AssertThat(call_history.at(38), Is().EqualTo(5u)); - AssertThat(call_history.at(39), Is().EqualTo(6u)); - AssertThat(call_history.at(40), Is().EqualTo(7u)); - AssertThat(call_history.at(41), Is().EqualTo(8u)); - AssertThat(call_history.at(42), Is().EqualTo(9u)); - AssertThat(call_history.at(43), Is().EqualTo(10u)); - AssertThat(call_history.at(44), Is().EqualTo(11u)); - AssertThat(call_history.at(45), Is().EqualTo(12u)); - AssertThat(call_history.at(46), Is().EqualTo(13u)); + AssertThat(call_history.at(28), Is().EqualTo(1u)); + AssertThat(call_history.at(29), Is().EqualTo(2u)); + AssertThat(call_history.at(30), Is().EqualTo(3u)); + AssertThat(call_history.at(31), Is().EqualTo(4u)); + AssertThat(call_history.at(32), Is().EqualTo(5u)); + AssertThat(call_history.at(33), Is().EqualTo(6u)); + AssertThat(call_history.at(34), Is().EqualTo(7u)); + AssertThat(call_history.at(35), Is().EqualTo(8u)); + AssertThat(call_history.at(36), Is().EqualTo(9u)); + AssertThat(call_history.at(37), Is().EqualTo(10u)); + AssertThat(call_history.at(38), Is().EqualTo(11u)); + AssertThat(call_history.at(39), Is().EqualTo(12u)); + AssertThat(call_history.at(40), Is().EqualTo(13u)); }); }); @@ -4411,19 +4365,18 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(6u)); + AssertThat(call_history.size(), Is().EqualTo(7u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 5 nodes + AssertThat(call_history.at(1), Is().EqualTo(2u)); + AssertThat(call_history.at(2), Is().EqualTo(1u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(5), Is().EqualTo(1u)); + AssertThat(call_history.at(6), Is().EqualTo(2u)); }); it("finishes during initial transposition of even variables in BDD 4 [const &]", [&]() { @@ -4468,13 +4421,11 @@ go_bandit([]() { // verify that this change makes sense and is as intended. AssertThat(call_history.size(), Is().EqualTo(8u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(3u)); AssertThat(call_history.at(1), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(2), Is().EqualTo(0u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); // 2 out of 5 nodes + AssertThat(call_history.at(2), Is().EqualTo(1u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); // - First top-down sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -4483,7 +4434,7 @@ go_bandit([]() { AssertThat(call_history.at(7), Is().EqualTo(3u)); }); - it("collapses during repeated transposition with variables 1 and 2 in BDD 12a [&&]", + it("collapses during repeated transposition in BDD 12a [&&]", [&]() { std::vector call_history; bdd out = bdd_exists(ep & exec_policy::access::Priority_Queue, @@ -4508,33 +4459,29 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(14u)); + AssertThat(call_history.size(), Is().EqualTo(13u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); // width + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(6), Is().EqualTo(0u)); - AssertThat(call_history.at(7), Is().EqualTo(1u)); - AssertThat(call_history.at(8), Is().EqualTo(2u)); - AssertThat(call_history.at(9), Is().EqualTo(3u)); - AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); // - Second top-down sweep - AssertThat(call_history.at(11), Is().EqualTo(0u)); - AssertThat(call_history.at(12), Is().EqualTo(2u)); - AssertThat(call_history.at(13), Is().EqualTo(3u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(3u)); }); - it( - "finishes during repeated transposition with variables 1 and 2 in BDD 12b [&&]", [&]() { + it("finishes during repeated transposition in BDD 12b [&&]", [&]() { std::vector call_history; bdd out = bdd_exists(ep & exec_policy::access::Priority_Queue, bdd_12b, @@ -4616,30 +4563,27 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(15u)); + AssertThat(call_history.size(), Is().EqualTo(14u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); // width + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(6), Is().EqualTo(0u)); - AssertThat(call_history.at(7), Is().EqualTo(1u)); - AssertThat(call_history.at(8), Is().EqualTo(2u)); - AssertThat(call_history.at(9), Is().EqualTo(3u)); - AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); // - Second top-down sweep - AssertThat(call_history.at(11), Is().EqualTo(0u)); - AssertThat(call_history.at(12), Is().EqualTo(2u)); - AssertThat(call_history.at(13), Is().EqualTo(3u)); - AssertThat(call_history.at(14), Is().EqualTo(4u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(3u)); + AssertThat(call_history.at(13), Is().EqualTo(4u)); }); it("finishes during repeated transposition with variables 1 and 2 in BDD 13 [&&]", [&]() { @@ -4803,9 +4747,9 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(26u)); + AssertThat(call_history.size(), Is().EqualTo(23u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(7u)); AssertThat(call_history.at(1), Is().EqualTo(6u)); AssertThat(call_history.at(2), Is().EqualTo(5u)); @@ -4813,31 +4757,26 @@ go_bandit([]() { AssertThat(call_history.at(4), Is().EqualTo(3u)); AssertThat(call_history.at(5), Is().EqualTo(2u)); AssertThat(call_history.at(6), Is().EqualTo(1u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. AssertThat(call_history.at(7), Is().EqualTo(0u)); - AssertThat(call_history.at(8), Is().EqualTo(1u)); - AssertThat(call_history.at(9), Is().EqualTo(2u)); - AssertThat(call_history.at(10), Is().EqualTo(3u)); // 7 out of 16 nodes // - First top-down sweep - AssertThat(call_history.at(11), Is().EqualTo(0u)); - AssertThat(call_history.at(12), Is().EqualTo(1u)); - AssertThat(call_history.at(13), Is().EqualTo(2u)); - AssertThat(call_history.at(14), Is().EqualTo(3u)); - AssertThat(call_history.at(15), Is().EqualTo(4u)); - AssertThat(call_history.at(16), Is().EqualTo(5u)); - AssertThat(call_history.at(17), Is().EqualTo(6u)); - AssertThat(call_history.at(18), Is().EqualTo(7u)); + AssertThat(call_history.at(8), Is().EqualTo(0u)); + AssertThat(call_history.at(9), Is().EqualTo(1u)); + AssertThat(call_history.at(10), Is().EqualTo(2u)); + AssertThat(call_history.at(11), Is().EqualTo(3u)); + AssertThat(call_history.at(12), Is().EqualTo(4u)); + AssertThat(call_history.at(13), Is().EqualTo(5u)); + AssertThat(call_history.at(14), Is().EqualTo(6u)); + AssertThat(call_history.at(15), Is().EqualTo(7u)); // - Second top-down sweep - AssertThat(call_history.at(19), Is().EqualTo(1u)); - AssertThat(call_history.at(20), Is().EqualTo(2u)); - AssertThat(call_history.at(21), Is().EqualTo(3u)); - AssertThat(call_history.at(22), Is().EqualTo(4u)); - AssertThat(call_history.at(23), Is().EqualTo(5u)); - AssertThat(call_history.at(24), Is().EqualTo(6u)); - AssertThat(call_history.at(25), Is().EqualTo(7u)); + AssertThat(call_history.at(16), Is().EqualTo(1u)); + AssertThat(call_history.at(17), Is().EqualTo(2u)); + AssertThat(call_history.at(18), Is().EqualTo(3u)); + AssertThat(call_history.at(19), Is().EqualTo(4u)); + AssertThat(call_history.at(20), Is().EqualTo(5u)); + AssertThat(call_history.at(21), Is().EqualTo(6u)); + AssertThat(call_history.at(22), Is().EqualTo(7u)); }); it("finishes early during repeated transposition [&&]", [&]() { @@ -4871,21 +4810,20 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(8u)); + AssertThat(call_history.size(), Is().EqualTo(9u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(2u)); // 4 out of 8 nodes + AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(4), Is().EqualTo(0u)); - AssertThat(call_history.at(5), Is().EqualTo(1u)); - AssertThat(call_history.at(6), Is().EqualTo(2u)); - AssertThat(call_history.at(7), Is().EqualTo(3u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); // NOTE: Even though there are three levels that should be quantified, we only do one // partial quantification. @@ -5165,9 +5103,9 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(47u)); + AssertThat(call_history.size(), Is().EqualTo(41u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(13u)); AssertThat(call_history.at(1), Is().EqualTo(12u)); AssertThat(call_history.at(2), Is().EqualTo(11u)); @@ -5181,46 +5119,38 @@ go_bandit([]() { AssertThat(call_history.at(10), Is().EqualTo(3u)); AssertThat(call_history.at(11), Is().EqualTo(2u)); AssertThat(call_history.at(12), Is().EqualTo(1u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. AssertThat(call_history.at(13), Is().EqualTo(0u)); - AssertThat(call_history.at(14), Is().EqualTo(1u)); - AssertThat(call_history.at(15), Is().EqualTo(2u)); - AssertThat(call_history.at(16), Is().EqualTo(3u)); - AssertThat(call_history.at(17), Is().EqualTo(4u)); - AssertThat(call_history.at(18), Is().EqualTo(5u)); - AssertThat(call_history.at(19), Is().EqualTo(6u)); // 13 out of 34 nodes // - First top-down sweep - AssertThat(call_history.at(20), Is().EqualTo(0u)); - AssertThat(call_history.at(21), Is().EqualTo(1u)); - AssertThat(call_history.at(22), Is().EqualTo(2u)); - AssertThat(call_history.at(23), Is().EqualTo(3u)); - AssertThat(call_history.at(24), Is().EqualTo(4u)); - AssertThat(call_history.at(25), Is().EqualTo(5u)); - AssertThat(call_history.at(26), Is().EqualTo(6u)); - AssertThat(call_history.at(27), Is().EqualTo(7u)); - AssertThat(call_history.at(28), Is().EqualTo(8u)); - AssertThat(call_history.at(29), Is().EqualTo(9u)); - AssertThat(call_history.at(30), Is().EqualTo(10u)); - AssertThat(call_history.at(31), Is().EqualTo(11u)); - AssertThat(call_history.at(32), Is().EqualTo(12u)); - AssertThat(call_history.at(33), Is().EqualTo(13u)); + AssertThat(call_history.at(14), Is().EqualTo(0u)); + AssertThat(call_history.at(15), Is().EqualTo(1u)); + AssertThat(call_history.at(16), Is().EqualTo(2u)); + AssertThat(call_history.at(17), Is().EqualTo(3u)); + AssertThat(call_history.at(18), Is().EqualTo(4u)); + AssertThat(call_history.at(19), Is().EqualTo(5u)); + AssertThat(call_history.at(20), Is().EqualTo(6u)); + AssertThat(call_history.at(21), Is().EqualTo(7u)); + AssertThat(call_history.at(22), Is().EqualTo(8u)); + AssertThat(call_history.at(23), Is().EqualTo(9u)); + AssertThat(call_history.at(24), Is().EqualTo(10u)); + AssertThat(call_history.at(25), Is().EqualTo(11u)); + AssertThat(call_history.at(26), Is().EqualTo(12u)); + AssertThat(call_history.at(27), Is().EqualTo(13u)); // - Second top-down sweep - AssertThat(call_history.at(34), Is().EqualTo(1u)); - AssertThat(call_history.at(35), Is().EqualTo(2u)); - AssertThat(call_history.at(36), Is().EqualTo(3u)); - AssertThat(call_history.at(37), Is().EqualTo(4u)); - AssertThat(call_history.at(38), Is().EqualTo(5u)); - AssertThat(call_history.at(39), Is().EqualTo(6u)); - AssertThat(call_history.at(40), Is().EqualTo(7u)); - AssertThat(call_history.at(41), Is().EqualTo(8u)); - AssertThat(call_history.at(42), Is().EqualTo(9u)); - AssertThat(call_history.at(43), Is().EqualTo(10u)); - AssertThat(call_history.at(44), Is().EqualTo(11u)); - AssertThat(call_history.at(45), Is().EqualTo(12u)); - AssertThat(call_history.at(46), Is().EqualTo(13u)); + AssertThat(call_history.at(28), Is().EqualTo(1u)); + AssertThat(call_history.at(29), Is().EqualTo(2u)); + AssertThat(call_history.at(30), Is().EqualTo(3u)); + AssertThat(call_history.at(31), Is().EqualTo(4u)); + AssertThat(call_history.at(32), Is().EqualTo(5u)); + AssertThat(call_history.at(33), Is().EqualTo(6u)); + AssertThat(call_history.at(34), Is().EqualTo(7u)); + AssertThat(call_history.at(35), Is().EqualTo(8u)); + AssertThat(call_history.at(36), Is().EqualTo(9u)); + AssertThat(call_history.at(37), Is().EqualTo(10u)); + AssertThat(call_history.at(38), Is().EqualTo(11u)); + AssertThat(call_history.at(39), Is().EqualTo(12u)); + AssertThat(call_history.at(40), Is().EqualTo(13u)); }); }); @@ -5493,9 +5423,9 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please verify // that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(47u)); + AssertThat(call_history.size(), Is().EqualTo(41u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(13u)); AssertThat(call_history.at(1), Is().EqualTo(12u)); AssertThat(call_history.at(2), Is().EqualTo(11u)); @@ -5509,46 +5439,38 @@ go_bandit([]() { AssertThat(call_history.at(10), Is().EqualTo(3u)); AssertThat(call_history.at(11), Is().EqualTo(2u)); AssertThat(call_history.at(12), Is().EqualTo(1u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. AssertThat(call_history.at(13), Is().EqualTo(0u)); - AssertThat(call_history.at(14), Is().EqualTo(1u)); - AssertThat(call_history.at(15), Is().EqualTo(2u)); - AssertThat(call_history.at(16), Is().EqualTo(3u)); - AssertThat(call_history.at(17), Is().EqualTo(4u)); - AssertThat(call_history.at(18), Is().EqualTo(5u)); - AssertThat(call_history.at(19), Is().EqualTo(6u)); // 13 out of 34 nodes // - Top-down sweep - AssertThat(call_history.at(20), Is().EqualTo(0u)); - AssertThat(call_history.at(21), Is().EqualTo(1u)); - AssertThat(call_history.at(22), Is().EqualTo(2u)); - AssertThat(call_history.at(23), Is().EqualTo(3u)); - AssertThat(call_history.at(24), Is().EqualTo(4u)); - AssertThat(call_history.at(25), Is().EqualTo(5u)); - AssertThat(call_history.at(26), Is().EqualTo(6u)); - AssertThat(call_history.at(27), Is().EqualTo(7u)); - AssertThat(call_history.at(28), Is().EqualTo(8u)); - AssertThat(call_history.at(29), Is().EqualTo(9u)); - AssertThat(call_history.at(30), Is().EqualTo(10u)); - AssertThat(call_history.at(31), Is().EqualTo(11u)); - AssertThat(call_history.at(32), Is().EqualTo(12u)); - AssertThat(call_history.at(33), Is().EqualTo(13u)); + AssertThat(call_history.at(14), Is().EqualTo(0u)); + AssertThat(call_history.at(15), Is().EqualTo(1u)); + AssertThat(call_history.at(16), Is().EqualTo(2u)); + AssertThat(call_history.at(17), Is().EqualTo(3u)); + AssertThat(call_history.at(18), Is().EqualTo(4u)); + AssertThat(call_history.at(19), Is().EqualTo(5u)); + AssertThat(call_history.at(20), Is().EqualTo(6u)); + AssertThat(call_history.at(21), Is().EqualTo(7u)); + AssertThat(call_history.at(22), Is().EqualTo(8u)); + AssertThat(call_history.at(23), Is().EqualTo(9u)); + AssertThat(call_history.at(24), Is().EqualTo(10u)); + AssertThat(call_history.at(25), Is().EqualTo(11u)); + AssertThat(call_history.at(26), Is().EqualTo(12u)); + AssertThat(call_history.at(27), Is().EqualTo(13u)); // - Nested Sweeping (x0 is gone) - AssertThat(call_history.at(34), Is().EqualTo(13u)); - AssertThat(call_history.at(35), Is().EqualTo(12u)); - AssertThat(call_history.at(36), Is().EqualTo(11u)); - AssertThat(call_history.at(37), Is().EqualTo(10u)); - AssertThat(call_history.at(38), Is().EqualTo(9u)); - AssertThat(call_history.at(39), Is().EqualTo(8u)); - AssertThat(call_history.at(40), Is().EqualTo(7u)); - AssertThat(call_history.at(41), Is().EqualTo(6u)); - AssertThat(call_history.at(42), Is().EqualTo(5u)); - AssertThat(call_history.at(43), Is().EqualTo(4u)); - AssertThat(call_history.at(44), Is().EqualTo(3u)); - AssertThat(call_history.at(45), Is().EqualTo(2u)); - AssertThat(call_history.at(46), Is().EqualTo(1u)); + AssertThat(call_history.at(28), Is().EqualTo(13u)); + AssertThat(call_history.at(29), Is().EqualTo(12u)); + AssertThat(call_history.at(30), Is().EqualTo(11u)); + AssertThat(call_history.at(31), Is().EqualTo(10u)); + AssertThat(call_history.at(32), Is().EqualTo(9u)); + AssertThat(call_history.at(33), Is().EqualTo(8u)); + AssertThat(call_history.at(34), Is().EqualTo(7u)); + AssertThat(call_history.at(35), Is().EqualTo(6u)); + AssertThat(call_history.at(36), Is().EqualTo(5u)); + AssertThat(call_history.at(37), Is().EqualTo(4u)); + AssertThat(call_history.at(38), Is().EqualTo(3u)); + AssertThat(call_history.at(39), Is().EqualTo(2u)); + AssertThat(call_history.at(40), Is().EqualTo(1u)); }); it("switches to nested sweeping after maximum transpositions with BDD 12b [&&]", [&]() { @@ -5615,30 +5537,27 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please verify // that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(15u)); + AssertThat(call_history.size(), Is().EqualTo(14u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); AssertThat(call_history.at(1), Is().EqualTo(3u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); // width + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - First top-down sweep - AssertThat(call_history.at(6), Is().EqualTo(0u)); - AssertThat(call_history.at(7), Is().EqualTo(1u)); - AssertThat(call_history.at(8), Is().EqualTo(2u)); - AssertThat(call_history.at(9), Is().EqualTo(3u)); - AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); // - Nested sweep looking for the 'next_inner' bottom-up - AssertThat(call_history.at(11), Is().EqualTo(4u)); - AssertThat(call_history.at(12), Is().EqualTo(3u)); - AssertThat(call_history.at(13), Is().EqualTo(2u)); - AssertThat(call_history.at(14), Is().EqualTo(0u)); + AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(11), Is().EqualTo(3u)); + AssertThat(call_history.at(12), Is().EqualTo(2u)); + AssertThat(call_history.at(13), Is().EqualTo(0u)); }); it("nested sweeping is done after transposing on deepest variable [&&]", [&]() { @@ -5689,25 +5608,24 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please verify // that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(10u)); + AssertThat(call_history.size(), Is().EqualTo(11u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); // 2 out of 5 nodes + AssertThat(call_history.at(1), Is().EqualTo(2u)); + AssertThat(call_history.at(2), Is().EqualTo(1u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(3), Is().EqualTo(0u)); - AssertThat(call_history.at(4), Is().EqualTo(1u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(5), Is().EqualTo(1u)); + AssertThat(call_history.at(6), Is().EqualTo(2u)); + AssertThat(call_history.at(7), Is().EqualTo(3u)); // - Check nested sweep has nothing left to-do - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(1u)); - AssertThat(call_history.at(9), Is().EqualTo(0u)); + AssertThat(call_history.at(8), Is().EqualTo(2u)); + AssertThat(call_history.at(9), Is().EqualTo(1u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); }); it("uses nested sweeping if no shallow variables are to-be quantified [&&]", [&]() { @@ -5790,33 +5708,34 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please verify // that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(18u)); + AssertThat(call_history.size(), Is().EqualTo(21u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(7u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(2u)); - AssertThat(call_history.at(4), Is().EqualTo(3u)); // 7 out of 16 nodes + AssertThat(call_history.at(1), Is().EqualTo(6u)); + AssertThat(call_history.at(2), Is().EqualTo(5u)); + AssertThat(call_history.at(3), Is().EqualTo(4u)); + AssertThat(call_history.at(4), Is().EqualTo(3u)); + AssertThat(call_history.at(5), Is().EqualTo(2u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(5), Is().EqualTo(0u)); - AssertThat(call_history.at(6), Is().EqualTo(1u)); - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(3u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); - AssertThat(call_history.at(10), Is().EqualTo(5u)); - AssertThat(call_history.at(11), Is().EqualTo(6u)); - AssertThat(call_history.at(12), Is().EqualTo(7u)); + AssertThat(call_history.at(8), Is().EqualTo(0u)); + AssertThat(call_history.at(9), Is().EqualTo(1u)); + AssertThat(call_history.at(10), Is().EqualTo(2u)); + AssertThat(call_history.at(11), Is().EqualTo(3u)); + AssertThat(call_history.at(12), Is().EqualTo(4u)); + AssertThat(call_history.at(13), Is().EqualTo(5u)); + AssertThat(call_history.at(14), Is().EqualTo(6u)); + AssertThat(call_history.at(15), Is().EqualTo(7u)); // - Nested Sweep - AssertThat(call_history.at(13), Is().EqualTo(4u)); - AssertThat(call_history.at(14), Is().EqualTo(3u)); - AssertThat(call_history.at(15), Is().EqualTo(2u)); - AssertThat(call_history.at(16), Is().EqualTo(1u)); - AssertThat(call_history.at(17), Is().EqualTo(0u)); + AssertThat(call_history.at(16), Is().EqualTo(4u)); + AssertThat(call_history.at(17), Is().EqualTo(3u)); + AssertThat(call_history.at(18), Is().EqualTo(2u)); + AssertThat(call_history.at(19), Is().EqualTo(1u)); + AssertThat(call_history.at(20), Is().EqualTo(0u)); }); }); }); @@ -7025,7 +6944,7 @@ go_bandit([]() { return true; }); - AssertThat(calls, Is().EqualTo(1)); + AssertThat(calls, Is().EqualTo(3)); node_test_stream out_nodes(out); diff --git a/test/adiar/zdd/test_project.cpp b/test/adiar/zdd/test_project.cpp index 82ae796df..4b91b1bf6 100644 --- a/test/adiar/zdd/test_project.cpp +++ b/test/adiar/zdd/test_project.cpp @@ -675,28 +675,28 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(12u)); + AssertThat(call_history.size(), Is().EqualTo(15u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); // 1 out of 4 nodes + AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(2), Is().EqualTo(0u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(2u)); - AssertThat(call_history.at(5), Is().EqualTo(3u)); - AssertThat(call_history.at(6), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); // - Nested sweep looking for the 'next_inner' bottom-up - AssertThat(call_history.at(7), Is().EqualTo(4u)); - AssertThat(call_history.at(8), Is().EqualTo(3u)); - AssertThat(call_history.at(9), Is().EqualTo(2u)); // <-- still exists - AssertThat(call_history.at(10), Is().EqualTo(1u)); - AssertThat(call_history.at(11), Is().EqualTo(0u)); + AssertThat(call_history.at(10), Is().EqualTo(4u)); + AssertThat(call_history.at(11), Is().EqualTo(3u)); + AssertThat(call_history.at(12), Is().EqualTo(2u)); // <-- still exists + AssertThat(call_history.at(13), Is().EqualTo(1u)); + AssertThat(call_history.at(14), Is().EqualTo(0u)); }); it("does not prune on 'shortcutting' terminals during transposition [&& zdd_7]", [&]() { @@ -739,22 +739,20 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(6u)); + AssertThat(call_history.size(), Is().EqualTo(7u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(3u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); // 1 out of 4 nodes + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(2), Is().EqualTo(0u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(3u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(4), Is().EqualTo(1u)); + AssertThat(call_history.at(5), Is().EqualTo(3u)); // - Nested sweep looking for the 'next_inner' bottom-up - AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(0u)); }); it("prunes idempotent to-be quantified nodes during transposition [&&]", [&]() { @@ -808,25 +806,24 @@ go_bandit([]() { // // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(9u)); + AssertThat(call_history.size(), Is().EqualTo(11u)); - // - First check for at least one variable satisfying the predicate. - // This is then used for the inital transposition + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); // 1 out of 4 nodes + AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); // - Pruning sweep - AssertThat(call_history.at(2), Is().EqualTo(0u)); - AssertThat(call_history.at(3), Is().EqualTo(2u)); - AssertThat(call_history.at(4), Is().EqualTo(3u)); - AssertThat(call_history.at(5), Is().EqualTo(4u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(5), Is().EqualTo(2u)); + AssertThat(call_history.at(6), Is().EqualTo(3u)); + AssertThat(call_history.at(7), Is().EqualTo(4u)); // - Nested sweep looking for the 'next_inner' bottom-up - AssertThat(call_history.at(6), Is().EqualTo(4u)); - AssertThat(call_history.at(7), Is().EqualTo(3u)); - AssertThat(call_history.at(8), Is().EqualTo(0u)); + AssertThat(call_history.at(8), Is().EqualTo(4u)); + AssertThat(call_history.at(9), Is().EqualTo(3u)); + AssertThat(call_history.at(10), Is().EqualTo(0u)); }); }); @@ -934,20 +931,17 @@ go_bandit([]() { // NOTE: Test failure does NOT indicate a bug, but only indicates a // change. Please verify that this change makes sense and is as // intended. - AssertThat(call_history.size(), Is().EqualTo(7u)); + AssertThat(call_history.size(), Is().EqualTo(6u)); - // - First check for at least one variable NOT satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(2u)); AssertThat(call_history.at(1), Is().EqualTo(1u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. AssertThat(call_history.at(2), Is().EqualTo(0u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); // 2 out of 4 nodes // - First top-down sweep - AssertThat(call_history.at(4), Is().EqualTo(0u)); - AssertThat(call_history.at(5), Is().EqualTo(1u)); - AssertThat(call_history.at(6), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(4), Is().EqualTo(1u)); + AssertThat(call_history.at(5), Is().EqualTo(2u)); }); it("computes zdd_1 with dom = { x | x % 2 == 1 }", [&]() { @@ -1147,12 +1141,10 @@ go_bandit([]() { // intended. AssertThat(call_history.size(), Is().EqualTo(9u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(4u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. - AssertThat(call_history.at(1), Is().EqualTo(0u)); - AssertThat(call_history.at(2), Is().EqualTo(2u)); // width and 3 out of 5 nodes + AssertThat(call_history.at(1), Is().EqualTo(2u)); + AssertThat(call_history.at(2), Is().EqualTo(0u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -1539,9 +1531,9 @@ go_bandit([]() { // NOTE: Test failure does NOT indicate a bug, but only indicates a // change. Please verify that this change makes sense and is as // intended. - AssertThat(call_history.size(), Is().EqualTo(47u)); + AssertThat(call_history.size(), Is().EqualTo(41u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(13u)); AssertThat(call_history.at(1), Is().EqualTo(12u)); AssertThat(call_history.at(2), Is().EqualTo(11u)); @@ -1555,46 +1547,38 @@ go_bandit([]() { AssertThat(call_history.at(10), Is().EqualTo(3u)); AssertThat(call_history.at(11), Is().EqualTo(2u)); AssertThat(call_history.at(12), Is().EqualTo(1u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. AssertThat(call_history.at(13), Is().EqualTo(0u)); - AssertThat(call_history.at(14), Is().EqualTo(1u)); - AssertThat(call_history.at(15), Is().EqualTo(2u)); - AssertThat(call_history.at(16), Is().EqualTo(3u)); - AssertThat(call_history.at(17), Is().EqualTo(4u)); - AssertThat(call_history.at(18), Is().EqualTo(5u)); - AssertThat(call_history.at(19), Is().EqualTo(6u)); // 13 out of 34 nodes // - First top-down sweep - AssertThat(call_history.at(20), Is().EqualTo(0u)); - AssertThat(call_history.at(21), Is().EqualTo(1u)); - AssertThat(call_history.at(22), Is().EqualTo(2u)); - AssertThat(call_history.at(23), Is().EqualTo(3u)); - AssertThat(call_history.at(24), Is().EqualTo(4u)); - AssertThat(call_history.at(25), Is().EqualTo(5u)); - AssertThat(call_history.at(26), Is().EqualTo(6u)); - AssertThat(call_history.at(27), Is().EqualTo(7u)); - AssertThat(call_history.at(28), Is().EqualTo(8u)); - AssertThat(call_history.at(29), Is().EqualTo(9u)); - AssertThat(call_history.at(30), Is().EqualTo(10u)); - AssertThat(call_history.at(31), Is().EqualTo(11u)); - AssertThat(call_history.at(32), Is().EqualTo(12u)); - AssertThat(call_history.at(33), Is().EqualTo(13u)); + AssertThat(call_history.at(14), Is().EqualTo(0u)); + AssertThat(call_history.at(15), Is().EqualTo(1u)); + AssertThat(call_history.at(16), Is().EqualTo(2u)); + AssertThat(call_history.at(17), Is().EqualTo(3u)); + AssertThat(call_history.at(18), Is().EqualTo(4u)); + AssertThat(call_history.at(19), Is().EqualTo(5u)); + AssertThat(call_history.at(20), Is().EqualTo(6u)); + AssertThat(call_history.at(21), Is().EqualTo(7u)); + AssertThat(call_history.at(22), Is().EqualTo(8u)); + AssertThat(call_history.at(23), Is().EqualTo(9u)); + AssertThat(call_history.at(24), Is().EqualTo(10u)); + AssertThat(call_history.at(25), Is().EqualTo(11u)); + AssertThat(call_history.at(26), Is().EqualTo(12u)); + AssertThat(call_history.at(27), Is().EqualTo(13u)); // - Second top-down sweep - AssertThat(call_history.at(34), Is().EqualTo(1u)); - AssertThat(call_history.at(35), Is().EqualTo(2u)); - AssertThat(call_history.at(36), Is().EqualTo(3u)); - AssertThat(call_history.at(37), Is().EqualTo(4u)); - AssertThat(call_history.at(38), Is().EqualTo(5u)); - AssertThat(call_history.at(39), Is().EqualTo(6u)); - AssertThat(call_history.at(40), Is().EqualTo(7u)); - AssertThat(call_history.at(41), Is().EqualTo(8u)); - AssertThat(call_history.at(42), Is().EqualTo(9u)); - AssertThat(call_history.at(43), Is().EqualTo(10u)); - AssertThat(call_history.at(44), Is().EqualTo(11u)); - AssertThat(call_history.at(45), Is().EqualTo(12u)); - AssertThat(call_history.at(46), Is().EqualTo(13u)); + AssertThat(call_history.at(28), Is().EqualTo(1u)); + AssertThat(call_history.at(29), Is().EqualTo(2u)); + AssertThat(call_history.at(30), Is().EqualTo(3u)); + AssertThat(call_history.at(31), Is().EqualTo(4u)); + AssertThat(call_history.at(32), Is().EqualTo(5u)); + AssertThat(call_history.at(33), Is().EqualTo(6u)); + AssertThat(call_history.at(34), Is().EqualTo(7u)); + AssertThat(call_history.at(35), Is().EqualTo(8u)); + AssertThat(call_history.at(36), Is().EqualTo(9u)); + AssertThat(call_history.at(37), Is().EqualTo(10u)); + AssertThat(call_history.at(38), Is().EqualTo(11u)); + AssertThat(call_history.at(39), Is().EqualTo(12u)); + AssertThat(call_history.at(40), Is().EqualTo(13u)); }); it("switches to Nested Sweeping for exploding ZDD 5", [&]() { @@ -1971,9 +1955,9 @@ go_bandit([]() { // NOTE: Test failure does NOT indicate a bug, but only indicates a // change. Please verify that this change makes sense and is as // intended. - AssertThat(call_history.size(), Is().EqualTo(47u)); + AssertThat(call_history.size(), Is().EqualTo(41u)); - // - First check for at least one variable satisfying the predicate. + // - Generate predicate profile AssertThat(call_history.at(0), Is().EqualTo(13u)); AssertThat(call_history.at(1), Is().EqualTo(12u)); AssertThat(call_history.at(2), Is().EqualTo(11u)); @@ -1987,46 +1971,38 @@ go_bandit([]() { AssertThat(call_history.at(10), Is().EqualTo(3u)); AssertThat(call_history.at(11), Is().EqualTo(2u)); AssertThat(call_history.at(12), Is().EqualTo(1u)); - - // - Upper bound partial quantifications; capped at N/3(ish) nodes. AssertThat(call_history.at(13), Is().EqualTo(0u)); - AssertThat(call_history.at(14), Is().EqualTo(1u)); - AssertThat(call_history.at(15), Is().EqualTo(2u)); - AssertThat(call_history.at(16), Is().EqualTo(3u)); - AssertThat(call_history.at(17), Is().EqualTo(4u)); - AssertThat(call_history.at(18), Is().EqualTo(5u)); - AssertThat(call_history.at(19), Is().EqualTo(6u)); // 13 out of 34 nodes // - Top-down sweep - AssertThat(call_history.at(20), Is().EqualTo(0u)); - AssertThat(call_history.at(21), Is().EqualTo(1u)); - AssertThat(call_history.at(22), Is().EqualTo(2u)); - AssertThat(call_history.at(23), Is().EqualTo(3u)); - AssertThat(call_history.at(24), Is().EqualTo(4u)); - AssertThat(call_history.at(25), Is().EqualTo(5u)); - AssertThat(call_history.at(26), Is().EqualTo(6u)); - AssertThat(call_history.at(27), Is().EqualTo(7u)); - AssertThat(call_history.at(28), Is().EqualTo(8u)); - AssertThat(call_history.at(29), Is().EqualTo(9u)); - AssertThat(call_history.at(30), Is().EqualTo(10u)); - AssertThat(call_history.at(31), Is().EqualTo(11u)); - AssertThat(call_history.at(32), Is().EqualTo(12u)); - AssertThat(call_history.at(33), Is().EqualTo(13u)); + AssertThat(call_history.at(14), Is().EqualTo(0u)); + AssertThat(call_history.at(15), Is().EqualTo(1u)); + AssertThat(call_history.at(16), Is().EqualTo(2u)); + AssertThat(call_history.at(17), Is().EqualTo(3u)); + AssertThat(call_history.at(18), Is().EqualTo(4u)); + AssertThat(call_history.at(19), Is().EqualTo(5u)); + AssertThat(call_history.at(20), Is().EqualTo(6u)); + AssertThat(call_history.at(21), Is().EqualTo(7u)); + AssertThat(call_history.at(22), Is().EqualTo(8u)); + AssertThat(call_history.at(23), Is().EqualTo(9u)); + AssertThat(call_history.at(24), Is().EqualTo(10u)); + AssertThat(call_history.at(25), Is().EqualTo(11u)); + AssertThat(call_history.at(26), Is().EqualTo(12u)); + AssertThat(call_history.at(27), Is().EqualTo(13u)); // - Nested Sweeping (x0 is gone) - AssertThat(call_history.at(34), Is().EqualTo(13u)); - AssertThat(call_history.at(35), Is().EqualTo(12u)); - AssertThat(call_history.at(36), Is().EqualTo(11u)); - AssertThat(call_history.at(37), Is().EqualTo(10u)); - AssertThat(call_history.at(38), Is().EqualTo(9u)); - AssertThat(call_history.at(39), Is().EqualTo(8u)); - AssertThat(call_history.at(40), Is().EqualTo(7u)); - AssertThat(call_history.at(41), Is().EqualTo(6u)); - AssertThat(call_history.at(42), Is().EqualTo(5u)); - AssertThat(call_history.at(43), Is().EqualTo(4u)); - AssertThat(call_history.at(44), Is().EqualTo(3u)); - AssertThat(call_history.at(45), Is().EqualTo(2u)); - AssertThat(call_history.at(46), Is().EqualTo(1u)); + AssertThat(call_history.at(28), Is().EqualTo(13u)); + AssertThat(call_history.at(29), Is().EqualTo(12u)); + AssertThat(call_history.at(30), Is().EqualTo(11u)); + AssertThat(call_history.at(31), Is().EqualTo(10u)); + AssertThat(call_history.at(32), Is().EqualTo(9u)); + AssertThat(call_history.at(33), Is().EqualTo(8u)); + AssertThat(call_history.at(34), Is().EqualTo(7u)); + AssertThat(call_history.at(35), Is().EqualTo(6u)); + AssertThat(call_history.at(36), Is().EqualTo(5u)); + AssertThat(call_history.at(37), Is().EqualTo(4u)); + AssertThat(call_history.at(38), Is().EqualTo(3u)); + AssertThat(call_history.at(39), Is().EqualTo(2u)); + AssertThat(call_history.at(40), Is().EqualTo(1u)); }); }); }); From 7483409673a991815a423fcb3995a2674e45dede Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Tue, 30 Apr 2024 16:43:54 +0200 Subject: [PATCH 3/6] Format latest changes --- src/adiar/bdd/restrict.cpp | 7 +- src/adiar/internal/algorithms/quantify.h | 74 +--- src/adiar/internal/algorithms/select.h | 17 +- src/adiar/zdd/subset.cpp | 21 +- test/adiar/bdd/test_quantify.cpp | 530 +++++++++++------------ 5 files changed, 309 insertions(+), 340 deletions(-) diff --git a/src/adiar/bdd/restrict.cpp b/src/adiar/bdd/restrict.cpp index 7ef1b3182..b87b849b9 100644 --- a/src/adiar/bdd/restrict.cpp +++ b/src/adiar/bdd/restrict.cpp @@ -1,6 +1,5 @@ #include #include - #include #include @@ -13,11 +12,13 @@ namespace adiar { ////////////////////////////////////////////////////////////////////////////// template - class bdd_restrict_policy : public bdd_policy, public AssignmentPolicy + class bdd_restrict_policy + : public bdd_policy + , public AssignmentPolicy { public: template - bdd_restrict_policy(const Arg &a) + bdd_restrict_policy(const Arg& a) : AssignmentPolicy(a) {} diff --git a/src/adiar/internal/algorithms/quantify.h b/src/adiar/internal/algorithms/quantify.h index 10f596ebd..27c609f2e 100644 --- a/src/adiar/internal/algorithms/quantify.h +++ b/src/adiar/internal/algorithms/quantify.h @@ -1232,29 +1232,19 @@ namespace adiar::internal { // ------------------------------------------------------------------------------------------- // CASE: Not to-be quantified node. - if (!_pred_result) { - return n; - } + if (!_pred_result) { return n; } // ------------------------------------------------------------------------------------------- // CASE: Prune low() // // TODO (ZDD): Remove 'Policy::keep_terminal' depending on semantics in Policy - if (Policy::collapse_to_terminal(n.low())) { - return n.low(); - } - if (n.low().is_terminal() && !Policy::keep_terminal(n.low())) { - return n.high(); - } + if (Policy::collapse_to_terminal(n.low())) { return n.low(); } + if (n.low().is_terminal() && !Policy::keep_terminal(n.low())) { return n.high(); } // ------------------------------------------------------------------------------------------- // CASE: Prune high() - if (Policy::collapse_to_terminal(n.high())) { - return n.high(); - } - if (n.high().is_terminal() && !Policy::keep_terminal(n.high())) { - return n.low(); - } + if (Policy::collapse_to_terminal(n.high())) { return n.high(); } + if (n.high().is_terminal() && !Policy::keep_terminal(n.high())) { return n.low(); } // ------------------------------------------------------------------------------------------- // No pruning possible. Do nothing. @@ -1363,7 +1353,6 @@ namespace adiar::internal struct quantify__pred_profile { private: - public: /// \brief Total number of nodes in the diagram. size_t dd_size; @@ -1399,36 +1388,24 @@ namespace adiar::internal }; /// \brief The *deepest* to-be quantified level. - var_data deepest_var - { - 0, - std::numeric_limits::max(), - Policy::max_id+1 - }; + var_data deepest_var{ 0, std::numeric_limits::max(), Policy::max_id + 1 }; /// \brief The *shallowest* to-be quantified level. - var_data shallowest_var - { - Policy::max_label+1, - std::numeric_limits::max(), - Policy::max_id+1 - }; + var_data shallowest_var{ Policy::max_label + 1, + std::numeric_limits::max(), + Policy::max_id + 1 }; /// \brief The *widest* to-be quantified level. - var_data widest_var - { - Policy::max_label+1, + var_data widest_var{ + Policy::max_label + 1, std::numeric_limits::max(), 0, }; /// \brief The *narrowest* to-be quantified level. - var_data narrowest_var - { - Policy::max_label+1, - std::numeric_limits::max(), - Policy::max_id+1 - }; + var_data narrowest_var{ Policy::max_label + 1, + std::numeric_limits::max(), + Policy::max_id + 1 }; }; ////////////////////////////////////////////////////////////////////////////////////////////////// @@ -1439,7 +1416,8 @@ namespace adiar::internal __quantify__pred_profile(const typename Policy::dd_type& dd, const predicate& pred) { - // TODO: tighten definition of 'shallow' and 'deep' variables based on widest level + // TODO: tighten 'shallow' to only be above shallowest widest level (inclusive) + // TODO: tighten 'deep' to not be 'shallow' quantify__pred_profile res; res.dd_size = dd_nodecount(dd); @@ -1449,14 +1427,14 @@ namespace adiar::internal level_info_stream lis(dd); const size_t third_dd_size = res.dd_size / 3; - size_t nodes_below = 0u; + size_t nodes_below = 0u; while (lis.can_pull()) { const level_info li = lis.pull(); if (pred(li.label()) == Policy::quantify_onset) { - res.quant_all_vars += 1u; - res.quant_all_size += li.width(); - res.quant_deep_vars += nodes_below + 1 <= third_dd_size; + res.quant_all_vars += 1u; + res.quant_all_size += li.width(); + res.quant_deep_vars += nodes_below + 1 <= third_dd_size; res.quant_shallow_vars += res.dd_size - third_dd_size <= nodes_below + li.width(); { // Shallowest variable (always updated due to bottom-up direction). @@ -1465,17 +1443,11 @@ namespace adiar::internal res.shallowest_var.width = li.width(); } // Deepest variable. - if (res.deepest_var.level < li.level()) { - res.deepest_var = res.shallowest_var; - } + if (res.deepest_var.level < li.level()) { res.deepest_var = res.shallowest_var; } // Widest variable - if (res.widest_var.width < li.width()) { - res.widest_var = res.shallowest_var; - } + if (res.widest_var.width < li.width()) { res.widest_var = res.shallowest_var; } // Narrowest variable - if (li.width() < res.narrowest_var.width) { - res.narrowest_var = res.shallowest_var; - } + if (li.width() < res.narrowest_var.width) { res.narrowest_var = res.shallowest_var; } } nodes_below += li.width(); diff --git a/src/adiar/internal/algorithms/select.h b/src/adiar/internal/algorithms/select.h index 9de2eaf64..79a5c67c4 100644 --- a/src/adiar/internal/algorithms/select.h +++ b/src/adiar/internal/algorithms/select.h @@ -133,9 +133,7 @@ namespace adiar::internal if (std::holds_alternative(rec)) { const node rec_node = std::get(rec); - if constexpr (Policy::skip_reduce) { - output_changes |= rec_node != n; - } + if constexpr (Policy::skip_reduce) { output_changes |= rec_node != n; } // Output/Forward outgoing arcs __select_recurse_out(pq, aw, n.uid().as_ptr(false), rec_node.low()); @@ -155,9 +153,7 @@ namespace adiar::internal const typename Policy::pointer_type rec_target = std::get(rec); - if constexpr (Policy::skip_reduce) { - output_changes = true; - } + if constexpr (Policy::skip_reduce) { output_changes = true; } // Output/Forward extension of arc while (pq.can_pull() && pq.top().target == n.uid()) { @@ -222,22 +218,19 @@ namespace adiar::internal #ifdef ADIAR_STATS stats_select.lpq.unbucketed += 1u; #endif - return __select>( + return __select>( ep, dd, policy, aux_available_memory, max_pq_size); } else if (!external_only && max_pq_size <= pq_memory_fits) { #ifdef ADIAR_STATS stats_select.lpq.internal += 1u; #endif - return __select>( + return __select>( ep, dd, policy, aux_available_memory, max_pq_size); } else { #ifdef ADIAR_STATS stats_select.lpq.external += 1u; #endif - return __select>( + return __select>( ep, dd, policy, aux_available_memory, max_pq_size); } } diff --git a/src/adiar/zdd/subset.cpp b/src/adiar/zdd/subset.cpp index f6f926356..44584c6dd 100644 --- a/src/adiar/zdd/subset.cpp +++ b/src/adiar/zdd/subset.cpp @@ -110,11 +110,13 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// template - class zdd_offset_policy : public zdd_policy, public AssignmentPolicy + class zdd_offset_policy + : public zdd_policy + , public AssignmentPolicy { public: template - zdd_offset_policy(const Arg &a) + zdd_offset_policy(const Arg& a) : AssignmentPolicy(a) {} @@ -122,9 +124,7 @@ namespace adiar internal::select_rec process(const zdd::node_type& n) { - if (AssignmentPolicy::current_matches()) { - return n.low(); - } + if (AssignmentPolicy::current_matches()) { return n.low(); } return n; } @@ -188,7 +188,9 @@ namespace adiar ////////////////////////////////////////////////////////////////////////////////////////////////// template - class zdd_onset_policy : public zdd_policy, public AssignmentPolicy + class zdd_onset_policy + : public zdd_policy + , public AssignmentPolicy { public: template @@ -213,12 +215,15 @@ namespace adiar if (AssignmentPolicy::has_level_incl()) { // If recursion goes past the intended level, then it is replaced with // the false terminal. - const zdd::pointer_type low = n.low().is_terminal() || n.low().label() > AssignmentPolicy::level_incl() + const zdd::pointer_type low = + n.low().is_terminal() || n.low().label() > AssignmentPolicy::level_incl() ? zdd::pointer_type(false) : n.low(); // If this applies to high, then the node should be skipped entirely. - if (n.high().is_terminal() || n.high().label() > AssignmentPolicy::level_incl()) { return low; } + if (n.high().is_terminal() || n.high().label() > AssignmentPolicy::level_incl()) { + return low; + } return zdd::node_type(n.uid(), low, n.high()); } return n; diff --git a/test/adiar/bdd/test_quantify.cpp b/test/adiar/bdd/test_quantify.cpp index 4e74a5b30..276e1610a 100644 --- a/test/adiar/bdd/test_quantify.cpp +++ b/test/adiar/bdd/test_quantify.cpp @@ -3620,157 +3620,156 @@ go_bandit([]() { AssertThat(call_history.at(7), Is().EqualTo(3u)); }); - it("collapses during repeated transposition in BDD 12a [&&]", - [&]() { - std::vector call_history; - bdd out = bdd_exists(ep & exec_policy::access::Random_Access, - bdd_12a, - [&call_history](const bdd::label_type x) -> bool { - call_history.push_back(x); - return 0 < x && x < 3; - }); - - 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()); - - // TODO: meta variables... - - // Check call history - // - // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please - // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(13u)); - - // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); - AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); - - // - First top-down sweep - AssertThat(call_history.at(5), Is().EqualTo(0u)); - AssertThat(call_history.at(6), Is().EqualTo(1u)); - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(3u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); - - // - Second top-down sweep - AssertThat(call_history.at(10), Is().EqualTo(0u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(3u)); - }); + it("collapses during repeated transposition in BDD 12a [&&]", [&]() { + std::vector call_history; + bdd out = bdd_exists(ep & exec_policy::access::Random_Access, + bdd_12a, + [&call_history](const bdd::label_type x) -> bool { + call_history.push_back(x); + return 0 < x && x < 3; + }); + + 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()); + + // TODO: meta variables... + + // Check call history + // + // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please + // verify that this change makes sense and is as intended. + AssertThat(call_history.size(), Is().EqualTo(13u)); + + // - Generate predicate profile + AssertThat(call_history.at(0), Is().EqualTo(4u)); + AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); + + // - First top-down sweep + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); + + // - Second top-down sweep + AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(3u)); + }); it("finishes during repeated transposition in BDD 12b [&&]", [&]() { - std::vector call_history; - bdd out = bdd_exists(ep & exec_policy::access::Random_Access, - bdd_12b, - [&call_history](const bdd::label_type x) -> bool { - call_history.push_back(x); - return 0 < x && x < 3; - }); - - /* expected - // 1 ---- x0 - // / \ - // / \ ---- x1 - // / \ - // | | ---- x2 - // | | - // ? ? ---- x3 - // / \ / \ - // | \ T | - // | \__ / - // 7 8 ---- x4 - // / \ / \ - // T F F T - // - // The 'T' terminal at 'x3' is due to the pair (7,8) collapsing to the - // 'T' terminal. This tuple is created from (7,F,8) which in turn is - // created from (5,6,8) from the quantification (3,4) from (2). - */ - node_test_stream out_nodes(out); + std::vector call_history; + bdd out = bdd_exists(ep & exec_policy::access::Random_Access, + bdd_12b, + [&call_history](const bdd::label_type x) -> bool { + call_history.push_back(x); + return 0 < x && x < 3; + }); - AssertThat(out_nodes.can_pull(), Is().True()); // (8) - AssertThat(out_nodes.pull(), - Is().EqualTo(node( - 4, node::max_id, node::pointer_type(false), node::pointer_type(true)))); + /* expected + // 1 ---- x0 + // / \ + // / \ ---- x1 + // / \ + // | | ---- x2 + // | | + // ? ? ---- x3 + // / \ / \ + // | \ T | + // | \__ / + // 7 8 ---- x4 + // / \ / \ + // T F F T + // + // The 'T' terminal at 'x3' is due to the pair (7,8) collapsing to the + // 'T' terminal. This tuple is created from (7,F,8) which in turn is + // created from (5,6,8) from the quantification (3,4) from (2). + */ + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().True()); // (7) - AssertThat( - out_nodes.pull(), - Is().EqualTo( - node(4, node::max_id - 1, node::pointer_type(true), node::pointer_type(false)))); + AssertThat(out_nodes.can_pull(), Is().True()); // (8) + AssertThat(out_nodes.pull(), + Is().EqualTo(node( + 4, node::max_id, node::pointer_type(false), node::pointer_type(true)))); - AssertThat(out_nodes.can_pull(), Is().True()); // (5,6,8) - AssertThat( - out_nodes.pull(), - Is().EqualTo(node( - 3, node::max_id, node::pointer_type(true), node::pointer_type(4, node::max_id)))); + AssertThat(out_nodes.can_pull(), Is().True()); // (7) + AssertThat( + out_nodes.pull(), + Is().EqualTo( + node(4, node::max_id - 1, node::pointer_type(true), node::pointer_type(false)))); - AssertThat(out_nodes.can_pull(), Is().True()); // (5,6) - AssertThat(out_nodes.pull(), - Is().EqualTo(node(3, - node::max_id - 1, - node::pointer_type(4, node::max_id - 1), - node::pointer_type(4, node::max_id)))); + AssertThat(out_nodes.can_pull(), Is().True()); // (5,6,8) + AssertThat( + out_nodes.pull(), + Is().EqualTo(node( + 3, node::max_id, node::pointer_type(true), node::pointer_type(4, node::max_id)))); - AssertThat(out_nodes.can_pull(), Is().True()); // (1) - AssertThat(out_nodes.pull(), - Is().EqualTo(node(0, - node::max_id, - node::pointer_type(3, node::max_id - 1), - node::pointer_type(3, node::max_id)))); + AssertThat(out_nodes.can_pull(), Is().True()); // (5,6) + AssertThat(out_nodes.pull(), + Is().EqualTo(node(3, + node::max_id - 1, + node::pointer_type(4, node::max_id - 1), + node::pointer_type(4, node::max_id)))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); // (1) + AssertThat(out_nodes.pull(), + Is().EqualTo(node(0, + node::max_id, + node::pointer_type(3, node::max_id - 1), + node::pointer_type(3, node::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(4u, 2u))); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(3u, 2u))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(4u, 2u))); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0u, 1u))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(3u, 2u))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0u, 1u))); - // TODO: meta variables... + AssertThat(out_meta.can_pull(), Is().False()); - // Check call history - // - // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please - // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(14u)); + // TODO: meta variables... - // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); - AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + // Check call history + // + // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please + // verify that this change makes sense and is as intended. + AssertThat(call_history.size(), Is().EqualTo(14u)); - // - First top-down sweep - AssertThat(call_history.at(5), Is().EqualTo(0u)); - AssertThat(call_history.at(6), Is().EqualTo(1u)); - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(3u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); + // - Generate predicate profile + AssertThat(call_history.at(0), Is().EqualTo(4u)); + AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); - // - Second top-down sweep - AssertThat(call_history.at(10), Is().EqualTo(0u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(3u)); - AssertThat(call_history.at(13), Is().EqualTo(4u)); - }); + // - First top-down sweep + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); + + // - Second top-down sweep + AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(3u)); + AssertThat(call_history.at(13), Is().EqualTo(4u)); + }); it("finishes during repeated transposition with variables 1 and 2 in BDD 13 [&&]", [&]() { std::vector call_history; @@ -4434,157 +4433,156 @@ go_bandit([]() { AssertThat(call_history.at(7), Is().EqualTo(3u)); }); - it("collapses during repeated transposition in BDD 12a [&&]", - [&]() { - std::vector call_history; - bdd out = bdd_exists(ep & exec_policy::access::Priority_Queue, - bdd_12a, - [&call_history](const bdd::label_type x) -> bool { - call_history.push_back(x); - return 0 < x && x < 3; - }); - - 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()); - - // TODO: meta variables... - - // Check call history - // - // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please - // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(13u)); - - // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); - AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); - - // - First top-down sweep - AssertThat(call_history.at(5), Is().EqualTo(0u)); - AssertThat(call_history.at(6), Is().EqualTo(1u)); - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(3u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); - - // - Second top-down sweep - AssertThat(call_history.at(10), Is().EqualTo(0u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(3u)); - }); + it("collapses during repeated transposition in BDD 12a [&&]", [&]() { + std::vector call_history; + bdd out = bdd_exists(ep & exec_policy::access::Priority_Queue, + bdd_12a, + [&call_history](const bdd::label_type x) -> bool { + call_history.push_back(x); + return 0 < x && x < 3; + }); + + 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()); + + // TODO: meta variables... + + // Check call history + // + // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please + // verify that this change makes sense and is as intended. + AssertThat(call_history.size(), Is().EqualTo(13u)); + + // - Generate predicate profile + AssertThat(call_history.at(0), Is().EqualTo(4u)); + AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); + + // - First top-down sweep + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); + + // - Second top-down sweep + AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(3u)); + }); it("finishes during repeated transposition in BDD 12b [&&]", [&]() { - std::vector call_history; - bdd out = bdd_exists(ep & exec_policy::access::Priority_Queue, - bdd_12b, - [&call_history](const bdd::label_type x) -> bool { - call_history.push_back(x); - return 0 < x && x < 3; - }); - - /* expected - // 1 ---- x0 - // / \ - // / \ ---- x1 - // / \ - // | | ---- x2 - // | | - // ? ? ---- x3 - // / \ / \ - // | \ T | - // | \__ / - // 7 8 ---- x4 - // / \ / \ - // T F F T - // - // The 'T' terminal at 'x3' is due to the pair (7,8) collapsing to the - // 'T' terminal. This tuple is created from (7,F,8) which in turn is - // created from (5,6,8) from the quantification (3,4) from (2). - */ - node_test_stream out_nodes(out); + std::vector call_history; + bdd out = bdd_exists(ep & exec_policy::access::Priority_Queue, + bdd_12b, + [&call_history](const bdd::label_type x) -> bool { + call_history.push_back(x); + return 0 < x && x < 3; + }); - AssertThat(out_nodes.can_pull(), Is().True()); // (8) - AssertThat(out_nodes.pull(), - Is().EqualTo(node( - 4, node::max_id, node::pointer_type(false), node::pointer_type(true)))); + /* expected + // 1 ---- x0 + // / \ + // / \ ---- x1 + // / \ + // | | ---- x2 + // | | + // ? ? ---- x3 + // / \ / \ + // | \ T | + // | \__ / + // 7 8 ---- x4 + // / \ / \ + // T F F T + // + // The 'T' terminal at 'x3' is due to the pair (7,8) collapsing to the + // 'T' terminal. This tuple is created from (7,F,8) which in turn is + // created from (5,6,8) from the quantification (3,4) from (2). + */ + node_test_stream out_nodes(out); - AssertThat(out_nodes.can_pull(), Is().True()); // (7) - AssertThat( - out_nodes.pull(), - Is().EqualTo( - node(4, node::max_id - 1, node::pointer_type(true), node::pointer_type(false)))); + AssertThat(out_nodes.can_pull(), Is().True()); // (8) + AssertThat(out_nodes.pull(), + Is().EqualTo(node( + 4, node::max_id, node::pointer_type(false), node::pointer_type(true)))); - AssertThat(out_nodes.can_pull(), Is().True()); // (5,6,8) - AssertThat( - out_nodes.pull(), - Is().EqualTo(node( - 3, node::max_id, node::pointer_type(true), node::pointer_type(4, node::max_id)))); + AssertThat(out_nodes.can_pull(), Is().True()); // (7) + AssertThat( + out_nodes.pull(), + Is().EqualTo( + node(4, node::max_id - 1, node::pointer_type(true), node::pointer_type(false)))); - AssertThat(out_nodes.can_pull(), Is().True()); // (5,6) - AssertThat(out_nodes.pull(), - Is().EqualTo(node(3, - node::max_id - 1, - node::pointer_type(4, node::max_id - 1), - node::pointer_type(4, node::max_id)))); + AssertThat(out_nodes.can_pull(), Is().True()); // (5,6,8) + AssertThat( + out_nodes.pull(), + Is().EqualTo(node( + 3, node::max_id, node::pointer_type(true), node::pointer_type(4, node::max_id)))); - AssertThat(out_nodes.can_pull(), Is().True()); // (1) - AssertThat(out_nodes.pull(), - Is().EqualTo(node(0, - node::max_id, - node::pointer_type(3, node::max_id - 1), - node::pointer_type(3, node::max_id)))); + AssertThat(out_nodes.can_pull(), Is().True()); // (5,6) + AssertThat(out_nodes.pull(), + Is().EqualTo(node(3, + node::max_id - 1, + node::pointer_type(4, node::max_id - 1), + node::pointer_type(4, node::max_id)))); - AssertThat(out_nodes.can_pull(), Is().False()); + AssertThat(out_nodes.can_pull(), Is().True()); // (1) + AssertThat(out_nodes.pull(), + Is().EqualTo(node(0, + node::max_id, + node::pointer_type(3, node::max_id - 1), + node::pointer_type(3, node::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(4u, 2u))); + level_info_test_stream out_meta(out); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(3u, 2u))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(4u, 2u))); - AssertThat(out_meta.can_pull(), Is().True()); - AssertThat(out_meta.pull(), Is().EqualTo(level_info(0u, 1u))); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(3u, 2u))); - AssertThat(out_meta.can_pull(), Is().False()); + AssertThat(out_meta.can_pull(), Is().True()); + AssertThat(out_meta.pull(), Is().EqualTo(level_info(0u, 1u))); - // TODO: meta variables... + AssertThat(out_meta.can_pull(), Is().False()); - // Check call history - // - // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please - // verify that this change makes sense and is as intended. - AssertThat(call_history.size(), Is().EqualTo(14u)); + // TODO: meta variables... - // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); - AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + // Check call history + // + // NOTE: Test failure does NOT indicate a bug, but only indicates a change. Please + // verify that this change makes sense and is as intended. + AssertThat(call_history.size(), Is().EqualTo(14u)); - // - First top-down sweep - AssertThat(call_history.at(5), Is().EqualTo(0u)); - AssertThat(call_history.at(6), Is().EqualTo(1u)); - AssertThat(call_history.at(7), Is().EqualTo(2u)); - AssertThat(call_history.at(8), Is().EqualTo(3u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); + // - Generate predicate profile + AssertThat(call_history.at(0), Is().EqualTo(4u)); + AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(1u)); + AssertThat(call_history.at(4), Is().EqualTo(0u)); - // - Second top-down sweep - AssertThat(call_history.at(10), Is().EqualTo(0u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(3u)); - AssertThat(call_history.at(13), Is().EqualTo(4u)); - }); + // - First top-down sweep + AssertThat(call_history.at(5), Is().EqualTo(0u)); + AssertThat(call_history.at(6), Is().EqualTo(1u)); + AssertThat(call_history.at(7), Is().EqualTo(2u)); + AssertThat(call_history.at(8), Is().EqualTo(3u)); + AssertThat(call_history.at(9), Is().EqualTo(4u)); + + // - Second top-down sweep + AssertThat(call_history.at(10), Is().EqualTo(0u)); + AssertThat(call_history.at(11), Is().EqualTo(2u)); + AssertThat(call_history.at(12), Is().EqualTo(3u)); + AssertThat(call_history.at(13), Is().EqualTo(4u)); + }); it("finishes during repeated transposition with variables 1 and 2 in BDD 13 [&&]", [&]() { std::vector call_history; From 27a31edd2ee4a2634330ed9d24cbb04e826011cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 2 May 2024 09:01:36 +0200 Subject: [PATCH 4/6] Reverse predicate profile direction --- src/adiar/internal/algorithms/quantify.h | 31 ++- test/adiar/bdd/test_quantify.cpp | 300 +++++++++++------------ test/adiar/zdd/test_project.cpp | 84 +++---- 3 files changed, 210 insertions(+), 205 deletions(-) diff --git a/src/adiar/internal/algorithms/quantify.h b/src/adiar/internal/algorithms/quantify.h index 27c609f2e..7c42727bc 100644 --- a/src/adiar/internal/algorithms/quantify.h +++ b/src/adiar/internal/algorithms/quantify.h @@ -1424,33 +1424,38 @@ namespace adiar::internal res.dd_width = dd_width(dd); res.dd_vars = dd_varcount(dd); - level_info_stream lis(dd); + level_info_stream lis(dd); const size_t third_dd_size = res.dd_size / 3; - size_t nodes_below = 0u; + + size_t nodes_above = 0u; + size_t nodes_below = res.dd_size; while (lis.can_pull()) { const level_info li = lis.pull(); + + nodes_below -= li.width(); + if (pred(li.label()) == Policy::quantify_onset) { res.quant_all_vars += 1u; res.quant_all_size += li.width(); - res.quant_deep_vars += nodes_below + 1 <= third_dd_size; - res.quant_shallow_vars += res.dd_size - third_dd_size <= nodes_below + li.width(); + res.quant_deep_vars += nodes_below < third_dd_size; + res.quant_shallow_vars += nodes_above <= third_dd_size; - { // Shallowest variable (always updated due to bottom-up direction). - res.shallowest_var.level = li.level(); - res.shallowest_var.nodes_below = nodes_below; - res.shallowest_var.width = li.width(); + { // Deepest variable (always updated due to top-down direction). + res.deepest_var.level = li.level(); + res.deepest_var.nodes_below = nodes_below; + res.deepest_var.width = li.width(); } - // Deepest variable. - if (res.deepest_var.level < li.level()) { res.deepest_var = res.shallowest_var; } + // Shallowest variable + if (res.shallowest_var.level < li.level()) { res.shallowest_var = res.deepest_var; } // Widest variable - if (res.widest_var.width < li.width()) { res.widest_var = res.shallowest_var; } + if (res.widest_var.width < li.width()) { res.widest_var = res.deepest_var; } // Narrowest variable - if (li.width() < res.narrowest_var.width) { res.narrowest_var = res.shallowest_var; } + if (li.width() < res.narrowest_var.width) { res.narrowest_var = res.deepest_var; } } - nodes_below += li.width(); + nodes_above += li.width(); } return res; } diff --git a/test/adiar/bdd/test_quantify.cpp b/test/adiar/bdd/test_quantify.cpp index 276e1610a..c2a826585 100644 --- a/test/adiar/bdd/test_quantify.cpp +++ b/test/adiar/bdd/test_quantify.cpp @@ -2614,10 +2614,10 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(11u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(3u)); - AssertThat(call_history.at(1), Is().EqualTo(2u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); // - Pruning sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -2663,11 +2663,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(11u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - Pruning sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -2704,9 +2704,9 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(4u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(2u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); AssertThat(call_history.at(1), Is().EqualTo(1u)); - AssertThat(call_history.at(2), Is().EqualTo(0u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -2750,11 +2750,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(13u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - Pruning sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -2793,9 +2793,9 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(7u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(2u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); AssertThat(call_history.at(1), Is().EqualTo(1u)); - AssertThat(call_history.at(2), Is().EqualTo(0u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -2866,10 +2866,10 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(11u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(3u)); - AssertThat(call_history.at(1), Is().EqualTo(2u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); // - Pruning sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -2915,11 +2915,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(11u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - Pruning sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -2956,9 +2956,9 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(4u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(2u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); AssertThat(call_history.at(1), Is().EqualTo(1u)); - AssertThat(call_history.at(2), Is().EqualTo(0u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -3002,11 +3002,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(13u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - Pruning sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -3045,9 +3045,9 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(7u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(2u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); AssertThat(call_history.at(1), Is().EqualTo(1u)); - AssertThat(call_history.at(2), Is().EqualTo(0u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -3190,11 +3190,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(15u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - Pruning sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -3554,10 +3554,10 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(7u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(3u)); - AssertThat(call_history.at(1), Is().EqualTo(2u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); // - First top-down sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -3608,10 +3608,10 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(8u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(3u)); - AssertThat(call_history.at(1), Is().EqualTo(2u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); // - First top-down sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -3647,11 +3647,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(13u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - First top-down sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -3751,11 +3751,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(14u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - First top-down sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -3935,14 +3935,14 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(23u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(7u)); - AssertThat(call_history.at(1), Is().EqualTo(6u)); - AssertThat(call_history.at(2), Is().EqualTo(5u)); - AssertThat(call_history.at(3), Is().EqualTo(4u)); - AssertThat(call_history.at(4), Is().EqualTo(3u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(1u)); - AssertThat(call_history.at(7), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(5u)); + AssertThat(call_history.at(6), Is().EqualTo(6u)); + AssertThat(call_history.at(7), Is().EqualTo(7u)); // - First top-down sweep AssertThat(call_history.at(8), Is().EqualTo(0u)); @@ -3998,11 +3998,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(9u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - First top-down sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -4291,20 +4291,20 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(41u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(13u)); - AssertThat(call_history.at(1), Is().EqualTo(12u)); - AssertThat(call_history.at(2), Is().EqualTo(11u)); - AssertThat(call_history.at(3), Is().EqualTo(10u)); - AssertThat(call_history.at(4), Is().EqualTo(9u)); - AssertThat(call_history.at(5), Is().EqualTo(8u)); - AssertThat(call_history.at(6), Is().EqualTo(7u)); - AssertThat(call_history.at(7), Is().EqualTo(6u)); - AssertThat(call_history.at(8), Is().EqualTo(5u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); - AssertThat(call_history.at(10), Is().EqualTo(3u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(1u)); - AssertThat(call_history.at(13), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(5u)); + AssertThat(call_history.at(6), Is().EqualTo(6u)); + AssertThat(call_history.at(7), Is().EqualTo(7u)); + AssertThat(call_history.at(8), Is().EqualTo(8u)); + AssertThat(call_history.at(9), Is().EqualTo(9u)); + AssertThat(call_history.at(10), Is().EqualTo(10u)); + AssertThat(call_history.at(11), Is().EqualTo(11u)); + AssertThat(call_history.at(12), Is().EqualTo(12u)); + AssertThat(call_history.at(13), Is().EqualTo(13u)); // - First top-down sweep AssertThat(call_history.at(14), Is().EqualTo(0u)); @@ -4367,10 +4367,10 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(7u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(3u)); - AssertThat(call_history.at(1), Is().EqualTo(2u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); // - First top-down sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -4421,10 +4421,10 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(8u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(3u)); - AssertThat(call_history.at(1), Is().EqualTo(2u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); // - First top-down sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -4460,11 +4460,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(13u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - First top-down sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -4564,11 +4564,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(14u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - First top-down sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -4748,14 +4748,14 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(23u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(7u)); - AssertThat(call_history.at(1), Is().EqualTo(6u)); - AssertThat(call_history.at(2), Is().EqualTo(5u)); - AssertThat(call_history.at(3), Is().EqualTo(4u)); - AssertThat(call_history.at(4), Is().EqualTo(3u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(1u)); - AssertThat(call_history.at(7), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(5u)); + AssertThat(call_history.at(6), Is().EqualTo(6u)); + AssertThat(call_history.at(7), Is().EqualTo(7u)); // - First top-down sweep AssertThat(call_history.at(8), Is().EqualTo(0u)); @@ -4811,11 +4811,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(9u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - First top-down sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -5104,20 +5104,20 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(41u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(13u)); - AssertThat(call_history.at(1), Is().EqualTo(12u)); - AssertThat(call_history.at(2), Is().EqualTo(11u)); - AssertThat(call_history.at(3), Is().EqualTo(10u)); - AssertThat(call_history.at(4), Is().EqualTo(9u)); - AssertThat(call_history.at(5), Is().EqualTo(8u)); - AssertThat(call_history.at(6), Is().EqualTo(7u)); - AssertThat(call_history.at(7), Is().EqualTo(6u)); - AssertThat(call_history.at(8), Is().EqualTo(5u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); - AssertThat(call_history.at(10), Is().EqualTo(3u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(1u)); - AssertThat(call_history.at(13), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(5u)); + AssertThat(call_history.at(6), Is().EqualTo(6u)); + AssertThat(call_history.at(7), Is().EqualTo(7u)); + AssertThat(call_history.at(8), Is().EqualTo(8u)); + AssertThat(call_history.at(9), Is().EqualTo(9u)); + AssertThat(call_history.at(10), Is().EqualTo(10u)); + AssertThat(call_history.at(11), Is().EqualTo(11u)); + AssertThat(call_history.at(12), Is().EqualTo(12u)); + AssertThat(call_history.at(13), Is().EqualTo(13u)); // - First top-down sweep AssertThat(call_history.at(14), Is().EqualTo(0u)); @@ -5424,20 +5424,20 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(41u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(13u)); - AssertThat(call_history.at(1), Is().EqualTo(12u)); - AssertThat(call_history.at(2), Is().EqualTo(11u)); - AssertThat(call_history.at(3), Is().EqualTo(10u)); - AssertThat(call_history.at(4), Is().EqualTo(9u)); - AssertThat(call_history.at(5), Is().EqualTo(8u)); - AssertThat(call_history.at(6), Is().EqualTo(7u)); - AssertThat(call_history.at(7), Is().EqualTo(6u)); - AssertThat(call_history.at(8), Is().EqualTo(5u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); - AssertThat(call_history.at(10), Is().EqualTo(3u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(1u)); - AssertThat(call_history.at(13), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(5u)); + AssertThat(call_history.at(6), Is().EqualTo(6u)); + AssertThat(call_history.at(7), Is().EqualTo(7u)); + AssertThat(call_history.at(8), Is().EqualTo(8u)); + AssertThat(call_history.at(9), Is().EqualTo(9u)); + AssertThat(call_history.at(10), Is().EqualTo(10u)); + AssertThat(call_history.at(11), Is().EqualTo(11u)); + AssertThat(call_history.at(12), Is().EqualTo(12u)); + AssertThat(call_history.at(13), Is().EqualTo(13u)); // - Top-down sweep AssertThat(call_history.at(14), Is().EqualTo(0u)); @@ -5538,11 +5538,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(14u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - First top-down sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -5609,10 +5609,10 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(11u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(3u)); - AssertThat(call_history.at(1), Is().EqualTo(2u)); - AssertThat(call_history.at(2), Is().EqualTo(1u)); - AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); // - Pruning sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -5709,14 +5709,14 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(21u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(7u)); - AssertThat(call_history.at(1), Is().EqualTo(6u)); - AssertThat(call_history.at(2), Is().EqualTo(5u)); - AssertThat(call_history.at(3), Is().EqualTo(4u)); - AssertThat(call_history.at(4), Is().EqualTo(3u)); - AssertThat(call_history.at(5), Is().EqualTo(2u)); - AssertThat(call_history.at(6), Is().EqualTo(1u)); - AssertThat(call_history.at(7), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(5u)); + AssertThat(call_history.at(6), Is().EqualTo(6u)); + AssertThat(call_history.at(7), Is().EqualTo(7u)); // - Pruning sweep AssertThat(call_history.at(8), Is().EqualTo(0u)); diff --git a/test/adiar/zdd/test_project.cpp b/test/adiar/zdd/test_project.cpp index 4b91b1bf6..e282d7f13 100644 --- a/test/adiar/zdd/test_project.cpp +++ b/test/adiar/zdd/test_project.cpp @@ -678,11 +678,11 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(15u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(1u)); - AssertThat(call_history.at(4), Is().EqualTo(0u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); // - Pruning sweep AssertThat(call_history.at(5), Is().EqualTo(0u)); @@ -742,9 +742,9 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(7u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(3u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); AssertThat(call_history.at(1), Is().EqualTo(1u)); - AssertThat(call_history.at(2), Is().EqualTo(0u)); + AssertThat(call_history.at(2), Is().EqualTo(3u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -809,10 +809,10 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(11u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); - AssertThat(call_history.at(1), Is().EqualTo(3u)); - AssertThat(call_history.at(2), Is().EqualTo(2u)); - AssertThat(call_history.at(3), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(2u)); + AssertThat(call_history.at(2), Is().EqualTo(3u)); + AssertThat(call_history.at(3), Is().EqualTo(4u)); // - Pruning sweep AssertThat(call_history.at(4), Is().EqualTo(0u)); @@ -934,9 +934,9 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(6u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(2u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); AssertThat(call_history.at(1), Is().EqualTo(1u)); - AssertThat(call_history.at(2), Is().EqualTo(0u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); // - First top-down sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -1142,9 +1142,9 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(9u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(4u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); AssertThat(call_history.at(1), Is().EqualTo(2u)); - AssertThat(call_history.at(2), Is().EqualTo(0u)); + AssertThat(call_history.at(2), Is().EqualTo(4u)); // - Pruning sweep AssertThat(call_history.at(3), Is().EqualTo(0u)); @@ -1534,20 +1534,20 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(41u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(13u)); - AssertThat(call_history.at(1), Is().EqualTo(12u)); - AssertThat(call_history.at(2), Is().EqualTo(11u)); - AssertThat(call_history.at(3), Is().EqualTo(10u)); - AssertThat(call_history.at(4), Is().EqualTo(9u)); - AssertThat(call_history.at(5), Is().EqualTo(8u)); - AssertThat(call_history.at(6), Is().EqualTo(7u)); - AssertThat(call_history.at(7), Is().EqualTo(6u)); - AssertThat(call_history.at(8), Is().EqualTo(5u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); - AssertThat(call_history.at(10), Is().EqualTo(3u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(1u)); - AssertThat(call_history.at(13), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(5u)); + AssertThat(call_history.at(6), Is().EqualTo(6u)); + AssertThat(call_history.at(7), Is().EqualTo(7u)); + AssertThat(call_history.at(8), Is().EqualTo(8u)); + AssertThat(call_history.at(9), Is().EqualTo(9u)); + AssertThat(call_history.at(10), Is().EqualTo(10u)); + AssertThat(call_history.at(11), Is().EqualTo(11u)); + AssertThat(call_history.at(12), Is().EqualTo(12u)); + AssertThat(call_history.at(13), Is().EqualTo(13u)); // - First top-down sweep AssertThat(call_history.at(14), Is().EqualTo(0u)); @@ -1958,20 +1958,20 @@ go_bandit([]() { AssertThat(call_history.size(), Is().EqualTo(41u)); // - Generate predicate profile - AssertThat(call_history.at(0), Is().EqualTo(13u)); - AssertThat(call_history.at(1), Is().EqualTo(12u)); - AssertThat(call_history.at(2), Is().EqualTo(11u)); - AssertThat(call_history.at(3), Is().EqualTo(10u)); - AssertThat(call_history.at(4), Is().EqualTo(9u)); - AssertThat(call_history.at(5), Is().EqualTo(8u)); - AssertThat(call_history.at(6), Is().EqualTo(7u)); - AssertThat(call_history.at(7), Is().EqualTo(6u)); - AssertThat(call_history.at(8), Is().EqualTo(5u)); - AssertThat(call_history.at(9), Is().EqualTo(4u)); - AssertThat(call_history.at(10), Is().EqualTo(3u)); - AssertThat(call_history.at(11), Is().EqualTo(2u)); - AssertThat(call_history.at(12), Is().EqualTo(1u)); - AssertThat(call_history.at(13), Is().EqualTo(0u)); + AssertThat(call_history.at(0), Is().EqualTo(0u)); + AssertThat(call_history.at(1), Is().EqualTo(1u)); + AssertThat(call_history.at(2), Is().EqualTo(2u)); + AssertThat(call_history.at(3), Is().EqualTo(3u)); + AssertThat(call_history.at(4), Is().EqualTo(4u)); + AssertThat(call_history.at(5), Is().EqualTo(5u)); + AssertThat(call_history.at(6), Is().EqualTo(6u)); + AssertThat(call_history.at(7), Is().EqualTo(7u)); + AssertThat(call_history.at(8), Is().EqualTo(8u)); + AssertThat(call_history.at(9), Is().EqualTo(9u)); + AssertThat(call_history.at(10), Is().EqualTo(10u)); + AssertThat(call_history.at(11), Is().EqualTo(11u)); + AssertThat(call_history.at(12), Is().EqualTo(12u)); + AssertThat(call_history.at(13), Is().EqualTo(13u)); // - Top-down sweep AssertThat(call_history.at(14), Is().EqualTo(0u)); From 8c05ec848866638f0116e94cb3fc47f31f143722 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 2 May 2024 09:07:07 +0200 Subject: [PATCH 5/6] Reintroduce width dictates 'deep' and 'shallow' variables --- src/adiar/internal/algorithms/quantify.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/adiar/internal/algorithms/quantify.h b/src/adiar/internal/algorithms/quantify.h index 7c42727bc..262aebdbf 100644 --- a/src/adiar/internal/algorithms/quantify.h +++ b/src/adiar/internal/algorithms/quantify.h @@ -1430,6 +1430,7 @@ namespace adiar::internal size_t nodes_above = 0u; size_t nodes_below = res.dd_size; + bool seen_widest = false; while (lis.can_pull()) { const level_info li = lis.pull(); @@ -1439,8 +1440,8 @@ namespace adiar::internal if (pred(li.label()) == Policy::quantify_onset) { res.quant_all_vars += 1u; res.quant_all_size += li.width(); - res.quant_deep_vars += nodes_below < third_dd_size; - res.quant_shallow_vars += nodes_above <= third_dd_size; + res.quant_deep_vars += seen_widest && nodes_below < third_dd_size; + res.quant_shallow_vars += !seen_widest && nodes_above <= third_dd_size; { // Deepest variable (always updated due to top-down direction). res.deepest_var.level = li.level(); @@ -1456,6 +1457,7 @@ namespace adiar::internal } nodes_above += li.width(); + seen_widest |= li.width() == res.dd_width; } return res; } From 6f272c392de97bb13ccd1600191fd5d64d4a65bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Thu, 2 May 2024 09:11:20 +0200 Subject: [PATCH 6/6] Make width further restrict definition of 'deep' variables Compared to using 'seen_widest' in the previous commit, this better encapsulate a diamond-shaped but BDD that gets wide early. The 'deep' variables are then symmetrically only the ones as deep as the ones at the top (measured in number of nodes, not number of levels). --- src/adiar/internal/algorithms/quantify.h | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/adiar/internal/algorithms/quantify.h b/src/adiar/internal/algorithms/quantify.h index 262aebdbf..b583a9e29 100644 --- a/src/adiar/internal/algorithms/quantify.h +++ b/src/adiar/internal/algorithms/quantify.h @@ -1426,11 +1426,10 @@ namespace adiar::internal level_info_stream lis(dd); - const size_t third_dd_size = res.dd_size / 3; + size_t shallow_threshold = res.dd_size / 3; - size_t nodes_above = 0u; - size_t nodes_below = res.dd_size; - bool seen_widest = false; + size_t nodes_above = 0u; + size_t nodes_below = res.dd_size; while (lis.can_pull()) { const level_info li = lis.pull(); @@ -1440,8 +1439,8 @@ namespace adiar::internal if (pred(li.label()) == Policy::quantify_onset) { res.quant_all_vars += 1u; res.quant_all_size += li.width(); - res.quant_deep_vars += seen_widest && nodes_below < third_dd_size; - res.quant_shallow_vars += !seen_widest && nodes_above <= third_dd_size; + res.quant_deep_vars += nodes_below < shallow_threshold; + res.quant_shallow_vars += nodes_above <= shallow_threshold; { // Deepest variable (always updated due to top-down direction). res.deepest_var.level = li.level(); @@ -1456,8 +1455,10 @@ namespace adiar::internal if (li.width() < res.narrowest_var.width) { res.narrowest_var = res.deepest_var; } } + if (li.width() == res.dd_width) { + shallow_threshold = std::min(shallow_threshold, nodes_above); + } nodes_above += li.width(); - seen_widest |= li.width() == res.dd_width; } return res; }