Skip to content

Commit

Permalink
Transpose input on first existing to-be quantified variable
Browse files Browse the repository at this point in the history
This makes sure the more expensive quantification sweep is not wasted.
Assuming the user did not provide non-existing variables, this should
only add an O(1) overhead to the start of the quantification algorithm
  • Loading branch information
SSoelvsten committed Jul 4, 2023
1 parent d0b40bd commit b8fdd71
Show file tree
Hide file tree
Showing 2 changed files with 113 additions and 5 deletions.
43 changes: 38 additions & 5 deletions src/adiar/internal/algorithms/quantify.h
Original file line number Diff line number Diff line change
Expand Up @@ -780,13 +780,46 @@ namespace adiar::internal
// (assuming we have to quantify the on-set) still use the
// bottom-most level to transpose the DAG.
if constexpr (quantify_policy::quantify_onset) {
typename quantify_policy::label_t label = gen();
if (quantify_policy::MAX_LABEL < label) { return dd; }

// TODO: get bottom-most level that actually exists in DAG.
// Obtain the bottom-most onset level that exists in the diagram.
typename quantify_policy::label_t transposition_level = gen();
if (quantify_policy::MAX_LABEL < transposition_level) { return dd; }

{
level_info_stream<true> in_meta(dd);
typename quantify_policy::label_t dd_level = in_meta.pull().level();

while (true) {
// Go forward in the diagram's levels, until we are at or above
// the current candidate
while (in_meta.can_pull() && transposition_level < dd_level) {
dd_level = in_meta.pull().level();
}
// There is no onset level in the diagram? If so, then nothing is
// going to change and we may just return the input.
if (!in_meta.can_pull() && transposition_level < dd_level) {
return dd;
}

adiar_debug(dd_level <= transposition_level,
"Must be at or above candidate level");

// Did we find the current candidate or skipped past it?
if (dd_level == transposition_level) {
break;
} else { // dd_level < transposition_level
transposition_level = gen();

// Did we run out of 'onset' levels?
if (quantify_policy::MAX_LABEL < transposition_level) {
return dd;
}
}
}
}

// Quantify the 'transposition_level' as part of the initial transposition step
multi_quantify_policy__gen<quantify_policy> inner_impl(op, gen);
return nested_sweep<>(quantify<quantify_policy>(dd, label, op), inner_impl);
return nested_sweep<>(quantify<quantify_policy>(dd, transposition_level, op), inner_impl);
} else { // !quantify_policy::quantify_onset
multi_quantify_policy__gen<quantify_policy> inner_impl(op, gen);
return nested_sweep<>(dd, inner_impl);
Expand Down
75 changes: 75 additions & 0 deletions test/adiar/bdd/test_quantify.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -348,6 +348,29 @@ go_bandit([]() {
nw << n10_8 << n10_7 << n10_6 << n10_5 << n10_4 << n10_3 << n10_2 << n10_1;
}

////////////////////////////////////////////////////////////////////////////
// BDD 11 : Same as BDD 3, but with gaps in-between the levelsn
/*
// 1 ---- x2
// / \
// | 2 ---- x4
// \ / \
// 3 4 ---- x6
// / \ / \
// T F F T
*/
shared_levelized_file<bdd::node_t> bdd_11;

node n11_4 = node(6, node::MAX_ID, ptr_uint64(false), ptr_uint64(true));
node n11_3 = node(6, node::MAX_ID-1, ptr_uint64(true), ptr_uint64(false));
node n11_2 = node(4, node::MAX_ID, n11_3.uid(), n11_4.uid());
node n11_1 = node(2, node::MAX_ID, n11_3.uid(), n11_2.uid());

{ // Garbage collect writer to free write-lock
node_writer nw_11(bdd_11);
nw_11 << n11_4 << n11_3 << n11_2 << n11_1;
}

////////////////////////////////////////////////////////////////////////////
describe("bdd_exists(const bdd&, bdd::label_t)", [&]() {
it("should quantify T terminal-only BDD as itself", [&]() {
Expand Down Expand Up @@ -1816,6 +1839,27 @@ go_bandit([]() {
});

describe("bdd_exists(const bdd&, IT begin, IT end)", [&]() {
it("returns original file for [].begin() in BDD 1 [&]", [&]() {
const std::vector<bdd::label_t> vars = { };
const bdd out = bdd_exists(bdd_1, vars.begin(), vars.end());

AssertThat(out.file_ptr(), Is().EqualTo(bdd_1));
});

it("returns original file for [3, 5].rbegin() in BDD 11 [&]", [&]() {
const std::vector<bdd::label_t> vars = { 3,5 };
const bdd out = bdd_exists(bdd_11, vars.rbegin(), vars.rend());

AssertThat(out.file_ptr(), Is().EqualTo(bdd_11));
});

it("returns original file for [0, 3].rbegin() in BDD 11 [&]", [&]() {
const std::vector<bdd::label_t> vars = { 0,3 };
const bdd out = bdd_exists(bdd_11, vars.rbegin(), vars.rend());

AssertThat(out.file_ptr(), Is().EqualTo(bdd_11));
});

it("quantifies [1, 3].rbegin() in BDD 4 [&&]", [&]() {
std::vector<bdd::label_t> vars = { 1 , 3 };

Expand Down Expand Up @@ -1876,6 +1920,37 @@ go_bandit([]() {

AssertThat(out_meta.can_pull(), Is().False());
});

it("quantifies [4, 2, 0].begin() in BDD 4 [const &]", [&]() {
const bdd in = bdd_4;
const std::vector<bdd::label_t> vars = { 4, 2, 0 };

bdd out = bdd_exists(in, vars.begin(), vars.end());

node_test_stream out_nodes(out);

AssertThat(out_nodes.can_pull(), Is().True()); // (5)
AssertThat(out_nodes.pull(), Is().EqualTo(node(3, node::MAX_ID,
ptr_uint64(false),
ptr_uint64(true))));

AssertThat(out_nodes.can_pull(), Is().True()); // (2')
AssertThat(out_nodes.pull(), Is().EqualTo(node(1, node::MAX_ID,
ptr_uint64(3, ptr_uint64::MAX_ID),
ptr_uint64(true))));

AssertThat(out_nodes.can_pull(), Is().False());

level_info_test_stream out_meta(out);

AssertThat(out_meta.can_pull(), Is().True());
AssertThat(out_meta.pull(), Is().EqualTo(level_info(3u,1u)));

AssertThat(out_meta.can_pull(), Is().True());
AssertThat(out_meta.pull(), Is().EqualTo(level_info(1u,1u)));

AssertThat(out_meta.can_pull(), Is().False());
});
});

////////////////////////////////////////////////////////////////////////////
Expand Down

0 comments on commit b8fdd71

Please sign in to comment.