dd.h

#ifndef ADIAR_INTERNAL_DD_H
#define ADIAR_INTERNAL_DD_H
 
#include <variant>
 
#include <adiar/exec_policy.h>
 
#include <adiar/internal/cut.h>
#include <adiar/internal/data_types/arc.h>
#include <adiar/internal/data_types/node.h>
#include <adiar/internal/io/arc_file.h>
#include <adiar/internal/io/node_file.h>
 
namespace adiar::internal
{
  // TODO (MDD):
  // TODO (QMDD):
  // TODO (ADD (64-bit)):
  //   template both 'dd' and '__dd' with the node type (and derive the
  //   corresponding arc type).
 
  class dd;
 
  using no_file = std::monostate;
 
  class __dd
  {
  public:
    using node_type = node;
 
    using shared_node_file_type = shared_levelized_file<node_type>;
 
    using pointer_type = node_type::pointer_type;
 
    using uid_type = node_type::uid_type;
 
    using level_type = node_type::level_type;
 
    using signed_level_type = node_type::signed_level_type;
 
    using label_type = level_type;
 
    using signed_label_type = signed_level_type;
 
    using arc_type = arc;
 
    using shared_arc_file_type = shared_levelized_file<arc_type>;
 
    std::variant<no_file, shared_node_file_type, shared_arc_file_type> _union;
 
    bool _negate = false;
 
    signed_label_type _shift = 0;
 
    exec_policy _policy;
 
    // Constructors
 
    __dd() = default;
 
    __dd(const shared_node_file_type& f)
      : _union(f)
    {}
 
    __dd(const shared_arc_file_type& f, const exec_policy& ep)
      : _union(f)
      , _policy(ep)
    {}
 
    __dd(const dd& dd);
 
    // Accessors
    // TODO: change from 'file_t' to 'file::value_type'.
 
    template <typename file_t>
    bool
    has() const
    {
      return std::holds_alternative<file_t>(_union);
    }
 
    template <typename file_t>
    const file_t&
    get() const
    {
      return std::get<file_t>(_union);
    }
 
    bool
    empty() const
    {
      return has<no_file>();
    }
 
    // TODO (optimisation):
    //   Add precondition to be with 'arcs' only?
 
    size_t
    size() const
    {
      if (has<shared_arc_file_type>()) {
        // TODO (QMDD): Divide by node::outdegree instead of 2u
        return get<shared_arc_file_type>()->size() / 2u;
      }
      if (has<shared_node_file_type>()) { return get<shared_node_file_type>()->size(); }
      return 0u;
    }
 
    cut::size_type
    max_1level_cut(const cut ct) const
    {
      if (has<shared_arc_file_type>()) {
        const shared_arc_file_type& af = get<shared_arc_file_type>();
        return af->max_1level_cut + (ct.includes(false) ? af->number_of_terminals[false] : 0u)
          + (ct.includes(true) ? af->number_of_terminals[true] : 0u);
      }
      if (has<shared_node_file_type>()) { return get<shared_node_file_type>()->max_1level_cut[ct]; }
      return 0u;
    }
 
    cut::size_type
    max_2level_cut(const cut ct) const
    {
      if (has<shared_arc_file_type>()) {
        const shared_arc_file_type& af = get<shared_arc_file_type>();
        return std::min( // 3/2 times the 1-level cut
          (3 * af->max_1level_cut) / 2 + (ct.includes(false) ? af->number_of_terminals[false] : 0u)
            + (ct.includes(true) ? af->number_of_terminals[true] : 0u),
          // At most the number of nodes + 1
          (af->size() / 2u) + 1);
      }
      if (has<shared_node_file_type>()) { return get<shared_node_file_type>()->max_2level_cut[ct]; }
      return 0u;
    }
 
    size_t
    number_of_terminals(const bool value) const
    {
      if (has<shared_arc_file_type>()) {
        return get<shared_arc_file_type>()->number_of_terminals[this->_negate ^ value];
      }
      if (has<shared_node_file_type>()) {
        return get<shared_node_file_type>()->number_of_terminals[this->_negate ^ value];
      }
      return 0u;
    }
 
    size_t
    number_of_terminals() const
    {
      if (has<shared_arc_file_type>()) {
        const shared_arc_file_type& af = get<shared_arc_file_type>();
        return af->number_of_terminals[false] + af->number_of_terminals[true];
      }
      if (has<shared_node_file_type>()) {
        const shared_node_file_type& nf = get<shared_node_file_type>();
        return nf->number_of_terminals[false] + nf->number_of_terminals[true];
      }
      return 0u;
    }
  };
 
  class dd
  {
    // Constants
  public:
    using node_type = node;
 
    using pointer_type = node_type::pointer_type;
 
    using uid_type = node_type::uid_type;
 
    using level_type = node_type::level_type;
 
    using signed_level_type = node_type::signed_level_type;
 
    using label_type = level_type;
 
    using signed_label_type = signed_level_type;
 
    static constexpr label_type max_label = node_type::max_label;
 
    using id_type = node_type::id_type;
 
    static constexpr id_type max_id = node_type::max_id;
 
    using terminal_type = typename node_type::terminal_type;
 
    using node_file_type = levelized_file<node_type>;
 
    using shared_node_file_type = shared_file_ptr<node_file_type>;
 
    // Internal state
  protected:
    shared_node_file_type _file;
 
    void
    deref()
    {
      this->_file.reset();
    }
 
    //
    // TODO: move to 'bdd' or generalize to 'attribute'?
    bool _negate = false;
 
    signed_label_type _shift = 0;
 
    // Constructors
  public:
    dd(const shared_node_file_type& f, bool negate = false, signed_label_type shift = 0)
      : _file(f)
      , _negate(negate)
      , _shift(shift)
    {}
 
    dd(const dd& dd) = default;
 
    dd(dd&& dd) = default;
 
    // NOTE:
    //
    //   To implement the specific DD, add the following move-conversion that runs the Reduce
    //   algorithm.
    //
    // dd(__dd &&dd)
 
  public:
    const shared_node_file_type
    file_ptr() const
    {
      return this->_file;
    }
 
    const node_file_type*
    operator->() const
    {
      return this->_file.get();
    }
 
    bool
    is_negated() const
    {
      return this->_negate;
    }
 
    signed_label_type
    shift() const
    {
      return this->_shift;
    }
 
    cut::size_type
    max_1level_cut(const cut ct) const
    {
      return this->_file->max_1level_cut[negate_cut_type(ct)];
    }
 
    cut::size_type
    max_2level_cut(const cut ct) const
    {
      return this->_file->max_2level_cut[negate_cut_type(ct)];
    }
 
 
    size_t
    size() const
    {
      return this->_file->size();
    }
 
    size_t
    width() const
    {
      return this->_file->width;
    }
 
    size_t
    number_of_terminals(const bool value) const
    {
      return this->_file->number_of_terminals[this->_negate ^ value];
    }
 
    size_t
    number_of_terminals() const
    {
      return this->number_of_terminals(false) + this->number_of_terminals(true);
    }
 
  private:
    cut
    negate_cut_type(const cut ct) const
    {
      if (!this->_negate) { return ct; }
 
      switch (ct) {
      case cut::Internal_False: return cut::Internal_True;
      case cut::Internal_True: return cut::Internal_False;
      default: return ct;
      }
    }
  };
 
  inline __dd::__dd(const dd& dd)
    : _union(dd.file_ptr())
    , _negate(dd.is_negated())
    , _shift(dd.shift())
  {}
 
  template <typename DD, typename __DD>
  class dd_policy
  {
  public:
    using dd_type = DD;
 
    using __dd_type = __DD;
 
    using node_type = typename dd_type::node_type;
 
    using pointer_type = typename dd_type::pointer_type;
 
    using uid_type = typename dd_type::uid_type;
 
    using children_type = typename node_type::children_type;
 
    using level_type = typename dd_type::level_type;
 
    using signed_level_type = typename dd_type::signed_level_type;
 
    using label_type = typename dd_type::label_type;
 
    using signed_label_type = typename dd_type::signed_label_type;
 
    static constexpr label_type max_label = dd_type::max_label;
 
    using id_type = typename dd_type::id_type;
 
    static constexpr id_type max_id = dd_type::max_id;
 
    using terminal_type = typename dd_type::terminal_type;
 
    using shared_node_file_type = typename __dd_type::shared_node_file_type;
 
    using shared_arc_file_type = typename __dd_type::shared_arc_file_type;
 
  public:
    static inline pointer_type
    reduction_rule(const node_type& n);
 
    static inline children_type
    reduction_rule_inv(const pointer_type& child);
  };
 
}
 
#endif // ADIAR_INTERNAL_DD_H