Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bdd/relprev/renaming prefix #681

Merged
merged 3 commits into from
Jun 24, 2024
Merged

Bdd/relprev/renaming prefix #681

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c9dd6c0
Update/Fix comments in 'select' and 'quantify' algorithms
SSoelvsten Jun 22, 2024
1bc745b
Fix formatting and comments in 'shift_replace(const ptr_uint64&)'
SSoelvsten Jun 24, 2024
89547ed
Clean up unit tests for 'bdd_not'
SSoelvsten Jun 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/adiar/internal/algorithms/quantify.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1418,7 +1418,7 @@ namespace adiar::internal
};

//////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Obtain the deepest level that satisfies (or not) the requested level.
/// \brief Obtain statistics on the variables in a Decision Diagram satisfying the predicate.
//////////////////////////////////////////////////////////////////////////////////////////////////
template <typename Policy>
inline quantify__pred_profile<Policy>
Expand Down Expand Up @@ -1557,7 +1557,7 @@ namespace adiar::internal

unreduced_t transposed;

// If transposition__max_iterations is 0, then only quantify the lowest level (with pruning).
// If transposition__max_iterations is 0, then only prune quantified levels.
if (transposition__max_iterations == 0) {
// Singleton Quantification of bottom-most level
#ifdef ADIAR_STATS
Expand Down
39 changes: 18 additions & 21 deletions src/adiar/internal/algorithms/select.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,12 +21,12 @@

namespace adiar::internal
{
//////////////////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////////////
// Select Algorithm
// ==================
//
// Given a Decision Diagram, a subset of the levels are removed and bridged
// over in either the 'high' or the 'low' direction.
// Given a Decision Diagram, a subset of the levels are removed and bridged over in either the
// 'high' or the 'low' direction.
/*
// _( )_ ---- xi _( )_ ---- xi
// / \ / \
Expand All @@ -36,18 +36,17 @@ namespace adiar::internal
*/
// Examples of uses are `bdd_restrict` and `zdd_onset` / `zdd_offset`
//
// As such, this is merely a niche-case of the Intercut algorithm, where the
// *onset* levels are removed and bridged over in a uniform direction (and the
// edges crossing said level only have suppressed nodes added). Yet compared
// to the Intercut algorithm, this implementation is optimised both in terms
// of time and space.
//////////////////////////////////////////////////////////////////////////////

//////////////////////////////////////////////////////////////////////////////
// As such, this is merely a niche-case of the Intercut algorithm, where the *onset* levels are
// removed and bridged over in a uniform direction (and the edges crossing said level only have
// suppressed nodes added). Yet compared to the Intercut algorithm, this implementation is
// optimised both in terms of time and space.
//////////////////////////////////////////////////////////////////////////////////////////////////

//////////////////////////////////////////////////////////////////////////////////////////////////
/// Struct to hold statistics
extern statistics::select_t stats_select;

//////////////////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////////////
// Data Structures
using select_request = request_data<1, with_parent>;

Expand All @@ -60,11 +59,10 @@ namespace adiar::internal
1u,
0u>;

/// Return a desired `node` to be output or a `node::pointer_type` to skip to
/// one of its children.
/// Return a desired `node` to be output or a `node::pointer_type` to skip to one of its children.
using select_rec = std::variant<node, node::pointer_type>;

//////////////////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////////////
// Helper functions
template <typename PriorityQueue>
inline void
Expand All @@ -80,7 +78,7 @@ namespace adiar::internal
}
}

//////////////////////////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////////////
template <typename Policy, typename PriorityQueue>
typename Policy::__dd_type
__select(const exec_policy& ep,
Expand Down Expand Up @@ -192,12 +190,11 @@ namespace adiar::internal
typename Policy::__dd_type
select(const exec_policy& ep, const typename Policy::dd_type& dd, Policy& policy)
{
// Compute amount of memory available for auxiliary data structures after
// having opened all streams.
// Compute amount of memory available for auxiliary data structures after having opened all
// streams.
//
// We then may derive an upper bound on the size of auxiliary data
// structures and check whether we can run them with a faster internal
// memory variant.
// We then may derive an upper bound on the size of auxiliary data structures and check whether
// we can run them with a faster internal memory variant.
const tpie::memory_size_type aux_available_memory =
memory_available() - node_stream<>::memory_usage() - arc_writer::memory_usage();

Expand Down
15 changes: 8 additions & 7 deletions src/adiar/internal/data_types/ptr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -818,8 +818,8 @@ namespace adiar::internal
inline ptr_uint64
cnot(const ptr_uint64& p, const bool negate)
{
const ptr_uint64::raw_type shifted_negate =
static_cast<ptr_uint64::raw_type>(negate) << ptr_uint64::data_shift;
const ptr_uint64::raw_type shifted_negate = static_cast<ptr_uint64::raw_type>(negate)
<< ptr_uint64::data_shift;

return p.is_terminal() ? p._raw ^ shifted_negate : p._raw;
}
Expand Down Expand Up @@ -870,18 +870,19 @@ namespace adiar::internal
inline ptr_uint64
shift_replace(const ptr_uint64& p, const ptr_uint64::signed_level_type levels)
{
// Evil type hacks (Thanks, Quake III)
// Evil type hack to obtain `p.level()` as a signed integer (Thanks, Quake III)
const ptr_uint64::level_type p_level__unsigned = p.level();
const ptr_uint64::signed_level_type p_level__signed =
(*reinterpret_cast<const ptr_uint64::signed_level_type *>(&p_level__unsigned));
(*reinterpret_cast<const ptr_uint64::signed_level_type*>(&p_level__unsigned));

// Evil type hack to obtain `p.level() + levels` as an unsigned integer (Thanks, Quake III)
const ptr_uint64::signed_level_type p_new_level__signed = p_level__signed + levels;
const ptr_uint64::level_type p_new_level__unsigned =
(*reinterpret_cast<const ptr_uint64::level_type *>(&p_new_level__signed));
(*reinterpret_cast<const ptr_uint64::level_type*>(&p_new_level__signed));

// Shift levels back and combine with other bits
const ptr_uint64::raw_type level_bits =
static_cast<ptr_uint64::raw_type>(p_new_level__unsigned) << ptr_uint64::level_shift;
const ptr_uint64::raw_type level_bits = static_cast<ptr_uint64::raw_type>(p_new_level__unsigned)
<< ptr_uint64::level_shift;

constexpr ptr_uint64::raw_type non_levels_mask =
~(static_cast<ptr_uint64::raw_type>(ptr_uint64::max_level) << ptr_uint64::level_shift);
Expand Down
168 changes: 116 additions & 52 deletions test/adiar/bdd/test_negate.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,89 +73,105 @@ go_bandit([]() {

bdd bdd_2(bdd_2_nf);

it("should doube-negate a T terminal-only BDD back into a T terminal-only BDD", [&]() {
bdd out = bdd_not(bdd_not(terminal_T));

// Check if it is correct
node_test_stream ns(out);
describe("bdd_not(const bdd&)", [&]() {
it("negates a T terminal BDD into an F terminal BDD", [&]() {
bdd out = bdd_not(terminal_T);

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(true)));
AssertThat(ns.can_pull(), Is().False());
});
// Check if it is correct
node_test_stream ns(out);

it("should doube-negate an F terminal-only BDD back into an F terminal-only BDD", [&]() {
bdd out = bdd_not(bdd_not(terminal_T));
AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(false)));
AssertThat(ns.can_pull(), Is().False());
});

// Check if it is correct
node_test_stream ns(out);
it("double-negates T terminal BDD back into T terminal", [&]() {
bdd temp = bdd_not(bdd_1);
bdd out = bdd_not(temp);

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(true)));
AssertThat(ns.can_pull(), Is().False());
});
// Check if it is correct
node_test_stream ns(out);

it("should double-negate terminal-children in BDD 1 back to the original", [&]() {
// Checkmate, constructivists...
AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_F_ptr, terminal_T_ptr)));

bdd out = bdd_not(bdd_not(bdd_1));
AssertThat(ns.can_pull(), Is().True());
AssertThat(
ns.pull(),
Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_T_ptr)));

// Check if it is correct
node_test_stream ns(out);
AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(),
Is().EqualTo(node(0,
node::max_id,
ptr_uint64(2, ptr_uint64::max_id),
ptr_uint64(1, ptr_uint64::max_id))));

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_F_ptr, terminal_T_ptr)));
AssertThat(ns.can_pull(), Is().False());
});

AssertThat(ns.can_pull(), Is().True());
AssertThat(
ns.pull(),
Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_T_ptr)));
it("negates a F terminal BDD into an T terminal BDD", [&]() {
bdd out = bdd_not(terminal_F);

AssertThat(ns.can_pull(), Is().True());
AssertThat(
ns.pull(),
Is().EqualTo(node(
0, node::max_id, ptr_uint64(2, ptr_uint64::max_id), ptr_uint64(1, ptr_uint64::max_id))));
// Check if it is correct
node_test_stream ns(out);

AssertThat(ns.can_pull(), Is().False());
});
AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(true)));
AssertThat(ns.can_pull(), Is().False());
});

describe("bdd_not(const &)", [&]() {
it("should negate a T terminal-only BDD into an F terminal-only BDD", [&]() {
bdd out = bdd_not(terminal_T);
it("double-negates F terminal BDD back into F terminal", [&]() {
bdd temp = bdd_not(terminal_F);
bdd out = bdd_not(temp);

// Check if it is correct
node_test_stream ns(out);

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(false)));

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

it("should negate a F terminal-only BDD into an T terminal-only BDD", [&]() {
bdd out = bdd_not(terminal_F);
it("negates terminal-children in BDD 1", [&]() {
bdd out = bdd_not(bdd_1);

// Check if it is correct
node_test_stream ns(out);

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(true)));
AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_T_ptr, terminal_F_ptr)));

AssertThat(ns.can_pull(), Is().True());
AssertThat(
ns.pull(),
Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_F_ptr)));

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(),
Is().EqualTo(node(0,
node::max_id,
ptr_uint64(2, ptr_uint64::max_id),
ptr_uint64(1, ptr_uint64::max_id))));

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

it("should negate terminal-children in BDD 1", [&]() {
bdd out = bdd_not(bdd_1);
it("unnegates terminal-children in negated BDD 1", [&]() {
bdd temp(bdd_1_nf, true);
bdd out = bdd_not(temp);

// Check if it is correct
node_test_stream ns(out);

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_T_ptr, terminal_F_ptr)));
AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_F_ptr, terminal_T_ptr)));

AssertThat(ns.can_pull(), Is().True());
AssertThat(
ns.pull(),
Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_F_ptr)));
Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_T_ptr)));

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(),
Expand All @@ -167,7 +183,7 @@ go_bandit([]() {
AssertThat(ns.can_pull(), Is().False());
});

it("should double-negate terminal-children in BDD 1 back to the original", [&]() {
it("double-negates terminal-children in BDD 1 back to the original", [&]() {
bdd temp = bdd_not(bdd_1);
bdd out = bdd_not(temp);

Expand All @@ -192,7 +208,7 @@ go_bandit([]() {
AssertThat(ns.can_pull(), Is().False());
});

it("should negate terminal-children in BDD 2", [&]() {
it("negates terminal-children in BDD 2", [&]() {
bdd out = bdd_not(bdd_2_nf);

node_test_stream ns(out);
Expand Down Expand Up @@ -221,8 +237,8 @@ go_bandit([]() {
});
});

describe("bdd_not(&&)", [&]() {
it("should negate a T terminal-only BDD into an F terminal-only BDD", [&]() {
describe("bdd_not(bdd&&)", [&]() {
it("negates a T terminal into an F terminal", [&]() {
bdd out = bdd_not(terminal_T_nf);

// Check if it is correct
Expand All @@ -233,7 +249,18 @@ go_bandit([]() {
AssertThat(ns.can_pull(), Is().False());
});

it("should negate a F terminal-only BDD into an T terminal-only BDD", [&]() {
it("double-negates a T terminal back into a T terminal", [&]() {
bdd out = bdd_not(bdd_not(terminal_T));

// Check if it is correct
node_test_stream ns(out);

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(true)));
AssertThat(ns.can_pull(), Is().False());
});

it("negates a F terminal into an T terminal", [&]() {
bdd out = bdd_not(terminal_F);

// Check if it is correct
Expand All @@ -244,7 +271,18 @@ go_bandit([]() {
AssertThat(ns.can_pull(), Is().False());
});

it("should negate terminal-children in BDD 1", [&]() {
it("double-negates an F terminal back into an F terminal", [&]() {
bdd out = bdd_not(bdd_not(terminal_F));

// Check if it is correct
node_test_stream ns(out);

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(false)));
AssertThat(ns.can_pull(), Is().False());
});

it("negates terminal-children in BDD 1", [&]() {
bdd out = bdd_not(bdd_1_nf);

// Check if it is correct
Expand All @@ -268,7 +306,33 @@ go_bandit([]() {
AssertThat(ns.can_pull(), Is().False());
});

it("should negate terminal-children in BDD 2", [&]() {
it("double-negates terminal-children in BDD 1 back to the original", [&]() {
// Checkmate, constructivists...

bdd out = bdd_not(bdd_not(bdd_1));

// Check if it is correct
node_test_stream ns(out);

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(), Is().EqualTo(node(2, node::max_id, terminal_F_ptr, terminal_T_ptr)));

AssertThat(ns.can_pull(), Is().True());
AssertThat(
ns.pull(),
Is().EqualTo(node(1, node::max_id, ptr_uint64(2, ptr_uint64::max_id), terminal_T_ptr)));

AssertThat(ns.can_pull(), Is().True());
AssertThat(ns.pull(),
Is().EqualTo(node(0,
node::max_id,
ptr_uint64(2, ptr_uint64::max_id),
ptr_uint64(1, ptr_uint64::max_id))));

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

it("negates terminal-children in BDD 2", [&]() {
bdd out = bdd_not(bdd_2_nf);

node_test_stream ns(out);
Expand Down
Loading