diff --git a/src/adiar/internal/algorithms/quantify.h b/src/adiar/internal/algorithms/quantify.h index 8f9d9f04f..748e511d2 100644 --- a/src/adiar/internal/algorithms/quantify.h +++ b/src/adiar/internal/algorithms/quantify.h @@ -218,7 +218,7 @@ namespace adiar::internal && req.target.second().is_node() && req.target.first().label() == req.target.second().label()) { adiar_assert(!req.target.second().is_nil(), - "req.target.second().is_node ==> !req.target.second().is_nil()"); + "req.target.second().is_node() ==> !req.target.second().is_nil()"); quantify_pq_2.push({ req.target, {v.children()}, req.data }); @@ -646,8 +646,11 @@ namespace adiar::internal quantify_priority_queue_2_t::memory_fits(inner_remaining_memory); const size_t pq_2_bound = + // Obtain 1-level cut from subset __quantify_ilevel_upper_bound - (typename quantify_policy::dd_type(outer_file), _op); + (typename quantify_policy::dd_type(outer_file), _op) + // Add crossing arcs + + (inner_pq_1.size()); const size_t max_pq_2_size = ep.memory_mode() == exec_policy::memory::Internal ? std::min(pq_2_memory_fits, pq_2_bound) diff --git a/test/adiar/bdd/test_quantify.cpp b/test/adiar/bdd/test_quantify.cpp index 2f9b52efc..43e0d8cfa 100644 --- a/test/adiar/bdd/test_quantify.cpp +++ b/test/adiar/bdd/test_quantify.cpp @@ -729,6 +729,56 @@ go_bandit([]() { ; } + //////////////////////////////////////////////////////////////////////////////////////////////// + // BDD 16 + // + // Designed to make outer root arcs dominate the 1-level cut within Nested Sweeping. + // + // NOTE: Designing this counter-example such that it is fully reduced is not easy to do (nor + // easy to understand). So, we "cheat" by making x4 a level full of duplicates. + /* + // _1_ ---- x0 + // / \ + // _2_ \ ---- x1 + // / \ \ + // 3 4 \ ---- x2 + // / \ / \ \ + // 5 6 7 8 \ ---- x3 + // /| |\ /| |\ \ + // ---- 9 ---- | ---- x4 <--- nodes for x6 having 1-level cut = 1 + // \.|./ \.|./ | + // a b | ---- x5 <--- forwarding of all in-going arcs of (a) to (b/c) + // / \ / \ | + // T F F T c ---- x6 <--- transposition quantification + // / \ + // F T + */ + shared_levelized_file bdd_16; + + { + const node nc = node(6, node::max_id, ptr_uint64(false), ptr_uint64(true)); + const node nb = node(5, node::max_id, ptr_uint64(false), ptr_uint64(true)); + const node na = node(5, node::max_id-1, ptr_uint64(true), ptr_uint64(false)); + + const node n9_3 = node(4, node::max_id, na.uid(), nb.uid()); + const node n9_2 = node(4, node::max_id-1, na.uid(), nb.uid()); + const node n9_1 = node(4, node::max_id-2, na.uid(), nb.uid()); + + const node n8 = node(3, node::max_id, n9_2.uid(), n9_3.uid()); + const node n7 = node(3, node::max_id-1, n9_1.uid(), n9_3.uid()); + const node n6 = node(3, node::max_id-2, n9_2.uid(), n9_1.uid()); + const node n5 = node(3, node::max_id-3, n9_1.uid(), n9_2.uid()); + const node n4 = node(2, node::max_id, n7.uid(), n8.uid()); + const node n3 = node(2, node::max_id-1, n5.uid(), n6.uid()); + const node n2 = node(1, node::max_id, n3.uid(), n4.uid()); + const node n1 = node(0, node::max_id, n2.uid(), nc.uid()); + + node_writer nw(bdd_16); + nw << nc << nb << na + << n9_3 << n9_2 << n9_1 + << n8 << n7 << n6 << n5 << n4 << n3 << n2 << n1; + } + //////////////////////////////////////////////////////////////////////////// describe("bdd_exists(const bdd&, bdd::label_type)", [&]() { it("should quantify T terminal-only BDD as itself", [&]() { @@ -2731,6 +2781,27 @@ go_bandit([]() { // TODO: meta variables... }); + + it("accounts for number of root arcs from Outer Sweep [&&]", [&]() { + /* expected + // + // T + */ + bdd out = bdd_exists(ep, bdd_16, [](int x) -> bool { return x != 5; }); + + 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 + }); }); describe("quantify_alg == Auto", [&]() { @@ -4088,6 +4159,39 @@ go_bandit([]() { // TODO: meta variables }); + + it("accounts for number of root arcs from Outer Sweep [&]", [&]() { + int var = 6; + + /* expected + // + // T + */ + bdd out = bdd_exists(ep, bdd_16, [&var]() -> optional { + var -= 1; + + if (var < 0) { + return make_optional(); + } + if (var == 5) { + var -= 1; + } + return var; + }); + + 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 + }); }); }); @@ -4682,6 +4786,27 @@ go_bandit([]() { // TODO: meta variables }); + + it("accounts for number of root arcs from Outer Sweep [&&]", [&]() { + /* expected + // + // F + */ + bdd out = bdd_forall(ep, bdd_16, [](int x) -> bool { return x != 5; }); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + // TODO: meta variables + }); }); describe("quantify_alg == Auto", [&]() { @@ -4949,6 +5074,39 @@ go_bandit([]() { // TODO: meta variables }); + + it("accounts for number of root arcs from Outer Sweep [&]", [&]() { + int var = 6; + + /* expected + // + // F + */ + bdd out = bdd_forall(ep, bdd_16, [&var]() -> optional { + var -= 1; + + if (var < 0) { + return make_optional(); + } + if (var == 5) { + var -= 1; + } + return var; + }); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(false))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream out_meta(out); + + AssertThat(out_meta.can_pull(), Is().False()); + + // TODO: meta variables + }); }); }); diff --git a/test/adiar/zdd/test_project.cpp b/test/adiar/zdd/test_project.cpp index 81bff8075..fd5fa908d 100644 --- a/test/adiar/zdd/test_project.cpp +++ b/test/adiar/zdd/test_project.cpp @@ -240,6 +240,52 @@ go_bandit([]() { ; } + // { ... } + // + // See BDD 16 in test/adiar/bdd/test_quantify.cpp for more details. + /* + // _1_ ---- x0 + // / \ + // _2_ \ ---- x1 + // / \ \ + // 3 4 \ ---- x2 + // / \ / \ \ + // 5 6 7 8 \ ---- x3 + // /| |\ /| |\ \ + // ---- 9 ---- | ---- x4 + // \.|./ \.|./ | + // a b | ---- x5 + // / \ / \ | + // F T T T c ---- x6 + // / \ + // F T + */ + shared_levelized_file zdd_6; + + { + const node nc = node(6, node::max_id, ptr_uint64(false), ptr_uint64(true)); + const node nb = node(5, node::max_id, ptr_uint64(true), ptr_uint64(true)); + const node na = node(5, node::max_id-1, ptr_uint64(false), ptr_uint64(true)); + + const node n9_3 = node(4, node::max_id, na.uid(), nb.uid()); + const node n9_2 = node(4, node::max_id-1, na.uid(), nb.uid()); + const node n9_1 = node(4, node::max_id-2, na.uid(), nb.uid()); + + const node n8 = node(3, node::max_id, n9_2.uid(), n9_3.uid()); + const node n7 = node(3, node::max_id-1, n9_1.uid(), n9_3.uid()); + const node n6 = node(3, node::max_id-2, n9_2.uid(), n9_1.uid()); + const node n5 = node(3, node::max_id-3, n9_1.uid(), n9_2.uid()); + const node n4 = node(2, node::max_id, n7.uid(), n8.uid()); + const node n3 = node(2, node::max_id-1, n5.uid(), n6.uid()); + const node n2 = node(1, node::max_id, n3.uid(), n4.uid()); + const node n1 = node(0, node::max_id, n2.uid(), nc.uid()); + + node_writer nw(zdd_6); + nw << nc << nb << na + << n9_3 << n9_2 << n9_1 + << n8 << n7 << n6 << n5 << n4 << n3 << n2 << n1; + } + // TODO: Turn 'GreaterThanOrEqualTo' in max 1-level cuts below into an // 'EqualTo'. @@ -940,6 +986,42 @@ go_bandit([]() { AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(4u)); }); + + it("accounts for number of root arcs from Outer Sweep [const &]", [&](){ + const zdd in = zdd_6; + + /* Expected: { Ø, {5} } + // + // 1 ---- x5 + // / \ + // T T + */ + zdd out = zdd_project(ep, in, [](const zdd::label_type x) { return x == 5; }); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(5, node::max_id, + terminal_T, + terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream ms(out); + + AssertThat(ms.can_pull(), Is().True()); + AssertThat(ms.pull(), Is().EqualTo(level_info(5,1u))); + + AssertThat(ms.can_pull(), Is().False()); + + AssertThat(out->max_1level_cut[cut::Internal], Is().GreaterThanOrEqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().GreaterThanOrEqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); }); describe("quantify_alg == Auto", [&]() { @@ -2648,6 +2730,42 @@ go_bandit([]() { AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); AssertThat(out->number_of_terminals[true], Is().EqualTo(4u)); }); + + it("accounts for number of root arcs from Outer Sweep [const &]", [&](){ + const zdd in = zdd_6; + + /* Expected: { Ø, {5} } + // + // 1 ---- x5 + // / \ + // T T + */ + zdd out = zdd_project(ep, in, [](const zdd::label_type x) { return x == 5; }); + + node_test_stream out_nodes(out); + + AssertThat(out_nodes.can_pull(), Is().True()); + AssertThat(out_nodes.pull(), Is().EqualTo(node(5, node::max_id, + terminal_T, + terminal_T))); + + AssertThat(out_nodes.can_pull(), Is().False()); + + level_info_test_stream ms(out); + + AssertThat(ms.can_pull(), Is().True()); + AssertThat(ms.pull(), Is().EqualTo(level_info(5,1u))); + + AssertThat(ms.can_pull(), Is().False()); + + AssertThat(out->max_1level_cut[cut::Internal], Is().GreaterThanOrEqualTo(1u)); + AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(0u)); + AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u)); + AssertThat(out->max_1level_cut[cut::All], Is().GreaterThanOrEqualTo(2u)); + + AssertThat(out->number_of_terminals[false], Is().EqualTo(0u)); + AssertThat(out->number_of_terminals[true], Is().EqualTo(2u)); + }); }); });