Skip to content

Commit

Permalink
Fix Quantify::PriorityQueue2 does not account for Nested Sweep's cros…
Browse files Browse the repository at this point in the history 
…sing arcs
  • Loading branch information
@SSoelvsten
SSoelvsten committed Dec 6, 2023
1 parent 945dc7f commit 62bf812
Show file tree
Hide file tree
Showing 3 changed files with 281 additions and 2 deletions.
7 changes: 5 additions & 2 deletions src/adiar/internal/algorithms/quantify.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 });

Expand Down Expand Up @@ -646,8 +646,11 @@ namespace adiar::internal
quantify_priority_queue_2_t<memory_mode::Internal>::memory_fits(inner_remaining_memory);

const size_t pq_2_bound =
// Obtain 1-level cut from subset
__quantify_ilevel_upper_bound<quantify_policy, get_1level_cut, 0u>
(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)
Expand Down
158 changes: 158 additions & 0 deletions test/adiar/bdd/test_quantify.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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::node_type> 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", [&]() {
Expand Down Expand Up @@ -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", [&]() {
Expand Down Expand Up @@ -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<bdd::label_type> {
var -= 1;

if (var < 0) {
return make_optional<bdd::label_type>();
}
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
});
});
});

Expand Down Expand Up @@ -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", [&]() {
Expand Down Expand Up @@ -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<bdd::label_type> {
var -= 1;

if (var < 0) {
return make_optional<bdd::label_type>();
}
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
});
});
});

Expand Down
118 changes: 118 additions & 0 deletions test/adiar/zdd/test_project.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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::node_type> 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'.

Expand Down Expand Up @@ -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", [&]() {
Expand Down Expand Up @@ -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));
});
});
});

Expand Down

0 comments on commit 62bf812

Please sign in to comment.