Accumulate BDD operations over an Iterator

[SSoelvsten]

Motivation

The end user may want to do something like the following

  adiar::bdd acc = adiar::bdd_true();
  for (auto &it = bdd_vec.begin(); it != bdd_vec.end(); it++) {
    acc = bdd_apply(acc, *it, op);
  }

Optimisations

A more fancy way to do the same is with a FIFO queue for a more bottom-up tree-like approach.

  // Empty list?

  std::queue<adiar::bdd> tmp;
  { // Populate FIFO queue with pairs of BDDs
    auto it = bdd_vec.cbegin();
    while (it != bdd_vec.cend()) {
      const auto dd_1 = *(it++);
      if (it == bdd_vec.cend()) {
        if (tmp.empty()) { return dd_1; }
          tmp.push(dd_1);
          break;
        }

      const auto dd_2 = *(it++);
      if (it == bdd_vec.cend() && tmp.empty()) {
        return bdd_apply(dd_1, dd_2, op);
      }
      tmp.push(bdd_apply(dd_1, dd_2, op));
    }
  }

  // Merge pairs in the FIFO queue
  while (true) {
    const auto dd_1 = tmp.front(); tmp.pop();
    const auto dd_2 = tmp.front(); tmp.pop();

    if (tmp.empty()) {
      return bdd_apply(dd_1, dd_2, op);
    }
    tmp.push(bdd_apply(dd_1, dd_2, op));
  }

In practice, Jaco had very good experience with doing the above with the Sylvan BDD package. For Adiar, this probably also will help a lot. One can further improve it by doing the following:

• Minimize the number of l-values such that the dd_1 and dd_2 can be garbage collected after the top-down sweep of bdd_apply has finished. Alternatively, use std::move(...).

Tasks

We should provide the fancy version above as part of Adiar's API. If one wants to save on memory, we could provide both versions (which one is chosen with an enum). The implementation of both approaches could be placed in adiar/internal/util.h or in adiar/internal/algorithms/prod2.h.

• Add overloads for BDD and ZDD generators.
  • [ ] Add __bdd bdd_apply(generator<bdd>, op) (and all the operator's aliases)
  • [ ] Add unit tests for the new bdd_apply(generator<bdd>, op) and its overloads.
  • [ ] Add __zdd zdd_binop(generator<zdd>, op) (and all the operator's aliases)
  • [ ] Add unit tests for the new zdd_binop(generator<zdd>, op) and its overloads.
• Add overloads for iterators. Notice, the bdd_and and bdd_or functions with an iterator already exist in the API (#532). We need to use if constexpr and std::is_integral<IT::value_type>::value/std::is_same<...>::value to resolve which algorithm to run.
  • [ ] template<typename IT> bdd bdd_apply(begin, end, op) (and all the operator's aliases)
  • [ ] Add unit tests for the new bdd_apply(generator<bdd>, op) and its overloads.
  • [ ] template<typename IT> zdd zdd_binop(begin, end, op) (and all the operator's aliases)
  • [ ] Add unit tests for the new zdd_binop(generator<zdd>, op) and its overloads.

[SSoelvsten]

I saw the following quote on the Wikipedia article for Exclusive Or:

Since it is associative, it may be considered to be an n-ary operator which is true if and only if an odd number of arguments are true. That is, a XOR b XOR ... may be treated as XOR(a,b,...).

So, we might want to add a is_associative(op) predicate to <adiar/internal/bool_op.h> to identify whether we actually can do this bottom-up tree accumulation (or have to do it left-to-right?).