Skip to content

Commit

Permalink
Improve constant on initial (pruning) transposition with simpler Sele…
Browse files Browse the repository at this point in the history 
…ct algorithm
  • Loading branch information
@SSoelvsten
SSoelvsten committed Apr 22, 2024
1 parent 768dde3 commit 28772e9
Show file tree
Hide file tree
Showing 3 changed files with 53 additions and 137 deletions.
149 changes: 30 additions & 119 deletions src/adiar/internal/algorithms/quantify.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
#include <adiar/functional.h>

#include <adiar/internal/algorithms/nested_sweeping.h>
#include <adiar/internal/algorithms/select.h>
#include <adiar/internal/assert.h>
#include <adiar/internal/block_size.h>
#include <adiar/internal/bool_op.h>
Expand Down Expand Up @@ -393,36 +394,6 @@ namespace adiar::internal
continue;
}

// -----------------------------------------------------------------------------------------
// CASE: Pruning Quantification
// Prune based on terminals for shallow to-be quantified variables dealt with during
// nested sweeping.
if constexpr (Policy::pruning_quantification) {
if (policy.should_prune()) {
adiar_assert(req.target.second().is_nil(),
"Pruning should only happen above to-be quantified variable");

const typename Policy::pointer_type prune_target = policy.prune(children_fst);

if (prune_target.is_terminal()) {
if (req.data.source.is_nil()) {
return typename Policy::dd_type(prune_target.value());
}

const __quantify_recurse_in__output_terminal handler(aw, prune_target);
request_foreach(pq, req.target, handler);

continue;
} else if (prune_target.is_node()) {
quantify_request<0>::target_t rec(prune_target, Policy::pointer_type::nil());
const __quantify_recurse_in__forward handler(pq, rec);
request_foreach(pq, req.target, handler);

continue;
}
}
}

// -----------------------------------------------------------------------------------------
// CASE: Regular Level
// The variable should stay: proceed as in the Product Construction by simulating both
Expand Down Expand Up @@ -601,37 +572,6 @@ namespace adiar::internal
continue;
}

// -----------------------------------------------------------------------------------------
// CASE: Pruning Quantification
// Prune based on terminals for shallow to-be quantified variables dealt with during
// nested sweeping.
if constexpr (Policy::pruning_quantification) {
if (policy.should_prune()) {
adiar_assert(req.target.second().is_nil(),
"Pruning should only happen above to-be quantified variable");

const typename Policy::pointer_type prune_target = policy.prune(children_fst);

if (prune_target.is_terminal()) {
if (req.data.source.is_nil()) {
return typename Policy::dd_type(prune_target.value());
}

const __quantify_recurse_in__output_terminal handler(aw, prune_target);
request_foreach(pq_1, pq_2, req.target, handler);

continue;
} else if (prune_target.is_node()) {
quantify_request<0>::target_t rec(prune_target, Policy::pointer_type::nil());

const __quantify_recurse_in__forward handler(pq_1, rec);
request_foreach(pq_1, pq_2, req.target, handler);

continue;
}
}
}

// -----------------------------------------------------------------------------------------
// CASE: Regular Level
// The variable should stay: proceed as in the Product Construction by simulating both
Expand Down Expand Up @@ -1017,11 +957,6 @@ namespace adiar::internal
/// \brief Disable logic for partial quantification during sweep.
////////////////////////////////////////////////////////////////////////////////////////////////
static constexpr bool partial_quantification = false;

////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Disable logic for pruning quantification during sweep.
////////////////////////////////////////////////////////////////////////////////////////////////
static constexpr bool pruning_quantification = false;
};

//////////////////////////////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -1131,11 +1066,6 @@ namespace adiar::internal
////////////////////////////////////////////////////////////////////////////////////////////////
static constexpr bool partial_quantification = false;

////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Disable logic for pruning quantification during sweep.
////////////////////////////////////////////////////////////////////////////////////////////////
static constexpr bool pruning_quantification = false;

// bool has_sweep(typename Policy::label_type) const;

////////////////////////////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -1273,79 +1203,65 @@ namespace adiar::internal
using pred_t = predicate<typename Policy::label_type>;

private:
////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Deepest level that needs to-be quantified.
////////////////////////////////////////////////////////////////////////////////////////////////
const typename Policy::label_type _deepest;

////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Predicate for whether a level should be swept on (or not).
////////////////////////////////////////////////////////////////////////////////////////////////
const pred_t& _pred;

////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Stores result of `_pred` to save on computation time
/// \brief Stores result of `_pred` to save on computation time.
////////////////////////////////////////////////////////////////////////////////////////////////
bool _pred_result;

public:
////////////////////////////////////////////////////////////////////////////////////////////////
pruning_quantify_policy(const pred_t& pred, typename Policy::label_type deepest)
: _deepest(deepest)
, _pred(pred)
pruning_quantify_policy(const pred_t& pred)
: _pred(pred)
, _pred_result(false)
{}

////////////////////////////////////////////////////////////////////////////////////////////////
inline bool
should_quantify(typename Policy::label_type level)
{
const bool result = level == _deepest;
_pred_result = should_prune(level);
return result;
}

////////////////////////////////////////////////////////////////////////////////////////////////
inline bool
should_prune(typename Policy::label_type level) const
void
setup_level(typename Policy::label_type level)
{
return _pred(level) == Policy::quantify_onset;
_pred_result = _pred(level) == Policy::quantify_onset;
}

inline bool
should_prune() const
internal::select_rec
process(const typename Policy::node_type& n)
{
return _pred_result;
}
// -------------------------------------------------------------------------------------------
// CASE: Not to-be quantified node.
if (!_pred_result) {
return n;
}

////////////////////////////////////////////////////////////////////////////////////////////////
typename Policy::pointer_type
prune(const typename Policy::node_type::children_type& c) const
{
const typename Policy::pointer_type max_child = std::max(c[0], c[1]);
// -------------------------------------------------------------------------------------------
// CASE: Prune max child
const typename Policy::pointer_type max_child = std::max(n.low(), n.high());

if (Policy::collapse_to_terminal(max_child)) {
// Collapse to terminal
return max_child;
}
if (max_child.is_terminal() && !Policy::keep_terminal(max_child)) {
// Non-collapsing and irrelevant, terminal. Skip to 'other'
return std::min(c[0], c[1]);
return std::min(n.low(), n.high());
}

// Return 'nothing'
return Policy::pointer_type::nil();
// TODO: Symmetric for 'false' pointer (NOTE: it's not 'max')

// No pruning possible. Do nothing.
return n;
}

////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Enable partial quantification logic.
////////////////////////////////////////////////////////////////////////////////////////////////
static constexpr bool partial_quantification = false;
typename Policy::dd_type
terminal(bool terminal_val)
{
return typename Policy::dd_type(terminal_val);
}

////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Disable logic for pruning quantification during sweep.
////////////////////////////////////////////////////////////////////////////////////////////////
static constexpr bool pruning_quantification = true;
static constexpr bool skip_reduce = false;
};

//////////////////////////////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -1399,11 +1315,6 @@ namespace adiar::internal
/// \brief Enable partial quantification logic.
////////////////////////////////////////////////////////////////////////////////////////////////
static constexpr bool partial_quantification = true;

////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Disable logic for pruning quantification during sweep.
////////////////////////////////////////////////////////////////////////////////////////////////
static constexpr bool pruning_quantification = false;
};

//////////////////////////////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -1572,8 +1483,8 @@ namespace adiar::internal
#ifdef ADIAR_STATS
stats_quantify.singleton_sweeps += 1u;
#endif
pruning_quantify_policy<Policy> pruning_impl(pred, label);
transposed = __quantify(ep, std::move(dd), pruning_impl);
pruning_quantify_policy<Policy> pruning_impl(pred);
transposed = select(ep, std::move(dd), pruning_impl);
} else {
// Partial Quantification
#ifdef ADIAR_STATS
Expand Down
9 changes: 5 additions & 4 deletions test/adiar/bdd/test_quantify.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3206,7 +3206,7 @@ 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(15u));

// - First check for at least one variable satisfying the predicate.
// This is then used for the inital transposition
Expand All @@ -3227,9 +3227,10 @@ go_bandit([]() {

// - Nested sweep looking for the 'next_inner' bottom-up
AssertThat(call_history.at(10), Is().EqualTo(4u));
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(11), Is().EqualTo(3u));
AssertThat(call_history.at(12), Is().EqualTo(2u));
AssertThat(call_history.at(13), Is().EqualTo(1u));
AssertThat(call_history.at(14), Is().EqualTo(0u));
});

it("kills intermediate dead partial solutions multiple times", [&]() {
Expand Down
32 changes: 18 additions & 14 deletions test/adiar/zdd/test_project.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -675,7 +675,7 @@ 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(12u));

// - First check for at least one variable satisfying the predicate.
// This is then used for the inital transposition
Expand All @@ -692,10 +692,11 @@ go_bandit([]() {
AssertThat(call_history.at(6), Is().EqualTo(4u));

// - Nested sweep looking for the 'next_inner' bottom-up
AssertThat(call_history.at(7), Is().EqualTo(3u));
AssertThat(call_history.at(8), Is().EqualTo(2u)); // <-- still exists
AssertThat(call_history.at(9), Is().EqualTo(1u));
AssertThat(call_history.at(10), Is().EqualTo(0u));
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));
});

it("does not prune on 'shortcutting' terminals during transposition [&& zdd_7]", [&]() {
Expand Down Expand Up @@ -738,7 +739,7 @@ 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(8u));

// - First check for at least one variable satisfying the predicate.
// This is then used for the inital transposition
Expand All @@ -753,8 +754,9 @@ go_bandit([]() {
AssertThat(call_history.at(4), Is().EqualTo(3u));

// - Nested sweep looking for the 'next_inner' bottom-up
AssertThat(call_history.at(5), Is().EqualTo(1u));
AssertThat(call_history.at(6), Is().EqualTo(0u));
AssertThat(call_history.at(5), Is().EqualTo(3u));
AssertThat(call_history.at(6), Is().EqualTo(1u));
AssertThat(call_history.at(7), Is().EqualTo(0u));
});

it("prunes idempotent to-be quantified nodes during transposition [&&]", [&]() {
Expand Down Expand Up @@ -808,7 +810,7 @@ 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.
// This is then used for the inital transposition
Expand All @@ -824,8 +826,9 @@ go_bandit([]() {
AssertThat(call_history.at(5), Is().EqualTo(4u));

// - Nested sweep looking for the 'next_inner' bottom-up
AssertThat(call_history.at(6), Is().EqualTo(3u));
AssertThat(call_history.at(7), Is().EqualTo(0u));
AssertThat(call_history.at(6), Is().EqualTo(4u));
AssertThat(call_history.at(7), Is().EqualTo(3u));
AssertThat(call_history.at(8), Is().EqualTo(0u));
});
});

Expand Down Expand Up @@ -1144,7 +1147,7 @@ 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.
AssertThat(call_history.at(0), Is().EqualTo(4u));
Expand All @@ -1159,8 +1162,9 @@ go_bandit([]() {
AssertThat(call_history.at(5), Is().EqualTo(4u));

// - Nested sweep checking if any other than the deepest variable needs quantifying
AssertThat(call_history.at(6), Is().EqualTo(2u));
AssertThat(call_history.at(7), Is().EqualTo(0u));
AssertThat(call_history.at(6), Is().EqualTo(4u));
AssertThat(call_history.at(7), Is().EqualTo(2u));
AssertThat(call_history.at(8), Is().EqualTo(0u));
});

it("quantifies exploding zdd_5 with unbounded transpositions", [&]() {
Expand Down

0 comments on commit 28772e9

Please sign in to comment.