Prune subtrees and nodes during initial And-Transposition

src/adiar/bdd/apply.cpp

@@ -31,6 +31,11 @@ namespace adiar
       : _op(op)
     {}
 
+  public:
+    void
+    setup_next_level(const bdd::label_type /*next_level*/) const
+    {}
+
   public:
     /// \brief Flip internal copy of operator
     void

src/adiar/bdd/relprod.cpp

@@ -2,17 +2,185 @@
 #include <adiar/bdd/bdd_policy.h>
 #include <adiar/types.h>
 
+#include <adiar/internal/algorithms/prod2.h>
 #include <adiar/internal/algorithms/replace.h>
+#include <adiar/internal/bool_op.h>
 
 namespace adiar
 {
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief   Product Construction policy for the BDD Relational Product.
+  ///
+  /// \details To improve performance, the `bdd_and` can be replaced with a special version that
+  ///          simultaneously prunes its subtrees based on the quantification predicate.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  template <typename LevelPredicate>
+  class relprod_prod2_policy
+    : public bdd_policy
+    , public internal::and_op
+    , public internal::prod2_mixed_level_merger<bdd_policy>
+  {
+  private:
+    const LevelPredicate& _pred;
+    bool _prune_level = false;
+
+  public:
+    relprod_prod2_policy(const LevelPredicate& pred)
+      : _pred(pred)
+    {}
+
+  public:
+    void
+    setup_next_level(const bdd::label_type next_level)
+    {
+      using result_type           = typename LevelPredicate::result_type;
+      constexpr bool is_total_map = is_convertible<result_type, label_type>;
+
+      if constexpr (is_total_map) {
+        this->_prune_level = this->_pred(next_level);
+      } else {
+        this->_prune_level = !this->_pred(next_level).has_value();
+      }
+    }
+
+  public:
+    /// \brief Flip internal copy of operator
+    void
+    flip()
+    {
+      adiar_assert(internal::and_op::is_commutative());
+      /* Do nothing...  */
+    }
+
+  public:
+    /// \brief Hook for case of two BDDs with the same node file.
+    __bdd
+    resolve_same_file(const bdd& bdd_1, const bdd& bdd_2) const
+    {
+      return bdd_1.is_negated() == bdd_2.is_negated() ? bdd_1 : bdd_terminal(false);
+    }
+
+    /// \brief Hook for either of the two BDDs being a terminal.
+    __bdd
+    resolve_terminal_root(const bdd& bdd_1, const bdd& bdd_2) const
+    {
+      adiar_assert(bdd_isterminal(bdd_1) || bdd_isterminal(bdd_2));
+
+      if (bdd_isterminal(bdd_1) && bdd_isterminal(bdd_2)) {
+        return bdd_terminal(internal::and_op::operator()(dd_valueof(bdd_1), dd_valueof(bdd_2)));
+      } else if (bdd_isterminal(bdd_1) && dd_valueof(bdd_1)) {
+        adiar_assert(internal::and_op::is_left_idempotent(dd_valueof(bdd_1)));
+        return bdd_2;
+      } else if (bdd_isterminal(bdd_2) && dd_valueof(bdd_2)) {
+        adiar_assert(internal::and_op::is_right_idempotent(dd_valueof(bdd_2)));
+        return bdd_1;
+      }
+      // and_op::can_left_shortcut(bdd_1) || and_op::can_right_shortcut(bdd_2)
+      return bdd_terminal(false);
+    }
+
+  private:
+    /// \brief Applies shortcutting on a recursion target, if possible.
+    pair<internal::tuple<bdd::pointer_type>, bool>
+    __resolve_request(const internal::tuple<bdd::pointer_type>& r) const
+    {
+      if (internal::and_op::can_left_shortcut(r[0]) || internal::and_op::can_right_shortcut(r[1])) {
+        return {{ bdd::pointer_type(false), bdd::pointer_type(false) }, true};
+      }
+      return { r, false };
+    }
+
+    bool
+    __is_true(const internal::tuple<bdd::pointer_type>& t) const
+    {
+      return (t[0] == bdd::pointer_type(true) && t[1] == bdd::pointer_type(true));
+    }
+
+  public:
+    /// \brief Hook for changing the targets of a new node's children.
+    internal::prod2_rec
+    resolve_request(const internal::tuple<bdd::pointer_type>& r_low,
+                    const internal::tuple<bdd::pointer_type>& r_high) const
+    {
+      const auto [low, low_false]   = this->__resolve_request(r_low);
+      const auto [high, high_false] = this->__resolve_request(r_high);
+
+      // Prune subtree(s) if either child is 'false' and is quantified later.
+      if (this->_prune_level && (low_false || high_false)) {
+        return internal::prod2_rec_skipto{ low_false ? high : low };
+      }
+      // Prune subtree(s) if either child is 'true' and is quantified later.
+      if (this->_prune_level && (this->__is_true(low) || this->__is_true(high))) {
+        return internal::prod2_rec_skipto{ bdd::pointer_type(true) };
+      }
+      // Skip node with duplicated children requests
+      //
+      // NOTE: One could think to also prune 'redundant' nodes. Yet, these cannot be created as the
+      //       tuples `(f1,f2)` and `(g1,g2)` could only have `(f1,g1) = (f2,g2)` if `f1 = f2` and
+      //       `g1 = g2`.
+      //
+      //       The only exception would be if `f1`, `f2`, `g1`, and `g2` are terminals. Yet, with
+      //       the would 'and' operation, this can only happen if they are shortcutting to the
+      //       'false' terminal. Yet, this would only happen at the very bottom. With most variable
+      //       orderings, this would be the next-state variable at the very bottom.
+      //
+      //       In practice, it seems very unlikely these few edges are not cheaper to handle, than
+      //       having this additional branch in the code (even if it is very predictable).
+      /*
+      if (low == high) { return internal::prod2_rec_skipto{ low }; }
+      */
+
+      return internal::prod2_rec_output{ low, high };
+    }
+
+    /// \brief Hook for applying an operator to a pair of terminals.
+    bdd::pointer_type
+    operator()(const bdd::pointer_type& a, const bdd::pointer_type& b) const
+    {
+      return internal::and_op::operator()(a, b);
+    }
+
+  public:
+    /// \brief Hook for deriving the cut type of the left-hand-side.
+    internal::cut
+    left_cut() const
+    {
+      return internal::cut(!internal::and_op::can_left_shortcut(false),
+                           !internal::and_op::can_left_shortcut(true));
+    }
+
+    /// \brief Hook for deriving the cut type of the right-hand-side.
+    internal::cut
+    right_cut() const
+    {
+      return internal::cut(!internal::and_op::can_right_shortcut(false),
+                           !internal::and_op::can_right_shortcut(true));
+    }
+
+    /// \brief Due to pruning, this prod2 policy may introduce skipping of nodes.
+    static constexpr bool no_skip = false;
+  };
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  template <typename LevelPredicate>
+  __bdd
+  bdd_relprod__and(const exec_policy& ep,
+                   const bdd& states,
+                   const bdd& relation,
+                   const LevelPredicate& pred)
+  {
+    relprod_prod2_policy<LevelPredicate> policy(pred);
+    return internal::prod2(ep, states, relation, policy);
+  }
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   bdd
   bdd_relprod(const exec_policy& ep,
               const bdd& states,
               const bdd& relation,
               const predicate<bdd::label_type>& pred)
   {
-    return bdd_exists(ep, bdd_and(ep, states, relation), pred);
+    return bdd_exists(ep, bdd_relprod__and(ep, states, relation, pred), pred);
   }
 
   bdd
@@ -28,7 +196,7 @@ namespace adiar
               const function<optional<bdd::label_type>(bdd::label_type)>& m,
               replace_type m_type)
   {
-    __bdd tmp_1 = bdd_and(ep, states, relation);
+    __bdd tmp_1 = bdd_relprod__and(ep, states, relation, m);
 
     const bdd tmp_2 =
       bdd_exists(ep, std::move(tmp_1), [&m](bdd::label_type x) { return !m(x).has_value(); });
@@ -80,7 +248,7 @@ namespace adiar
     const bdd tmp_1 = bdd_replace(
       ep, states, [&m](bdd::label_type x) { return m(x).value(); }, m_type);
 
-    __bdd tmp_2 = bdd_and(ep, std::move(tmp_1), relation);
+    __bdd tmp_2 = bdd_relprod__and(ep, std::move(tmp_1), relation, m);
 
     const bdd tmp_3 =
       bdd_exists(ep, std::move(tmp_2), [&m](bdd::label_type x) { return !m(x).has_value(); });

src/adiar/internal/algorithms/prod2.h

@@ -279,7 +279,7 @@ namespace adiar::internal
   __prod2_ra(const exec_policy& ep,
              const typename Policy::dd_type& in_pq,
              const typename Policy::dd_type& in_ra,
-             const Policy& policy,
+             Policy& policy,
              const size_t pq_memory,
              const size_t max_pq_size)
   {
@@ -311,6 +311,7 @@ namespace adiar::internal
       typename Policy::label_type out_label = prod_pq.current_level();
       typename Policy::id_type out_id       = 0;
 
+      policy.setup_next_level(out_label);
       in_nodes_ra.setup_next_level(out_label);
 
       // Update maximum 1-level cut
@@ -401,7 +402,7 @@ namespace adiar::internal
   __prod2_pq(const exec_policy& ep,
              const typename Policy::dd_type& in_0,
              const typename Policy::dd_type& in_1,
-             const Policy& policy,
+             Policy& policy,
              const size_t pq_1_memory,
              const size_t max_pq_1_size,
              const size_t pq_2_memory,
@@ -436,6 +437,8 @@ namespace adiar::internal
       const typename Policy::label_type out_label = prod_pq_1.current_level();
       typename Policy::id_type out_id             = 0;
 
+      policy.setup_next_level(out_label);
+
       // Update max 1-level cut
       out_arcs->max_1level_cut = std::max(out_arcs->max_1level_cut, prod_pq_1.size());
 

src/adiar/zdd/binop.cpp

@@ -81,6 +81,11 @@ namespace adiar
       , _can_right_shortcut{ zdd_prod2_policy::can_right_shortcut(op) }
     {}
 
+  public:
+    void
+    setup_next_level(const bdd::label_type /*next_level*/) const
+    {}
+
   public:
     /// \brief Flip internal copy of operator
     void