Skip to content

Commit

Permalink
Overload 'bdd_exists' and 'bdd_forall' to skip initial transposition …
Browse files Browse the repository at this point in the history 
…if possible
  • Loading branch information
@SSoelvsten
SSoelvsten committed Jun 13, 2024
1 parent 3d24c12 commit d678643
Show file tree
Hide file tree
Showing 8 changed files with 4,114 additions and 1,032 deletions.
212 changes: 212 additions & 0 deletions src/adiar/bdd.h
View file

Large diffs are not rendered by default.

56 changes: 56 additions & 0 deletions src/adiar/bdd/quantify.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,10 @@ namespace adiar
return bdd_exists(exec_policy(), f, var);
}

// TODO bdd_exists(__bdd&& f, bdd::label_type var)
//
// Use nested sweeping to skip some of the Reduce step!

__bdd
bdd_exists(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars)
{
Expand All @@ -115,6 +119,18 @@ namespace adiar
return bdd_exists(exec_policy(), std::move(f), vars);
}

__bdd
bdd_exists(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars)
{
return internal::quantify<bdd_quantify_policy<true>>(ep, std::move(f), vars);
}

__bdd
bdd_exists(__bdd&& f, const predicate<bdd::label_type>& vars)
{
return bdd_exists(exec_policy(), std::move(f), vars);
}

__bdd
bdd_exists(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars)
{
Expand All @@ -139,6 +155,18 @@ namespace adiar
return bdd_exists(exec_policy(), std::move(f), vars);
}

__bdd
bdd_exists(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars)
{
return internal::quantify<bdd_quantify_policy<true>>(ep, std::move(f), vars);
}

__bdd
bdd_exists(__bdd&& f, const generator<bdd::label_type>& vars)
{
return bdd_exists(exec_policy(), std::move(f), vars);
}

//////////////////////////////////////////////////////////////////////////////

__bdd
Expand All @@ -153,6 +181,10 @@ namespace adiar
return bdd_forall(exec_policy(), f, var);
}

// TODO bdd_forall(__bdd&& f, bdd::label_type var)
//
// Use nested sweeping to skip some of the Reduce step!

__bdd
bdd_forall(const exec_policy& ep, const bdd& f, const predicate<bdd::label_type>& vars)
{
Expand All @@ -177,6 +209,18 @@ namespace adiar
return bdd_forall(exec_policy(), std::move(f), vars);
}

__bdd
bdd_forall(const exec_policy& ep, __bdd&& f, const predicate<bdd::label_type>& vars)
{
return internal::quantify<bdd_quantify_policy<false>>(ep, std::move(f), vars);
}

__bdd
bdd_forall(__bdd&& f, const predicate<bdd::label_type>& vars)
{
return bdd_forall(exec_policy(), std::move(f), vars);
}

__bdd
bdd_forall(const exec_policy& ep, const bdd& f, const generator<bdd::label_type>& vars)
{
Expand All @@ -200,4 +244,16 @@ namespace adiar
{
return bdd_forall(exec_policy(), std::move(f), vars);
}

__bdd
bdd_forall(const exec_policy& ep, __bdd&& f, const generator<bdd::label_type>& vars)
{
return internal::quantify<bdd_quantify_policy<false>>(ep, std::move(f), vars);
}

__bdd
bdd_forall(__bdd&& f, const generator<bdd::label_type>& vars)
{
return bdd_forall(exec_policy(), std::move(f), vars);
}
}
82 changes: 74 additions & 8 deletions src/adiar/internal/algorithms/quantify.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1507,7 +1507,7 @@ namespace adiar::internal

const quantify__pred_profile<Policy> pred_profile = __quantify__pred_profile<Policy>(dd, pred);

// -----------------------------------------------------------------------
// ---------------------------------------------------------------------------------------------
// Case: Nothing to do
if (pred_profile.quant_all_vars == 0u) {
#ifdef ADIAR_STATS
Expand All @@ -1516,14 +1516,14 @@ namespace adiar::internal
return dd;
}

// -----------------------------------------------------------------------
// ---------------------------------------------------------------------------------------------
// Case: Only one variable to quantify
//
// TODO: pred_profile.quant_all_vars == 1u

switch (ep.template get<exec_policy::quantify::algorithm>()) {
case exec_policy::quantify::Singleton: {
// ---------------------------------------------------------------------
// -------------------------------------------------------------------------------------------
// Case: Repeated single variable quantification
#ifdef ADIAR_STATS
stats_quantify.singleton_sweeps += 1u;
Expand All @@ -1540,7 +1540,7 @@ namespace adiar::internal
}

case exec_policy::quantify::Nested: {
// ---------------------------------------------------------------------
// -------------------------------------------------------------------------------------------
// Case: Nested Sweeping

// Do Partial Quantification as long as...
Expand Down Expand Up @@ -1612,7 +1612,42 @@ namespace adiar::internal

// LCOV_EXCL_START
default:
// ---------------------------------------------------------------------
// -------------------------------------------------------------------------------------------
adiar_unreachable();
// LCOV_EXCL_STOP
}
}

template <typename Policy>
typename Policy::__dd_type
quantify(const exec_policy& ep,
typename Policy::__dd_type &&__dd,
const predicate<typename Policy::label_type>& pred)
{
switch (ep.template get<exec_policy::quantify::algorithm>()) {
case exec_policy::quantify::Singleton: {
// -------------------------------------------------------------------------------------------
// Case: Repeated single variable quantification
return quantify<Policy>(ep, typename Policy::dd_type(std::move(__dd)), pred);
}

case exec_policy::quantify::Nested: {
// -------------------------------------------------------------------------------------------
// Case: Nested Sweeping
//
// TODO: Also go-to 'dd_type()' variant, if heuristic claims it is a good idea to do some
// partial quantification.
if (__dd.template has<typename Policy::shared_node_file_type>()) {
return quantify<Policy>(ep, typename Policy::dd_type(std::move(__dd)), pred);
}

multi_quantify_policy__pred<Policy> inner_impl(pred);
return nested_sweep<>(ep, std::move(__dd), inner_impl);
}

// LCOV_EXCL_START
default:
// -------------------------------------------------------------------------------------------
adiar_unreachable();
// LCOV_EXCL_STOP
}
Expand Down Expand Up @@ -1717,7 +1752,7 @@ namespace adiar::internal
{
switch (ep.template get<exec_policy::quantify::algorithm>()) {
case exec_policy::quantify::Singleton: {
// ---------------------------------------------------------------------------------------
// -------------------------------------------------------------------------------------------
// Case: Repeated single variable quantification
// TODO: correctly handle Policy::quantify_onset
optional<typename Policy::label_type> on_level = lvls();
Expand Down Expand Up @@ -1788,7 +1823,7 @@ namespace adiar::internal
}

case exec_policy::quantify::Nested: {
// -----------------------------------------------------------------------------------------
// -------------------------------------------------------------------------------------------
// Case: Nested Sweeping
//
// NOTE: read-once access with 'gen' makes repeated transposition not possible. Yet, despite
Expand Down Expand Up @@ -1869,7 +1904,38 @@ namespace adiar::internal

// LCOV_EXCL_START
default:
// -----------------------------------------------------------------------------------------
// -------------------------------------------------------------------------------------------
adiar_unreachable();
// LCOV_EXCL_STOP
}
}

template <typename Policy>
typename Policy::__dd_type
quantify(const exec_policy& ep,
typename Policy::__dd_type &&__dd,
const typename multi_quantify_policy__generator<Policy>::generator_t& lvls)
{
switch (ep.template get<exec_policy::quantify::algorithm>()) {
case exec_policy::quantify::Singleton: {
// -------------------------------------------------------------------------------------------
// Case: Repeated single variable quantification
return quantify<Policy>(ep, typename Policy::dd_type(std::move(__dd)), lvls);
}
case exec_policy::quantify::Nested: {
// -------------------------------------------------------------------------------------------
// Case: Nested Sweeping
if (__dd.template has<typename Policy::shared_node_file_type>()) {
return quantify<Policy>(ep, typename Policy::dd_type(std::move(__dd)), lvls);
}

multi_quantify_policy__generator<Policy> inner_impl(lvls);
return nested_sweep<>(ep, std::move(__dd), inner_impl);
}

// LCOV_EXCL_START
default:
// -------------------------------------------------------------------------------------------
adiar_unreachable();
// LCOV_EXCL_STOP
}
Expand Down
Loading

0 comments on commit d678643

Please sign in to comment.